Pain with reduction of bind

Author: YaZko

theories/Core/ITreeDefinition.v

@@ -160,9 +160,10 @@ Definition subst {E : Type -> Type} {T U : Type} (k : T -> itree E U)
     | VisF e h => Vis e (fun x => _subst (h x))
     end.
 
-Definition bind {E : Type -> Type} {T U : Type} (u : itree E T) (k : T -> itree E U)
-  : itree E U :=
-  subst k u.
+Notation bind u k := (subst k u).
+(* Definition bind {E : Type -> Type} {T U : Type} (u : itree E T) (k : T -> itree E U) *)
+(*   : itree E U := *)
+(*   subst k u. *)
 
 (** Monadic composition of continuations (i.e., Kleisli composition).
  *)
@@ -221,7 +222,7 @@ Ltac fold_subst :=
   repeat (change (ITree.subst ?k ?t) with (ITree.bind t k)).
 
 Ltac fold_monad :=
-  repeat (change (@ITree.bind ?E) with (@mbind (itree E) _));
+  repeat (change (@ITree.subst ?E) with (@mbind (itree E) _));
   repeat (change (go (@RetF ?E _ _ _ ?r)) with (@mret (itree E) _ _ r));
   repeat (change (@ITree.map ?E) with (@fmap (itree E) _)).
 
@@ -239,11 +240,11 @@ End ITree.
  *)
 
 Module ITreeNotations.
-Notation "t1 ≫= k2" := (ITree.bind t1 k2) : itree_scope.
-Notation "x ← t1 ; t2" := (ITree.bind t1 (fun x => t2)) : itree_scope.
-Notation "t1 ;; t2" := (ITree.bind t1 (fun _ => t2)) : itree_scope.
+Notation "t1 ≫= k2" := (ITree.subst k2 t1) : itree_scope.
+Notation "x ← t1 ; t2" := (ITree.subst (fun x => t2) t1) : itree_scope.
+Notation "t1 ;; t2" := (ITree.subst (fun _ => t2) t1) : itree_scope.
 Notation "' p ← t1 ; t2" :=
-  (ITree.bind t1 (fun x_ => match x_ with p => t2 end))
+  (ITree.subst (fun x_ => match x_ with p => t2 end) t1)
   (at level 20, p pattern, t1 at level 100, t2 at level 200, only parsing) : itree_scope.
 Infix ">=>" := ITree.cat (at level 60, right associativity) : itree_scope.
 End ITreeNotations.

theories/Core/KTreeFacts.v

@@ -325,6 +325,13 @@ Proof.
   split; typeclasses eauto.
 Qed.
 
+CoInductive stream := | cons : nat -> stream -> stream.
+
+(* CoFixpoint zeros := cons 0 zeros. *)
+
+(* Goal zeros = zeros. *)
+(* cbn. *)
+Import ITreeNotations.
 (* Equation merging the sequence of two [iter] into one *)
 Lemma cat_iter:
   forall {E: Type -> Type} {a b c} (f: ktree E a (a + b)) (g: ktree E b (b + c)),
@@ -336,22 +343,12 @@ Proof.
     assoc_l, AssocL_Coproduct,
     bimap, Bimap_Coproduct,
     cat, Cat_Kleisli, inl_, Inl_Kleisli, inr_, Inr_Kleisli, case_, Case_Kleisli, case_sum,
-    lift_ktree_.
-  cbn.
-  Unset Printing Notations.
-  simpl.
-  cbn.
-
-
-  unfold_ktree.
+    lift_ktree_, mbind, MBind_itree.
   (* We move to the eworld *)
   einit.
-  intros.
-  revert a0.
   (* First coinductive point in the simulation: at the entry point of the iteration over f *)
   ecofix CIH.
   intros.
-  cbn.
   setoid_rewrite bind_ret_l.
   (* We unfold one step on both sides *)
   match goal with
@@ -371,7 +368,7 @@ Proof.
       |- euttG _ _ _ _ _ ?t _ => remember t
     end.
     clear CIHH.
-    rewrite <- bind_ret_l.
+    (* rewrite <- bind_ret_l. *)
     ebase.
     right. apply CIHL.
   - (* If we exit the first loop *)

theories/Eq/Eqit.v

@@ -1187,8 +1187,8 @@ Proof.
 Qed.
 
 #[global] Instance eqit_bind {E R S} b1 b2 :
-  Proper (eqit eq b1 b2 ==> pointwise_relation _ (eqit eq b1 b2) ==>
-          eqit eq b1 b2) (@ITree.bind E R S).
+  Proper (pointwise_relation _ (eqit eq b1 b2) ==> eqit eq b1 b2 ==>
+          eqit eq b1 b2) (@ITree.subst E R S).
 Proof.
   repeat intro; eapply eqit_bind'; eauto.
   intros; subst; auto.
@@ -1229,8 +1229,8 @@ Lemma bind_ret_r' {E R} (u : itree E R) (f : R -> R) :
   ITree.bind u (fun r => Ret (f r)) ≅ u.
 Proof.
   intro H. rewrite <- (bind_ret_r u) at 2. apply eqit_bind.
-  - reflexivity.
   - hnf. intros. apply eqit_Ret. auto.
+  - reflexivity.
 Qed.
 
 Lemma bind_bind {E R S T} :

theories/Eq/Shallow.v

@@ -110,10 +110,10 @@ Proof. reflexivity. Qed.
 
 #[global]
 Instance observing_bind {E R S} :
-  Proper (observing eq ==> eq ==> observing eq) (@ITree.bind E R S).
+  Proper (eq ==> observing eq ==> observing eq) (@ITree.subst E R S).
 Proof.
   repeat intro; subst. constructor. unfold observe. cbn.
-  rewrite (observing_observe H). reflexivity.
+  rewrite (observing_observe H0). reflexivity.
 Qed.
 
 Lemma bind_ret_ {E R S} (r : R) (k : R -> itree E S) :