Ssreflect Users Discussion List

[Georges Gonthier <>]

   This is a well-known design flaw of the Print Assumptions command, which 
equates module abstraction with axioms. There are no axioms in the ssreflect 
library, only definitions packaged in submodules and made opaque by signature 
ascription.
   The "-o" option of the independent checker "coqchk" has the same design 
error (contrary to what the command documentation implies). It is anyway 
probably not an option for you, because it breaks down fairly early on the 
ssreflect library :
  - in finfun, for the distributed library, because it interprets the 
signature ascription of finfun.FunFinfunSig more strictly than coqtop.
  - in choice, for the current working library, apparently because it imposes 
stronger universe checks than coqtop.

   Sorry,
Georges

-----Original Message-----
From: Vincent Siles [] 
Sent: 13 June 2011 10:25
To: 
Subject: how to describe some of the choices made for ssreflect for a "not 
used to coq" reviewer ?

Dear everyone,
I'm wondering if anyone already encountered the following problem and how to 
deal with it "in a nice way":
I have a fully formalized program within ssreflect, which doesn't rely on any 
axioms. I can even compute with it within Coq.

However, "Print Assumptions" will return

Axioms:
card : forall T : finType, mem_pred T -> nat cardEdef : card = (fun (T : 
finType) (mA : mem_pred T) => size (enum_mem mA)) Finite.EnumDef.enum : 
forall cT : finType, seq cT Finite.EnumDef.enumDef : Finite.enum =
                         (fun cT : finType =>
                          Finite.mixin_enum (Finite.class cT))


I know that this follows the following scheme:
Axiom A : foo.
Axiom Adef : A = <actual code of A>.

Is there a "standard" reference to this design choice I can point to so that 
any reviewer can be convinced that my work does not actually rely on any 
axioms ?

Cheers,
Vincent