The Coq mailing list

[Chantal KELLER <chantal.keller AT wanadoo.fr>]

Hi,

You can change yout goal into

1 subgoal
x : nat
y : nat
H : 2 * y = x \/ 1 + 2 * y = x
______________________________________(1/1)
2 * S y = S (S x)

by apply the tactic "unfold div2P in H."

But what you say next is not true : "2*y = x" is not a consequence of
H!! You would have to prove your current goal under the hypothesis "2*y
= x" then under the hypothesis "1+2*y = x"... but this is obviously false !

You shoud not use the tactic "constructor". You first need to destruct
H, before choosing which branch of your goal you are able to prove.


Here is a complete proof:

intros x y h.
unfold div2P in *.            (* unfolds the def of div2P everywhere *)
destruct h.                   (* destructs the or *)
left. rewrite <- H. ring.     (* in the first case, you can prouve the
property on the lhs *)

right. rewrite <- H. ring.    (* in the second case, you can prouve the
 property on the rhs *)


Chantal KELLER.



crateo a écrit :
> 
> 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.

-- 
Chantal KELLER
chantal.keller AT wanadoo.fr