From 93836821bace2e1c234d4c552abefb6eed161761 Mon Sep 17 00:00:00 2001 From: Steve Zdancewic Date: Tue, 25 Nov 2025 09:45:05 -0500 Subject: [PATCH 1/2] change the definition of MonadBr to match MonadTrigger --- theories/Core/Utils.v | 2 +- theories/Interp/Fold.v | 2 +- theories/Interp/FoldCTree.v | 2 +- theories/Interp/FoldStateT.v | 4 ++-- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/theories/Core/Utils.v b/theories/Core/Utils.v index 99a079e..43101d3 100644 --- a/theories/Core/Utils.v +++ b/theories/Core/Utils.v @@ -11,7 +11,7 @@ Polymorphic Class MonadTrigger (E : Type -> Type) (M : Type -> Type) : Type := mtrigger : forall {X}, E X -> M X. Polymorphic Class MonadBr (B : Type -> Type) (M : Type -> Type) : Type := - mbr : forall X (b: B X), M X. + mbr : forall {X}, B X -> M X. Polymorphic Class MonadStep (M : Type -> Type) : Type := mstep : M unit. diff --git a/theories/Interp/Fold.v b/theories/Interp/Fold.v index 77de5df..00fb118 100644 --- a/theories/Interp/Fold.v +++ b/theories/Interp/Fold.v @@ -61,7 +61,7 @@ Definition interp {E B M : Type -> Type} {Mstep : MonadStep M} {Mbranch : MonadBr B M} (h : E ~> M) : ctree E B ~> M := - fold h mbr. + fold h (@mbr B M Mbranch). Arguments interp {E B M FM MM IM _ _ _} h [T]. diff --git a/theories/Interp/FoldCTree.v b/theories/Interp/FoldCTree.v index 8d0e3ec..7515189 100644 --- a/theories/Interp/FoldCTree.v +++ b/theories/Interp/FoldCTree.v @@ -122,7 +122,7 @@ Section FoldCTree. | GuardF t => Guard (interp h t) | StepF t => Step (Guard (interp h t)) | VisF e k => bind (h _ e) (fun x => Guard (interp h (k x))) - | BrF c k => bind (mbr _ c) (fun x => Guard (interp h (k x))) + | BrF c k => bind (mbr c) (fun x => Guard (interp h (k x))) end)%function. (** Unfold lemma. *) diff --git a/theories/Interp/FoldStateT.v b/theories/Interp/FoldStateT.v index b8c3216..18ce555 100644 --- a/theories/Interp/FoldStateT.v +++ b/theories/Interp/FoldStateT.v @@ -33,7 +33,7 @@ Arguments fequ : simpl never. #[global] Instance MonadBr_stateT {S M C} {MM : Monad M} {AM : MonadBr C M}: MonadBr C (stateT S M) := - fun X c s => f <- mbr _ c;; ret (s,f). + fun X c s => f <- mbr c;; ret (s,f). #[global] Instance MonadTrigger_stateT {E S M} {MM : Monad M} {MT: MonadTrigger E M} : MonadTrigger E (stateT S M) := @@ -225,7 +225,7 @@ Section State. | GuardF t => Guard (interp_state h t s) | StepF t => Step (Guard (interp_state h t s)) | VisF e k => bind (h _ e s) (fun xs => Guard (interp_state h (k (snd xs)) (fst xs))) - | BrF c k => bind (mbr (M := stateT _ _) _ c s) (fun xs => Guard (interp_state h (k (snd xs)) (fst xs))) + | BrF c k => bind (mbr (M := stateT _ _) c s) (fun xs => Guard (interp_state h (k (snd xs)) (fst xs))) end)%function. Lemma unfold_interp_state `{C- Date: Tue, 25 Nov 2025 09:49:14 -0500 Subject: [PATCH 2/2] most of a port of ITrees mrec to CTrees --- theories/Interp/Recursion.v | 180 ++++++++++++++ theories/Interp/RecursionFacts.v | 389 +++++++++++++++++++++++++++++++ 2 files changed, 569 insertions(+) create mode 100644 theories/Interp/Recursion.v create mode 100644 theories/Interp/RecursionFacts.v diff --git a/theories/Interp/Recursion.v b/theories/Interp/Recursion.v new file mode 100644 index 0000000..d7a1870 --- /dev/null +++ b/theories/Interp/Recursion.v @@ -0,0 +1,180 @@ +From ExtLib Require Import + Structures.Functor + Structures.Monad. + +From ITree Require Import + Basics.Basics + Indexed.Sum. + +Import ITree.Basics.Basics.Monads. + +From CTree Require Import + CTree + Eq + Eq.Epsilon + Eq.IterFacts + Eq.SSimAlt + Misc.Pure + Fold. + +Import CTreeNotations. +Open Scope ctree_scope. + +(** * General recursion *) + +(** *** Mutual recursion *) + +(* Implementation of the fixpoint combinator over interaction + * trees. + * + * The implementation is based on the discussion here + * https://gmalecha.github.io/reflections/2018/compositional-coinductive-recursion-in-coq + *) + +(* The indexed type [D : Type -> Type] gives the signature of + a set of functions. For example, a pair of mutually recursive + [even : nat -> bool] and [odd : nat -> bool] can be declared + as follows: + +[[ + Inductive D : Type -> Type := + | Even : nat -> D bool + | Odd : nat -> D bool. +]] + + Their mutually recursive definition can then be written finitely + (without [Fixpoint]): + +[[ + Definition def : D ~> itree (D +' void1) := fun _ d => + match d with + | Even n => match n with + | O => ret true + | S m => trigger (Odd m) + end + | Odd n => match n with + | O => ret false + | S m => trigger (Even m) + end + end. +]] + + The function [interp_mrec] below then ties the knot. + +[[ + Definition f : D ~> itree void1 := + interp_mrec def. + + Definition even (n : nat) : itree void1 bool := f _ (Even n). + Definition odd (n : nat) : itree void1 bool := f _ (Odd n). +]] + + The result is still in the [itree] monad of possibly divergent + computations, because [mutfix_itree] doesn't care whether + the mutually recursive definition is well-founded. + + *) + +(** Interpret an itree in the context of a mutually recursive + definition ([ctx]). *) +Definition interp_mrec {D E B : Type -> Type} + (ctx : D ~> ctree (D +' E) B) : ctree (D +' E) B ~> ctree E B := + fun R => + CTree.iter (fun t : ctree (D +' E) B R => + match observe t with + | RetF r => Ret (inr r) + | StuckF => Stuck + | StepF t => Step (Ret (inl t)) + | GuardF t => Ret (inl t) + | VisF (inl1 d) k => Ret (inl (ctx _ d >>= k)) + | VisF (inr1 e) k => Vis e (fun x => Ret (inl (k x))) + | BrF c k => Br c (fun x => Ret (inl (k x))) + end). + +Arguments interp_mrec {D E B} ctx [T]. + +(** Unfold a mutually recursive definition into separate trees, + resolving the mutual references. *) +Definition mrec {D E B : Type -> Type} + (ctx : D ~> ctree (D +' E) B) : D ~> ctree E B := + fun R d => interp_mrec ctx (ctx _ d). + +Arguments mrec {D E B} ctx [T]. + +(** Make a recursive call in the handler argument of [mrec]. *) +Definition trigger_inl1 {D E B : Type -> Type} : D ~> ctree (D +' E) B + := fun _ d => CTree.trigger (inl1 d). + +Arguments trigger_inl1 {D E B} [T]. + +(** Here's some syntactic sugar with a notation [mrec-fix]. *) + +(** Short for endofunctions, used in [mrec_fix] and [rec_fix]. *) +(* Local Notation endo T := (T -> T). *) + +(* Definition mrec_fix {D E : Type -> Type} *) +(* (ctx : endo (D ~> itree (D +' E))) *) +(* : D ~> itree E *) +(* := mrec (ctx trigger_inl1). *) + +(* Notation "'mrec-fix' f d := g" := *) +(* (let D := _ in *) +(* mrec_fix (D := D) (fun (f : forall T, D T -> _) T (d : D T) => g)) *) +(* (at level 200, f ident, d pattern). *) +(* (* No idea what a good level would be. *) *) + +(** *** Simple recursion *) + +Inductive callE (A B : Type) : Type -> Type := +| Call : A -> callE A B B. + +Arguments Call {A B}. + +(** Get the [A] contained in a [callE A B]. *) +Definition unCall {A B T} (e : callE A B T) : A := + match e with + | Call a => a + end. + +(** Lift a function on [A] to a morphism on [callE]. *) +Definition calling {A B} {F : Type -> Type} + (f : A -> F B) : callE A B ~> F := + fun _ e => + match e with + | Call a => f a + end. + +(* TODO: This is identical to [callWith] but [rec] finds a universe + inconsistency with [calling], and not with [calling']. + The inconsistency now pops up later (currently in [Events.Env]) *) +Definition calling' {X Y} {F B : Type -> Type} + (f : X -> ctree F B Y) : callE X Y ~> ctree F B := + fun _ e => + match e with + | Call a => f a + end. + +(* Interpret a single recursive definition. *) +Definition rec {E B : Type -> Type} {X Y : Type} + (body : X -> ctree (callE X Y +' E) B Y) : + X -> ctree E B Y := + fun a => mrec (calling' body) (Call a). + +(** An easy way to construct an event suitable for use with [rec]. + [call] is an event representing the recursive call. Since in general, the + function might have other events of type [E], the resulting itree has + type [(callE A B +' E)]. +*) +Definition call {E B X Y} (x:X) : ctree (callE X Y +' E) B Y := + CTree.trigger (inl1 (Call x)). + +(* (** Here's some syntactic sugar with a notation [mrec-fix]. *) *) + +(* Definition rec_fix {E : Type -> Type} {A B : Type} *) +(* (body : endo (A -> itree (callE A B +' E) B)) *) +(* : A -> itree E B *) +(* := rec (body call). *) + +(* Notation "'rec-fix' f a := g" := (rec_fix (fun f a => g)) *) +(* (at level 200, f ident, a pattern). *) +(* No idea what a good level would be. *) diff --git a/theories/Interp/RecursionFacts.v b/theories/Interp/RecursionFacts.v new file mode 100644 index 0000000..203afbb --- /dev/null +++ b/theories/Interp/RecursionFacts.v @@ -0,0 +1,389 @@ +(** * Properties of [Recursion.mrec] and [Recursion.rec]. *) + +(** The main facts to take away are [mrec_as_interp] and [rec_as_interp]: + [mrec] and [rec] are special cases of [interp], using [mrecursive] and + [recursive] as handlers. + *) + +From ExtLib Require Import + Structures.Functor + Structures.Monad. + +Unset Universe Checking. +From CTree Require Import + CTreeDefinitions + Eq + Eq.Epsilon + Eq.SSimAlt + Eq.SBisimAlt + Interp.Fold + Interp.FoldCTree + Misc.Pure + Recursion. + + +Import CTreeNotations. +Open Scope ctree_scope. + +From Stdlib Require Import + Program.Tactics + Setoid + Morphisms + RelationClasses. + +From ITree Require Import + Basics.Utils + Basics.Category + Basics.Basics + Basics.Function + Indexed.Sum + Indexed.Function + Indexed.Relation. + +Import CoindNotations. + +Section Facts. + +Context {D E B : Type -> Type} (ctx : D ~> ctree (D +' E) B). + +(** Unfolding of [interp_mrec]. *) + +Definition _interp_mrec {R : Type} (ot : ctreeF (D +' E) B R _) : ctree E B R := + match ot with + | RetF r => Ret r + | StuckF => Stuck + | StepF t => Step (Guard (interp_mrec ctx t)) + | GuardF t => Guard (interp_mrec ctx t) + | VisF e k => + match e with + | inl1 d => Guard (interp_mrec ctx (ctx _ d >>= k)) + | inr1 e => Vis e (fun x => Guard (interp_mrec ctx (k x))) + end + | BrF c k => Br c (fun x => Guard (interp_mrec ctx (k x))) + end. + +Lemma unfold_interp_mrec R (t : ctree (D +' E) B R) : + interp_mrec ctx t ≅ _interp_mrec (observe t). +Proof. + unfold interp_mrec. + rewrite unfold_iter. + destruct observe; cbn. + - rewrite bind_ret_l; reflexivity. + - rewrite bind_stuck; reflexivity. + - rewrite bind_step. rewrite bind_ret_l. + step. constructor. + step. constructor. reflexivity. + - rewrite bind_ret_l; reflexivity. + - destruct e; cbn. + + rewrite bind_ret_l; reflexivity. + + rewrite bind_vis. + step. constructor. intros. + rewrite bind_ret_l. + reflexivity. + - rewrite bind_br. + step. constructor. intros. + rewrite bind_ret_l. + reflexivity. +Qed. + +(** [mrec ctx] is equivalent to [interp (mrecursive ctx)], + where [mrecursive] is defined as follows. *) +Definition mrecursive (f : D ~> ctree (D +' E) B) + : (D +' E) ~> ctree E B := + case_ (mrec f) CTree.trigger. + +Global Instance eq_itree_mrec {R} : + Proper (equ eq ==> equ eq) (@interp_mrec _ _ _ ctx R). +Proof. + cbn. + coinduction C CIH. + intros. + rewrite !unfold_interp_mrec. + step in H. inv H; cbn; try econstructor. + - reflexivity. + - eapply CIH; eauto. + - step. constructor. eapply CIH; auto. + - destruct e. + + constructor. + apply CIH. + upto_bind_eq. assumption. + + constructor. + intros. + step. + constructor. + apply CIH. + apply REL. + - intros. + step. constructor. apply CIH. apply REL. +Qed. + +Theorem interp_mrec_bind {U T} (t : ctree _ B U) (k : U -> ctree _ B T) : + interp_mrec ctx (CTree.bind t k) ≅ + CTree.bind (interp_mrec ctx t) (fun x => interp_mrec ctx (k x)). +Proof. + revert t k. + coinduction C CIH. + intros t k. + rewrite (unfold_interp_mrec _ t). + rewrite (unfold_bind t). + destruct (observe t); cbn. + - rewrite bind_ret_. + reflexivity. + - reflexivity. + - constructor. fold_subst. + rewrite bind_ret_l. + rewrite bind_guard. + step. constructor. apply CIH. + - constructor. apply CIH. + - destruct e. + + cbn. + constructor. + rewrite <- bind_bind. + apply CIH. + + cbn. constructor. + intros x. + fold_subst. + rewrite bind_guard. + rewrite bind_ret_l. + step. constructor. + apply CIH. + - constructor. + intros x. + fold_subst. + rewrite bind_guard. + rewrite bind_ret_l. + step. constructor. + apply CIH. +Qed. + +Theorem interp_mrec_trigger {U} (a : (D +' E) U) : + interp_mrec ctx (CTree.trigger a) + ≲ mrecursive ctx _ a. +Proof. + rewrite unfold_interp_mrec; unfold mrecursive. + destruct a; cbn. + rewrite bind_ret_r. apply ssim_guard_l. reflexivity. + unfold CTree.trigger. + apply ssim_vis_id. + intros. split; auto. + apply ssim_guard_l. rewrite unfold_interp_mrec. cbn. reflexivity. +Qed. + +Lemma interp_mrec_guard {T} (c : ctree _ _ T) : + Guard (interp_mrec ctx c) ~ interp_mrec ctx (Guard c). +Proof. + rewrite (unfold_interp_mrec _ (Guard c)). + unfold _interp_mrec, fold. + cbn. + reflexivity. +Qed. + + + +Theorem interp_mrec_as_interp {T} (c : ctree _ _ T) : + interp_mrec ctx c ~ interp (mrecursive ctx) c. +Proof. + rewrite <- (sb_guard (interp (mrecursive ctx) c)). + apply sbisim_sbisim'. + red. + revert_until T. + coinduction R CIH. intros. + rewrite unfold_interp_mrec. unfold _interp_mrec, fold. + unfold interp, fold. + setoid_rewrite unfold_iter. + destruct (observe c). + - unfold ret, Monad_ctree. + apply step_sb'_guard_r. + rewrite bind_ret_l. + reflexivity. + - unfold mstuck, MonadStuck_ctree. rewrite bind_stuck. + apply step_sb'_guard_r. + reflexivity. + - unfold mstep, MonadStep_ctree. + unfold fmap, Functor_ctree. rewrite bind_map. + apply step_sb'_guard_r. + rewrite bind_step. rewrite bind_ret_l. + apply step_sb'_step; auto. + intros side'. + apply step_sb'_guard_l'. + intros. + apply CIH. + - unfold ret, Monad_ctree. rewrite bind_ret_l. + apply step_sb'_guard. + apply CIH. + - destruct e. + + unfold mrecursive, case_, Case_sum1, case_sum1. + unfold fmap at 1, Functor_ctree at 1. + rewrite bind_map. + apply step_sb'_guard. + rewrite interp_mrec_bind. + apply st'_clo_bind_eq. reflexivity. + intros. + apply CIH. + + unfold mrecursive, case_, Case_sum1, case_sum1. + unfold CTree.trigger. + unfold fmap, Functor_ctree. + rewrite bind_map. + rewrite bind_vis. + setoid_rewrite bind_ret_l. + apply step_sb'_guard_r. + apply step_sb'_vis_id. intros. split; auto. + intros. + apply step_sb'_guard_l'. + intros. + apply CIH. + - apply step_sb'_guard_r. + unfold mbr, MonadBr_ctree, branch. + unfold fmap, Functor_ctree. + rewrite bind_map. + rewrite bind_br. + setoid_rewrite bind_ret_l. + apply step_sb'_br. + intros x. exists x. + apply step_sb'_guard_l'. + intros. + apply CIH. + intros x. exists x. + apply step_sb'_guard_l'. + intros. + apply CIH. +Qed. + + +Theorem mrec_as_interp {T} (d : D T) : + mrec ctx d ~ interp (mrecursive ctx) (ctx _ d). +Proof. + apply interp_mrec_as_interp. +Qed. + +(* SAZ: Todo: + - why don't typeclasses for MonadBr find the [B -< B] instance? + - where should this live? + +Lemma interp_trigger {E' D' F' C U} `{C -< D'} (h : E' ~> ctree F' D') (e: E' U) : + interp h (CTree.trigger e) ~ Guard (h _ e). + *) + +Lemma interp_trigger {E' F' B' U} (h : E' ~> ctree F' B') (e: E' U) : + interp h (@CTree.trigger _ B' _ e) ~ Guard (h _ e). +Proof. + unfold CTree.trigger. + rewrite interp_vis. + setoid_rewrite interp_ret. + setoid_rewrite sb_guard. + rewrite bind_ret_r. + reflexivity. +Qed. + +Lemma interp_mrecursive {T} (d : D T) : + interp (mrecursive ctx) (@trigger_inl1 D E B _ d) ~ mrec ctx d. +Proof. + unfold mrecursive. unfold trigger_inl1. + rewrite interp_trigger. + cbn. + setoid_rewrite sb_guard. + reflexivity. +Qed. + +(* SAZ: not sure where this is needed, and the typeclasses around `bif` don't seem to work. + + *) +(* +Theorem unfold_interp_mrec_h {T} (t : ctree (D +' E) B T) + : interp_mrec ctx (interp (case_ ctx inr_) t) + ~ interp_mrec ctx t. +Proof. + rewrite <- tau_eutt. + revert t. ginit; gcofix CIH. intros. + rewrite (itree_eta t); destruct (observe t); + try (rewrite 2 unfold_interp_mrec; cbn; gstep; repeat constructor; auto with paco; fail). + rewrite interp_vis. + rewrite (unfold_interp_mrec _ (Vis _ _)). + destruct e; cbn. + - rewrite 2 interp_mrec_bind. + gstep; constructor. + guclo eqit_clo_bind; econstructor; [reflexivity|]. + intros ? _ []; rewrite unfold_interp_mrec; cbn; auto with paco. + - unfold inr_, Handler.Inr_sum1_Handler, Handler.Handler.inr_, Handler.Handler.htrigger. + rewrite bind_trigger, unfold_interp_mrec; cbn. + rewrite tau_euttge. + gstep; constructor. + intros; red. gstep; constructor. + rewrite unfold_interp_mrec; cbn. + auto with paco. +Qed. +*) +End Facts. + + + +Global Instance Proper_interp_mrec {D E B} : + @Proper ((D ~> ctree (D +' E) B) -> (ctree (D +' E) B ~> ctree E B)) + (Relation.i_pointwise (fun _ => sbisim eq) ==> + Relation.i_respectful (fun _ => sbisim eq) (fun _ => sbisim eq)) + interp_mrec. +Proof. + + intros f g Hfg R t1 t2 H. + apply sbisim_sbisim'. + revert t1 t2 H. +Admitted. + +Local Opaque interp_mrec. + + +(** [rec body] is equivalent to [interp (recursive body)], + where [recursive] is defined as follows. *) +Definition recursive {E B } {X Y} (f : X -> ctree (callE X Y +' E) B Y) : (callE X Y +' E) ~> ctree E B := + case_ (calling' (rec f)) CTree.trigger. + +(* SAZ: TODO - update this after the change to sbisim *) +Lemma rec_as_interp {E B} {X Y} (f : X -> ctree (callE X Y +' E) B Y) (x : X) : + rec f x ~ interp (recursive f) (f x). +Proof. + unfold rec. + rewrite mrec_as_interp. +Admitted. + +Lemma interp_recursive_call {E B} {X Y} (f : X -> ctree ((callE X Y) +' E) B Y) (x:X) : + interp (recursive f) (@call E B X Y x) ~ rec f x. +Proof. + unfold recursive. unfold call. + rewrite interp_trigger. cbn. + setoid_rewrite sb_guard. + reflexivity. +Qed. + +(* + SAZ: TODO: Not sure what the appropriate analogue of this is for ctrees + *) +(* +Global Instance euttge_interp_mrec {D E} : + @Proper ((D ~> ctree (D +' E)) -> (ctree (D +' E) ~> ctree E)) + (Relation.i_pointwise (fun _ => euttge eq) ==> + Relation.i_respectful (fun _ => euttge eq) (fun _ => euttge eq)) + interp_mrec. +Proof. + intros f g Hfg R. + ginit; gcofix CIH; intros t1 t2 Ht. + rewrite 2 unfold_interp_mrec. + punfold Ht; induction Ht; cbn; pclearbot. + 3: { destruct e; gstep; constructor. + + gfinal; left. apply CIH. + eapply eqit_bind; auto. apply Hfg. + + gstep; constructor. auto with paco. + } + 1,2: gstep; constructor; auto with paco. + 1: rewrite unfold_interp_mrec, tau_euttge; auto. + discriminate. +Qed. +*) + +(* + SAZ: TODO: Need the appropriate analogue for ctrees +Global Instance euttge_interp_mrec' {E D R} (ctx : D ~> ctree (D +' E)) : + Proper (euttge eq ==> euttge eq) (@interp_mrec _ _ ctx R). +Proof. + do 4 red. eapply euttge_interp_mrec. reflexivity. +Qed. +*)