The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 12/15/2015 07:22 PM, Gregory Malecha wrote:
> Hello --
>
> I just did a "Print Assumptions foo" on my final theorem and found out that
> some of my development depends on the following axiom:
>
> Eqdep.Eq_rect_eq.eq_rect_eq : forall (U : Type) (p : U)
>                                  (Q : U -> Type) (x : Q p)
>                                  (h : p = p), x = eq_rect p Q x p h
>
> After tracing down the bug for about 20 minutes, I found that it was
> introduced by a call to [intuition]. [intuition] uses some hint databases
> that include axioms. The above axiom was included by the following chain of
> includes and definitions.
>
> Coq.Classes.EquivDec
> which includes
> Coq.Program.Program
> which includes
> Coq.Program.Equality
> which defines the following
>
> Ltac is_ground_goal :=
>    match goal with
>      |- ?T => is_ground T
>    end.
>
> (** Try to find a contradiction. *)
> Hint Extern 10 => is_ground_goal ; progress exfalso : exfalso.
>
> and includes
> Coq.Logic.Eqdep
> which contains the hint
> Hint Resolve eq_dep_eq: eqdep v62.
>
> I assume that one of these databases (eqdep or v62) is included by default.
>
> This seems like bad behavior and I'm wondering if it is possible to prevent
> tactics from using axioms that occur in hint databases. I'm also wondering
> if anyone knows a fragment of the standard library that is safe to use and
> avoid axioms.

intuition is really a shorthand for "intuition auto with *"  - so if you 
want intuition to restrict the hint database, you need to provide its 
secondary tactic instead of allowing that to default to "auto with *".

There aren't many built in tactics that do things like "auto with *".  
Another is firstorder, which is an enhanced version of intuition.  I 
can't think of any more.

-- Jonathan