(** Mathematics for Computer Scientists 2 (G52MC2)
    Thorsten Altenkirch

    L09 (Natural numbers and some algebra)

    The material in this file contains coq proofs
    which can be read and animated with coqide or xemacs+proofgeneral.

**)

Section l09.

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

Eval compute in (mult 3 5).

Definition nth_odd (n : nat) : nat :=
  2*n + 1.

Eval compute in (nth_odd 3).

Fixpoint sum_odd (m : nat) : nat :=
  match m with
  | 0 => 0
  | S m' => nth_odd m' + sum_odd m'
  end.

Eval compute in (sum_odd 3).

Require Import Coq.Arith.Arith.

Theorem odd_sum : 
  forall n:nat,sum_odd n = n*n.
intro n.
induction n.
simpl.
reflexivity.
simpl.
rewrite IHn.
unfold nth_odd.
ring.
(*
replace (S (n + n * S n)) 
  with (1 + n + n * S n).
replace (n * S n) with (n + n*n).
replace (2 * n) with (n + n).
rewrite plus_assoc.
pattern (n + n + 1).
rewrite plus_comm.
rewrite plus_assoc.
reflexivity.
simpl.
rewrite plus_0_r.
reflexivity.
pattern (n * S n).
rewrite mult_comm.
simpl.
reflexivity.
simpl.
reflexivity.
Qed.
*)