coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]how to prove basic arithmatic properties?

From: Jean-Marc Notin <notin AT lix.polytechnique.fr>
To: Carter Tazio Schonwald <carter.schonwald AT yale.edu>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]how to prove basic arithmatic properties?
Date: Wed, 21 Mar 2007 17:08:56 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Organization: CNRS - LIX

Here is the proof for distrib_mult_sum:

Theorem distrib_mult_sum : forall a b c : nat ,
     mult a (sum b c) = sum (mult a b) (mult a c).
Proof.
  induction a; simpl.
    trivial.

    intros b c.
    rewrite IHa.
    replace (sum (sum b c) (sum (mult a b) (mult a c))) with (sum b (sum
(sum c (mult a b)) (mult a c))).
    rewrite (commute_sum c); repeat rewrite assoc_sum; trivial.
    repeat rewrite assoc_sum; trivial.
Qed.

The proofs of assoc_mult and comm_mult can be made using
distrib_mult_sum, i guess...

--
Jean-Marc Notin
LIX - Équipe LogiCal

Attachment: signature.asc
Description: Ceci est une partie de message num�riquement sign�e

[Coq-Club]how to prove basic arithmatic properties?, Carter Tazio Schonwald
- Re: [Coq-Club]how to prove basic arithmatic properties?, Benjamin Gregoire
- Re: [Coq-Club]how to prove basic arithmatic properties?, Jean-Marc Notin
  - Re: [Coq-Club]how to prove basic arithmatic properties?, Jean-Marc Notin