The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Mon, Mar 11, 2013 at 03:43:01PM +0100, Arnaud Spiwack wrote:
> This sounds to me like piling a hack over a hack. 

I don't think it is an hack.  On the contrary updating the global
environment of a prover by side effect is an hack, and it has been used
to implement abstract, admit and on-demand generation of elimination
principles.

> Plus, do we really want
> to have "Axiom deamon : False" in the environment? I would personally feel
> a bit uncomfortable about that.

Why?  Do you feel uncomfortable having Obj.magic available in OCaml?

The real question is: are there parts of the system that would grab a
lemma from the environment and use it without telling you?
As far as I know it is not the case.

But all of this also applies to the solution you propose.  Can you be
sure no tactic will ever produce this special constr constructor by
mistake?  And even today, can you be sure a tactic does not add to the
environement an axiom?  We all suppoose that tactics have been
implemented in a reasonable way, and we grep for "[Aa]dmit" our .v file,
but this is easy to crack.  My proposal does not make things worse.

Print Assumptions is there to tell you if your theorem is axiom free, or
to list the axiom you currently rely on.  My proposal was just to print
the type of the goal you proved with the daemon axiom (that is stored in
the elimination predicate), given that the type of daemon is not that
informative taken alone.

The only thing I don't like is having a line "Axiom deamon : False"
in the prelude, that could puzzle a newcomer.
It would be better to have this axiom hardcoded in the environment with
a name that is not exposed to the user, but available to the tactics.

BTW, Isabelle's "sorry" command is implemented in this way too.
It just calls this deamon lemma "oracle", and the environments holds a
list of oracles IIRC.  I.e. to admit a subgoal you don't add names to
the environment. These names are already there, and can be used to prove
any statement, a sort of family of axioms for "forall A : Prop, A".

> In any case, if you want
> to have an irreducible/opaque let-in for "abstract", you'll have to stick
> you hand into Term.constr, won't you?

No, an opaque identity function is enough.

Cheers
-- 
Enrico Tassi