The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 08/19/2016 08:06 PM, Jonathan Leivent wrote:
> ...  But, if one has control over the content of the files containing 
> axioms, I would think that making them instances of typeclasses would 
> be a better approach than relying on redefined tactics:
>
> (*module1*)
> Class Admitted := admitted : False.
> Ltac Admit := elim admitted.
>
> (*module2*)
> Axiom admitted_axiom : False.
> Instance Admitted_instance : Admitted := admitted_axiom.

Actually, module2 could be eliminated - and each usage would just be 
required to do this:

Context {admitted_axiom : Admitted}.

If this were established as a standard, it might be possible to 
deprecate the Axiom declarative form completely.

Considering this, how much of an incompatibility would it be to do the 
following - everywhere in the standard library where Axiom Name : AType 
appears, replace it by:

Class AxiomClass := Name : AType.

Then, rebuild the standard library.  There will be definitions that fail 
- those that rely on the axioms.  In each case, take the failed 
definition and wrap it in a Section that includes the relevant Context 
for the required axioms (or just add the context directly to the 
definition's arguments).

Then, there are two kinds of modules - those where at least one Context 
declaration occurs at top level and those where all Context declarations 
are within Sections.  The standard library should only ever contain the 
latter.  Maybe have a coqc option such that coqc will not allow Contexts 
at top-level unless the option is turned on.  Have the .vo files 
resulting from modules compiled with this option tagged in some way so 
that it is easy for a tool like coqchk to spot them.

There would not be any new or differently named modules in the standard 
library, and all symbols they declare would still be present.  The 
impact on existing developments would be that if they rely on axioms, 
they would need to add the appropriate Contexts.  It would even be 
possible to have a compatibility file that provided all the Contexts 
that appear in the standard library.

OK - maybe it wouldn't be so hard to fix the standard library and 
plugins after all...

-- Jonathan