Rewriting with `interp_bind` doesn't properly generalize

[jeehoonkang]

Hi, thank you for creating such a wonderful library.

I'm working on tutorial/Introduction.v, and in the proof of fib_correct_aux, rewriting with the lemma interp_bind doesn't properly generalize for my use case. Here is my proof script snippet (I'm posting only a snippet of my code because it's meant to be an exercise):

rewrite interp_bind, interp_recursive_call, IH; auto. rewrite bind_ret.
Fail rewrite interp_bind.
rewrite (interp_bind (recursive fib_body) (call (S n'')) (fun y => Ret (fib_spec n'' + y))).

For the failed line, Coq says:

The command has indeed failed with message:
Found no subterm matching "interp ?i (x <- ?i0;; ?i1 x)" in the current goal.

[YaZko]

Hello @jeehoonkang.

Could you give us a bit more context so that we can reproduce the failing goal on our side?
It looked to me like substituting the first instance of autorewrite with itree on line 369 by your snippet, but this leads to no failure on my side whether arguments are provided explicitly to interp_bind or not. So I assume you have modified something else?

Thanks,
Yannick

[jeehoonkang]

@YaZko Thanks for helping me. Here is the link to my working files: http://cp.kaist.ac.kr:9002/Introduction.v (I will turn down the web server after this issue is resolved.)

[YaZko]

Right so the issue is that on line 312 of your file, you unfold manually fib_body and rec_fix.
This is of course fine, but you could achieve the same thing alternatively simply by computation, with simpl for instance.
By choosing not to reduce, you end up on line 314 with an instance of the pbind typeclass operation from ExtLib, applied to the Monad_itree. You can see that either because of the scope annotation in your goal %monad, or more explicitly via Set Printing All.
In contrast, interp_bind is explicitly defined in terms of ITree.bind'. So without any help, Coq fails to unfold the pbind instance in order to unify both, but adding arguments helps him doing so.
Simply adding a simpl before the failing command hence solves the issue.

Hope it helps,
Yannick

[jeehoonkang]

Yannick, thank you a lot for helping me.