The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

To do this, you need to provide a proof of P 0.
In your context you have no information about P. The only thing you could do
is apply Eq and have to prove Q 0. But you have no information about Q either.
Your hypothesis Other doesn't apply here *because your are defining C2*.
Since you are defining in, it does not exist yet, so the "forall" in
Other doesn't
catch it.

Let's be clear: while doing a proof of an Instance, the object you are
creating does not exist
until the Qed. Interactive proof is here to ease your way to define
things, but things only
exists at the end of the proof.

Vincent

2011/11/14 Victor Porton 
<porton AT narod.ru>:
> 14.11.2011, 20:22, "Alexandre Pilkiewicz" 
>Â <alexandre.pilkiewicz AT polytechnique.org>:
>> Just for your information
>>
>> <<<
>> Require Import Setoid.
>> Hypothesis P: nat->Prop.
>> Hypothesis Q: nat->Prop.
>>
>> Axiom Eq: forall x:nat, P(x)<->Q(x).
>>
>> Class C := {
>>  num: nat;
>>  cond: P num
>> }.
>>
>> Lemma Other: forall obj:C, Q num.
>> Proof.
>>   intros. rewrite <- Eq. apply cond.
>> Qed.
>> Your "Other" axiom is provable. Which means that obviously it won't
>> allow you to magically prove "P x" for an arbitrary x,
>> like you seem to think it should. Once again, while you are defining a
>> instance of C, this instance does not exists. It would allow you to
>> prove False quite easily.
>
> Yes, it is provable. But it isn't obvious for Coq prover. It is what I need 
> with the purpose of testing, to make some statement which is to be proved 
> explicitly.
>
> I don't think that it would prove "P x" for an arbitrary x. I am just 
> playing around with testing different features of Coq.
>
> Alexandre, thanks for your information, but you haven't answered my 
> question: How to prove [Instance C2]?
>
>> <<<
>> Require Import Setoid.
>> Definition P (n:nat) := False.
>> Definition Q (n:nat) := False.
>>
>> Lemma Eq: forall x:nat, P(x)<->Q(x).
>> Proof. unfold P, Q. tauto. Qed.
>>
>> Class C := {
>>  num: nat;
>>  cond: P num
>> }.
>>
>> Section sect.
>>  Hypothesis Other: forall obj:C, Q num.
>>
>>  Instance C2: C := { num:=0 }.
>>  Proof. generalize Other. admit. Defined.
>>
>> End sect.
>>
>> Lemma Other: forall obj:C, Q num.
>> Proof.
>>   intros. rewrite <- Eq. apply cond.
>> Qed.
>> Goal False.
>>   pose proof (C2 Other). apply cond.
>> Qed.
>>
>> On Mon, Nov 14, 2011 at 11:05 AM, Victor Porton 
>>Â <porton AT narod.ru>
>>  wrote:
>>
>>>  Hypothesis P: nat->Prop.
>>>  Hypothesis Q: nat->Prop.
>>>
>>>  Axiom Eq: forall x:nat, P(x)<->Q(x).
>>>
>>>  Class C := {
>>>   num: nat;
>>>   cond: P num
>>>  }.
>>>
>>>  Section sect.
>>>   Hypothesis Other: forall obj:C, Q num.
>>>
>>>   Instance C2: C := { num:=0 }.
>>>   Proof. generalize Other. admit. Save.
>>>  End sect.
>>>
>>>  Axiom ax: forall obj:C, Q num.
>>>
>>>  Definition C3 := C2(ax).
>
> --
> Victor Porton - http://portonvictor.org
>