What does `auto` do differently under the hood?

Consider this code:

From Coq Require Import ZArith.
Notation ℤ := Z.
Open Scope Z_scope.

Hint Resolve Z.sub_add: localHints.

Definition f (x: ℤ): ℤ := x - 100.
Definition g (x: ℤ): {y | f y = x} := ltac:(debug eauto with localHints).

It does not type check. But this does:

From Coq Require Import ZArith.
Notation ℤ := Z.
Open Scope Z_scope.
Definition f (x: ℤ): ℤ := x - 100.

Definition g (x: ℤ): {y | f y = x} := ltac:(debug eauto using Z.sub_add).

I know that auto tries to use simple eapply under the hood and it is not strong enough to solve this goal — eapply without simple is needed. But why does the using option work?

Here is what debug says:

Debug: 1 depth=5
Debug: 1.1 depth=4 simple eapply exist
Debug: 1.1.1 depth=4 simple apply Z.sub_add
g is defined

When I literally write this down in a proof script, it predictably fails.

Definition g (x: ℤ): {y | f y = x}.
Proof.
  simple eapply exist.
  simple apply Z.sub_add.
Unable to unify "?M1384 - ?M1383 + ?M1383 = ?M1384" with 
"f ?y = x".

What is going on?

Apparently this was reported before: `auto using` uses more powerful unification than `simple apply` · Issue #6198 · coq/coq · GitHub

Although I personally replied to this issue, I didn’t really investigate the reason of this behavior discrepancy at that time.

Now I did, and it turns out it has something to do with hint database transparency. As documented in Programmable proof search — Coq 8.13.1 documentation, implicitly created hint databases have a default transparency set to opaque.

But with the using clause, eauto will create a local database with a transparent transparency:

This explains the difference, and is confirmed by the fact that the following typechecks:

From Coq Require Import ZArith.
Notation ℤ := Z.
Open Scope Z_scope.

Create HintDb localHints.

Hint Resolve Z.sub_add: localHints.

Definition f (x: ℤ): ℤ := x - 100.
Definition g (x: ℤ): {y | f y = x} := ltac:(debug eauto with localHints).

And the following as well:

From Coq Require Import ZArith.
Notation ℤ := Z.
Open Scope Z_scope.

Hint Resolve Z.sub_add: localHints.

Hint Constants Transparent : localHints.

Definition f (x: ℤ): ℤ := x - 100.
Definition g (x: ℤ): {y | f y = x} := ltac:(debug eauto with localHints).
1 Like