Theorem add_com n m : n + m = m + n.
Proof.
revert m.
induction n as [|n IHn].
- intros m.
simpl.
induction m as [|m IHm].
+ simpl. trivial.
+ simpl. rewrite <- IHm. reflexivity.
- intros m.
induction m as [|m IHm].
+ simpl.
rewrite IHn. simpl. reflexivity.
+ simpl.
rewrite IHn.
simpl.
rewrite <- IHm.
simpl.
rewrite IHn.
reflexivity.
Qed.
Proof.
revert m.
induction n as [|n IHn].
- intros m.
simpl.
induction m as [|m IHm].
+ simpl. trivial.
+ simpl. rewrite <- IHm. reflexivity.
- intros m.
induction m as [|m IHm].
+ simpl.
rewrite IHn. simpl. reflexivity.
+ simpl.
rewrite IHn.
simpl.
rewrite <- IHm.
simpl.
rewrite IHn.
reflexivity.
Qed.
Prove the following theorems; replace Abort command with Qed. If theorem A (including add_com) appears before theorem B
in this file, you can use A to prove B.
Theorem add_assoc : forall x y z : nat, x + (y + z) = (x + y) + z.
Proof.
Abort.
Theorem mul_com' : forall x y : nat, x * y = y * x.
Proof.
Abort.
Fixpoint add' (n m : nat) :=
match n with
| O => m
| S n' => add' n' (S m)
end.
Lemma add'_S n m : add' n (S m) = S (add' n m).
Proof.
Abort.
Theorem add'_comm : forall n m, add' n m = add' m n.
Proof.
Abort.
Theorem plus'_assoc : forall n m k, add' n (add' m k) = add' (add' n m) k.
Proof.
Abort.
Theorem add'_add : forall n m, add' n m = n + m.
Proof.
Abort.