intuition silently assumes axioms

[robbertkrebbers]

Consider:

From Coq Require Import ZArith.ZArith Program.Program.

Lemma foo {A} (n : nat) (a a0 : A)
  (e : Z.succ (Z.of_nat n) = 0%Z) :
  Z.eq_dec (Z.succ (Z.of_nat n)) 0 = left e ->
  Some a = Some a0.
Proof. intuition. Qed.

Print Assumptions foo.

This gives

Axioms:
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

It sounds very wrong that intuition silently creates a proof that involves axioms without the user explicitly being aware of that.

This example is derived from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/782, but in that Iris MR a different issue is discussed: the proof created by intuition creates some additional universe constraints.

Coq Version

$ coqc --version
The Coq Proof Assistant, version 8.13.1 (March 2021)
compiled on Mar 13 2021 10:35:46 with OCaml 4.11.1

This also happens with more recent versions, e.g., 8.15

[robbertkrebbers]

I just noticed that this evens happens with From Coq Require Program.Program, so if someone somewhere in my dependency chain requires Program, I get these axioms.

[Alizter]

I've seen Program introducing axioms before: https://github.com/coq/coq/issues/15408

[robbertkrebbers]

I think this one is even worse than https://github.com/coq/coq/issues/15408, this is not just when using Program, but when using a perfectly ordinary tactic like intuition.

[JasonGross]

Note that intuition is intuition auto with * (https://github.com/coq/coq/issues/7725), so intuition will use any hint in any database. Is this caused by axiom being used in some hint, or does it also show up if you do intuition idtac?

[JasonGross]

(I do seem to recall this also being an issue with tauto, which is intuition fail)

[robbertkrebbers]

Good catch. That looks like a horrible default for intuition. I see we also patched that default in std++, see https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/tactics.v#L29

Indeed, with intuition idtac the issue does not arise.