Introduction to the Calculus of Inductive Constructions contains an example of the Post Correspondence Problem, where
eauto is used to automatically find a solution. However, I failed to reproduce the result.
Inductive word : Type := emp | a : word -> word | b : word -> word. Inductive post : word -> word -> Prop := start : post emp emp | R1 : forall x y, post x y -> post (a x) (b (a (a y))) | R2 : forall x y, post x y -> post (a (b x)) (a (a y)) | R3 : forall x y, post (b (b (a x))) (b (b y)). Inductive sol : Prop := sola : forall x, post (a x) (a x) -> sol | solb : forall x, post (b x) (b x) -> sol. Hint Constructors word. Hint Constructors post. Lemma ok : sol. eauto 6. Defined.
In the article,
ok will be found
ok = solb (b (a (a (b (b (b (a (a emp)))))))) (R3 (a (b (b (b (a (a emp)))))) (a (a (b (b (b (a (a emp))))))) (R2 (b (b (a (a emp)))) (b (b (b (a (a emp))))) (R3 (a emp) (b (a (a emp))) (R1 emp emp start)))) : sol
But when I try to run the code,
Error: Some unresolved existential variables remain. The context is
1 subgoal (ID 56) subgoal 1 (ID 56) is: word
(I’m new to Coq and doesn’t know the exact meanings of hint db,
Defined, and I have no idea why this happens…)
What’s wrong and how to fix this problem? Thanks!
Coq version: 8.11