The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

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.

I don't entirely agree. Sort of by definition, you cannot update the global environment by any other mean than side effect. That said, it could probably be more principled. I don't think the question of whether a tactic should be given the right to update said environment is that clear cut.

 

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.

Well, it makes unsafe for a tactic from searching through the environment to look for thing. It's not very serious though. As long as it's clear, the tactics can just search through the environment-but-the-distinguished-unsafe-term

 

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.

Agreed.

> 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.

To be fair, I still haven't understood how this is supposed to play out? Is it a non-local modification of the proof term?

Let's make that a concrete question: what would be the proof term generated by

Goal True /\ True.

Proof.

split.

- abstract (exact I)

- exact I

Defined.

--

Arnaud