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: Luke Palmer <lrpalmer AT gmail.com>
  • 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 09:23:53 -0700
  • 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=VudEasq1PYLXLWzWKwstlh+MHPVPtEf4snrfvL4U9bXhGN8HM+8FXPZEy0lzScsSOp EQ8O6iMietF3zZUoyTj/b6029ihAIx+l7etVprru0W09RHlfCutZFPt+SQODQCfvhUAY TVdl4vHEQOBP36UFtNfUXJ7P/GJKFQyzAX1x0=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Mon, Jan 12, 2009 at 12:16 PM, crateo <crateo AT gmail.com> 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.

I don't see how you're going to get the H you want.

To unfold div2P x y, you can "unfold div2P in H" or "red in H".

However, you are going to run into trouble, as you applied "constructor" too soon.  The branch of the disjunction you are trying to create depends on the disjunction you are given (H).  So destruct H *first*, then use "left" or "right" depending on which one it is in each case.

(I don't know what "constructor" does, but I didn't have to use it to complete this proof)

Happy mathhacking!

Luke



Archive powered by MhonArc 2.6.16.

Top of Page