Skip to content

Commit 8e0f1cc

Browse files
committed
Pain with reduction of bind
1 parent 56e8313 commit 8e0f1cc

File tree

4 files changed

+23
-25
lines changed

4 files changed

+23
-25
lines changed

theories/Core/ITreeDefinition.v

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -160,9 +160,10 @@ Definition subst {E : Type -> Type} {T U : Type} (k : T -> itree E U)
160160
| VisF e h => Vis e (fun x => _subst (h x))
161161
end.
162162

163-
Definition bind {E : Type -> Type} {T U : Type} (u : itree E T) (k : T -> itree E U)
164-
: itree E U :=
165-
subst k u.
163+
Notation bind u k := (subst k u).
164+
(* Definition bind {E : Type -> Type} {T U : Type} (u : itree E T) (k : T -> itree E U) *)
165+
(* : itree E U := *)
166+
(* subst k u. *)
166167

167168
(** Monadic composition of continuations (i.e., Kleisli composition).
168169
*)
@@ -221,7 +222,7 @@ Ltac fold_subst :=
221222
repeat (change (ITree.subst ?k ?t) with (ITree.bind t k)).
222223

223224
Ltac fold_monad :=
224-
repeat (change (@ITree.bind ?E) with (@mbind (itree E) _));
225+
repeat (change (@ITree.subst ?E) with (@mbind (itree E) _));
225226
repeat (change (go (@RetF ?E _ _ _ ?r)) with (@mret (itree E) _ _ r));
226227
repeat (change (@ITree.map ?E) with (@fmap (itree E) _)).
227228

@@ -239,11 +240,11 @@ End ITree.
239240
*)
240241

241242
Module ITreeNotations.
242-
Notation "t1 ≫= k2" := (ITree.bind t1 k2) : itree_scope.
243-
Notation "x ← t1 ; t2" := (ITree.bind t1 (fun x => t2)) : itree_scope.
244-
Notation "t1 ;; t2" := (ITree.bind t1 (fun _ => t2)) : itree_scope.
243+
Notation "t1 ≫= k2" := (ITree.subst k2 t1) : itree_scope.
244+
Notation "x ← t1 ; t2" := (ITree.subst (fun x => t2) t1) : itree_scope.
245+
Notation "t1 ;; t2" := (ITree.subst (fun _ => t2) t1) : itree_scope.
245246
Notation "' p ← t1 ; t2" :=
246-
(ITree.bind t1 (fun x_ => match x_ with p => t2 end))
247+
(ITree.subst (fun x_ => match x_ with p => t2 end) t1)
247248
(at level 20, p pattern, t1 at level 100, t2 at level 200, only parsing) : itree_scope.
248249
Infix ">=>" := ITree.cat (at level 60, right associativity) : itree_scope.
249250
End ITreeNotations.

theories/Core/KTreeFacts.v

Lines changed: 9 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -325,6 +325,13 @@ Proof.
325325
split; typeclasses eauto.
326326
Qed.
327327

328+
CoInductive stream := | cons : nat -> stream -> stream.
329+
330+
(* CoFixpoint zeros := cons 0 zeros. *)
331+
332+
(* Goal zeros = zeros. *)
333+
(* cbn. *)
334+
Import ITreeNotations.
328335
(* Equation merging the sequence of two [iter] into one *)
329336
Lemma cat_iter:
330337
forall {E: Type -> Type} {a b c} (f: ktree E a (a + b)) (g: ktree E b (b + c)),
@@ -336,22 +343,12 @@ Proof.
336343
assoc_l, AssocL_Coproduct,
337344
bimap, Bimap_Coproduct,
338345
cat, Cat_Kleisli, inl_, Inl_Kleisli, inr_, Inr_Kleisli, case_, Case_Kleisli, case_sum,
339-
lift_ktree_.
340-
cbn.
341-
Unset Printing Notations.
342-
simpl.
343-
cbn.
344-
345-
346-
unfold_ktree.
346+
lift_ktree_, mbind, MBind_itree.
347347
(* We move to the eworld *)
348348
einit.
349-
intros.
350-
revert a0.
351349
(* First coinductive point in the simulation: at the entry point of the iteration over f *)
352350
ecofix CIH.
353351
intros.
354-
cbn.
355352
setoid_rewrite bind_ret_l.
356353
(* We unfold one step on both sides *)
357354
match goal with
@@ -371,7 +368,7 @@ Proof.
371368
|- euttG _ _ _ _ _ ?t _ => remember t
372369
end.
373370
clear CIHH.
374-
rewrite <- bind_ret_l.
371+
(* rewrite <- bind_ret_l. *)
375372
ebase.
376373
right. apply CIHL.
377374
- (* If we exit the first loop *)

theories/Eq/Eqit.v

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1187,8 +1187,8 @@ Proof.
11871187
Qed.
11881188

11891189
#[global] Instance eqit_bind {E R S} b1 b2 :
1190-
Proper (eqit eq b1 b2 ==> pointwise_relation _ (eqit eq b1 b2) ==>
1191-
eqit eq b1 b2) (@ITree.bind E R S).
1190+
Proper (pointwise_relation _ (eqit eq b1 b2) ==> eqit eq b1 b2 ==>
1191+
eqit eq b1 b2) (@ITree.subst E R S).
11921192
Proof.
11931193
repeat intro; eapply eqit_bind'; eauto.
11941194
intros; subst; auto.
@@ -1229,8 +1229,8 @@ Lemma bind_ret_r' {E R} (u : itree E R) (f : R -> R) :
12291229
ITree.bind u (fun r => Ret (f r)) ≅ u.
12301230
Proof.
12311231
intro H. rewrite <- (bind_ret_r u) at 2. apply eqit_bind.
1232-
- reflexivity.
12331232
- hnf. intros. apply eqit_Ret. auto.
1233+
- reflexivity.
12341234
Qed.
12351235

12361236
Lemma bind_bind {E R S T} :

theories/Eq/Shallow.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -110,10 +110,10 @@ Proof. reflexivity. Qed.
110110

111111
#[global]
112112
Instance observing_bind {E R S} :
113-
Proper (observing eq ==> eq ==> observing eq) (@ITree.bind E R S).
113+
Proper (eq ==> observing eq ==> observing eq) (@ITree.subst E R S).
114114
Proof.
115115
repeat intro; subst. constructor. unfold observe. cbn.
116-
rewrite (observing_observe H). reflexivity.
116+
rewrite (observing_observe H0). reflexivity.
117117
Qed.
118118

119119
Lemma bind_ret_ {E R S} (r : R) (k : R -> itree E S) :

0 commit comments

Comments
 (0)