coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: crateo <crateo AT gmail.com>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] applying PROP's
- Date: Mon, 12 Jan 2009 11:16:12 -0800 (PST)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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.
- [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.