The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

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.

--

gregory malecha