coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jean-Francois Monin <Jean-Francois.Monin AT imag.fr>
- To: crateo <crateo AT gmail.com>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] applying PROP's
- Date: Mon, 19 Jan 2009 17:41:31 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hint: tactics elim, case; example elim H. Then search by yourself.
JF
On Mon, Jan 12, 2009 at 11:16:12AM -0800, crateo wrote:
>
> Hi, i'm a newbie in all this thing, and i'm struck in this problem. Please,
> give me one answer if you can : P. Here we go:
>
> I have this in coq:
>
> Fixpoint div2 (n : nat) : nat :=
> match n with
> |0=> 0
> |S 0=>0
> | S (S p) => S (div2 p)
> end.
> Definition div2P (x y : nat) : Prop := 2 * y = x \/ 1 + 2 * y = x.
> Require Export ArithRing.
> Lemma th : forall x y : nat, div2P x y -> div2P (S (S x )) (S y).
> intros.
> constructor.
>
> and the result in the console is:
>
> 1 subgoal
> x : nat
> y : nat
> H : div2P x y
> ______________________________________(1/1)
> 2 * S y = S (S x)
>
> The thing is that we know that "div2P x y" is true, by the definition we
> made before. I would want to change it for something like:
>
> x:nat
> y:nat
> H0:2*y=x \/ 1+2*y=x
> H:2*y=x
> ===============
> 2*Sy = S(Sx)
>
> That should not be very difficult, because H0 and H are logical deduction of
> the fact that div2P x y is true.
>
>
> How, for the shake of the glory chicken, can i do that?
>
> Thanks in advance.
> --
> View this message in context:
> http://www.nabble.com/applying-PROP%27s-tp21421615p21421615.html
> Sent from the Coq mailing list archive at Nabble.com.
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
> http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
>
- [Coq-Club] applying PROP's, crateo
- Re: [Coq-Club] applying PROP's, Edsko de Vries
- Re: [Coq-Club] applying PROP's, Luke Palmer
- Re: [Coq-Club] applying PROP's, Chantal KELLER
- Re: [Coq-Club] applying PROP's, Jean-Francois Monin
Archive powered by MhonArc 2.6.16.