coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n.

From: Chris Dams <chris.dams.nl AT gmail.com>
To: frank maltman <frank.maltman AT googlemail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n.
Date: Sat, 21 May 2011 13:22:27 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=NSlmUB+iMjQORv0YDR1r1PEniqFlz0CgqZNYVYBlcv0K5Jq552NXNbME2YkmP0wxnn 8qJ0Z0/mOBBKvtCPS3l0byhEvuVyWKxlOH9J3NCcAdgIpfVv0vUKbS7SsYelPNGX6F76 pwbUwW0rpQzic1WNFATWZPt7MhL/ovu0BWuBg=

Dear Frank,

The idea is to get something of the form div2 (S (S m)) because div2
has been recursively defined as becomes apparent when you do Print
div2.

I found the following proof that utilizes this. The first S in (S n +
S n) moves to the front automatically because addition is recursive in
the first argument. The second one needs to helped a bit by using
plus_n_Sm.

Lemma divplus : forall n, div2 (n + n) = n.
intro n.
induction n as [|n IH]; [tauto|].
simpl.
rewrite <- plus_n_Sm.
f_equal.
assumption.
Qed.

[Coq-Club] Stuck on a proof of div2 (n + n) = n., frank maltman
- Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., Chris Dams
  - Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., frank maltman
    - Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., frank maltman
      - Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., julien forest
        
        Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., frank maltman
      - Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., Pierre Casteran
        
        Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., frank maltman
        
        Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., Pierre Casteran
        
        Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., frank maltman