Proof: Difference between revisions
Content added Content deleted
(Added Wren) |
(→{{header|Coq}}: complete solution) |
||
Line 220: | Line 220: | ||
=={{header|Coq}}== |
=={{header|Coq}}== |
||
<lang coq>(* 1.1 Define a countably infinite set of natural numbers {0, 1, 2, 3, ...}. *) |
|||
1.1., 1.2., 2.1. and 3.1.: |
|||
Inductive nat : Set := |
|||
<lang coq>Inductive nat : Set := |
|||
| O : nat |
| O : nat |
||
| S : nat -> nat. |
| S : nat -> nat. |
||
(* 2.1 Define the addition on natural numbers. *) |
|||
Fixpoint plus (n m:nat) {struct n} : nat := |
Fixpoint plus (n m:nat) {struct n} : nat := |
||
match n with |
match n with |
||
Line 231: | Line 231: | ||
| S p => S (p + m) |
| S p => S (p + m) |
||
end |
end |
||
where "n + m" := (plus n m) : nat_scope. |
where "n + m" := (plus n m) : nat_scope. |
||
(* 1.2 Define a countably infinite set of even natural numbers {0, 2, 4, 6, ...} within the previously defined set of natural numbers. *) |
|||
Inductive even : nat -> Set := |
|||
Inductive even : nat -> Prop := |
|||
| even_O : even O |
| even_O : even O |
||
| even_SSn : forall n:nat, |
| even_SSn : forall n:nat, |
||
even n -> even (S (S n)). |
even n -> even (S (S n)). |
||
(* 1.3 Define a countably infinite set of odd natural numbers {1, 3, 5, 7, ...} within the previously defined set of natural numbers. *) |
|||
Inductive odd : nat -> Prop := |
|||
| odd_1 : odd (S O) |
|||
| odd_SSn : forall n:nat, |
|||
odd n -> odd (S (S n)). |
|||
(* 3.1 Prove that the addition of any two even numbers is even. *) |
|||
Theorem even_plus_even : forall n m:nat, |
Theorem even_plus_even : forall n m:nat, |
||
even n -> even m -> even (n + m). |
even n -> even m -> even (n + m). |
||
Proof. |
Proof. |
||
intros n m H H0. |
intros n m H H0. |
||
elim H. |
elim H. |
||
trivial. |
trivial. |
||
intros. |
intros. |
||
simpl. |
simpl. |
||
case even_SSn. |
case even_SSn. |
||
intros. |
intros. |
||
apply even_SSn; assumption. |
apply even_SSn; assumption. |
||
assumption. |
assumption. |
||
Qed. |
|||
(* 3.2 Prove that the addition is always associative. *) |
|||
Lemma plus_assoc : forall a b c, a + (b + c) = (a + b) + c. |
|||
Proof. |
|||
induction a; [ solve [ auto ] | ]. |
|||
intros. simpl. rewrite IHa. reflexivity. |
|||
Qed. |
|||
(* 3.3 Prove that the addition is always commutative. *) |
|||
Lemma plus_comm : forall a b, a + b = b + a. |
|||
Proof. |
|||
induction a. |
|||
- induction b; [ solve [ auto ] | ]. |
|||
simpl. rewrite <- IHb. simpl. reflexivity. |
|||
- induction b. |
|||
+ simpl. rewrite IHa. reflexivity. |
|||
+ simpl. rewrite <- IHb. rewrite IHa. simpl. rewrite IHa. reflexivity. |
|||
Qed. |
|||
Fixpoint even_n_odd_Sn {n} (p : even n) : odd (S n) := |
|||
match p with |
|||
| even_O => odd_1 |
|||
| even_SSn _ p' => odd_SSn _ (even_n_odd_Sn p') |
|||
end. |
|||
Fixpoint odd_n_even_Sn {n} (p : odd n) : even (S n) := |
|||
match p with |
|||
| odd_1 => even_SSn O even_O |
|||
| odd_SSn _ p' => even_SSn _ (odd_n_even_Sn p') |
|||
end. |
|||
Lemma even_Sn_odd_n : forall n, even (S n) -> odd n. |
|||
Proof. |
|||
destruct n. |
|||
- intros. inversion H. |
|||
- intros. inversion H. subst. apply even_n_odd_Sn. assumption. |
|||
Qed. |
|||
Lemma odd_Sn_even_n : forall n, odd (S n) -> even n. |
|||
Proof. |
|||
destruct n. |
|||
- constructor. |
|||
- intros. inversion H. subst. apply odd_n_even_Sn. assumption. |
|||
Qed. |
|||
Lemma not_even_and_odd : forall n, even n -> odd n -> False. |
|||
Proof. |
|||
induction n. |
|||
- intros. inversion H0. |
|||
- intros. apply IHn. |
|||
+ apply (odd_Sn_even_n _ H0). |
|||
+ apply (even_Sn_odd_n _ H). |
|||
Qed. |
|||
(* 3.4 Try to prove that the addition of any two even numbers is odd (it should be rejected). *) |
|||
Goal forall n m, even n -> even m -> odd (n + m) -> False. |
|||
Proof. |
|||
destruct n. |
|||
- simpl. intros. apply (not_even_and_odd _ H0 H1). |
|||
- simpl. intros. |
|||
assert (Hx := even_plus_even _ _ H H0). simpl in Hx. |
|||
apply (not_even_and_odd _ Hx H1). |
|||
Qed. |
|||
(* 4.1 Prove that the addition of any two even numbers cannot be odd. *) |
|||
Goal forall n m, even n -> even m -> odd (n + m) -> False. |
|||
Proof. |
|||
intros. assert (Hx := even_plus_even _ _ H H0). |
|||
apply (not_even_and_odd _ Hx H1). |
|||
Qed. |
|||
(* 4.2 Try to prove that the addition of any two even numbers cannot be even (it should be rejected). *) |
|||
Goal forall n m, even n -> even m -> ~even (n + m) -> False. |
|||
Proof. |
|||
intros. apply H1. apply (even_plus_even _ _ H H0). |
|||
Qed. |
Qed. |
||
</lang> |
</lang> |