The Coq mailing list

[Carter Tazio Schonwald <carter.schonwald AT yale.edu>]

Hello all,
   as an exercise to familiarize myself with using coq to formalize 
proofs, i've been working on
proving the basic properties of addition and multiplication on the 
natural numbers (ie commutivity, associativity, and distributivity) 
starting from just an inductive datatype for natural numbers and 
recursive definitions for addition and multiplication. I'm somewhat 
stumped as to how to approach proving commutivity, associativity and 
distributivity of multiplication. Any suggestions?
thanks!
-Carter
I've attached the development  below
Inductive nat:Set := | O : nat | S : nat->nat.


Fixpoint sum (a:nat)(b:nat) {struct a}: nat :=
  match a with
    O => b
    |S c => S (sum c b) end.

Fixpoint mult ( a   b : nat ) {struct a} : nat :=
  match a with
    O => O
    | S c => sum b (mult c b) end.

Lemma identity : forall (a : nat), sum O a = a. 
induction a.
simpl.
trivial.
simpl.
trivial.
Qed.

Lemma identity' : forall (a : nat), sum a O = a. 
induction a.
simpl.
trivial.
simpl.
rewrite IHa.
trivial.
Qed.

Lemma extern: forall a b : nat, sum a (S b) = S (sum a b).
induction a.
simpl.
intros.
trivial.
intros.
simpl.
rewrite IHa.
trivial.
Qed.

Theorem commute_sum : forall (a b : nat), sum a b = sum b a.
induction a.
intros.
simpl.
rewrite identity'.
trivial.

intros.
simpl.
rewrite IHa.
rewrite extern.
trivial.
Qed.





Theorem assoc_sum1 : forall b c : nat, sum O (sum b c) = sum( sum O b) c.
intros.
apply identity.
Qed.

Theorem SnatEq : forall a b : nat, a =  b ->  S a = S b.
intros.
induction a.
destruct H.
trivial.
destruct H.
trivial.
Qed.





Theorem assoc_sum : forall (a b c : nat), sum a (sum b c) = sum (sum a b )c.
intros.
induction a.
simpl.
trivial.
simpl.
destruct IHa.
trivial.
Qed.
Theorem doubletime : forall a : nat ,  mult (S (S O)) a = sum a  a  .
intros.
simpl.
symmetry.
rewrite identity'.
trivial.
Qed.


Theorem Smultn : forall a n : nat , mult( S a) n = sum n (mult a n). 
intros.
simpl.
trivial.
Qed.

Theorem multO : forall a : nat , mult a O = O.
intros.
induction a.
simpl.
trivial.
rewrite Smultn.
simpl.
apply IHa.
Qed.

Theorem Smultninv : forall a n :nat,  sum n (mult a n) =  mult( S a) n.
intros.
symmetry.
apply Smultn.
Qed.


Theorem mult1  : forall a : nat, mult a (S O) = a.
intros.
induction a.
simpl.
trivial.
rewrite Smultn.
simpl.
induction a.
simpl.
trivial.
rewrite IHa.
trivial.
Qed.


Theorem assoc_multOc : forall a b : nat, mult a (mult b O) = mult (mult a b) 
O.
intros.
rewrite multO.
rewrite multO.
rewrite multO.
trivial.
Qed.

Theorem assoc_multOb : forall a c : nat, mult a (mult O c) = mult (mult a O) 
c.
simpl.
symmetry.
rewrite multO.
simpl.
trivial.
Qed.

Theorem trans_multOa : forall b c :nat , mult O (mult b c) = mult (mult O b) 
c.
intros.
simpl.
trivial.
Qed.

(*
how to prove these?

Theorem trans_mult : forall a b c : nat, mult a (mult b c) = mult (mult a b) 
c.

Theorem comm_mult : forall a b : nat, mult a b = mult b a .

Theorem distrib_mult_sum : forall a b c : nat ,
     mult a (sum b c) = sum (mult a b) (mult a c).
*)