(* ==================================================================== *) (* 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).