Messed up reduction behavior of bind

[YaZko]

When reducing an eta-expanded trigger e >>= k computation, we expose a [subst] rather than a [bindl], messing up subsequent rewrites --- minimal example thereafter. This should not happen, we need to double check what I messed up compared to how Li-yao has set-up the itrees.

Section Foo.
  Variable E : Type -> Type.
  Variable X : Type.
  Variable e : E X.

  Definition foo : ctree E unit := trigger e;; Ret tt.

  Goal foo ≅ foo.
    rewrite ctree_eta at 1.
    cbn.
    (* [subst] shows up, and it shouldn't *)
  Abort.
End Foo.

[YaZko]

This example is incorrect, [subst] showing up is completely normal in this case, and corresponds to what happens with [itrees].

I think what is messing up with me mainly is that with the companion, when running [coinduction ? ?] the endo b is immediately exposed, and therefore immediately reduce --- contrary to what happens with [paco] that actively waits for [punfold]. And this endo always exposes an additional [observe] that messes up the equational reasoning you expect to do at the [ctree] level.

Reducing using cbn -[ebt] typically has helped a lot, but I'm still quite unsure about the overall situation.

[YaZko]

Commit 00ffdc47feea4b00684cf793e45b43469a2c0a96 is an attempt to address this issue: bt does not reduce anymore by default, and a cbn* tactic unfolds it before reducing.

It seems decently satisfactory at the moment, I'll close the issue for now.