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: frank maltman <frank.maltman AT googlemail.com>
To: julien forest <julienfore AT gmail.com>, <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n.
Date: Sat, 21 May 2011 19:50:40 +0000
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=date:from:to:subject:message-id:in-reply-to:references:x-mailer :mime-version:content-type:content-transfer-encoding; b=TkDuPB2/OTOFvAq71b8QBxaWXFdg/x1F8aEql2lvWZriNhMErSN3MO8nkFYuAH/u/I OLz6gVp+A8kOKumoHNoh0k6m9Np4pNKSQoLOppcRWPsC8KI2bIH+a3zKYOYFQfY3lbwK /jWo8XGDm7MEq568CrSshhNeYVM7sL27qyJL8=

On Sat, 21 May 2011 21:24:14 +0200
julien forest
<julienfore AT gmail.com>
wrote:

> You can try this way.
>
> Require Import Arith Div2 Omega.
> Functional Scheme div2_ind := Induction for div2 Sort Prop.
> Lemma div2_lt_trans : forall m n, m < n -> Div2.div2 m < n.
> Proof.
> intros m; functional induction (div2 m) using div2_ind.
>
> tauto.
>
> intros;omega.
>
> intros.
> destruct n.
> omega.
> apply lt_n_S.
> apply IHn.
> omega.
> Qed.

Thank you! I must admit, I understand very little of it, not
having come across functional induction yet...

[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