The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 08/19/2016 07:18 PM, Jason Gross wrote:
> 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)

Yes - but as you say, provided one has control over the content of the 
file that the axiom is declared in.  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.

This has the added benefit of allowing the user to provide an 
alternative and possibly conditional instance to axioms.  That might not 
be useful for Admitted, but consider proof_irrelevance, and alternative 
instances that can provide non-axiomatic proofs of the irrelevance of 
particular Props, such as UIP_dec.  That way, the user can use some 
tactic or plugin that normally uses proof_irrelevance (perhaps Program), 
and in cases where UIP_dec (which would then search for the appropriate 
eqdep instance) suffices, that would get used instead.

Although, to be fair, if we were really to consider all parts of Coq 
that would benefit from a redesign to involve typeclasses, this usage 
might not be at the top of the list.

-- Jonathan