Ssreflect Users Discussion List

[Felipe Cerqueira <>]

On 5/4/16 5:14 PM, Felipe Cerqueira wrote:
> On 5/4/16 4:40 PM, Enrico Tassi wrote:
> > On Wed, May 04, 2016 at 11:43:59AM +0200, Felipe Cerqueira wrote:
> > > Hi everyone,
> > >
> > > I have a simple question about the coqchk output when importing 
> > > ssreflect.
> > > It seems to contain many Axioms from module types:
> > >
> > > |CONTEXT SUMMARY =============== * Theory: Set is predicative * Axioms:
> > > Ssreflect.fintype.SubsetDef.subsetEdef 
> > > Ssreflect.fintype.SubsetDef.subset
> > > MathComp.tuple.FinTuple.size_enum MathComp.finfun.FunFinfun.fun_of_finE
> > > MathComp.finfun.FunFinfun.fun_of_fin MathComp.finfun.FunFinfun.finfunE
> > > MathComp.finfun.FunFinfun.finfun MathComp.tuple.FinTuple.enumP
> > > Ssreflect.fintype.Finite.EnumDef.enumDef MathComp.tuple.FinTuple.enum
> > > Ssreflect.fintype.Finite.EnumDef.enum 
> > > Ssreflect.fintype.CardDef.cardEdef
> > > Ssreflect.fintype.CardDef.card MathComp.bigop.BigOp.bigopE
> > > MathComp.bigop.BigOp.bigop |
> > If you look at the files, all these "axioms" look like
> >
> >    Module Type EnumSig.
> >    Parameter enum : ∀ cT : type, seq cT.
> >    Axiom enumDef : enum = fun cT ⇒ mixin_enum (class cT).
> >    End EnumSig.
> >
> >    Module EnumDef : EnumSig.
> >    Definition enum cT := mixin_enum (class cT).
> >    Definition enumDef := erefl enum.
> >    End EnumDef.
> >
> > This trick hides a program's body behind a name and an unfolding 
> > equation (enum
> > and enumDef respectively).  The program is there, and the equation is 
> > proved by
> > reflexivity.
> > This way of doing things works around performance issues: Coq never
> > unfolds "enum" automatically, but you can rewrite with the equation in
> > the middle of a proof to unravel the body of enum.
> >
> > All in all, enum and enumDef are not Axioms even if they "do not 
> > compute".
> > Coqchk does not understand it.  I thought it was fixed in 8.5, but I 
> > guess I'm
> > wrong.
> >
> > Best,
>
> Hi Enrico,
>
> Thanks for the reply. Good to know that this doesn't occur in 8.5.
> I haven't ported my project to 8.5 yet because there was no additional 
> functionality that I needed so far.
> Sorry for the false alarm.
>
> Felipe
Hi,

I know that these are not axioms, but I just wanted to let you guys know 
that the issue still occurs in the latest version.

With Coq 8.5pl1 and ssreflect 1.6, running 'make validate' yields the 
following output:

CONTEXT SUMMARY
===============

* Theory: Set is predicativeTheory: Stratified type hierarchy

* Axioms:
    mathcomp.ssreflect.finfun.FunFinfun.finfunE
    mathcomp.ssreflect.finfun.FunFinfun.fun_of_finE
    mathcomp.ssreflect.fintype.SubsetDef.subsetEdef
    mathcomp.ssreflect.fintype.Finite.EnumDef.enumDef
    mathcomp.ssreflect.finfun.FunFinfun.fun_of_fin
    mathcomp.ssreflect.tuple.FinTuple.enumP
    mathcomp.ssreflect.tuple.FinTuple.enum
    mathcomp.ssreflect.bigop.BigOp.bigopE
    mathcomp.ssreflect.finfun.FunFinfun.finfun
    mathcomp.ssreflect.tuple.FinTuple.size_enum
    mathcomp.ssreflect.fintype.CardDef.card
    mathcomp.ssreflect.fintype.CardDef.cardEdef
    mathcomp.ssreflect.bigop.BigOp.bigop
    mathcomp.ssreflect.fintype.SubsetDef.subset
    mathcomp.ssreflect.fintype.Finite.EnumDef.enum

Thanks,
Felipe