search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.72k stars 637 forks source link

eauto does not use immediate hint #8218

Open ghost opened 5 years ago

ghost commented 5 years ago

Version

The Coq Proof Assistant, version 8.8.1 (July 2018) compiled on Jul 3 2018 10:30:00 with OCaml 4.06.1

Operating system

Windows 10

Description of the problem

In the second goal below, eauto is not able to finish the proof.

Axiom X : Set.

Axiom df : X -> X -> Prop.
Axiom eq : X -> X -> Prop.

Axiom eq_df : forall x y, eq x y -> df x y -> False.
Hint Immediate eq_df.

Goal forall x y z, eq x y -> eq y z -> df y z -> False.
Proof. eauto. Qed.

Goal forall x y z, eq x y -> eq y z -> df x y -> False.
Proof. eauto. Abort.
Zimmi48 commented 5 years ago

Your bug title is misleading as your first example shows that eauto does use immediate hints. The problem with the second example is not that the hint is not used, it is that the "trivial" completion procedure fails. It fails in the same way that intros; eapply eq_df; eassumption succeeds on the first goal and fail on the second (because eassumption doesn't pick the right hypothesis, see also #287). A solution is to use typeclasses eauto with core instead of eauto because it will backtrack until it finds the right solution.