(** Introduction to Formal Reasoning (G52IFR)
    Nuo Li

    T05

**)

Section T5.

Load Arith.


Fixpoint g (m n : nat) {struct m} : nat :=
  match m with 
  | 0 => n
  | S m' => S (g m' n)
  end.

(* What is g? Try a few examples *)
Eval compute in (g 1 2).
Eval compute in (g 10 12).

Lemma mult_1_bothSides : forall n, 1 * n * 1 = n.
intro.
simpl.
rewrite <- plus_n_O.
induction n.
reflexivity.
simpl.
rewrite IHn.
reflexivity.
Qed.




Fixpoint sum n {struct n} : nat := 
  match n with
    | 0 => 0
    | S k => sum k + (S k)
  end.

Hypothesis mult_comm : forall n m, n * m = m * n.


Lemma exchange : forall a b c d : nat, a + b + (c + d) = a + c + (b + d).
intros.
rewrite plus_assoc.
pattern (a + b + c).
rewrite <- plus_assoc.
rewrite (plus_comm b c).
rewrite plus_assoc.
rewrite plus_assoc.
split.
Qed.

Theorem gauss : forall n, 2 * sum n = n * (S n).
intro.
induction n.
reflexivity.
simpl.
rewrite <- plus_n_O.
rewrite exchange.
replace (sum n + sum n) with (n * S n).
rewrite plus_assoc.
rewrite plus_comm.
rewrite (plus_comm (n * S n) (S n)).
replace (S n + (S n + n * S n)) with ((S (S n)) * (S n)).
rewrite mult_comm.
split.
split.
rewrite <- IHn.
simpl.
rewrite <- plus_n_O.
split.
Qed.


End T5.


Lemma n_Sn : forall n : nat, n <> S n.
intro.
induction n.
intro.
discriminate H.
intro.
apply IHn.
apply peano8.
assumption.
Qed.


Lemma t2 : forall n, n = S n -> n = n + 1.
intros.
destruct (n_Sn n H).
Qed.


Notation "m <= n" := (leq m n).

Theorem le2n : forall n : nat, n <= (n + n).
intros.
exists n.
reflexivity.
Qed.

End T5.