The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

It's quite easy, I believe, to write a tactic that uses an axiom only if it's been imported, as long as you control both the file the tactic is written in and the file the axiom is declared in:
$ cat PreAxiomA.v
Ltac get_admitted := constr:(Set).
$ cat AxiomA.v
Require Import PreAxiomA.
Axiom admitted : False.
Ltac get_admitted ::= constr:(admitted).
$ cat Tactic.v
Require Import PreAxiomA.
Ltac stuff :=
  let maybe_axiom := get_admitted in
  lazymatch type of maybe_axiom with
  | False => idtac "axiom exists"
  | _ => idtac "no axiom"
  end.

(Code not tested, so no promises)

On Fri, Aug 19, 2016, 2:58 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 08/19/2016 03:44 PM, Ade Umut Huxtable wrote:
> Whether the split makes sense for a specific library is up to the maintainer to decide,

But, when talking about the standard library and standard plugins, it
seems like the user base should have considerable say in this regard.

> also allocating manpower might stop it from happening (ignorig project forks).

I don't understand what you mean there.

> Without the library commiting to the axiomless subset, an update is more likely to introduce actually used axioms in a user's development.

In the case when a lemma uses an axiom when there is an alternative
axiom-less proof (say by using UIP when UIP_dec would suffice), I think
such an unnecessary dependency on an axiom is a bug. Furthermore...

> It might be unrealistic to expect libraries to perform the split though, since apparently not even the standard library follows this suggestion...
>
> So: adding the feature "Print Module Assumptons X." to coqchk (or another tool) would be nice, but without library owner cooperation, users are at risk of suprise axioming. Also, having such a tool further lowers the motivation on libraries to actually bother with splitting.

... having the Print Module Assumptions X - or a checked variant that
would be something like Assert Module Assumptions X [assump1, assump2
...], or via a coqchk-like utility - when used by the standard library
itself would ease the maintenance of any such segregation of axioms.
The Assert mechanism would also provide users with an easy way to view
the assumption dependencies.

Still, despite your argument, it seems that the difficulties of dealing
with compatibility weigh quite heavily on Coq developers to the point
that such module splitting seems unlikely.

However, at least with the standard library, since all of the Coq script
source is available and should be understandable to Coq users, the users
that really care about segregating axioms can do so by making their own
copies of the standard library modules impacted.  This is less true of
plugins like Program mode and Psatz, where Coq users that depend on
those plugins are far less likely to understand their implementation to
the point of being able to do the segregation (and subsequent
maintenance) themselves.

-- Jonathan