Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] applying PROP's

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] applying PROP's


chronological Thread 
  • 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
> 
> 





Archive powered by MhonArc 2.6.16.

Top of Page