The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Dear Auger,

Although you did not understand what I asked (because I was unclear),
however your answer helped me to think better and to find a solution to my
problem.

Thanks anyway,

Marko Malikoviæ

> Le Mon, 25 Apr 2011 18:08:51 +0200 (CEST),
> Marko Maliković 
>Â <marko AT ffri.hr>
>  a écrit :
>
>> Hello all,
>>
>> Perhaps the following question is naive but I do not find a solution:
>>
>> Is it possible context, which contains a hypothesis with dependent
>> product, for example:
>>
>> H : forall A : Prop, A
>> ============================
>>  goal
>>
>> into the context with quantifier free hypothesis:
>>
>> A : Prop
>> H : A
>> ============================
>>  goal
>>
>> Are the above two proofs equivalent at all?
>>
>> Thanx and greetings,
>>
>> Marko Maliković
>>
>
> Your question is not clear, but your first case is rather a proof of
> "(forall A, A) -> goal" (which is trivial to prove, just apply H), and
> the second is rather a proof of "forall A, A -> goal" (which may be
> non trivial or even false, depending on "goal").
>
> So, as the things to prove are different, I guess that knowing if the
> proofs are equivalent has no real meaning.
>
> What is equivalent is rather:
> "
> A: Prop
> H: A
> ==============
> goal
> ",
> "
> A: Prop
> ==============
> forall (H:A) -> goal
> " and
> "
> ==============
> forall (A:Prop) (H:A) -> goal
> "
> but I guess you already know it
>


-----------------------
Dr. Sc. Marko Malikoviæ
Filozofski fakultet
Sveuèili¹te u Rijeci
---------------------
Ph.D. Marko Malikoviæ
Faculty of Humanities and Social Sciences
University of Rijeka, Croatia
-----------------------------
marko AT ffri.hr
http://www.ffri.hr/~marko
-------------------------