Couldn't reproduce the result of an example from Intro to CIC

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

I’m confused… After moving code around and reverting all the changes, `eauto` doesn’t seem to make any progress now.

``````1 subgoal (ID 50)

============================
sol
``````

Just two simple copy mistakes apparently:

• wrong `R3`, it should be: `R3 : forall x y, post x y -> post (b (b (a x))) (b (b y))`

• but more importantly hint missing: `Hint Constructors sol.`
(indeed, the answer to the problem starts with a `solb` so `eauto` must know he should search with `sol` constructors).

Thanks. I should have been more careful.