The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

I'm surprised that [C2] has type [C], so I think Victor has a legitimate 
point here.  The usual section behavior rules imply to me that [C2] 
should be parametrized over [Other].

On the other hand, the specific proposition used for [Other] is 
dangerously close to inconsistent (easily implies [False] for any 
interesting choice of [Q]), so there may be other serious issues in the 
code.

Victor Porton wrote:
> See also this my bug report:
>
> http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2642
>
> 14.11.2011, 18:58, "Thomas 
> Braibant"<thomas.braibant AT gmail.com>:
>
>    
> >   - C2 has type "C"
> >   - whatever the type of ax2, you cannot apply C to it, because "C" is
> >   not a function type.
> >   - it happens that "ax2 C" as type "Q num", but since your whole script
> >   does not has much sense to me, I cannot assume that it was what you
> >   wanted to write.
> >
> >   Cheers,
> >   thomas
> >
> >   On Mon, Nov 14, 2011 at 3:41 PM, 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. Admitted.
> > >    End sect.
> > >
> > >    Axiom ax2: forall obj:C, Q num.
> > >
> > >    Definition C3 := C2(ax2).
> > >