td2_sol

(* ==================================================================== *)
(* Proofs and computations                                              *)

(* Command to check computations *)
Eval compute in 2+2.

Parameter x : nat.

Eval compute in 0+x.
Eval compute in x+0.

Lemma calc : 200 + 200 = 400.
Proof.
simpl. (* perform the computations in the goal *)
reflexivity.
Qed.

(* easy *)
Lemma add0n : forall n:nat, 0 + n = n.
Proof.
trivial.
Qed.

(* this needs reasonning *)
Lemma addn0 : forall n, n+0 = n.
induction n.
  reflexivity.
simpl; rewrite IHn.
trivial.
Qed.

Lemma addSnm : forall n m, S n + m = S(n + m).
Proof.
trivial.
Qed.

Lemma addnSm : forall n m, n + S m = S (n + m).
induction n.
 simpl.
 reflexivity.
intros m; simpl; rewrite IHn.
reflexivity.
Qed.

Lemma add_com : forall n m, n + m = m + n.
induction n.
intros m; rewrite addn0.
reflexivity.
intros m; simpl; rewrite addnSm.
rewrite IHn.
reflexivity.
Qed.

Lemma add_ass : forall n m p, n + (m + p) = (n + m) + p.
induction n.
simpl.
intros; reflexivity.
simpl.
intros; rewrite IHn.
reflexivity.
Qed.

(* finish the  following proofs by Defined instead of Qed in order  *)
(* to compute with the proofs. *)

Lemma eq_dec : forall n m : nat, n=m \/ ~n=m.
induction n as [|n]; intros [|m]; auto.
destruct (IHn m) as [h|h].
rewrite h; auto.
right.
injection.
auto.
Defined.
Eval compute in (eq_dec 0 0).
Eval compute in (eq_dec 5 6).

Lemma div2 : forall n, exists m, n=m+m \/ n = S(m+m).
Proof.
induction n as [|n].
  exists 0; left; trivial.
destruct IHn as [m [e|e]].
 exists m; right; rewrite e; trivial.
exists (S m); left; rewrite e.
rewrite addnSm; trivial.
Defined.

Eval compute in (div2 0).
Eval compute in (div2 5).
Eval compute in (div2 100).