The Coq mailing list

[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