The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi Victor,

  maybe I can help? Let's forget about classes and see what happens under the 
hood.

<<<
Require Import Setoid. 
Hypothesis P: nat->Prop.
Hypothesis Q: nat->Prop.

Axiom Eq: forall x:nat, P(x)<->Q(x).

Record C := {
 num: nat;
 cond: P num
}.

Section sect.
 Hypothesis Other: forall obj:C, Q (num obj).

 Lemma C2 : C.
 Proof. apply Build_C with 0.
   rewrite Eq. apply Other.
>>>

This fails, as you have no object of type [C] with a [num] field
set to [0] already built. You're in the process of trying to build
one though.

Hope this helps,
-- Matthieu

Le 14 nov. 2011 à 17:05, Victor Porton a écrit :

> Please help me to replace an admission with an actual proof script in this 
> .v file. (It seems particularly difficult to specialize over an object 
> variable of type C. This is the part I haven't succeeded myself without 
> your help.)
> 
> [[[[
> 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