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

Using Rocq
1

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

2

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
3

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).

4

Thanks. I should have been more careful.