Can't automate lemme that works manually in Coq
(It seems like my previous question had too much irrelevant information, so I tried to digress the details. I'm not sure if this is still the same problem, but I'll delete another question if the same solution works for both.)
I am trying to explain some custom lists and predicates:
Inductive alphabet := A.
Definition sentence : Type := list alphabet.
Variable pred1 : sentence -> Prop.
Variable pred2 : sentence -> Prop.
Variable conclusion : Prop.
Now, with the following hypotheses:
Hypothesis H1 : forall (X : sentence),
pred1 X -> pred2 (X ++ X).
Hypothesis H2 : forall X,
pred2 X -> conclusion.
I want to prove
Example manual : pred1 [A] -> conclusion.
This is obviously true, as it conclusion
follows when someone sentence
has pred2
, and pred1
for anyone sentence
implies that repetition of it sentence
has pred2
. Written proof would be
intro. eapply H2. apply H1. exact H. Qed.
Please note that in the proof of use only intro
, apply
, eapply
and exact
. This means that the proof must provide direct automation as long as H1
it is H2
available in context. For example, the semi-automatic version
Example semiauto : pred1 [A] -> conclusion.
pose proof H1. pose proof H2. eauto. Qed.
works as you expected. Now try the fully automated version with prompts:
Hint Resolve H1 H2.
Example auto : pred1 [A] -> conclusion.
eauto.
intro.
eauto.
eapply H2.
eauto.
apply H1.
eauto. Qed.
This is strange. eauto
occurs not only at the beginning, but also at every step, except for the last. Why is this happening?
Some guesswork: the follow-up H1
includes a shape X ++ X
that could cause unification problems. Perhaps Coq does some implicit cleanup with help H1
when it's explicitly injected into the context, but not when it's just at the DB hint.
Any ideas?
The problem is transparency sentence
.
Based on Anton Trunov's answer, if you look very closely, you will notice that the difference between Print HintDb core
and Create HintDb foo. Print HintDb foo.
is what Print HintDb core
says
Unfoldable variable definitions: none
Unfoldable constant definitions: none
but Create HintDb foo. Print HintDb foo.
says
Unfoldable variable definitions: all
Unfoldable constant definitions: all
I've built the following simplified version of your example:
Require Import Coq.Lists.List.
Import ListNotations.
Definition sentence := list nat.
Variable pred1 : sentence -> Prop.
Variable pred2 : sentence -> Prop.
Hypothesis H1 : forall (X : sentence),
pred1 X -> pred2 (X ++ X).
Create HintDb foo.
Hint Resolve H1 : foo.
Hint Resolve H1 : bar.
Hint Resolve H1.
Example ex1 : pred1 [0] -> exists X, pred2 X.
eexists.
debug eauto.
Here we have that eauto
both eauto with bar
(and eauto with bar nocore
, which removes the underlying database from consideration eauto
) both fail, but eauto with foo
(and eauto with foo nocore
) succeeds. This suggests that the issue is transparency. After playing around a bit, I found that it eauto
would work if we write
Hint Transparent sentence.
Also, even without it, it eauto
works fine if I explicitly pass the X
expanded type to the variable :
Example ex2 : pred1 [0] -> exists X : list nat, pred2 X.
I'm not entirely sure why Coq behaves this way ... maybe it refuses to unify evars with terms that are of different types (if it ?X
has a type sentence
, when it X ++ X
has a type list
), or maybe it is a meta-unification override ... Me opened a bugtracker issue about this lack of documentation / bad behavior .
A possible workaround here is to add hints to the new user database:
Create HintDb my_hints.
Hint Resolve H1 H2 : my_hints.
Now we can finish the proof:
Example auto : pred1 [A] -> conclusion.
eauto with my_hints. Qed.
One more thing: the Coq reference manual tells ( §8.9.1 ) us that
You can query the database of prompts using the command
Create HintDb
. If a hint is added to an unknown database, it will be automatically created.
But if we omit a part Create HintDb my_hints.
, the tactic eauto
won't work. It looks like the same thing happens when hints are added to the default hints database core
.