Ssreflect Users Discussion List

[Enrico Tassi <>]

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,
-- 
Enrico Tassi