eauto fails with `Hint Immediate`/`Hint Resolve` on matching head symbol where `simple apply` succeeds

[mrhaandi]

Description of the problem

Possibly related: https://github.com/coq/coq/issues/6544 (but here the behavior is the other way around).

The documentation of Hint Immediate states that

adds the tactic simple apply qualid; solve [ trivial ] to the hint list associated with the head symbol of the type of qualid.

This appears contrary to the following example, where on a matching head symbol and successful simple apply the tactic eauto fails to use the hint. Also, Hint Resolve with a pattern fails whereas Hint Extern with the same pattern works.

Inductive test : nat -> nat -> Prop :=
  | test_intro n : test n (n + 1).

#[local] Hint Immediate test_intro : testdb_immediate.
#[local] Hint Resolve test_intro : testdb_resolve1.
#[local] Hint Resolve test_intro | 1 (test _ _) : testdb_resolve2.
#[local] Hint Extern 1 (test _ _) => simple apply test_intro; solve [ trivial ] : testdb_extern.

Goal test 0 1.
Proof.
  Succeed (simple apply test_intro; solve [ trivial ]). (* as expected *)
  Succeed (solve [eauto with testdb_extern]). (* as expected *)
  Fail (solve [eauto with testdb_resolve2]). (* surprising *)
  Fail (solve [eauto with testdb_resolve1]). (* consistent with testdb_resolve2 *)
  Fail (solve [eauto with testdb_immediate]). (* surprising, not as documented *)
  Fail (solve [eauto using test_intro]). (* consistent with above *)
Abort.

Coq Version

The Coq Proof Assistant, version 8.15.0 compiled with OCaml 4.14.0

(also tested with the 8.16 branch)

[QinshiWang]

In my opinion, it is a real bug rather than a documentation issue. We expect eauto as matching the head symbol and try simple eapply. It's very confusing if simple eapply works but eauto doesn't.

Inductive test : nat -> nat -> Prop :=
  | test_intro n : test n (n + 1).

#[local] Hint Immediate test_intro : testdb_immediate.
#[local] Hint Resolve test_intro : testdb_resolve1.
#[local] Hint Resolve test_intro | 1 (test _ _) : testdb_resolve2.
#[local] Hint Extern 1 (test _ _) => simple apply test_intro; solve [ trivial ] : testdb_extern.

Goal test 0 1.
Proof.
  debug auto with nocore testdb_resolve1.
Abort.

Here debug auto indicates simple apply test_intro fails.

(* debug auto: *)
* assumption. (*fail*)
* intro. (*fail*)
* simple apply test_intro (in testdb_resolve1). (*fail*)

[mrhaandi]

All of the above test cases succeed, if in auto.ml we set use_metas_eagerly_in_conv_on_closed_terms = true, which is also the default option for simple apply.

[mrhaandi]

Here is a minimal example, which I will use for regression tests:

Create HintDb db.
Parameter P : unit -> unit -> Prop.
Axiom HP : forall b, P b (id b).

#[local] Hint Resolve HP | 0 (P tt tt) : db.

Goal P tt tt.
Proof.
  Succeed solve [simple apply HP].
  Fail solve [debug auto with db]. (* reports simple apply HP (in db). (*fail*) *)
Abort.

[Blaisorblade]

@Janno informs me that simple apply is just false debug output, at least for TC search. For typeclasses eauto, the right tactic is class_apply, but I'm less sure what plain eauto uses:

(** Apply using the same opacity information as typeclass proof search. *)

Ltac class_apply c := autoapply c with typeclass_instances.

[Zimmi48]

The real issue is that there should be a way to access the internal version of simple apply that auto / eauto use.