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".
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).