The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

If I understand well you want to prove:

x : A
Hi : P x
======
forall y, P y

which is false.

Maybe you should try to prove something else :)

Best regards,
P.




2015-04-27 16:17 GMT+02:00 richard dapoigny 
<richard.dapoigny AT univ-savoie.fr>:
> Le 27/04/2015 15:57, Pierre Courtieu a écrit :
>>
>> Hi,
>>
>> This is no true and therefore not provable.
>>
>> But if you add parenthesis over the first quantified part then it is a
>> different property (and probably the on one you meant?) that is
>> provable by "intro h; assumption."
>>
>> (forall x, (* some complex function depending on x*)) -> forall y, (*
>> the same complex function depending on y*)
>>
>> For examepl:
>>
>> Variable A:Type.
>> Variable P: Type -> Prop.
>>
>> Goal (forall x, (P x)) -> (forall y, P y).
>> Proof.
>>    intro h.
>>    assumption.
>>
>> Best regards,
>> Pierre
>
> Thanks for the prompt answer!
> Yes I would like to have the goal you suggest but the problem is that the
> left part is generated by applying generalize x Hi (wher Hi is another
> hypothesis) and therefore I cannot obtain the whole expression due to a lack
> of parentheses
>
>>
>>
>> 2015-04-27 15:42 GMT+02:00 richard dapoigny
>> <richard.dapoigny AT univ-savoie.fr>:
>>>
>>> Hi all,
>>> I try to demonstrate a goal having the form:
>>> forall x, (* some complex function depending on x*) -> forall y, (* the
>>> same
>>> complex function depending on y*)
>>> Is there a simple way to do it?
>>> Thanks in advance,
>>> Richard
>
>