Hi, all!
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, Defined
complains 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, eauto
and Defined
, and I have no idea why this happens…)
What’s wrong and how to fix this problem? Thanks!
Coq version: 8.11