Do not apply discriminated unfold hints on arbitrary goals.

[ppedrot]

The current behaviour was to indiscriminately try to apply on any goal unfold hints for transparent constants from discriminated databases, since they were not indexed by the head constant. In particular, this might have unfolded the constant even if it was at the head of the goal, contrarily to what the documentation claimed.

I think it was written this way out of fear of the dnet pattern algorithm. In discriminated mode, transparent constants are considered to match everything, but maybe the author of the code was confused by the complexity of the dnet implementation.

This patch changes the semantics of auto tactics in fringe cases, and should be mostly backwards compatible.

Fixes #14874: Exponential blowup with Hint Unfold.

[ppedrot]

Here is a minimal example of a fringe case.

Create HintDb foo discriminated.

Definition F (n : nat) := n.

Inductive Pred : nat -> Prop := pred : forall n, Pred (S n).

#[local]
Hint Unfold F : foo.

#[local]
Hint Resolve pred : foo.

Print HintDb foo.

Goal forall n, Pred (F (S n)).
Proof.
intros n.
solve [ auto with foo ]. (* with this PR auto leaves the goal unchanged and this line fails *)
Qed.

[coqbot-app]

Hey, I have detected that there were CI failures at commit 3d8c49d without any failure in the test-suite.
I checked that the corresponding jobs for the base commit 1bba7d6 succeeded. You can ask me to try to extract a minimal test case from this so that it can be added to the test-suite.
If you tag me saying @coqbot ci minimize, I will minimize the following targets: ci-hott, ci-math_classes.

[ppedrot]

CI shows that only HoTT, math-classes and (by transitivity) corn are broken. It seems quite a small change in the end thus, so maybe it's worth pursueing and writing overlays. @mattam82 what do you think?

[ppedrot]

Let's close for the time being, I'll reopen after the deadzone known as summer.

[coqbot-app]

Hey, I have detected that there were CI failures at commit 641dd02 without any failure in the test-suite.
I checked that the corresponding jobs for the base commit 89818ca succeeded. You can ask me to try to extract a minimal test case from this so that it can be added to the test-suite.
If you tag me saying @coqbot ci minimize, I will minimize the following targets: ci-hott, ci-math_classes.

[coqbot-app]

Hey, I have detected that there were CI failures at commit 641dd02 without any failure in the test-suite.
I checked that the corresponding jobs for the base commit 89818ca succeeded. You can ask me to try to extract a minimal test case from this so that it can be added to the test-suite.
If you tag me saying @coqbot ci minimize, I will minimize the following targets: ci-hott, ci-math_classes.

[ppedrot]

Why are there CI failures in ml-api and refman? In the first case I don't see how it's related to this PR and in the second I don't even see any outstanding error.

[ppedrot]

All overlays were merged, so this is ready to go as-is and needs an assignee.

[SkySkimmer]

Maybe we could have a test for this?

[ppedrot]

Do you want a positive or a negative test?

[SkySkimmer]

Why not both?

[SkySkimmer]

ping

[ppedrot]

@SkySkimmer test added.

[SkySkimmer]

This test passes in master, shouldn't we test the changed behaviour?

[ppedrot]

You're right, let me add another discriminating test.

[SkySkimmer]

@coqbot merge now