Anonymous user
Proof: Difference between revisions
→{{header|Coq}}: complete solution
(Added Wren) |
(→{{header|Coq}}: complete solution) |
||
Line 220:
=={{header|Coq}}==
<lang coq>(* 1.1 Define a countably infinite set of natural numbers {0, 1, 2, 3, ...}. *)
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
(* 2.1 Define the addition on natural numbers. *)
Fixpoint plus (n m:nat) {struct n} : nat :=
match n with
Line 231:
| S p => S (p + m)
end
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 -> Prop :=
| even_O : even O
| even_SSn : forall n:nat,
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,
even n -> even m -> even (n + m).
Proof.
intros n m H H0.
elim H.
trivial.
intros.
simpl.
case even_SSn.
intros.
apply even_SSn; 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.
</lang>
| |||