(* 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 *) (* easy *) Lemma add0n : forall n:nat, 0 + n = n. (* this needs reasonning *) Lemma addn0 : forall n, n+0 = n. induction n. Lemma addSnm : forall n m, S n + m = S(n + m). Lemma addnSm : forall n m, n + S m = S (n + m). Lemma add_com : forall n m, n + m = m + n. Lemma add_ass : forall n m p, n + (m + p) = (n + m) + p. (* finish the two 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. 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). Eval compute in (div2 0). Eval compute in (div2 5). Eval compute in (div2 100).