From a0b0a2f4a9e628b3e6593e1fa524bb3119d054e0 Mon Sep 17 00:00:00 2001 From: Lef Ioannidis Date: Mon, 12 Oct 2026 10:10:56 -0700 Subject: [PATCH 1/6] Agentic fix to universe checking --- README.md | 9 +- dune-project | 4 +- examples/AltBisim/dune | 2 +- examples/CCS/Denotation.v | 180 ++++++++++------------ examples/CCS/OpDenot.v | 1 - examples/CCS/dune | 2 +- examples/Coffee/coffeeCTree.v | 41 +++-- examples/Coffee/dune | 2 +- examples/ImpBr/ImpBr.v | 41 +++-- examples/ImpBr/dune | 2 +- examples/SimpleSim/SimExample.v | 4 +- examples/SimpleSim/dune | 2 +- examples/Yield/Lang.v | 228 +++++++++++++++++----------- examples/Yield/Par.v | 64 ++++---- examples/Yield/Util.v | 15 +- examples/Yield/dune | 4 +- tests/ImpBrTest/ImpBrEx/ImpBrEx.v | 1 - tests/ImpBrTest/ImpBrEx/dune | 2 +- tests/ImpBrTest/extracted/Extract.v | 1 - tests/ImpBrTest/extracted/dune | 4 +- theories/Core/CTreeDefinitions.v | 44 ++++-- theories/Core/Index.v | 2 + theories/Core/Utils.v | 10 +- theories/Eq/Epsilon.v | 1 + theories/Eq/Equ.v | 63 ++++++-- theories/Eq/IterFacts.v | 1 + theories/Eq/SBisim.v | 37 +++-- theories/Eq/SBisimAlt.v | 1 + theories/Eq/SSim.v | 9 +- theories/Eq/SSimAlt.v | 9 +- theories/Eq/Shallow.v | 1 + theories/Eq/Trace.v | 10 ++ theories/Eq/Trans.v | 117 ++++++++------ theories/Eq/Visible.v | 1 + theories/Eq/WBisim.v | 15 +- theories/Interp/Fold.v | 12 +- theories/Interp/FoldCTree.v | 157 ++++++++++++------- theories/Interp/FoldStateT.v | 220 ++++++++++++++++----------- theories/Interp/ITree.v | 92 ++++++----- theories/Interp/Internalize.v | 17 ++- theories/Interp/Recursion.v | 57 +++---- theories/Interp/RecursionFacts.v | 131 ++++++++-------- theories/Interp/Refine.v | 26 ++-- theories/Misc/Head.v | 16 +- theories/Misc/Pure.v | 8 +- theories/dune | 5 +- 46 files changed, 951 insertions(+), 720 deletions(-) diff --git a/README.md b/README.md index cad7de0f..d1277a8e 100644 --- a/README.md +++ b/README.md @@ -51,9 +51,12 @@ cd ctrees dune build ``` -## Universe issue +## Universe checking -We currently unset locally universe checking in several places of the library. This is an annoying, but purely technical issue that affects in no way the soundness of our results. +Universe checking remains enabled throughout the library. The former +inconsistency came from monomorphic universe instances that identified event +and branch indices with the higher universes needed by nested choice trees, +state transformers, and interpreters. These declarations now keep their +universe levels independent and polymorphic. -Given the complexity of the issue, and its root tracing back to other libraries (for instance, importing simultaneously some parts of the [Interaction Tree] library and of the [RelationAlgebra] library triggers a universe inconsistency), we project to tackle the issue as part of the future support in Rocq for algebraic universes and the release of a universe polymorphic prelude. diff --git a/dune-project b/dune-project index 355cb7e4..b2163f43 100644 --- a/dune-project +++ b/dune-project @@ -1,5 +1,5 @@ -(lang dune 3.8) -(using coq 0.7) +(lang dune 3.24) +(using rocq 0.11) (name rocq-ctree) (license "MIT") diff --git a/examples/AltBisim/dune b/examples/AltBisim/dune index d9a93f45..c005e6fc 100644 --- a/examples/AltBisim/dune +++ b/examples/AltBisim/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name CTreeBisimExample) (theories CTree) ) diff --git a/examples/CCS/Denotation.v b/examples/CCS/Denotation.v index 902db66f..905b2ac0 100644 --- a/examples/CCS/Denotation.v +++ b/examples/CCS/Denotation.v @@ -5,7 +5,6 @@ Denotation of [ccs] into [ctree]s .. coq:: none |*) -Unset Universe Checking. From Stdlib Require Export List @@ -53,8 +52,10 @@ Variant ActionE : Type -> Type := Notation ccsE := ActionE. Notation ccsC := (B2 +' B3 +' B4). -Definition ccsT' T := ctree' ccsE ccsC T. -Definition ccsT := ctree ccsE ccsC. +Universe ccs_u. +Definition ccsT (T : Type@{ccs_u}) : Type@{ccs_u} := + @ctree@{_ _ _ _ ccs_u ccs_u} ccsE ccsC T. +Definition ccsT' (T : Type@{ccs_u}) := ctreeF ccsE ccsC T (ccsT T). Definition ccs' := ccsT' void. Definition ccs := ccsT void. @@ -71,7 +72,7 @@ Section Combinators. Definition plus (P Q : ccs) : ccs := br2 P Q. - Definition h_new (c : chan) : ActionE ~> ctree ccsE ccsC := + Definition h_new (c : chan) : forall T, ActionE T -> ccsT T := fun _ e => let '(Act a) := e in match a with | Send c' @@ -81,7 +82,7 @@ Section Combinators. #[global] Arguments h_new c [T] _. Definition new : chan -> ccs -> ccs := - fun c P => interp (h_new c) P. + fun c P => interp (M := @ctree@{_ _ _ _ ccs_u ccs_u} ccsE ccsC) (h_new c) P. Definition para : ccs -> ccs -> ccs := cofix F (P : ccs) (Q : ccs) := @@ -237,7 +238,7 @@ Proof. rewrite <- eq1; eauto. Qed. -Lemma trans_brS' {E C X Y} : forall (c : C Y) (k : Y -> ctree E C X) x u, +Polymorphic Lemma trans_brS' {E C X Y} : forall (c : C Y) (k : Y -> ctree E C X) x u, u ≅ k x -> trans τ (BrS c k) u. Proof. @@ -249,28 +250,31 @@ Lemma trans_prefix_inv : forall l a p p', p' ≅ p /\ l = comm a. Proof. intros * tr. - apply trans_trigger_inv in tr as (? & ? & ->). + unfold prefix in tr. + apply Trans.trans_trigger_inv in tr as (? & ? & ->). destruct x; split; auto. Qed. Lemma trans_prefix : forall a p, trans (comm a) (prefix a p) p. Proof. - intros; eapply trans_trigger. + intros; unfold prefix; apply Trans.trans_trigger'. Qed. (* TO MOVE *) Ltac ssplit := split; [| split]. Ltac eex := do 2 eexists. -Lemma trans_trigger_inv' : forall {E C X} (e : E X) l u, - trans l (trigger e : ctree E C X) u -> - exists x, u ≅ Ret x /\ l = obs e x. +Polymorphic Lemma trans_trigger_inv'@{d q +} : forall + {E : Type -> Type} {C : Type -> Type} {X : Type} (e : E X) l + (u : @ctree@{_ _ _ _ d q} E C X), + trans l (trigger e : @ctree@{_ _ _ _ d q} E C X) u -> + exists x, u ≅ (Ret x : @ctree@{_ _ _ _ d q} E C X) /\ l = obs e x. Proof. intros * TR. - unfold trigger in TR. + rewrite Equ.unfold_trigger in TR. now apply trans_vis_inv in TR. Qed. -Lemma trans_vis' {E C R X} : forall (e : E X) x (k : X -> ctree E C R) u, +Polymorphic Lemma trans_vis' {E C R X} : forall (e : E X) x (k : X -> ctree E C R) u, u ≅ k x -> trans (obs e x) (Vis e k) u. Proof. @@ -290,12 +294,14 @@ Definition can_comm (c : chan) (a : @label ccsE) : bool := Lemma trans_hnew_inv : forall a l c p, trans l (h_new c (Act a)) p -> - l = obs (Act a) tt /\ can_comm c l /\ p ≅ Ret tt. + l = obs (Act a) tt /\ can_comm c l /\ p ≅ (Ret tt : ccsT unit). Proof. intros * tr. - cbn in *; destruct a; cbn in *; destruct (c =? c0) eqn:comm; cbn in *. + destruct a; cbn [h_new] in tr; + destruct (c =? c0) eqn:comm; cbn [h_new] in tr. all : try now eapply Stuck_is_stuck in tr. - all: unfold can_comm; apply trans_trigger_inv' in tr as ([] & ? & ?); subst; rewrite comm; eauto. + all: unfold can_comm; apply trans_trigger_inv' in tr as ([] & EQ & ->); + rewrite comm; auto. Qed. Lemma new_guard : forall c t, new c (Guard t) ≅ Guard (new c t). @@ -322,12 +328,9 @@ Proof. - edestruct IHtr as (q & tr' & eq); eauto. exists q; split; auto. unfold new; rewrite unfold_interp, <- Heqobsp. - cbn; unfold Utils.mbr, MonadBr_ctree, branch. - eapply trans_bind_r with x. - eapply trans_br; [|reflexivity]. - apply trans_ret. - apply trans_guard. - apply tr'. + cbn -[CTree.branch MonadBr_ctree]. + unfold Utils.mbr, MonadBr_ctree; rewrite bind_branch. + eapply trans_br with (x := x); [apply trans_guard; exact tr' | reflexivity]. - edestruct IHtr as (q & tr' & eq); eauto. exists q; split; auto. unfold new; rewrite unfold_interp, <- Heqobsp. @@ -340,42 +343,20 @@ Proof. rewrite <- H. apply observe_equ_eq in Heqop'. now rewrite Heqop'. - - destruct e, a. - all: cbn in *; destruct (c =? c0) eqn:comm'; inv comm. - + eexists; split. - unfold new; rewrite unfold_interp, <- Heqobsp. - cbn; unfold Utils.mbr, MonadBr_ctree, branch. - eapply trans_bind_l. - intros abs; inv abs. - rewrite comm'. - unfold trigger. - eapply trans_vis'. - reflexivity. - rewrite bind_ret_l, sb_guard, H. - unfold new. - rewrite unfold_interp. - rewrite <- Heqop', <- unfold_interp. - reflexivity. - + eexists; split. - unfold new; rewrite unfold_interp, <- Heqobsp. - cbn; unfold Utils.mbr, MonadBr_ctree, branch. - eapply trans_bind_l. - intros abs; inv abs. - rewrite comm'. - unfold trigger. - eapply trans_vis'. - reflexivity. - rewrite bind_ret_l, sb_guard, H. - unfold new. - rewrite unfold_interp. - rewrite <- Heqop', <- unfold_interp. - reflexivity. + - destruct e as [a]; destruct a as [ch | ch]. + all: cbn [can_comm] in comm; + destruct (c =? ch) eqn:COMM; inv comm. + all: eexists; split. + all: try solve [unfold new; rewrite unfold_interp, <- Heqobsp; + cbn [h_new]; rewrite COMM; apply Trans.trans_trigger]. + all: rewrite sb_guard, H. + all: apply observe_equ_eq in Heqop'; rewrite Heqop'; reflexivity. - tauto. Qed. -Lemma trans_new_inv_aux : forall l T U, +Lemma trans_new_inv_aux : forall l (T U : ccs'), trans_ l T U -> - forall c p q, + forall c (p q : ccs), (go T ≅ new c p \/ go T ≅ Guard (new c p)) -> go U ≅ q -> exists q', can_comm c l = true /\ trans l p q' /\ @@ -387,22 +368,17 @@ Proof. - destruct EQ1 as [EQ1 | EQ1]. + unfold new in EQ1; rewrite unfold_interp in EQ1. unfold trans, transR. - cbn. + cbn -[CTree.branch MonadBr_ctree]. desobs p; try now (step in EQ1; inv EQ1). - * destruct e,a; cbn in *. - ** destruct (c =? c1); cbn in *. - *** step in EQ1; dependent induction EQ1; inv x0. - *** step in EQ1; inv EQ1. - ** destruct (c =? c1); cbn in *. - *** step in EQ1; dependent induction EQ1; inv x0. - *** step in EQ1; inv EQ1. - * cbn in EQ1. - unfold Utils.mbr, MonadBr_ctree, branch in EQ1. - cbn in * |-. - rewrite unfold_bind in EQ1; cbn in EQ1. + * destruct e,a; cbn [h_new] in EQ1; + destruct (c =? c1); cbn [h_new] in EQ1; + try solve [step in EQ1; dependent induction EQ1; inv x0]; + rewrite bind_trigger in EQ1; step in EQ1; inv EQ1. + * cbn -[CTree.branch MonadBr_ctree] in EQ1. + unfold Utils.mbr, MonadBr_ctree in EQ1; rewrite bind_branch in EQ1. inv_equ. rename EQ into eqx. specialize (eqx x). - cbn in * |-; rewrite bind_ret_l in eqx. + cbn -[CTree.trigger CTree.bind] in * |-. edestruct (IHtr (k0 x)) as (q' & comm & tr' & EQ). now right; rewrite <- ctree_eta. eauto. @@ -415,7 +391,7 @@ Proof. - destruct EQ1 as [EQ1 | EQ1]. + unfold new in EQ1; rewrite unfold_interp in EQ1. unfold trans, transR. - cbn. + cbn -[CTree.trigger CTree.bind]. desobs p; try now (step in EQ1; inv EQ1). * inv_equ. edestruct (IHtr t0) as (q' & comm & tr' & EQ). @@ -425,13 +401,10 @@ Proof. eexists; ssplit; auto. econstructor; apply tr'. rewrite <- EQ2; eauto. - * destruct e,a; cbn in *. - ** destruct (c =? c0); cbn in *. - *** step in EQ1; dependent induction EQ1; inv x0. - *** step in EQ1; inv EQ1. - ** destruct (c =? c0); cbn in *. - *** step in EQ1; dependent induction EQ1; inv x0. - *** step in EQ1; inv EQ1. + * destruct e,a; cbn [h_new] in EQ1; + destruct (c =? c0); cbn [h_new] in EQ1; + try solve [step in EQ1; dependent induction EQ1; inv x0]; + rewrite bind_trigger in EQ1; step in EQ1; inv EQ1. + inv_equ. edestruct IHtr as (q' & comm & tr' & EQ). left; rewrite EQ1, <- ctree_eta; reflexivity. @@ -442,46 +415,47 @@ Proof. - destruct EQ1 as [EQ1 | EQ1]; inv_equ. + unfold new in EQ1; rewrite unfold_interp in EQ1. unfold trans, transR. - cbn. + cbn -[CTree.trigger CTree.bind]. desobs p; try now (step in EQ1; inv EQ1). * inv_equ. eexists; ssplit; auto. constructor; reflexivity. rewrite <- EQ2, <- ctree_eta, H; auto. - * destruct e,a; cbn in *. - ** destruct (c =? c0); cbn in *. - *** step in EQ1; dependent induction EQ1; inv x0. - *** step in EQ1; inv EQ1. - ** destruct (c =? c0); cbn in *. - *** step in EQ1; dependent induction EQ1; inv x0. - *** step in EQ1; inv EQ1. + * destruct e,a; cbn [h_new] in EQ1; + destruct (c =? c0); cbn [h_new] in EQ1; + try solve [step in EQ1; dependent induction EQ1; inv x0]; + rewrite bind_trigger in EQ1; step in EQ1; inv EQ1. - destruct EQ1 as [EQ1 | EQ1]; [ | inv_equ]. - unfold new in EQ1; rewrite unfold_interp in EQ1. - unfold trans,transR; cbn. - desobs p; inv_equ. - cbn in *. - destruct e0,a; cbn in *; destruct (c =? c0) eqn:EQ; inv_equ. - + rewrite bind_trigger in EQ1. - inv_equ. - rewrite EQ; eexists; ssplit; auto. - constructor; reflexivity. - rewrite <- EQ2, <- ctree_eta, <- H; auto. - + rewrite bind_trigger in EQ1. - inv_equ. - rewrite EQ; eexists; ssplit; auto. - constructor; reflexivity. - rewrite <- EQ2, <- ctree_eta, <- H; auto. + unfold new in EQ1. + destruct (observe p) as [r | | t0 | t0 | U0 e0 k0 | U0 c0 k0] eqn:EP; + rewrite (ctree_eta p), EP in EQ1. + + destruct r. + + rewrite FoldCTree.interp_stuck in EQ1; inv_equ. + + rewrite FoldCTree.interp_step in EQ1; inv_equ. + + rewrite FoldCTree.interp_guard in EQ1; inv_equ. + + rewrite FoldCTree.interp_vis in EQ1. + destruct e0 as [a]; destruct a as [ch | ch]; + cbn [h_new] in EQ1; + destruct (c =? ch) eqn:COMM. + all: try solve [rewrite bind_stuck in EQ1; inv_equ]. + all: pose proof (trans_vis e x k) as TR. + all: rewrite H, EQ1 in TR; + apply Trans.trans_trigger_inv in TR as ([] & ET & EL). + all: exists (k0 tt); ssplit. + all: try solve [rewrite EL; cbn [can_comm]; rewrite COMM; reflexivity]. + all: try solve [rewrite EL, (ctree_eta p), EP; apply trans_vis]. + all: rewrite <- EQ2, <- ctree_eta; exact ET. + + rewrite FoldCTree.interp_br' in EQ1; inv_equ. - destruct EQ1 as [EQ1 | EQ1]; inv_equ. unfold new in EQ1; rewrite unfold_interp in EQ1. - unfold trans,transR; cbn. + unfold trans,transR; cbn -[CTree.trigger CTree.bind]. desobs p; inv_equ. destruct r0. - cbn in *. - destruct e,a; cbn in *. - * destruct (c =? c0); cbn in *; inv_equ. - * destruct (c =? c0); cbn in *; inv_equ. + destruct e,a; cbn [h_new] in EQ1; + destruct (c =? c0); cbn [h_new] in EQ1; + rewrite ?bind_trigger in EQ1; inv_equ. Qed. Lemma trans_new_inv : forall l c p p', diff --git a/examples/CCS/OpDenot.v b/examples/CCS/OpDenot.v index 86917a90..320911a7 100644 --- a/examples/CCS/OpDenot.v +++ b/examples/CCS/OpDenot.v @@ -1,4 +1,3 @@ -Unset Universe Checking. From CTree Require Import CTree diff --git a/examples/CCS/dune b/examples/CCS/dune index 047c96fb..1f5ea64a 100644 --- a/examples/CCS/dune +++ b/examples/CCS/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name CTreeCCS) (theories CTree) ) \ No newline at end of file diff --git a/examples/Coffee/coffeeCTree.v b/examples/Coffee/coffeeCTree.v index b1abb6b7..30a07885 100644 --- a/examples/Coffee/coffeeCTree.v +++ b/examples/Coffee/coffeeCTree.v @@ -55,10 +55,12 @@ Proof. intros H. setoid_rewrite ctree_eta in H. play in H. setoid_rewrite bind_ret_l in EQ. - apply trans_br_inv in TR as (? & TR). destruct x1. inv_trans. - - play in EQ. inv_trans. subst. discriminate. - - eapply ssim_br_l_inv with (x := true) in EQ. - play in EQ. inv_trans. subst; discriminate. + apply trans_br_inv in TR as (? & TR). destruct x1; + [| eapply ssim_br_l_inv with (x := true) in EQ]; play in EQ; + apply Trans.trans_trigger_inv in TR as ([] & EQt & _); + rewrite EQt in TR0; + apply Trans.trans_trigger_inv in TR0 as ([] & _ & BAD); inv BAD; auto. + all: match goal with H : obs _ _ = obs _ _ |- _ => inv H end. Unshelve. all: auto. Qed. @@ -67,18 +69,12 @@ Proof. coinduction R CH. setoid_rewrite ctree_eta. cbn. setoid_rewrite bind_ret_l. apply step_ss_br_l. intros. - destruct x. - - rewrite bind_trigger. apply step_ss_vis; auto. intros []. - exists tt. split; auto. - step. apply step_ss_br_r with (x := true). - eapply ssim_bind_chain. reflexivity. cbn. intros _. - apply step_ss_vis_id. auto. - - rewrite bind_trigger. - apply step_ss_vis; auto; intros []; exists tt; split; auto. - step. - apply step_ss_br_r with (x := false). - apply ssim_bind_chain. reflexivity. intros _. - apply step_ss_vis_id. auto. + destruct x; rewrite !bind_trigger; + apply step_ss_vis; auto; intros []; exists tt; split; auto; step. + 1: apply step_ss_br_r with (x := true). + 2: apply step_ss_br_r with (x := false). + all: eapply ssim_bind_chain; [reflexivity | cbn; intros _]. + all: apply step_ss_vis_id; auto. Qed. Tactic Notation "play" "using" tactic(tac) := @@ -98,13 +94,10 @@ Proof. destruct s. 2: play; now step. setoid_rewrite bind_ret_l in H. - play in H. destruct x1; inv_trans; subst. - + play using (apply trans_br21; etrans). - step. play. - step. destruct s; auto. play in H. play. - + play using (apply trans_br22; etrans). - step. play. - step. destruct s; auto. - play in H. play. + play in H. destruct x1; + [play using (apply trans_br21; etrans) | play using (apply trans_br22; etrans)]. + all: apply Trans.trans_trigger_inv in TR as ([] & EQt & EQl); subst l. + all: step; cbn; eexists; split; [apply Trans.trans_trigger' | ]. + all: rewrite EQt in H; step; destruct s; auto; play in H; play. - pose proof (ssim_tracincl _ _ coffee_ssim); auto. Qed. diff --git a/examples/Coffee/dune b/examples/Coffee/dune index 326b5e30..e0163c31 100644 --- a/examples/Coffee/dune +++ b/examples/Coffee/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name CTreeCoffee) (theories CTree) ) diff --git a/examples/ImpBr/ImpBr.v b/examples/ImpBr/ImpBr.v index 9f590e97..232ac8dd 100755 --- a/examples/ImpBr/ImpBr.v +++ b/examples/ImpBr/ImpBr.v @@ -1,4 +1,3 @@ -Unset Universe Checking. From Stdlib Require Import Arith.PeanoNat @@ -33,8 +32,8 @@ From CTree Require Import Interp.FoldStateT. Import ListNotations. -Import MonadNotation. -Local Open Scope monad_scope. +Import CTreeNotations. +Local Open Scope ctree_scope. Local Open Scope string_scope. (*| @@ -73,15 +72,17 @@ Variant MemE : Type -> Type := Section Semantics. - Notation computation := (ctree MemE B2). + Universe computation_u. + Definition computation (T : Type@{computation_u}) : Type@{computation_u} := + @ctree@{_ _ _ _ computation_u computation_u} MemE B2 T. Fixpoint denote_expr (e : expr) : computation value := match e with - | Var v => trigger (rd v) - | Lit n => ret n - | Plus a b => l <- denote_expr a ;; r <- denote_expr b ;; ret (l + r) - | Minus a b => l <- denote_expr a ;; r <- denote_expr b ;; ret (l - r) - | Mult a b => l <- denote_expr a ;; r <- denote_expr b ;; ret (l * r) + | Var v => trigger (rd v) + | Lit n => Ret n + | Plus a b => (l <- denote_expr a;; r <- denote_expr b;; Ret (l + r))%ctree + | Minus a b => (l <- denote_expr a;; r <- denote_expr b;; Ret (l - r))%ctree + | Mult a b => (l <- denote_expr a;; r <- denote_expr b;; Ret (l * r))%ctree end. Definition while (step : computation (unit + unit)) : computation unit := @@ -91,21 +92,20 @@ Section Semantics. Fixpoint denote_imp (s : stmt) : computation unit := match s with - | Assign x e => v <- denote_expr e ;; trigger (wr x v) - | Seq a b => denote_imp a ;; denote_imp b - | If i t e => - v <- denote_expr i ;; - if is_true v then denote_imp t else denote_imp e + | Assign x e => (v <- denote_expr e;; trigger (wr x v))%ctree + | Seq a b => (denote_imp a;; denote_imp b)%ctree + | If i t e => (v <- denote_expr i;; + if is_true v then denote_imp t else denote_imp e)%ctree | While t b => - while (v <- denote_expr t ;; - if is_true v - then denote_imp b ;; ret (inl tt) - else ret (inr tt)) + while (v <- denote_expr t;; + if is_true v + then denote_imp b;; Ret (inl tt) + else Ret (inr tt))%ctree | Branch a b => br2 (denote_imp a) (denote_imp b) - | Skip => ret tt + | Skip => Ret tt | Block => Stuck @@ -233,9 +233,8 @@ from Section 2 are indeed equivalent. repeat setoid_rewrite sb_guard. cbn. rewrite interp_state_ret. - unfold trigger. rewrite interp_state_vis. + rewrite interp_state_trigger. cbn. rewrite bind_ret_l, sb_guard. - cbn. rewrite interp_state_ret. apply sb_ret. rewrite alist_add_alist_add; [reflexivity |]. apply RelDec_Correct_string. diff --git a/examples/ImpBr/dune b/examples/ImpBr/dune index 1395468f..49cad153 100755 --- a/examples/ImpBr/dune +++ b/examples/ImpBr/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name CTreeImp) (theories CTree) ) diff --git a/examples/SimpleSim/SimExample.v b/examples/SimpleSim/SimExample.v index 2e09e1ee..932e570c 100644 --- a/examples/SimpleSim/SimExample.v +++ b/examples/SimpleSim/SimExample.v @@ -58,11 +58,11 @@ Proof. unfold br2. rewrite bind_br. apply step_sb_br_id. intros. destruct x. - - rewrite bind_trigger. + - rewrite !bind_trigger. apply step_sb_vis_id. intros []. split; [| auto]. rewrite sb_guard. apply CH. - - rewrite bind_trigger. + - rewrite !bind_trigger. apply step_sb_vis_id. intros []. split; [| auto]. rewrite sb_guard. apply CH. diff --git a/examples/SimpleSim/dune b/examples/SimpleSim/dune index 881d647c..aaa2f082 100644 --- a/examples/SimpleSim/dune +++ b/examples/SimpleSim/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name CTreeSimExample) (theories CTree) ) diff --git a/examples/Yield/Lang.v b/examples/Yield/Lang.v index 63018378..b6470994 100644 --- a/examples/Yield/Lang.v +++ b/examples/Yield/Lang.v @@ -14,15 +14,11 @@ From ExtLib Require Import Data.List Data.Map.FMapAList. -(* Universe issue, TO FIX *) -Unset Universe Checking. -Unset Auto Template Polymorphism. From ITree Require Import ITree Basics.CategoryKleisli Events.State - Events.StateFacts Events.MapDefault. From Coinduction Require Import all. @@ -74,15 +70,21 @@ Variant MemE : Type -> Type := | rd (x : var) : MemE value | wr (x : var) (v : value) : MemE unit. +Set Universe Polymorphism. Section Denote1. + Universes d q sd sq yd yq md mq. Definition is_true (v : value) : bool := if (v =? 0)%nat then false else true. Context (E := yieldE +' forkE +' MemE). - Definition while (step : ctree E void1 (unit + unit)) : ctree E void1 unit := + + Definition while + (step : @ctree@{_ _ _ _ d q} E void1 (unit + unit)) : + @ctree@{_ _ _ _ d q} E void1 unit := CTree.iter (fun _ => step) tt. - Fixpoint denote_expr (e : expr) : ctree E void1 value := + Fixpoint denote_expr (e : expr) : + @ctree@{_ _ _ _ d q} E void1 value := match e with | Var v => x <- trigger (rd v) ;; trigger Yield;; ret x | Lit n => ret n @@ -91,7 +93,8 @@ Section Denote1. | Mult a b => l <- denote_expr a ;; r <- denote_expr b ;; ret (l * r) end. - Fixpoint denote_imp (s : stmt) : ctree E void1 unit := + Fixpoint denote_imp (s : stmt) : + @ctree@{_ _ _ _ d q} E void1 unit := match s with | Assign x e => v <- denote_expr e ;; u <- trigger (wr x v) ;; ret u | Seq a b => denote_imp a ;; denote_imp b @@ -118,40 +121,54 @@ Section Denote1. Definition interp_concurrency (t : stmt) : completed := schedule 1 (fun _ => denote_imp t) (Some Fin.F1). - Definition handle_spawn : (yieldE +' spawnE +' MemE) ~> ctree (yieldE +' MemE) Bn := + Definition handle_spawn : (yieldE +' spawnE +' MemE) ~> + @ctree@{_ _ _ _ sd sq} (yieldE +' MemE) Bn := fun _ e => match e with | inl1 y => trigger y - | inr1 (inl1 s) => match s with Spawn => ret tt end (* erase spawn events *) + | inr1 (inl1 s) => match s in spawnE T return + @ctree@{_ _ _ _ sd sq} (yieldE +' MemE) Bn T with Spawn => Ret tt end | inr1 (inr1 m) => trigger m end. - Definition interp_spawn : @completed MemE -> ctree (yieldE +' MemE) Bn unit := - Fold.interp handle_spawn (T := unit). - - Definition handle_yield : (yieldE +' MemE) ~> ctree MemE Bn := + Definition interp_spawn : @completed MemE -> + @ctree@{_ _ _ _ sd sq} (yieldE +' MemE) Bn unit := + Fold.interp handle_spawn (T:=unit). + Definition handle_yield : (yieldE +' MemE) ~> + @ctree@{_ _ _ _ yd yq} MemE Bn := fun _ e => match e with - | inl1 s => match s with Yield => ret tt end (* erase yield events *) + | inl1 s => match s in yieldE T return + @ctree@{_ _ _ _ yd yq} MemE Bn T with Yield => Ret tt end | inr1 m => trigger m end. - Definition interp_yield : ctree (yieldE +' MemE) Bn unit -> ctree MemE Bn unit := + Definition interp_yield : + @ctree@{_ _ _ _ sd sq} (yieldE +' MemE) Bn unit -> + @ctree@{_ _ _ _ yd yq} MemE Bn unit := Fold.interp handle_yield (T:=unit). - (* list of key value pairs *) Definition env := alist var value. - - Definition handle_state : MemE ~> Monads.stateT env (ctree void1 Bn) := + Definition handle_state : MemE ~> + Monads.stateT env (@ctree@{_ _ _ _ md mq} void1 Bn) := fun _ e s => match e with | rd x => Ret (s, lookup_default x 0%nat s) | wr x v => Ret (Maps.add x v s, tt) end. - Definition interp_imp (t : stmt) : Monads.stateT env (ctree void1 Bn) unit := + + Definition interp_imp (t : stmt) : + Monads.stateT env (@ctree@{_ _ _ _ md mq} void1 Bn) unit := interp_state handle_state (interp_yield (interp_spawn (interp_concurrency t))). + #[local] Arguments CTree.trigger : simpl never. + #[local] Arguments CTree.branch : simpl never. + #[local] Arguments CTree.bind : simpl never. + #[local] Arguments Fold.interp : simpl never. + #[local] Arguments interp_state : simpl never. + #[local] Arguments MonadBr_ctree : simpl never. + Lemma schedule_forks_equ t1 t2 : (schedule 1 (fun _ : fin 1 => denote_imp (Fork t1 (Fork t2 Skip))) (Some Fin.F1)) ≅ @@ -163,26 +180,41 @@ Section Denote1. (fun _ => denote_imp t1)) None)). Proof. + cbn. repeat setoid_rewrite bind_trigger. rewrite rewrite_schedule. simp schedule_match. cbn. CTree.fold_subst. - unfold trigger. step. cbn. constructor. intros []. + rewrite (bind_ret_l tt (fun _ => trigger Spawn;; + Guard (schedule 2 (cons_vec (denote_imp t2) (fun _ => denote_imp t1)) None))). + etransitivity. + { apply equ_schedule with + (y := cons_vec (denote_imp t1) + (fun _ => Vis (subevent _ Par.Fork) (fun b : bool => if b then denote_imp t2 else Ret tt))); intros i. + dependent destruction i. + - simp cons_vec. rewrite bind_ret_l; reflexivity. + - dependent destruction i; [| inv i]. + simp cons_vec. unfold replace_vec. cbn. + rewrite bind_ret_l, bind_trigger; reflexivity. } + cbn. + rewrite bind_trigger. rewrite rewrite_schedule. simp schedule_match. simp cons_vec. unfold replace_vec. cbn. step. cbn. constructor. intros []. - rewrite rewrite_schedule. simp schedule_match. simp cons_vec. cbn. + rewrite rewrite_schedule. simp schedule_match. simp cons_vec. + cbn. step. cbn. constructor. apply equ_schedule. intro i. dependent destruction i. - simp remove_vec. simp cons_vec. CTree.fold_subst. - rewrite bind_ret_l. reflexivity. + rewrite ?bind_ret_l. reflexivity. - dependent destruction i; [| inv i]. simp remove_vec. simp cons_vec. - unfold remove_front_vec. simp cons_vec. cbn. simp cons_vec. - rewrite bind_ret_l. reflexivity. + unfold remove_front_vec. simp cons_vec. + cbn. simp cons_vec. + rewrite ?bind_ret_l. reflexivity. Qed. Equations p : fin 2 -> fin 2 := @@ -256,12 +288,8 @@ Section Denote1. Proof. unfold interp_concurrency. do 2 rewrite schedule_forks_equ. - unfold trigger. - (* not sure why we can't just rewrite twice, but we can below *) - rewrite bind_vis. symmetry. rewrite bind_vis. - apply sb_vis. intros []. do 2 rewrite bind_ret_l. - do 2 rewrite bind_vis. - apply sb_vis. intros []. do 2 rewrite bind_ret_l. + repeat setoid_rewrite bind_trigger. + do 2 (apply sb_vis; intros []). apply sb_guard_lr. do 2 rewrite rewrite_schedule. simp schedule_match. @@ -279,25 +307,30 @@ Section Denote1. (trigger Yield;; br1 (interp_concurrency s)). Proof. - unfold interp_concurrency. cbn. + unfold interp_concurrency. + etransitivity. + { apply equ_schedule; intros i; cbn; apply bind_trigger. } + setoid_rewrite bind_trigger. rewrite rewrite_schedule. simp schedule_match. - cbn. unfold trigger. + cbn. rewrite replace_vec_unary. step. cbn. constructor. intros []. rewrite rewrite_schedule. simp schedule_match. - CTree.fold_subst. rewrite (bind_ret_l tt). - simp cons_vec. cbn. rewrite remove_vec_cons_2. + CTree.fold_subst. + simp cons_vec. cbn. + rewrite remove_vec_cons_2. step. cbn. constructor. rewrite rewrite_schedule. simp schedule_match. + rewrite bind_trigger. step. cbn. constructor. intros []. - CTree.fold_subst. rewrite (bind_ret_l tt). + CTree.fold_subst. step. constructor; intros i. dependent destruction i. 2: inv i. - apply equ_schedule. repeat intro. rewrite bind_ret_l. reflexivity. + apply equ_schedule. repeat intro. reflexivity. Qed. Lemma yield_equ s : @@ -306,7 +339,10 @@ Section Denote1. (trigger Yield;; br1 (interp_concurrency s)). Proof. - unfold interp_concurrency. cbn. + unfold interp_concurrency. + etransitivity. + { apply equ_schedule; intros i; cbn; apply bind_trigger. } + setoid_rewrite bind_trigger. rewrite rewrite_schedule. simp schedule_match. cbn. CTree.fold_subst. @@ -321,7 +357,7 @@ Section Denote1. CTree.fold_subst. step. cbn. constructor; intros i. dependent destruction i. 2: inv i. - apply equ_schedule. repeat intro. rewrite bind_ret_l. reflexivity. + apply equ_schedule. repeat intro. rewrite ?bind_ret_l. reflexivity. Qed. Lemma br1_guard {F X} (t : ctree F Bn X) : @@ -340,28 +376,29 @@ Section Denote1. interp_yield (interp_spawn (interp_concurrency (Fork s Skip))). Proof. rewrite yield_equ, fork_skip_equ. + setoid_rewrite (yield_equ s). unfold interp_yield, interp_spawn. - - repeat (unfold trigger; rewrite ?interp_bind, ?interp_vis, ?interp_ret, ?bind_ret_l, ?interp_guard, ?sb_guard; cbn). - rewrite ?interp_br', ?subevent_subevent, ?br1_guard. - repeat (unfold trigger; rewrite ?interp_bind, ?interp_vis, ?interp_ret, ?bind_ret_l, ?interp_guard, ?sb_guard; cbn). - rewrite yield_equ. - rewrite ?interp_guard, sb_guard. - repeat (unfold trigger; rewrite ?interp_bind, ?interp_vis, ?interp_ret, ?bind_ret_l, ?interp_guard, ?sb_guard; cbn). - rewrite ?interp_br', ?subevent_subevent, ?br1_guard. - repeat (unfold trigger; rewrite ?interp_bind, ?interp_vis, ?interp_ret, ?bind_ret_l, ?interp_guard, ?sb_guard; cbn). - unfold trigger. + repeat (rewrite ?FoldCTree.interp_bind, ?FoldCTree.interp_trigger, + ?FoldCTree.interp_ret, ?FoldCTree.interp_guard, ?FoldCTree.interp_br', + ?bind_bind, ?bind_ret_l, ?bind_guard, ?sb_guard, + ?subevent_subevent, ?br1_guard; cbn -[schedule denote_imp]). reflexivity. Qed. + + Lemma fork_skip_yield s : interp_spawn (interp_concurrency (Seq YieldS s)) ~ interp_spawn (interp_concurrency (Fork s Skip)). Proof. rewrite yield_equ, fork_skip_equ. unfold interp_spawn. - repeat (unfold trigger; rewrite ?interp_bind, ?interp_vis, ?interp_ret, ?bind_ret_l, ?interp_guard, ?sb_guard; cbn). + repeat (rewrite ?FoldCTree.interp_bind, ?FoldCTree.interp_trigger, + ?FoldCTree.interp_ret, ?FoldCTree.interp_guard, + ?bind_bind, ?bind_ret_l, ?bind_guard, ?sb_guard; + cbn -[schedule denote_imp]). upto_bind_eq; intros []. + rewrite ?bind_ret_l, ?sb_guard. reflexivity. Qed. @@ -371,9 +408,10 @@ Section Denote1. Proof. rewrite fork_skip_equ. unfold interp_yield, interp_spawn. - repeat (unfold trigger; rewrite ?interp_bind, ?interp_vis, ?interp_ret, ?bind_ret_l, ?interp_guard, ?sb_guard; cbn). - rewrite ?interp_br', ?subevent_subevent, br1_guard. - repeat (unfold trigger; rewrite ?interp_bind, ?interp_vis, ?interp_ret, ?bind_ret_l, ?interp_guard, ?sb_guard; cbn). + repeat (rewrite ?FoldCTree.interp_bind, ?FoldCTree.interp_trigger, + ?FoldCTree.interp_ret, ?FoldCTree.interp_guard, ?FoldCTree.interp_br', + ?bind_bind, ?bind_ret_l, ?bind_guard, ?sb_guard, + ?subevent_subevent, ?br1_guard; cbn -[schedule denote_imp]). reflexivity. Qed. @@ -388,14 +426,15 @@ Section Denote1. rewrite bind_ret_l. apply sb_guard. Qed. + Lemma commut_forks_unfold s : interp_concurrency (Fork (While (Lit 1%nat) YieldS) (Fork s Skip)) ~ interp_concurrency (Fork s (Fork (Seq YieldS (While (Lit 1%nat) YieldS)) Skip)). Proof. unfold interp_concurrency. do 2 rewrite schedule_forks_equ. - upto_bind_eq; intros []. - upto_bind_eq; intros []. + repeat setoid_rewrite bind_trigger. + do 2 (apply sb_vis; intros []). apply sb_guard_lr. apply schedule_order''. @@ -405,9 +444,12 @@ Section Denote1. Lemma assign_equ : interp_concurrency (Assign "x" (Lit 2)) ≅ - (vis (wr "x" 2) (fun _ => Guard (ret tt))). + (vis (wr "x" 2) (fun _ => Guard (ret tt)) : @completed MemE). Proof. - unfold interp_concurrency. cbn. + unfold interp_concurrency. + etransitivity. + { apply equ_schedule with (y := fun _ => Vis (subevent _ (wr "x" 2)) (fun x => Ret x)); + intros i; cbn; rewrite bind_ret_l, bind_trigger; reflexivity. } rewrite rewrite_schedule. simp schedule_match. cbn. CTree.fold_subst. @@ -416,15 +458,22 @@ Section Denote1. rewrite rewrite_schedule. simp schedule_match. cbn. step. constructor. - rewrite rewrite_schedule. simp schedule_match. reflexivity. + rewrite rewrite_schedule. simp schedule_match. + step; cbn; constructor; reflexivity. Qed. Lemma fork_assign_assign_equ : interp_concurrency (Fork (Assign "x" (Lit 2)) (Assign "x" (Lit 1%nat))) ≅ - trigger Spawn;; (vis (wr "x" 1%nat) (fun _ => (Guard (trigger Yield;; br1 ((vis (wr "x" 2) (fun _ => Guard (ret tt)))))))). + (trigger Spawn;; + vis (wr "x" 1%nat) (fun _ => Guard + (trigger Yield;; br1 (vis (wr "x" 2) (fun _ => Guard (Ret tt))))) + : @completed MemE). Proof. - unfold interp_concurrency. cbn. + unfold interp_concurrency. + etransitivity. + { apply equ_schedule; intros i; cbn; apply bind_trigger. } + rewrite bind_trigger. rewrite rewrite_schedule. simp schedule_match. cbn. CTree.fold_subst. @@ -441,15 +490,19 @@ Section Denote1. step. constructor. rewrite rewrite_schedule. simp schedule_match. - step. cbn. constructor. CTree.fold_subst. intros []. + step. cbn. + rewrite bind_trigger. + constructor. CTree.fold_subst. intros []. step. cbn. constructor. intros i. dependent destruction i. 2: inv i. rewrite remove_vec_cons_2. - rewrite rewrite_schedule. simp schedule_match. cbn. + rewrite rewrite_schedule. simp schedule_match. + cbn. step. constructor. intros []. - rewrite rewrite_schedule. simp schedule_match. cbn. + rewrite rewrite_schedule. simp schedule_match. + cbn. step. constructor. rewrite rewrite_schedule. simp schedule_match. reflexivity. @@ -477,39 +530,32 @@ Section Denote1. interp_imp (Assign "x" (Lit 2)) s. Proof. unfold interp_imp. - rewrite fork_assign_assign_equ, assign_equ. + setoid_rewrite fork_assign_assign_equ. + setoid_rewrite assign_equ. unfold interp_yield, interp_spawn. - rewrite interp_bind. unfold trigger. rewrite interp_vis. - cbn. rewrite bind_ret_l. setoid_rewrite interp_ret. - rewrite ?interp_bind, ?interp_guard, ?bind_guard, interp_state_guard. - rewrite sb_guard. - rewrite interp_ret, bind_ret_l. - - rewrite interp_vis; cbn. - unfold trigger; rewrite interp_vis; cbn. - rewrite bind_vis, interp_vis; cbn. - rewrite interp_state_bind, interp_state_trigger. - repeat (cbn; rewrite ?bind_bind, ?bind_ret_l, ?bind_guard, ?sb_guard, ?interp_guard, ?interp_state_guard). - unfold trigger. rewrite interp_bind, interp_vis; cbn. - rewrite bind_vis, interp_vis; cbn. - rewrite interp_state_bind, interp_state_trigger. - repeat (cbn; rewrite ?bind_bind, ?bind_ret_l, ?bind_guard, ?sb_guard, ?interp_guard, ?interp_state_guard). - unfold trigger. rewrite interp_bind, interp_vis; cbn. - repeat (cbn; rewrite ?bind_bind, ?bind_ret_l, ?bind_guard, ?sb_guard, ?interp_ret, ?interp_guard, ?interp_state_guard). - symmetry; rewrite ?sb_guard; symmetry. - rewrite ?interp_br', interp_state_br. - unfold branch; cbn. rewrite bind_br. + repeat (rewrite ?FoldCTree.interp_bind, ?FoldCTree.interp_trigger, + ?FoldCTree.interp_vis, ?FoldCTree.interp_guard, ?FoldCTree.interp_ret, + ?FoldCTree.interp_br', ?interp_state_bind, ?interp_state_trigger, + ?interp_state_vis, ?interp_state_guard, ?interp_state_ret, + ?bind_bind, ?bind_guard, ?bind_ret_l, ?subevent_subevent; cbn). + repeat apply sb_guard_l. + repeat apply sb_guard_r. + rewrite interp_state_br. + unfold mbr at 1; unfold MonadBr_ctree at 1. + cbn -[Fold.interp interp_state MonadBr_ctree]. + rewrite bind_branch. apply sb_br_l; [exact Fin.F1 |]. - intros ?. - repeat (cbn; rewrite ?bind_bind, ?bind_ret_l, ?bind_guard, ?sb_guard, ?interp_ret, ?interp_guard, ?interp_state_guard). - rewrite interp_vis; cbn. - unfold trigger; rewrite bind_vis, interp_vis; cbn. - rewrite interp_state_bind, interp_state_trigger. - repeat (cbn; rewrite ?bind_bind, ?bind_ret_l, ?bind_guard, ?sb_guard, ?interp_guard, ?interp_state_guard). - rewrite ?interp_ret, ?interp_state_ret. + intros i; dependent destruction i; [| now inversion i]. + repeat (rewrite ?FoldCTree.interp_bind, ?FoldCTree.interp_trigger, + ?FoldCTree.interp_vis, ?FoldCTree.interp_guard, ?FoldCTree.interp_ret, + ?FoldCTree.interp_br', ?interp_state_bind, ?interp_state_trigger, + ?interp_state_vis, ?interp_state_guard, ?interp_state_ret, + ?bind_bind, ?bind_guard, ?bind_ret_l, ?subevent_subevent; cbn). + repeat apply sb_guard_l. apply sb_ret. - rewrite alist_add_alist_add. 2: apply RelDec_Correct_string. reflexivity. + rewrite alist_add_alist_add; [reflexivity | apply RelDec_Correct_string]. Qed. + End Denote1. diff --git a/examples/Yield/Par.v b/examples/Yield/Par.v index 15f6152c..dfaf25f4 100644 --- a/examples/Yield/Par.v +++ b/examples/Yield/Par.v @@ -21,9 +21,6 @@ From RelationAlgebra Require Import From Equations Require Import Equations. -(* Universe issue, TO FIX *) -Unset Universe Checking. -Unset Auto Template Polymorphism. From ITree Require Import State. @@ -50,10 +47,13 @@ Variant spawnE : Type -> Type := | Spawn : spawnE unit. Section parallel. + Universes e q q'. Context {E : Type -> Type}. - Definition thread := ctree (yieldE +' forkE +' E) void1 unit. - Definition completed := ctree (yieldE +' spawnE +' E) Bn unit. + Definition thread := + @ctree@{e _ _ _ e q} (yieldE +' forkE +' E) void1 unit. + Definition completed := + @ctree@{e _ _ _ e q'} (yieldE +' spawnE +' E) Bn unit. Definition vec n := fin n -> thread. (** Scheduling a thread pool *) @@ -160,7 +160,8 @@ Section parallel. (*** how the scheduler behaves affects a thread *) (** inverting the case when a [schedule] is a [Br] *) - Lemma Br_schedule_inv n1 (e : Bn (fin n1)) k n2 (v : vec n2) i : + Polymorphic Lemma Br_schedule_inv n1 (e : Bn (fin n1)) + (k : fin n1 -> completed) n2 (v : vec n2) i : Br e k ≅ schedule n2 v (Some i) -> False. (* (exists k', v i ≅ Br e k' /\ *) (* forall i', k i' ≅ schedule n2 (replace_vec v i (k' i')) (Some i)). *) @@ -174,7 +175,7 @@ Section parallel. destruct c. Qed. - Lemma guard_schedule_inv t n (v : vec (S n)) (i : fin (S n)) : + Polymorphic Lemma guard_schedule_inv (t : completed) n (v : vec (S n)) (i : fin (S n)) : Guard t ≅ schedule _ v (Some i) -> (exists t', v i ≅ Guard t' /\ t ≅ schedule (S n) (replace_vec v i t') (Some i)) \/ @@ -190,7 +191,7 @@ Section parallel. - right; right. destruct r. split; auto. - step; rewrite Heqc; reflexivity. + step; rewrite Heqc; constructor; reflexivity. - left; eexists; split; eauto. step; rewrite Heqc; reflexivity. - destruct e; [destruct y | destruct s]; inv_equ. @@ -203,7 +204,7 @@ Section parallel. Qed. (** Helper lemmas for when [schedule] transitions with a [val] *) - Lemma trans_schedule_val_1 {X} n v i (x : X) t : + Polymorphic Lemma trans_schedule_val_1 {X} n v i (x : X) t : trans (val x) (schedule n v (Some i)) t -> n = 1%nat. Proof. @@ -216,7 +217,7 @@ Section parallel. induction H; intros n' ?t' v i x' Heql Heq Hequ; try inv Heql; subst. - rewrite <- ctree_eta in Hequ. destruct c. - now exfalso; apply Br_schedule_inv in Hequ. + exfalso; eapply (Br_schedule_inv n (branchn n) k n' v i); exact Hequ. - rewrite <- ctree_eta in Hequ. destruct n' as [| n]; [inv i |]. apply guard_schedule_inv in Hequ. @@ -239,7 +240,7 @@ Section parallel. destruct c. Qed. - Lemma trans_schedule_thread_val {X} v i (x : X) t : + Polymorphic Lemma trans_schedule_thread_val {X} v i (x : X) t : trans (val x) (schedule 1 v (Some i)) t -> trans (val x) (v i) Stuck. Proof. @@ -267,9 +268,9 @@ Section parallel. + destruct Hequ as [EQ EQ']. rewrite EQ' in H. rewrite rewrite_schedule in H. simp schedule_match in H. - apply trans_ret_inv in H. destruct H. inv H0. invert. - rewrite EQ. - cbn. + dependent destruction H. + unfold trans, transR; cbn. + step in EQ; inv EQ. constructor. - invert. rewrite rewrite_schedule in Hequ. @@ -297,6 +298,7 @@ Section parallel. rewrite <- ctree_eta in Hequ. rewrite rewrite_schedule in Hequ. simp schedule_match in Hequ. step in Hequ. inv Hequ. invert. exists n'. + dependent destruction H4. rewrite ctree_eta. rewrite <- Heq. rewrite <- H. rewrite REL. split; auto. } - destruct n'; inv_equ. @@ -328,7 +330,8 @@ Section parallel. - destruct e; [destruct y | destruct s; [destruct f |]]. try solve [step in Hequ; inv Hequ]. rewrite <- ctree_eta in Hequ. step in Hequ; inv Hequ. invert. - rewrite <- ctree_eta in Hequ. step in Hequ; inv Hequ. invert. + all: repeat invert. + step in Hequ; inv Hequ; invert. - destruct c. } { @@ -372,7 +375,7 @@ Section parallel. apply trans_schedule_obs_yield_None in H. destruct H as (?n' & ? & ?). subst. eexists. split. - + rewrite Hvi. constructor. + + unfold transR; cbn. step in Hvi; inv Hvi; constructor. + exists eq_refl. auto. Qed. @@ -382,9 +385,10 @@ Section parallel. False. Proof. intros Ht. - unfold trans in Ht. cbn in Ht. red in Ht. - rewrite rewrite_schedule in *. destruct n; inv Ht. invert. - destruct (observe (schedule_match schedule (S n) v None)) eqn:?; invert. + unfold trans, transR in Ht; cbn in Ht. + rewrite rewrite_schedule in Ht. + destruct n; [inv Ht; invert |]. + simp schedule_match in Ht; inv Ht; invert. Qed. (** [schedule] transitions with an [obs] of a [Spawn] *) @@ -526,7 +530,7 @@ Section parallel. (*** how a thread [trans] affects the scheduler [trans] *) (** thread transitions with a val *) - Lemma trans_thread_schedule_val_1 {X} v i (x : X) t : + Polymorphic Lemma trans_thread_schedule_val_1 {X} v i (x : X) t : trans (val x) (v i) t -> trans (val x) (schedule 1 v (Some i)) Stuck. Proof. @@ -628,6 +632,7 @@ Section parallel. rewrite rewrite_schedule at 1. simp schedule_match. econstructor. step. constructor. intros. apply equ_schedule. apply replace_vec_relation; repeat intro; auto. + invert; apply H. Qed. (** when the thread is a fork *) @@ -649,7 +654,7 @@ Section parallel. rewrite <- Heqc. constructor. rewrite <- (replace_vec_twice _ v i t (k false)). eapply IHvisible_; auto; rewrite replace_vec_eq; eauto. - - invert. + - invert. invert. rewrite rewrite_schedule at 1. simp schedule_match. rewrite <- Heqc. econstructor. apply equ_schedule. apply cons_vec_relation; auto. @@ -679,7 +684,7 @@ Section parallel. Qed. (*** Putting everything together *) - Lemma schedule_permutation n (v1 v2 : vec n) i (p q : fin n -> fin n) + Polymorphic Lemma schedule_permutation n (v1 v2 : vec n) i (p q : fin n -> fin n) (Hpq : forall i, p (q i) = i) (Hqp : forall i, q (p i) = i) (Hsb1 : forall i, v1 i ~ v2 (p i)) @@ -696,8 +701,8 @@ Section parallel. intros n v1 v2 i p q Hpq Hqp Hsb1 Hsb2 l t Ht. cbn in *. destruct l. - apply trans_schedule_thread_tau_some in Ht; auto. - assert (Hinjp : FinFun.Injective p) by (eapply bijective_injective; eauto). - assert (Hinjq : FinFun.Injective q) by (eapply bijective_injective; eauto). + assert (Hinjp : Finite.Injective p) by (eapply bijective_injective; eauto). + assert (Hinjq : Finite.Injective q) by (eapply bijective_injective; eauto). destruct n; try inv i. destruct Ht as (t' & Ht & Hequ). pose proof (Hsb1 i). step in H. destruct H as [Hf _]. @@ -719,11 +724,16 @@ Section parallel. + apply trans_schedule_obs_yield_Some in Ht; auto. destruct Ht. * (* The thread finished *) destruct H as (n' & Ht & (? & Hequ)); subst. cbn in *. - assert (Hinjp : FinFun.Injective p) by (eapply bijective_injective; eauto). - assert (Hinjq : FinFun.Injective q) by (eapply bijective_injective; eauto). + assert (Hinjp : Finite.Injective p) by (eapply bijective_injective; eauto). + assert (Hinjq : Finite.Injective q) by (eapply bijective_injective; eauto). epose proof (@remove_at_permutation_correct (yieldE +' forkE +' E) _ unit _ _ _ i Hpq Hqp Hinjp Hinjq) as (Hpq' & Hqp'). - edestruct (@remove_at_permutation_vectors (yieldE +' forkE +' E) void1 unit n') as (Hpq'' & Hqp''); eauto. + pose proof + (@remove_at_permutation_vectors (yieldE +' forkE +' E) void1 unit n' + v1 v2 i p q Hinjp Hinjq + _ _ + eq_refl eq_refl Hpq Hqp Hpq' Hqp' Hsb1 Hsb2) + as (Hpq'' & Hqp''). pose proof (Hsb1 i). step in H. destruct H as [Hf _]. edestruct Hf as (? & ? & ? & ? & ?); eauto; subst. apply trans_thread_schedule_val_SS in H. diff --git a/examples/Yield/Util.v b/examples/Yield/Util.v index 40b22cd3..de9a4ab7 100644 --- a/examples/Yield/Util.v +++ b/examples/Yield/Util.v @@ -21,9 +21,6 @@ From RelationAlgebra Require Import From Equations Require Import Equations. -(* Universe issue, TO FIX *) -Unset Universe Checking. -Unset Auto Template Polymorphism. From ITree Require Import State. @@ -346,10 +343,11 @@ Section Vectors. End Vectors. +Set Universe Polymorphism. Section Vector_brD_bound. - Context {E B : Type -> Type}. - Context {R : Type}. - Context (vec := fun n => fin n -> ctree E B R). + Universes r q. + Context {E : Type -> Type} {B : Type -> Type} {R : Type}. + Context (vec := fun n => fin n -> @ctree@{_ _ _ _ r q} E B R). (* Lemma remove_front_vec_brD_bound n n' (v : vec (S n)) : *) (* (forall i, brD_bound n' (v i)) -> *) @@ -673,7 +671,7 @@ Section Vector_brD_bound. Definition remove_at_permutation {n} (p : fin (S (S n)) -> fin (S (S n))) (r : fin (S (S n))) - (Hp : FinFun.Injective p) + (Hp : Finite.Injective p) : { p' : (fin (S n) -> fin (S n)) & (forall i, match (order_cases i r) with @@ -761,7 +759,7 @@ Section Vector_brD_bound. Lemma bijective_injective {n} (p q : fin n -> fin n) (Hqp: forall i, q (p i) = i) : - FinFun.Injective p. + Finite.Injective p. Proof. intros i1 i2 ?. apply (f_equal q) in H. do 2 rewrite Hqp in H. auto. Qed. @@ -1110,3 +1108,4 @@ Section Vector_brD_bound. } Qed. End Vector_brD_bound. +Unset Universe Polymorphism. diff --git a/examples/Yield/dune b/examples/Yield/dune index 9863f193..3aac4699 100644 --- a/examples/Yield/dune +++ b/examples/Yield/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name CTreeYield) - (theories CTree) + (theories CTree Equations) ) diff --git a/tests/ImpBrTest/ImpBrEx/ImpBrEx.v b/tests/ImpBrTest/ImpBrEx/ImpBrEx.v index 790e61b8..e89e9c7a 100644 --- a/tests/ImpBrTest/ImpBrEx/ImpBrEx.v +++ b/tests/ImpBrTest/ImpBrEx/ImpBrEx.v @@ -1,4 +1,3 @@ -Unset Universe Checking. From Stdlib Require Import Strings.String. diff --git a/tests/ImpBrTest/ImpBrEx/dune b/tests/ImpBrTest/ImpBrEx/dune index 5e8dd5c9..6f2617fe 100644 --- a/tests/ImpBrTest/ImpBrEx/dune +++ b/tests/ImpBrTest/ImpBrEx/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name ImpBrEx) (theories CTree CTreeImp) ) diff --git a/tests/ImpBrTest/extracted/Extract.v b/tests/ImpBrTest/extracted/Extract.v index bebcf27c..266dc406 100644 --- a/tests/ImpBrTest/extracted/Extract.v +++ b/tests/ImpBrTest/extracted/Extract.v @@ -1,7 +1,6 @@ Require Extraction. Require ExtrOcamlBasic. Require ExtrOcamlIntConv. -Unset Universe Checking. Require ImpBrEx.ImpBrEx. Extraction Language OCaml. diff --git a/tests/ImpBrTest/extracted/dune b/tests/ImpBrTest/extracted/dune index 02c1561c..f9c45e83 100644 --- a/tests/ImpBrTest/extracted/dune +++ b/tests/ImpBrTest/extracted/dune @@ -2,9 +2,9 @@ (name extracted) (wrapped false) ) -(coq.extraction +(rocq.extraction (prelude Extract) - (theories CTree CTreeImp ImpBrEx) + (theories Stdlib ExtLib Paco ITree Coinduction RelationAlgebra CTree CTreeImp ImpBrEx) (extracted_modules Applicative Ascii diff --git a/theories/Core/CTreeDefinitions.v b/theories/Core/CTreeDefinitions.v index f1fb5f4f..53b78b68 100644 --- a/theories/Core/CTreeDefinitions.v +++ b/theories/Core/CTreeDefinitions.v @@ -35,6 +35,7 @@ From ExtLib Require Import Set Implicit Arguments. Set Contextual Implicit. Set Primitive Projections. +Set Universe Polymorphism. (*| .. coq:: @@ -42,7 +43,8 @@ Set Primitive Projections. Section ctree. - Context {E : Type -> Type} {B : Type -> Type} {R : Type}. + Universe e b. + Context {E : Type@{e} -> Type} {B : Type@{b} -> Type} {R : Type}. (*| The type [ctree] is defined as the final coalgebra ("greatest fixed point") of the functor [ctreeF]. @@ -60,8 +62,8 @@ value returned by the environment | StuckF | StepF (t : ctree) | GuardF (t : ctree) - | VisF {X : Type} (e : E X) (k : X -> ctree) (* an external event *) - | BrF {X : Type} (c : B X) (k : X -> ctree) (* an internal non-deterministic branching *) + | VisF {X : Type@{e}} (e : E X) (k : X -> ctree) (* an external event *) + | BrF {X : Type@{b}} (c : B X) (k : X -> ctree) (* an internal non-deterministic branching *) . CoInductive ctree : Type := @@ -258,22 +260,29 @@ Functorial map ([fmap] in Haskell) Definition map {R S} (f : R -> S) (t : ctree E B R) : ctree E B S := bind t (fun x => Ret (f x)). + + + End CTree. + + Section AtomicTrees. + Universes d q. + Context {E : Type -> Type} {B : Type -> Type}. (*| Atomic itrees triggering a single event. |*) - Definition trigger : E ~> ctree E B := - fun R e => Vis e (fun x => Ret x). + Definition trigger (T : Type) (e : E T) : @ctree@{_ _ _ _ d q} E B T := + Vis e (fun x => Ret x). (*| Atomic ctrees with choice. |*) - Definition branch {X : Type} : forall (c : B X), ctree E B X := - fun c => Br c (fun x => Ret x). + Definition branch {X : Type} (c : B X) : @ctree@{_ _ _ _ d q} E B X := + Br c (fun x => Ret x). - Definition branchS {X : Type} : forall (c : B X), ctree E B X := - fun c => BrS c (fun x => Ret x). + Definition branchS {X : Type} (c : B X) : @ctree@{_ _ _ _ d q} E B X := + BrS c (fun x => Ret x). (*| Ignore the result of a tree. @@ -282,7 +291,8 @@ Ignore the result of a tree. Definition ignore {R} : ctree E B R -> ctree E B unit := map (fun _ => tt). - End CTree. + End AtomicTrees. + Arguments trigger {E B} [T] _. Ltac fold_bind := repeat match goal with @@ -403,18 +413,22 @@ Instances #[global] Instance MonadIter_ctree {E B} : MonadIter (ctree E B) := fun R I => @CTree.iter E B R I. -#[global] Instance MonadTrigger_ctree {E F B} `{E -< F} : MonadTrigger E (ctree F B) := - fun _ e => trigger e. +#[global] Instance MonadTrigger_ctree@{d q +} {E : Type -> Type} {F : Type -> Type} {B} + `{E -< F} : MonadTrigger E (@ctree@{_ _ _ _ d q} F B) := + fun X e => (CTree.trigger (subevent _ e) : @ctree@{_ _ _ _ d q} F B X). -#[global] Instance MonadBr_ctree {E C D} `{C -< D} : MonadBr C (ctree E D) := - fun _ c => branch c. +#[global] Instance MonadBr_ctree@{d q +} {E} {C : Type -> Type} {D : Type -> Type} + `{C -< D} : MonadBr C (@ctree@{_ _ _ _ d q} E D) := + fun X c => (CTree.branch (subevent _ c) : @ctree@{_ _ _ _ d q} E D X). #[global] Instance MonadStuck_ctree {E C} : MonadStuck (ctree E C) := fun _ => Stuck. -#[global] Instance MonadStep_ctree {E C} : MonadStep (ctree E C) := +#[global] Instance MonadStep_ctree@{d q +} {E C} : + MonadStep (@ctree@{_ _ _ _ d q} E C) := Step (Ret tt). + (*| ==================================== Inversion lemma relying on [JMeq_eq] diff --git a/theories/Core/Index.v b/theories/Core/Index.v index b1993cc5..5cda1dec 100644 --- a/theories/Core/Index.v +++ b/theories/Core/Index.v @@ -1,6 +1,8 @@ From ITree Require Import Basics Indexed.Sum. From CTree Require Import Core.Utils. +Set Universe Polymorphism. + Section Index. (*| diff --git a/theories/Core/Utils.v b/theories/Core/Utils.v index 43101d32..571960b7 100644 --- a/theories/Core/Utils.v +++ b/theories/Core/Utils.v @@ -7,11 +7,13 @@ From ITree Require Import Basics.Basics. Notation fin := Fin.t. -Polymorphic Class MonadTrigger (E : Type -> Type) (M : Type -> Type) : Type := - mtrigger : forall {X}, E X -> M X. +Polymorphic Class MonadTrigger@{ei +} + (E : Type@{ei} -> Type) (M : Type -> Type) : Type := + mtrigger : forall {X : Type@{ei} }, E X -> M X. -Polymorphic Class MonadBr (B : Type -> Type) (M : Type -> Type) : Type := - mbr : forall {X}, B X -> M X. +Polymorphic Class MonadBr@{bi +} + (B : Type@{bi} -> Type) (M : Type -> Type) : Type := + mbr : forall {X : Type@{bi} }, B X -> M X. Polymorphic Class MonadStep (M : Type -> Type) : Type := mstep : M unit. diff --git a/theories/Eq/Epsilon.v b/theories/Eq/Epsilon.v index 476d0fa9..4586cb4b 100644 --- a/theories/Eq/Epsilon.v +++ b/theories/Eq/Epsilon.v @@ -10,6 +10,7 @@ From CTree Require Import Import CTreeNotations. Open Scope ctree_scope. +Set Universe Polymorphism. (* end hide *) diff --git a/theories/Eq/Equ.v b/theories/Eq/Equ.v index c7515313..57c6d2d1 100644 --- a/theories/Eq/Equ.v +++ b/theories/Eq/Equ.v @@ -25,6 +25,7 @@ From CTree Require Import Eq.Shallow. Import CTree. +Set Universe Polymorphism. #[local] Ltac step_ := step; simpl body. #[local] Ltac step := step_. @@ -265,13 +266,16 @@ Proof. cbn. rewrite <- x in EQu. dependent destruction EQu. - rewrite <- x. eauto. + rewrite <- x. + constructor; intro z. + exact (CH _ _ (REL1 z) _ _ (REL z) (REL0 z)). - dependent destruction EQ. cbn. rewrite <- x in EQu. dependent destruction EQu. rewrite <- x. - eauto. + constructor; intro z. + exact (CH _ _ (REL1 z) _ _ (REL z) (REL0 z)). Qed. #[global] Instance equb_eq_equ {E B X} {Q : rel X X} : @@ -692,7 +696,7 @@ Sufficient condition to prove compatibility only over the simulation Lemma equ_clos_sym {E C X} : compat converse (@equ_clos E E C C X X). Proof. intros R t u EQ; inv EQ. - apply Equ_clos with u' t'; intuition. + apply Equ_clos with u' t'; intuition; symmetry; assumption. Qed. Lemma equ_clos_equ {E C X L} {c: Chain (fequ L)}: @@ -713,10 +717,10 @@ Proof. inv Equu; constructor; apply IH; econstructor; eauto. dependent induction H1; dependent induction H2. inv Equu. dependent induction H2; dependent induction H3. - econstructor; intros. apply IH; econstructor; eauto. + econstructor; intros. apply IH; econstructor; [apply REL | apply REL0 | apply REL1]. dependent induction H1; dependent induction H2. inv Equu. dependent induction H2; dependent induction H3. - econstructor; intros. apply IH; econstructor; eauto. + econstructor; intros. apply IH; econstructor; [apply REL | apply REL0 | apply REL1]. Qed. #[global] Instance equ_eq_equ_goal_gen {E C R L} (r : Chain (@fequ E C R R L)) : @@ -885,13 +889,33 @@ Proof. now rewrite unfold_bind. Qed. -Lemma bind_trigger {E B X Y} (e : E X) (k : X -> ctree E B Y) : - trigger e >>= k ≅ Vis e k. +Section AtomicEquations. + Universes d q d' q'. + Context {E : Type -> Type} {B : Type -> Type}. + +Lemma unfold_branch {X} (c : B X) : + (CTree.branch c : @ctree@{_ _ _ _ d q} E B X) = Br c (fun x => Ret x). +Proof. reflexivity. Qed. + +Lemma unfold_branchS {X} (c : B X) : + (CTree.branchS c : @ctree@{_ _ _ _ d q} E B X) = BrS c (fun x => Ret x). +Proof. reflexivity. Qed. + +Lemma unfold_trigger {X} (e : E X) : + (CTree.trigger e : @ctree@{_ _ _ _ d q} E B X) = Vis e (fun x => Ret x). +Proof. reflexivity. Qed. + +Lemma bind_trigger {X Y} + (e : E X) (k : X -> @ctree@{_ _ _ _ d' q'} E B Y) : + (CTree.trigger e : @ctree@{_ _ _ _ d q} E B X) >>= k ≅ Vis e k. Proof. - unfold trigger; rewrite bind_vis; setoid_rewrite bind_ret_l. + rewrite unfold_trigger, bind_vis; setoid_rewrite bind_ret_l. reflexivity. Qed. +End AtomicEquations. + + Lemma bind_stuck {E B X Y} (g : X -> ctree E B Y): Stuck >>= g ≅ Stuck. Proof. @@ -916,13 +940,30 @@ Proof. now rewrite unfold_bind. Qed. -Lemma bind_branch : forall {E C X Y} (c : C Y) (k : Y -> ctree E C X), - branch c >>= k ≅ Br c k. +Section BranchBindEquations. + Universes d q d' q'. + Context {E : Type -> Type} {C : Type -> Type}. + +Lemma bind_branch {X Y} + (c : C Y) (k : Y -> @ctree@{_ _ _ _ d' q'} E C X) : + (CTree.branch c : @ctree@{_ _ _ _ d q} E C Y) >>= k ≅ Br c k. Proof. - intros. rewrite unfold_bind. cbn. setoid_rewrite bind_ret_l. + rewrite unfold_branch, bind_br; setoid_rewrite bind_ret_l. reflexivity. Qed. +Lemma bind_branchS {X Y} + (c : C Y) (k : Y -> @ctree@{_ _ _ _ d' q'} E C X) : + (CTree.branchS c : @ctree@{_ _ _ _ d q} E C Y) >>= k ≅ BrS c k. +Proof. + rewrite unfold_branchS, bind_br; setoid_rewrite bind_step; + setoid_rewrite bind_ret_l. + reflexivity. +Qed. + +End BranchBindEquations. + + Tactic Notation "sinv" ident(H) := step in H; inv H. Lemma stuck_equ_bind {E B X Y} : diff --git a/theories/Eq/IterFacts.v b/theories/Eq/IterFacts.v index 67f53a31..7e7eabe9 100644 --- a/theories/Eq/IterFacts.v +++ b/theories/Eq/IterFacts.v @@ -15,6 +15,7 @@ From CTree Require Import Import CTree. Import CTreeNotations. +Set Universe Polymorphism. Definition iter_gen {E B X I} (step : I -> ctree E B (I + X)) (t : ctree E B (I + X)) := diff --git a/theories/Eq/SBisim.v b/theories/Eq/SBisim.v index 9665d347..233ecb6c 100644 --- a/theories/Eq/SBisim.v +++ b/theories/Eq/SBisim.v @@ -66,6 +66,7 @@ From RelationAlgebra Require Export Import CoindNotations. Set Implicit Arguments. +Set Universe Polymorphism. Import CTree. Import CTreeNotations. Import EquNotations. @@ -625,12 +626,17 @@ Lemma vis_chain_gen {E F C D: Type -> Type} {X X' Y Y': Type} L Proof. intros. apply (b_chain R). - split; intros ?? TR; inv_trans; subst. - do 2 eexists; intuition; eauto. - rewrite EQ; auto. - do 2 eexists; intuition; eauto. - rewrite EQ; apply H2. - apply H0. + split; intros ? ? TR; inv_trans; subst. + - exists (obs e' (right x)), (k' (right x)); repeat split. + + apply trans_vis. + + eapply equ_clos_sb_ctx; + [symmetry; exact EQ | reflexivity | exact (H1 x)]. + + exact (H x). + - exists (obs e (left x)), (k (left x)); repeat split. + + apply trans_vis. + + eapply equ_clos_sb_ctx; + [reflexivity | symmetry; exact EQ | exact (H2 x)]. + + exact (H0 x). Qed. Lemma vis_chain {E C X Y} @@ -1309,8 +1315,11 @@ produce any challenge for the other. @spin_gen E C Z X c ~ @spin_gen E C Z Y c'. Proof. intros R. - coinduction S _; split; cbn; - intros * TR; exfalso; eapply spinD_gen_is_stuck, TR. + coinduction S _; split; cbn. + - intros * TR; exfalso. + exact (spinD_gen_is_stuck l (spin_gen c) t' c TR). + - intros * TR; exfalso. + exact (spinD_gen_is_stuck l (spin_gen c') t' c' TR). Qed. (*| @@ -1371,13 +1380,13 @@ produce any challenge for the other. Lemma br2_spin_l {X} : forall (t : ctree E C X), br2 spin t ~ t. Proof. - intros; apply br2_is_stuck, spin_is_stuck. + intros; apply br2_is_stuck; exact (spin_is_stuck τ t t). Qed. Lemma br2_spin_r {X} : forall (t : ctree E C X), br2 t spin ~ t. Proof. - intros; rewrite br2_commut; apply br2_is_stuck, spin_is_stuck. + intros; rewrite br2_commut; apply br2_spin_l. Qed. (*| @@ -1539,6 +1548,7 @@ Not fond of this, need to give some thoughts about them do 2 eexists; intuition; eauto. apply trans_val_inv in TR0. rewrite TR0; eauto. + apply trans_ret. Qed. End WithParams. @@ -1689,9 +1699,10 @@ Section StrongSimulations. rewrite EQ; auto. - step; intros ?? TR. inv_trans; subst. - exists τ, (Ret tt); intuition; now rewrite EQ. - exists τ, (Ret tt). intuition. - rewrite EQ; apply Stuck_ssim. + exists τ, (Ret tt); split; [apply trans_step |]. + split; [now rewrite EQ | reflexivity]. + exists τ, (Ret tt); split; [apply trans_step |]. + split; [rewrite EQ; apply Stuck_ssim | reflexivity]. - step in H. cbn in H. destruct H as [_ ?]. specialize (H τ Stuck). lapply H; [| etrans]. intros. destruct H0 as (? & ? & ? & ? & ?). diff --git a/theories/Eq/SBisimAlt.v b/theories/Eq/SBisimAlt.v index 363a253a..7f9226ef 100644 --- a/theories/Eq/SBisimAlt.v +++ b/theories/Eq/SBisimAlt.v @@ -24,6 +24,7 @@ From RelationAlgebra Require Export Import CoindNotations. Import CTree. Set Implicit Arguments. +Set Universe Polymorphism. (* TODO: Decide where to set this *) Arguments trans : simpl never. diff --git a/theories/Eq/SSim.v b/theories/Eq/SSim.v index 289a129f..6c9d39e5 100644 --- a/theories/Eq/SSim.v +++ b/theories/Eq/SSim.v @@ -23,6 +23,7 @@ From RelationAlgebra Require Export Import CoindNotations. Import CTree. Set Implicit Arguments. +Set Universe Polymorphism. (* TODO: Decide where to set this *) Arguments trans : simpl never. @@ -651,11 +652,13 @@ Section Proof_Rules. intros. cbn; intros ? ? TR; inv_trans; subst; destruct (H0 x) as (x' & RR & LL); - cbn; eexists; eexists; intuition. - - rewrite EQ; eauto. - - assumption. + cbn; exists (obs f x'), (k' x'); repeat split. + - apply trans_vis. + - eapply H; [symmetry; exact EQ | reflexivity | exact RR]. + - exact LL. Qed. + Lemma step_ss_vis {Y Z Z' F D} (e : E Z) (f: F Z') (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) (L : rel _ _) {R : Chain (@ss E F C D X Y L)} : diff --git a/theories/Eq/SSimAlt.v b/theories/Eq/SSimAlt.v index 43c7edba..15309b17 100644 --- a/theories/Eq/SSimAlt.v +++ b/theories/Eq/SSimAlt.v @@ -22,6 +22,7 @@ From RelationAlgebra Require Export Import CoindNotations. Import CTree. Set Implicit Arguments. +Set Universe Polymorphism. (* TODO: Decide where to set this *) Arguments trans : simpl never. @@ -335,9 +336,10 @@ Section Proof_Rules. intros. split; [| split]; intros; inv_equ. cbn; inv_trans; subst; destruct (H x) as (x' & RR & LL); - cbn; do 3 eexists; intuition. - - rewrite EQ; eauto. - - assumption. + cbn; exists (obs f x'), (k' x'); repeat split. + - apply trans_vis. + - eapply HR; [symmetry; exact EQ | reflexivity | exact RR]. + - exact LL. Qed. Lemma step_ss'_vis_id {Z} (e : E Z) (f: F Z) @@ -498,6 +500,7 @@ Section Proof_Rules. split; [| split]; intros; inv_equ. inv_trans; subst. cbn; do 3 eexists; intuition; subs; eauto. + apply trans_step. Qed. Lemma step_ss'_step_l : diff --git a/theories/Eq/Shallow.v b/theories/Eq/Shallow.v index 362dacc3..b47fd83d 100644 --- a/theories/Eq/Shallow.v +++ b/theories/Eq/Shallow.v @@ -26,6 +26,7 @@ From Stdlib Require Import JMeq. Set Implicit Arguments. +Set Universe Polymorphism. (* end hide *) Definition eqeq {A : Type} (P : A -> Type) {a1 a2 : A} (p : a1 = a2) : P a1 -> P a2 -> Prop := diff --git a/theories/Eq/Trace.v b/theories/Eq/Trace.v index d2e9342f..c29693c2 100644 --- a/theories/Eq/Trace.v +++ b/theories/Eq/Trace.v @@ -9,6 +9,8 @@ From CTree Require Import Eq.Trans Eq.SSim Eq.SBisim. +Set Universe Polymorphism. + (*| Base coinductive definitions for execution traces and trace equivalence. @@ -44,6 +46,14 @@ Definition traceq {E C D X Y} Instances |*) +#[global] Instance htr_equ {E C X} (R : trace -> ctree E C X -> Prop) s : + Proper (equ eq ==> impl) (@htr E C X R s). +Proof. + intros t u EQ H; destruct s; cbn in *; auto. + destruct H as (t' & TR & HR). + exists t'; split; [now rewrite <- EQ | exact HR]. +Qed. + #[global] Instance traceq_equ : forall {E C X} s, Proper (equ eq ==> impl) (@has_trace E C X s). Proof. diff --git a/theories/Eq/Trans.v b/theories/Eq/Trans.v index 910860e0..e3403a24 100644 --- a/theories/Eq/Trans.v +++ b/theories/Eq/Trans.v @@ -61,6 +61,7 @@ Open Scope ctree. Set Implicit Arguments. Set Primitive Projections. +Set Universe Polymorphism. #[local] Tactic Notation "step" := __step_equ. #[local] Tactic Notation "step" "in" ident(H) := __step_in_equ H. @@ -71,7 +72,10 @@ Set Primitive Projections. Section Trans. - Context {E B : Type -> Type} {R : Type}. + Universes e b v. + Context {E : Type@{e} -> Type}. + Context {B : Type@{b} -> Type}. + Context {R : Type}. Notation S' := (ctree' E B R). Notation S := (ctree E B R). @@ -88,11 +92,11 @@ least annoying solution. |*) Variant label : Type := | τ - | obs {X : Type} (e : E X) (v : X) - | val {X : Type} (v : X). + | obs {X : Type@{e} } (e : E X) (v : X) + | val {X : Type@{v} } (v : X). Variant is_val : label -> Prop := - | Is_val : forall X (x : X), is_val (val x). + | Is_val : forall (X : Type@{v}) (x : X), is_val (val x). Lemma is_val_τ : ~ is_val τ. Proof. @@ -115,7 +119,7 @@ node, labelling the transition by the returned value. |*) Inductive trans_ : label -> hrel S' S' := - | Transbr {X} (c : B X) x k l t : + | Transbr {X : Type@{b} } (c : B X) x k l t : trans_ l (observe (k x)) t -> trans_ l (BrF c k) t @@ -127,7 +131,7 @@ node, labelling the transition by the returned value. u ≅ t -> trans_ τ (StepF t) (observe u) - | Transobs {X} (e : E X) k x t : + | Transobs {X : Type@{e} } (e : E X) k x t : k x ≅ t -> trans_ (obs e x) (VisF e k) (observe t) @@ -296,21 +300,27 @@ Elimination rules for [trans] |*) Lemma trans_etrans l: trans l ≦ etrans l. Proof. - unfold etrans; case l; ka. + unfold etrans; destruct l; cbn; intros p q step; try exact step. + now left. Qed. Lemma etrans_wtrans l: etrans l ≦ wtrans l. Proof. - unfold wtrans; ka. + unfold wtrans. rewrite <- dot1x at 1; rewrite <- dotx1 at 1. + apply dot_leq; [apply dot_leq; [apply str_refl | reflexivity] | apply str_refl]. Qed. Lemma trans_wtrans l: trans l ≦ wtrans l. Proof. rewrite trans_etrans. apply etrans_wtrans. Qed. Lemma τtrans_wtrans : τtrans ≦ wtrans τ. Proof. - unfold τtrans, wtrans, etrans; ka. + unfold τtrans, wtrans, etrans. rewrite itr_str_l. + etransitivity; [apply str_cons |]. + rewrite <- dotx1 at 1; rewrite <- dotx1 at 1. + apply dot_leq; [apply dot_leq; [reflexivity | apply leq_xcup; right; reflexivity] | apply str_refl]. Qed. Lemma pwtrans_wtrans l : pwtrans l ≦ wtrans l. Proof. - unfold pwtrans, wtrans, etrans; case l; ka. + unfold pwtrans, wtrans. + apply dot_leq; [apply dot_leq; [reflexivity | apply trans_etrans] | reflexivity]. Qed. Lemma trans_etrans_ l: forall p p', trans l p p' -> etrans l p p'. @@ -332,35 +342,45 @@ Elimination rules for [trans] Lemma wcons l: forall p p' p'', trans τ p p' -> wtrans l p' p'' -> wtrans l p p''. Proof. assert ((trans τ: srel SS SS) ⋅ wtrans l ≦ wtrans l) as H - by (unfold wtrans; ka). + by (unfold wtrans; rewrite 2 dotA, str_cons; reflexivity). intros. apply H. eexists; eassumption. Qed. Lemma wsnoc l: forall p p' p'', wtrans l p p' -> trans τ p' p'' -> wtrans l p p''. Proof. assert (wtrans l ⋅ trans τ ≦ wtrans l) as H - by (unfold wtrans; ka). + by (unfold wtrans; rewrite <- dotA, str_snoc; reflexivity). intros. apply H. eexists; eassumption. Qed. + Lemma wtrans_τ: wtrans τ ≡ (trans τ)^*. + Proof. + unfold wtrans, etrans. + rewrite <- dotA, dotplsx, dot1x, + (proj1 (leq_iff_cup _ _) (str_cons (trans τ))), str_trans. + reflexivity. + Qed. Lemma wconss l: forall p p' p'', wtrans τ p p' -> wtrans l p' p'' -> wtrans l p p''. Proof. - assert (wtrans τ ⋅ wtrans l ≦ wtrans l) as H by (unfold wtrans, etrans; ka). + assert (wtrans τ ⋅ wtrans l ≦ wtrans l) as H. + { rewrite wtrans_τ. apply str_ind_l. + unfold wtrans; rewrite 2 dotA, str_cons; reflexivity. } intros. apply H. eexists; eassumption. Qed. Lemma wsnocs l: forall p p' p'', wtrans l p p' -> wtrans τ p' p'' -> wtrans l p p''. Proof. - assert (wtrans l ⋅ wtrans τ ≦ wtrans l) as H by (unfold wtrans, etrans; ka). + assert (wtrans l ⋅ wtrans τ ≦ wtrans l) as H. + { rewrite wtrans_τ. apply str_ind_r. + unfold wtrans; rewrite <- dotA, str_snoc; reflexivity. } intros. apply H. eexists; eassumption. Qed. - Lemma wtrans_τ: wtrans τ ≡ (trans τ)^*. - Proof. - unfold wtrans, etrans. ka. - Qed. Lemma pwtrans_τ: pwtrans τ ≡ (trans τ)^+. Proof. - unfold pwtrans, etrans. ka. + unfold pwtrans. + rewrite <- itr_str_r. + rewrite !itr_str_l, <- dotA, str_trans. + reflexivity. Qed. #[global] Instance PreOrder_wtrans_τ: PreOrder (wtrans τ). @@ -467,11 +487,14 @@ End backward. Section BackwardBounded. - Context {E B : Type -> Type} {X : Type}. + Context {E : Type -> Type}. + Context {B : Type -> Type}. + Context {X : Type}. Context `{B2 -< B}. Context `{B3 -< B}. Context `{B4 -< B}. - Variable (l : @label E) (t t' u u' v v' w w' : ctree E B X). + Variable (l : @label E). + Variable (t t' u u' v v' w w' : ctree E B X). Lemma trans_brS21 : trans τ (brS2 t u) t. @@ -847,8 +870,9 @@ Lemma etrans_ret_inv {E B X} : forall x l (t : ctree E B X), (l = τ /\ t ≅ Ret x) \/ (l = val x /\ t ≅ Stuck). Proof. intros ? [] ? step; cbn in step. - - intuition; try (eapply trans_ret in step; now apply step). - inv H. + - destruct step as [step | step]. + + apply trans_ret_inv in step as [_ abs]. inv abs. + + left; split; [reflexivity | now symmetry]. - eapply trans_ret_inv in step; intuition. - eapply trans_ret_inv in step; intuition. Qed. @@ -1018,7 +1042,7 @@ Section wtrans. rewrite EQ in step3; apply trans_τ_str_ret_inv in step3; auto. rewrite EQ in step3. apply transs_is_stuck_inv in step3; [| apply Stuck_is_stuck]. - intuition. + right; split; [reflexivity | now symmetry]. Qed. Lemma wtrans_val_inv' : forall (x : X) (t v : ctree E B X), @@ -1494,41 +1518,34 @@ Proof. eapply wtrans_bind_r'; eauto. Qed. -Lemma trans_trigger : forall {E B X Y} (e : E X) x (k : X -> ctree E B Y), - trans (obs e x) (trigger e >>= k) (k x). +Section TriggerTransitions. + Universes d q d' q'. + Context {E : Type -> Type} {B : Type -> Type}. + +Lemma trans_trigger {X Y} (e : E X) x (k : X -> @ctree@{_ _ _ _ d' q'} E B Y) : + trans (obs e x) ((CTree.trigger e : @ctree@{_ _ _ _ d q} E B X) >>= k) (k x). Proof. - intros. - unfold CTree.trigger. - rewrite unfold_bind; cbn. - setoid_rewrite bind_ret_l. - constructor; auto. + rewrite bind_trigger; apply trans_vis. Qed. -Lemma trans_trigger' : forall {E B X Y} (e : E X) x (t : ctree E B Y), - trans (obs e x) (trigger e;; t) t. +Lemma trans_trigger' {X Y} (e : E X) x (t : @ctree@{_ _ _ _ d' q'} E B Y) : + trans (obs e x) ((CTree.trigger e : @ctree@{_ _ _ _ d q} E B X);; t) t. Proof. - intros. - unfold CTree.trigger. - rewrite unfold_bind; cbn. - setoid_rewrite bind_ret_l. - constructor; auto. + rewrite bind_trigger; apply trans_vis. Qed. -Lemma trans_trigger_inv : forall {E B X Y} (e : E X) (k : X -> ctree E B Y) l u, - trans l (trigger e >>= k) u -> - exists x, u ≅ k x /\ l = obs e x. +Lemma trans_trigger_inv {X Y} (e : E X) (k : X -> @ctree@{_ _ _ _ d' q'} E B Y) + l (u : @ctree@{_ _ _ _ d' q'} E B Y) : + trans l ((CTree.trigger e : @ctree@{_ _ _ _ d q} E B X) >>= k) u -> + exists x, u ≅ k x /\ l = obs e x. Proof. - intros * TR. - unfold trigger in TR. - apply trans_bind_inv in TR. - destruct TR as [(? & ? & TR & ?) |(? & TR & ?)]. - - apply trans_vis_inv in TR. - destruct TR as (? & ? & ->); eexists; split; eauto. - rewrite H0, H1, bind_ret_l; reflexivity. - - apply trans_vis_inv in TR. - destruct TR as (? & ? & abs); inv abs. + intros TR. + rewrite bind_trigger in TR; apply trans_vis_inv in TR. + exact TR. Qed. +End TriggerTransitions. + Lemma trans_branch : forall {E B : Type -> Type} {X : Type} {Y : Type} [l : label] [t t' : ctree E B X] (c : B Y) (k : Y -> ctree E B X) (x : Y), diff --git a/theories/Eq/Visible.v b/theories/Eq/Visible.v index 0a4f5260..c654bc07 100644 --- a/theories/Eq/Visible.v +++ b/theories/Eq/Visible.v @@ -21,6 +21,7 @@ Open Scope ctree. Set Implicit Arguments. Set Primitive Projections. +Set Universe Polymorphism. #[local] Tactic Notation "step" "in" ident(H) := __step_in_equ H. diff --git a/theories/Eq/WBisim.v b/theories/Eq/WBisim.v index e423271d..6239f0f6 100644 --- a/theories/Eq/WBisim.v +++ b/theories/Eq/WBisim.v @@ -59,6 +59,7 @@ Import CTree. Import CTreeNotations. Import EquNotations. Import SBisimNotations. +Set Universe Polymorphism. (*| Weak Bisimulation @@ -377,24 +378,24 @@ on the setoid side. unfold wtrans, etrans. ka. Qed. - Lemma cnv_wt (R : Chain wb) : (elem R: hrel _ _)° ≡ elem R. + Lemma cnv_wt (R : Chain wb) : (elem R: hrel _ _)^° ≡ elem R. Proof. apply RelationAlgebra.lattice.antisym; intros ???; apply sym_t,H. Qed. - Lemma cnv_gfp: RelationAlgebra.lattice.weq ((gfp wb: hrel _ _)°) (gfp wb). + Lemma cnv_gfp: RelationAlgebra.lattice.weq ((gfp wb: hrel _ _)^°) (gfp wb). Proof. apply cnv_wt. Qed. - Lemma cnv_wbisim: wbisimT° ≡ wbisimT. + Lemma cnv_wbisim: wbisimT^° ≡ wbisimT. Proof. apply cnv_wt. Qed. - Lemma cnv_wbisim': wbisim° ≡ wbisim. + Lemma cnv_wbisim': wbisim^° ≡ wbisim. Proof. apply cnv_wt. Qed. (*| By symmetry, similar results for left-to-right game |*) - Lemma wbisim_trans_front l: (trans l)° ⋅ wbisimT ≦ wbisimT ⋅ (wtrans l)°. + Lemma wbisim_trans_front l: (trans l)^° ⋅ wbisimT ≦ wbisimT ⋅ (wtrans l)^°. Proof. cnv_switch. rewrite 2cnvdot, cnv_invol, cnv_wbisim. apply wbisim_trans_back. Qed. - Lemma wbisim_etrans_front l: (etrans l)° ⋅ wbisimT ≦ wbisimT ⋅ (wtrans l)°. + Lemma wbisim_etrans_front l: (etrans l)^° ⋅ wbisimT ≦ wbisimT ⋅ (wtrans l)^°. Proof. cnv_switch. rewrite 2cnvdot, cnv_invol, cnv_wbisim. apply wbisim_etrans_back. Qed. - Lemma wbisim_wtrans_front l: (wtrans l)° ⋅ wbisimT ≦ wbisimT ⋅ (wtrans l)°. + Lemma wbisim_wtrans_front l: (wtrans l)^° ⋅ wbisimT ≦ wbisimT ⋅ (wtrans l)^°. Proof. cnv_switch. rewrite 2cnvdot, cnv_invol, cnv_wbisim. apply wbisim_wtrans_back. Qed. (*| diff --git a/theories/Interp/Fold.v b/theories/Interp/Fold.v index d7c6cd0c..48ebfa6d 100644 --- a/theories/Interp/Fold.v +++ b/theories/Interp/Fold.v @@ -13,6 +13,7 @@ From CTree Require Import CTree Eq. Set Implicit Arguments. +Set Universe Polymorphism. Import CTreeNotations. Open Scope ctree_scope. @@ -26,7 +27,7 @@ Open Scope ctree_scope. - a local scheduler [B ~> M] describing valid branches and defines for it a monad morphism [ctree E B ~> M] for any monad [M] with a loop operator. *) -Definition fold {E B M : Type -> Type} +Definition fold {E : Type -> Type} {B : Type -> Type} {M : Type -> Type} {FM : Functor M} {MM : Monad M} {IM : MonadIter M} {Mstuck : MonadStuck M} {Mstep : MonadStep M} (h : E ~> M) @@ -54,7 +55,7 @@ Arguments fold {E B M FM MM IM Mstuck Mstep} h g [T]. and re-emit external events (internalized in [M] via [MonadTrigger] *) -Definition interp {E B M : Type -> Type} +Definition interp {E : Type -> Type} {B : Type -> Type} {M : Type -> Type} {FM : Functor M} {MM : Monad M} {IM : MonadIter M} {Mstuck : MonadStuck M} @@ -65,12 +66,11 @@ Definition interp {E B M : Type -> Type} Arguments interp {E B M FM MM IM _ _ _} h [T]. -Definition refine {E B M : Type -> Type} +Definition refine {E : Type -> Type} {B : Type -> Type} {M : Type -> Type} {FM : Functor M} {MM : Monad M} {IM : MonadIter M} {TM : MonadTrigger E M} {Mstuck : MonadStuck M} {Mstep : MonadStep M} - (g : B ~> M) - := + (g : B ~> M) : ctree E B ~> M := fold (fun _ e => mtrigger e) g. Arguments refine {E B M FM MM IM TM _ _} g [T]. @@ -122,7 +122,7 @@ Proof. apply CH. apply REL. Qed. -#[global] Instance refine_equ {E C D X} (h : C ~> ctree E D): +#[global] Instance refine_equ {E C D X} h: Proper (equ eq ==> @equ E D X X eq) (@refine E C _ _ _ _ _ _ _ h X). Proof. cbn. diff --git a/theories/Interp/FoldCTree.v b/theories/Interp/FoldCTree.v index 75151895..3b18138a 100644 --- a/theories/Interp/FoldCTree.v +++ b/theories/Interp/FoldCTree.v @@ -1,5 +1,4 @@ (* begin hide *) -Unset Universe Checking. From ExtLib Require Import Structures.Functor @@ -18,6 +17,8 @@ From CTree Require Import Misc.Pure Fold. +Set Universe Polymorphism. + Import CTreeNotations. Open Scope ctree_scope. @@ -34,12 +35,17 @@ Section FoldCTree. Section With_Params. (** Specialization to [M = ctree F (B01 +' D)] *) - Context {E F C D: Type -> Type} {X : Type} - {h : E ~> ctree F D} {g : C ~> ctree F D}. + Universes d q d' q'. + Context {E : Type -> Type} {F : Type -> Type} + {C : Type -> Type} {D : Type -> Type} {X : Type} + {h : E ~> @ctree@{_ _ _ _ d' q'} F D} + {g : C ~> @ctree@{_ _ _ _ d' q'} F D}. + (** ** [interpE] and constructors *) - Definition fold_ctree : forall [T], ctree E C T -> ctree F D T := - fold h g. + Definition fold_ctree : forall [T : Type], + @ctree@{_ _ _ _ d q} E C T -> + @ctree@{_ _ _ _ d' q'} F D T := fold h g. (* fold (mstuck (M := ctree F D)) (mstep (M := ctree F D)) h (mbr (M := ctree F D)) g. *) (* fold (fun T => Stuck: ctree F D T) (Step (Ret tt)) h g. *) @@ -55,7 +61,7 @@ Section FoldCTree. end)%function. (** Unfold lemma. *) - Lemma unfold_fold_ctree (t: ctree E C X): + Lemma unfold_fold_ctree (t : ctree E C X): fold_ctree t ≅ fold_ctree_ t. Proof. unfold fold_ctree, fold, Basics.iter, MonadIter_ctree, mbr, MonadBr_ctree, CTree.branch. @@ -73,7 +79,7 @@ Section FoldCTree. Qed. Lemma fold_ctree_ret (x: X): - fold_ctree (Ret x) ≅ Ret x. + fold_ctree (Ret x : ctree E C X) ≅ (Ret x : @ctree@{_ _ _ _ d' q'} F D X). Proof. now rewrite unfold_fold_ctree. Qed. Lemma fold_ctree_vis {U} (e: E U) (k: U -> ctree E C X) : @@ -81,7 +87,7 @@ Section FoldCTree. Proof. now rewrite unfold_fold_ctree. Qed. Lemma fold_ctree_stuck : - fold_ctree (Stuck : ctree E C X) ≅ Stuck. + fold_ctree (Stuck : ctree E C X) ≅ (Stuck : @ctree@{_ _ _ _ d' q'} F D X). Proof. now rewrite unfold_fold_ctree. Qed. Lemma fold_ctree_guard (t : ctree E C X) : @@ -92,7 +98,7 @@ Section FoldCTree. fold_ctree (Step t) ≅ Step (Guard (fold_ctree t)). Proof. now rewrite unfold_fold_ctree. Qed. - Lemma fold_ctree_br {U} (c : C U) (k: _ -> ctree E C X) : + Lemma fold_ctree_br {U} (c : C U) (k: U -> ctree E C X) : fold_ctree (Br c k) ≅ x <- g _ c;; Guard (fold_ctree (k x)). Proof. now rewrite unfold_fold_ctree. Qed. @@ -113,6 +119,7 @@ Section FoldCTree. intros ?; constructor; auto. Qed. + (** Unfolding of [interp]. *) Notation interp_ h t := @@ -126,7 +133,7 @@ Section FoldCTree. end)%function. (** Unfold lemma. *) - Lemma unfold_interp `{C -< D} (t: ctree E C X): + Lemma unfold_interp `{C -< D} (t : @ctree@{_ _ _ _ d q} E C X): interp h t ≅ interp_ h t. Proof. unfold interp,fold, Basics.iter, MonadIter_ctree, mbr, MonadBr_ctree, CTree.branch. @@ -143,7 +150,8 @@ Section FoldCTree. Qed. Lemma interp_ret `{C -< D} (x: X): - interp h (Ret x : ctree E C X) ≅ Ret x. + interp h (Ret x : @ctree@{_ _ _ _ d q} E C X) ≅ + (Ret x : @ctree@{_ _ _ _ d' q'} F D X). Proof. now rewrite unfold_interp. Qed. Lemma interp_stuck `{C -< D} : @@ -163,13 +171,14 @@ Section FoldCTree. Proof. now rewrite unfold_interp. Qed. Lemma interp_br `{C -< D} {U} (c : C U) (k: _ -> ctree E C X) : - interp h (Br c k) ≅ x <- branch c;; Guard (interp h (k x)). + interp h (Br c k) ≅ x <- mbr c;; Guard (interp h (k x)). Proof. now rewrite unfold_interp. Qed. Lemma interp_br' `{C -< D} {U} (c : C U) (k: _ -> ctree E C X) : - interp h (Br c k) ≅ br c (fun x => Guard (interp h (k x))). - Proof. rewrite interp_br; unfold branch; rewrite bind_br; setoid_rewrite bind_ret_l. - reflexivity. + interp h (Br c k) ≅ + br c (fun x => Guard (interp h (k x))). + Proof. rewrite interp_br. unfold mbr, MonadBr_ctree. + rewrite bind_branch; reflexivity. Qed. #[global] Instance interp_equ `{C -< D} {R} : @@ -179,7 +188,7 @@ Section FoldCTree. coinduction r CIH. intros * EQ; step in EQ. rewrite 2 unfold_interp. - inv EQ. + inv EQ; rewrite <- H1, <- H2. - constructor; auto. - constructor; auto. - constructor; auto. @@ -202,7 +211,7 @@ Section FoldCTree. end)%function. (** Unfold lemma. *) - Lemma unfold_refine `{E -< F} (t: ctree E C X): + Lemma unfold_refine `{E -< F} (t : @ctree@{_ _ _ _ d q} E C X): refine g t ≅ refine_ g t. Proof. unfold refine,fold, Basics.iter, MonadIter_ctree, mbr, MonadBr_ctree, CTree.branch. @@ -219,27 +228,28 @@ Section FoldCTree. Qed. Lemma refine_ret `{E -< F} (x: X): - refine g (Ret x : ctree E C X) ≅ Ret x. + refine g (Ret x : @ctree@{_ _ _ _ d q} E C X) ≅ Ret x. Proof. now rewrite unfold_refine. Qed. Lemma refine_vis `{E -< F} {U} (e: E U) (k: U -> ctree E C X) : - refine g (Vis e k) ≅ x <- trigger e;; Guard (refine g (k x)). + refine g (Vis e k) ≅ x <- mtrigger e;; Guard (refine g (k x)). Proof. now rewrite unfold_refine. Qed. Lemma refine_trigger `{E -< F} (e: E X) : - refine g (trigger e : ctree E C X) ~ (trigger e : ctree F D X). + refine g (trigger e : @ctree@{_ _ _ _ d q} E C X) ~ + (mtrigger e : @ctree@{_ _ _ _ d' q'} F D X). Proof. - rewrite unfold_refine; cbn. + rewrite Equ.unfold_trigger, unfold_refine; cbn. setoid_rewrite sb_guard. - setoid_rewrite refine_ret. + setoid_rewrite unfold_refine; cbn. now rewrite bind_ret_r. Qed. - Lemma refine_guard `{E -< F} (t: ctree E C X) : + Lemma refine_guard `{E -< F} (t : @ctree@{_ _ _ _ d q} E C X) : refine g (Guard t) ≅ Guard (refine g t). Proof. now rewrite unfold_refine. Qed. - Lemma refine_step `{E -< F} (t: ctree E C X) : + Lemma refine_step `{E -< F} (t : @ctree@{_ _ _ _ d q} E C X) : refine g (Step t) ≅ Step (Guard (refine g t)). Proof. now rewrite unfold_refine. Qed. @@ -254,7 +264,7 @@ Section FoldCTree. coinduction r CIH. intros * EQ; step in EQ. rewrite 2 unfold_refine. - inv EQ; try constructor; auto. + inv EQ; rewrite <- H1, <- H2; try constructor; auto. - step; constructor; auto. - upto_bind_eq. intros ?; constructor; auto. @@ -264,13 +274,35 @@ Section FoldCTree. End With_Params. + + Lemma interp_trigger@{d q d' q' +} + {E : Type -> Type} {F : Type -> Type} {C : Type -> Type} {D : Type -> Type} + {h : E ~> @ctree@{_ _ _ _ d' q'} F D} `{C -< D} {U : Type} (e : E U) : + interp h (CTree.trigger e : @ctree@{_ _ _ _ d q} E C U) ≅ + (x <- h _ e;; Guard (Ret x) : @ctree@{_ _ _ _ d' q'} F D U). + Proof. + rewrite Equ.unfold_trigger, interp_vis; + setoid_rewrite interp_ret; reflexivity. + Qed. + + + + + + Arguments fold_ctree {E F C D} h g [T]. Section FoldBind. - Context {E F C D: Type -> Type} {X : Type}. + Universes d0 q0 d q d' q'. + Context {E : Type -> Type} {F : Type -> Type} + {C : Type -> Type} {D : Type -> Type} {X : Type}. - Lemma fold_ctree_bind (h : E ~> ctree F D) (g : C ~> ctree F D) {S} (t : ctree E C X) (k : X -> ctree _ _ S) : + Lemma fold_ctree_bind + (h : E ~> @ctree@{_ _ _ _ d' q'} F D) + (g : C ~> @ctree@{_ _ _ _ d' q'} F D) {S : Type} + (t : @ctree@{_ _ _ _ d0 q0} E C X) + (k : X -> @ctree@{_ _ _ _ d q} E C S) : fold_ctree h g (t >>= k) ≅ fold_ctree h g t >>= (fun x => fold_ctree h g (k x)). Proof. revert t. @@ -295,14 +327,22 @@ Section FoldCTree. now constructor. Qed. - Lemma interp_bind (h : E ~> ctree F D) `{C -< D} {S} (t : ctree E C X) (k : X -> ctree _ _ S) : + Lemma interp_bind + (h : E ~> @ctree@{_ _ _ _ d' q'} F D) + `{C -< D} {S : Type} + (t : @ctree@{_ _ _ _ d0 q0} E C X) + (k : X -> @ctree@{_ _ _ _ d q} E C S) : interp h (t >>= k) ≅ interp h t >>= (fun x => interp h (k x)). Proof. unfold interp. now setoid_rewrite fold_ctree_bind. Qed. - Lemma refine_bind (g : C ~> ctree F D) `{E -< F} {S} (t : ctree E C X) (k : X -> ctree _ _ S) : + Lemma refine_bind + (g : C ~> @ctree@{_ _ _ _ d' q'} F D) + `{E -< F} {S : Type} + (t : @ctree@{_ _ _ _ d0 q0} E C X) + (k : X -> @ctree@{_ _ _ _ d q} E C S) : refine g (t >>= k) ≅ refine g t >>= (fun x => refine g (k x)). Proof. unfold refine. @@ -313,6 +353,7 @@ Section FoldCTree. End FoldCTree. + (*| Counter-example showing that interp does not preserve sbisim in the general case. |*) @@ -322,7 +363,6 @@ Module CounterExample. Inductive VoidE : Type -> Type := | voidE : VoidE void. - (* Notation B012 := (B01 +' B2). *) #[local] Definition t1 := Ret 1 : ctree VoidE B2 nat. #[local] Definition t2 := br2 (Ret 1) (x <- trigger voidE;; match x : void with end) : ctree VoidE B2 nat. @@ -331,22 +371,33 @@ Module CounterExample. unfold t1, t2. rewrite br2_commut. rewrite br2_is_stuck. reflexivity. - red. intros. intro. inv_trans. destruct x. + red. intros. intro. + rewrite bind_trigger in H. + apply trans_vis_inv in H as (x & _ & _). destruct x. Qed. - #[local] Definition h : VoidE ~> ctree VoidE B2. - Proof. - intros. destruct X. exact (Step Stuck). - Defined. + Section Handler. + Universes d q. + #[local] Definition h : forall T, VoidE T -> @ctree@{_ _ _ _ d q} VoidE B2 T := + fun _ e => match e with voidE => Step Stuck end. + + + #[local] Definition interp_h := + @interp VoidE B2 (@ctree@{_ _ _ _ d q} VoidE B2) + _ _ _ _ _ (@MonadBr_ctree VoidE B2 B2 _) h. + End Handler. + Arguments interp_h [T] _. - Example interpE_sbsisim_counterexample : ~ (interp h t1 ~ interp h t2). + Example interpE_sbsisim_counterexample : ~ (interp_h t1 ~ interp_h t2). Proof. red. intros. unfold t2 in H. playR in H. + unfold interp_h. rewrite unfold_interp. cbn. setoid_rewrite bind_br. eapply trans_br with (x := false). 2: { rewrite bind_ret_l. reflexivity. } apply trans_guard. setoid_rewrite unfold_interp. cbn. rewrite bind_step. etrans. + unfold interp_h in TR. rewrite unfold_interp in TR. unfold t1, h in TR. cbn in TR. inv_trans. Qed. @@ -354,8 +405,8 @@ End CounterExample. Section epsilon_interp_theory. - Lemma interp_productive {E C F X} (h : E ~> ctree F C) : forall (t : ctree E C X), - productive (interp h t) -> productive t. + Lemma interp_productive {E C F X} h : forall (t : ctree E C X), + productive (interp (M := ctree F C) h t) -> productive t. Proof. intros. inversion H; subst; @@ -367,9 +418,9 @@ Section epsilon_interp_theory. try now econstructor. Qed. - Lemma epsilon_interp : forall {E C F X} - (h : E ~> ctree F C) (t t' : ctree E C X), - epsilon t t' -> epsilon (interp h t) (interp h t'). + Lemma epsilon_interp : forall {E C F X} h (t t' : ctree E C X), + epsilon t t' -> + epsilon (interp (M := ctree F C) h t) (interp h t'). Proof. intros. red in H. setoid_rewrite (ctree_eta t). setoid_rewrite (ctree_eta t'). genobs t ot. genobs t' ot'. clear t Heqot t' Heqot'. @@ -384,9 +435,9 @@ Section epsilon_interp_theory. End epsilon_interp_theory. -Lemma interp_ret_inv {E F B X} (h : E ~> ctree F B) : +Lemma interp_ret_inv {E F B X} h : forall (t : ctree E B X) r, - interp h t ≅ Ret r -> t ≅ Ret r. + interp (M := ctree F B) h t ≅ Ret r -> t ≅ Ret r. Proof. intros. setoid_rewrite (ctree_eta t) in H. setoid_rewrite (ctree_eta t). destruct (observe t) eqn:?; try now inv_equ. @@ -400,11 +451,10 @@ Proof. intros. rewrite bind_bind. upto_bind_eq; intros ?. rewrite bind_guard. setoid_rewrite bind_ret_l. reflexivity. Qed. -Lemma trans_val_interp {E F B X} - (h : E ~> ctree F B) : +Lemma trans_val_interp {E F B X} h : forall (t u : ctree E B X) (v : X), trans (val v) t u -> - trans (val v) (interp h t) Stuck. + trans (val v) (interp (M := ctree F B) h t) Stuck. Proof. intros. apply trans_val_epsilon in H as []. subs. @@ -413,11 +463,10 @@ Proof. rewrite interp_ret. etrans. Qed. -Lemma trans_tau_interp {E F B X} - (h : E ~> ctree F B) : +Lemma trans_tau_interp {E F B X} h : forall (t u : ctree E B X), trans τ t u -> - trans τ (interp h t) (Guard (interp h u)). + trans τ (interp (M := ctree F B) h t) (Guard (interp h u)). Proof. intros. apply trans_τ_epsilon in H as (? & ? & ?). subs. @@ -427,14 +476,13 @@ Proof. etrans. Qed. -Lemma trans_obs_interp_step {E F B X Y} - (h : E ~> ctree F B) : +Lemma trans_obs_interp_step {E F B X Y} h : forall (t u : ctree E B X) u' (e : E Y) x l, trans (obs e x) t u -> trans l (h _ e) u' -> ~ is_val l -> epsilon_det u' (Ret x) -> - trans l (interp h t) (u';; Guard (interp h u)). + trans l (interp (M := ctree F B) h t) (u';; Guard (interp h u)). Proof. intros. apply trans_obs_epsilon in H as (? & ? & ?). @@ -447,12 +495,11 @@ Proof. apply trans_bind_l; auto. Qed. -Lemma trans_obs_interp_pure {E F B X Y} - (h : E ~> ctree F B) : +Lemma trans_obs_interp_pure {E F B X Y} h : forall (t u : ctree E B X) (e : E Y) x, trans (obs e x) t u -> trans (val x) (h _ e) Stuck -> - epsilon (interp h t) (Guard (interp h u)). + epsilon (interp (M := ctree F B) h t) (Guard (interp h u)). Proof. intros t u e x TR TRh. apply trans_obs_epsilon in TR as (k & EPS & ?). subs. diff --git a/theories/Interp/FoldStateT.v b/theories/Interp/FoldStateT.v index 18ce555d..d8706e9e 100644 --- a/theories/Interp/FoldStateT.v +++ b/theories/Interp/FoldStateT.v @@ -1,4 +1,3 @@ -Unset Universe Checking. From Stdlib Require Import Classes.RelationPairs. @@ -23,13 +22,15 @@ From CTree Require Import Misc.Pure. Import SBisimNotations. -Import MonadNotation. -Open Scope monad_scope. Set Implicit Arguments. +Set Universe Polymorphism. (* TODO MOVE *) Arguments fequ : simpl never. +Section StateMonadOperations. +Import MonadNotation. +Open Scope monad_scope. #[global] Instance MonadBr_stateT {S M C} {MM : Monad M} {AM : MonadBr C M}: MonadBr C (stateT S M) := @@ -62,8 +63,11 @@ Definition refine_state {E C M} S ctree E C ~> stateT S M := refine g. #[global] Typeclasses Opaque fold_state interp_state refine_state. +End StateMonadOperations. Section State. + Import CTreeNotations. + Universes d q d' q'. Variable (S : Type). Variant stateE : Type -> Type := | Get : stateE S @@ -72,25 +76,30 @@ Section State. Definition get {E C} `{stateE -< E} : ctree E C S := trigger Get. Definition put {E C} `{stateE -< E} : S -> ctree E C unit := fun s => trigger (Put s). - Definition h_state {E C} : stateE ~> stateT S (ctree E C) := + Definition h_state {E C} : stateE ~> stateT S (@ctree@{_ _ _ _ d' q'} E C) := fun _ e s => match e with | Get => Ret (s, s) | Put s' => Ret (s', tt) end. - Definition pure_state {E C} : E ~> stateT S (ctree E C) - := fun _ e s => Vis e (fun x => Ret (s, x)). + Definition pure_state {E C} : E ~> stateT S (@ctree@{_ _ _ _ d' q'} E C) := + fun _ e s => (x <- CTree.trigger e;; Ret (s, x))%ctree. - Definition pure_state_choice {E C} : C ~> stateT S (ctree E C) - := fun _ c s => br c (fun x => Ret (s, x)). + Definition pure_state_choice {E C} : C ~> stateT S (@ctree@{_ _ _ _ d' q'} E C) := + fun _ c s => (x <- CTree.branch c;; Ret (s, x))%ctree. - Definition run_state {E C} - : ctree (stateE +' E) C ~> stateT S (ctree E C) := - fold_state (case_ h_state pure_state) pure_state_choice. + Definition run_state {E C} : + forall T : Type, + @ctree@{_ _ _ _ d q} (stateE +' E) C T -> + stateT S (@ctree@{_ _ _ _ d' q'} E C) T := + fold_state (case_sum1 h_state pure_state) pure_state_choice. End State. +Import MonadNotation. +Open Scope monad_scope. + Ltac break := match goal with | v: _ * _ |- _ => destruct v @@ -101,11 +110,13 @@ Ltac break := [itree E ~> stateT S (itree F)]. *) Section State. + Universes d q d' q'. + Variable (S : Type). - Context {E F C D : Type -> Type} - {R : Type} - (h : E ~> stateT S (ctree F D)) - (g : C ~> stateT S (ctree F D)). + Context {E : Type -> Type} {F : Type -> Type} + {C : Type -> Type} {D : Type -> Type} {R : Type} + (h : E ~> stateT S (@ctree@{_ _ _ _ d' q'} F D)) + (g : C ~> stateT S (@ctree@{_ _ _ _ d' q'} F D)). (** Unfolding of [fold]. *) Notation fold_state_ h g t s := @@ -118,7 +129,7 @@ Section State. | BrF c k => bind (g _ c s) (fun xs => Guard (fold_state h g (k (snd xs)) (fst xs))) end)%function. - Lemma unfold_fold_state (t : ctree E C R) (s : S) : + Lemma unfold_fold_state (t : @ctree@{_ _ _ _ d q} E C R) (s : S) : fold_state h g t s ≅ fold_state_ h g t s. Proof. unfold fold_state, fold, MonadIter_stateT0, iter, MonadIter_ctree, Basics.iter. @@ -144,7 +155,7 @@ Section State. #[global] Instance equ_fold_state: Proper (equ eq ==> eq ==> equ eq) - (fold_state h g (T := R)). + (fold_state h g (T := R) : @ctree@{_ _ _ _ d q} E C R -> _). Proof. unfold Proper, respectful. coinduction r IH; intros * EQ1 * <-. @@ -160,7 +171,8 @@ Section State. Lemma fold_state_ret (s : S) (r : R) : - (fold_state h g (Ret r) s) ≅ (Ret (s, r)). + fold_state h g (Ret r : @ctree@{_ _ _ _ d q} E C R) s ≅ + (Ret (s, r) : @ctree@{_ _ _ _ d' q'} F D (S * R)). Proof. rewrite ctree_eta. reflexivity. Qed. @@ -171,52 +183,53 @@ Section State. now rewrite ctree_eta. Qed. - Lemma fold_state_guard (t : ctree E C R) (s : S) : + Lemma fold_state_guard (t : @ctree@{_ _ _ _ d q} E C R) (s : S) : fold_state h g (Guard t) s ≅ Guard (fold_state h g t s). Proof. now rewrite unfold_fold_state; cbn. Qed. - Lemma fold_state_step (t : ctree E C R) (s : S) : + Lemma fold_state_step (t : @ctree@{_ _ _ _ d q} E C R) (s : S) : fold_state h g (Step t) s ≅ Step (Guard (fold_state h g t s)). Proof. now rewrite unfold_fold_state; cbn. Qed. Lemma fold_state_vis {T : Type} - (e : E T) (k : T -> ctree E C R) (s : S) : - fold_state h g (Vis e k) s ≅ h e s >>= fun sx => Guard (fold_state h g (k (snd sx)) (fst sx)). + (e : E T) (k : T -> @ctree@{_ _ _ _ d q} E C R) (s : S) : + fold_state h g (Vis e k) s ≅ + h e s >>= fun sx => Guard (fold_state h g (k (snd sx)) (fst sx)). Proof. rewrite unfold_fold_state; reflexivity. Qed. Lemma fold_state_br {T: Type} `{C -< D} - (c : C T) (k : T -> ctree E C R) (s : S) : - fold_state h g (br c k) s ≅ g c s >>= fun sx => Guard (fold_state h g (k (snd sx)) (fst sx)). + (c : C T) (k : T -> @ctree@{_ _ _ _ d q} E C R) (s : S) : + fold_state h g (br c k) s ≅ + g c s >>= fun sx => Guard (fold_state h g (k (snd sx)) (fst sx)). Proof. rewrite !unfold_fold_state; reflexivity. Qed. Lemma fold_state_trigger (e : E R) (s : S) : - fold_state h g (CTree.trigger e) s ≅ - h e s >>= fun x => Guard (Ret x). + fold_state h g (CTree.trigger e : @ctree@{_ _ _ _ d q} E C R) s ≅ + ((h e s >>= fun x => Guard (Ret x)) : @ctree@{_ _ _ _ d' q'} F D (S * R)). Proof. - unfold CTree.trigger. - rewrite fold_state_vis; cbn. + rewrite Equ.unfold_trigger, fold_state_vis; cbn. upto_bind_eq; intros []. rewrite fold_state_ret; auto. Qed. Lemma fold_state_trigger_sb (e : E R) (s : S) - : fold_state h g (CTree.trigger e) s ~ h e s. + : fold_state h g (CTree.trigger e : @ctree@{_ _ _ _ d q} E C R) s ~ h e s. Proof. - unfold CTree.trigger. rewrite fold_state_vis. + rewrite fold_state_trigger. rewrite <- (bind_ret_r (h e s)) at 2. - cbn. upto_bind_eq; intros []. - now rewrite sb_guard, fold_state_ret. + now rewrite sb_guard. Qed. + (** Unfolding of [interp]. *) Notation interp_state_ h t s := (match observe t with @@ -228,7 +241,8 @@ Section State. | 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- eq ==> equ (eq * Q)) - (interp_state (C := C) h (T := R)). + (interp_state (C := C) h (T := R) : @ctree@{_ _ _ _ d q} E C R -> _). Proof. unfold Proper, respectful. coinduction r IH; intros * EQ1 * <-. @@ -272,7 +286,7 @@ Section State. #[global] Instance equ_eq_interp_state `{C- eq ==> equ eq) - (interp_state (C := C) h (T := R)). + (interp_state (C := C) h (T := R) : @ctree@{_ _ _ _ d q} E C R -> _). Proof. cbn. intros. subst. eapply (equ_leq (eq * eq)%signature). @@ -282,19 +296,21 @@ Section State. Lemma interp_state_ret `{C- ctree E C R) (s : S) : - interp_state h (Vis e k) s ≅ h e s >>= fun sx => Guard (interp_state h (k (snd sx)) (fst sx)). + (e : E T) (k : T -> @ctree@{_ _ _ _ d q} E C R) (s : S) : + interp_state h (Vis e k) s ≅ + h e s >>= fun sx => Guard (interp_state h (k (snd sx)) (fst sx)). Proof. rewrite unfold_interp_state; reflexivity. Qed. Lemma interp_state_br {T: Type} `{C -< D} - (c : C T) (k : T -> ctree E C R) (s : S) : - interp_state h (Br c k) s ≅ branch c >>= fun x => Guard (interp_state h (k x) s). + (c : C T) (k : T -> @ctree@{_ _ _ _ d q} E C R) (s : S) : + interp_state h (Br c k) s ≅ + mbr c >>= fun x => Guard (interp_state h (k x) s). Proof. rewrite !unfold_interp_state; cbn. rewrite bind_bind. @@ -327,10 +345,11 @@ Section State. Qed. Lemma interp_state_trigger `{C -< D} : forall (e : E R) st, - interp_state h (CTree.trigger e : ctree E C R) st ≅ x <- h e st;; Guard (Ret x). + interp_state h (CTree.trigger e : @ctree@{_ _ _ _ d q} E C R) st ≅ + ((x <- h e st;; Guard (Ret x)) : @ctree@{_ _ _ _ d' q'} F D (S * R)). Proof. - intros. rewrite unfold_interp_state. cbn. - upto_bind. reflexivity. intros [] [] <-. + intros. rewrite Equ.unfold_trigger, interp_state_vis; cbn. + upto_bind_eq; intros []. now rewrite interp_state_ret. Qed. @@ -423,7 +442,7 @@ Section State. Lemma refine_state_vis `{E- ctree E C R) (s : S) : refine_state g (Vis e k) s ≅ - trigger e >>= fun x => Guard (refine_state g (k x) s). + mtrigger e >>= fun x => Guard (refine_state g (k x) s). Proof. rewrite unfold_refine_state; reflexivity. Qed. @@ -454,7 +473,8 @@ Qed. Section FoldBind. Variable (S : Type). - Context {E F C D : Type -> Type}. + Context {E : Type -> Type} {F : Type -> Type} + {C : Type -> Type} {D : Type -> Type}. Lemma fold_state_bind (h : E ~> stateT S (ctree F D)) @@ -516,7 +536,8 @@ End FoldBind. Section InterpState. -Context {E F B C : Type -> Type} {X St : Type} `{HasB: B -< C} +Context {E : Type -> Type} {F : Type -> Type} + {B : Type -> Type} {C : Type -> Type} {X : Type} {St : Type} `{HasB: B -< C} (h : E ~> stateT St (ctree F C)). Lemma epsilon_interp_state : forall (t t' : ctree E B X) s, @@ -596,18 +617,27 @@ Proof. + red. reflexivity. + eapply weq_ssim. apply update_val_rel_update_val_rel. now apply Hh. + cbn. intros [] [] [? <-]. apply ssim_ret. constructor; cbn; auto. - - rewrite !bind_map, !bind_bind. setoid_rewrite bind_branch. - cbn. - apply ssim_br_id; intros ?; rewrite ?bind_ret_l. + - rewrite !bind_map, !bind_bind. + unfold mbr, MonadBr_stateT, MonadBr_ctree. + cbn -[CTree.branch CTree.bind]. + rewrite !bind_branch. + apply ssim_br_id; intros ?; rewrite !bind_ret_l; cbn. apply ssim_ret; constructor; cbn; auto. Qed. -Definition lift_handler {E F B} (h : E ~> ctree F B) : E ~> Monads.stateT unit (ctree F B) := - fun _ e s => CTree.map (fun x => (tt, x)) (h _ e). +Section LiftHandler. +Universes d q. +Context {E : Type -> Type} {F : Type -> Type} {C : Type -> Type}. +Variable h : E ~> @ctree@{_ _ _ _ d q} F C. + +Definition lift_handler : + forall T, E T -> Monads.stateT unit (@ctree@{_ _ _ _ d q} F C) T := + fun _ e s => CTree.map (fun x => (tt, x)) (h e). -Lemma is_simple_lift_handler {E F B} (h : E ~> ctree F B) : - (forall Y (e : E Y), is_simple (h _ e)) -> - forall Y (e : E Y) st, is_simple (lift_handler h _ e st). + +Lemma is_simple_lift_handler : + (forall Y (e : E Y), is_simple (h e)) -> + forall Y (e : E Y) st, is_simple (lift_handler e st). Proof. intros. specialize (H Y e). red. destruct H; [left | right]; intros. @@ -626,9 +656,9 @@ Qed. (* Results on interp_state can be transported to interp using interp_lift_handler. *) -Lemma interp_lift_handler {E F B C X} `{HasB: B -< C} - (h : E ~> ctree F C) (t : ctree E B X) : - interp h t ≅ CTree.map (fun '(st, x) => x) (interp_state (lift_handler h) t tt). +Lemma interp_lift_handler {B : Type -> Type} {X} `{HasB: B -< C} + (t : ctree E B X) : + interp h t ≅ CTree.map (fun '(st, x) => x) (interp_state lift_handler t tt). Proof. revert t. coinduction R CH. intros. pose proof @map_equ. @@ -647,21 +677,25 @@ Proof. rewrite map_guard. constructor. apply CH. - rewrite interp_br, interp_state_br. - cbn. rewrite bind_branch, map_bind, bind_branch. + cbn. unfold mbr, MonadBr_ctree. + rewrite bind_branch, map_bind, bind_branch. constructor. intros. rewrite map_guard. step. constructor. apply CH. Qed. +End LiftHandler. + Theorem ssim_interp_h {E F1 F2 C D1 D2 X} `{HC1 : C -< D1} `{HC2 : C -< D2} (Ldest : rel (@label F1) (@label F2)) : - forall (h : E ~> ctree F1 D1) (h' : E ~> ctree F2 D2), + forall h h', (Ldest τ τ /\ forall (x : X), Ldest (val x) (val x)) -> (forall {Z} (e : E Z), h _ e (≲update_val_rel Ldest (@eq Z)) h' _ e) -> forall (t : ctree E C X), - interp h t (≲Ldest) interp h' t. + @interp E C (ctree F1 D1) _ _ _ _ _ _ h X t (≲Ldest) + @interp E C (ctree F2 D2) _ _ _ _ _ _ h' X t. Proof. intros. rewrite !interp_lift_handler. @@ -857,12 +891,15 @@ Proof. eauto. * constructor; auto. - (* Br *) - unfold MonadBr_stateT, mbr, MonadBr_ctree. cbn. rewrite bind_bind, bind_branch. + unfold MonadBr_stateT, mbr, MonadBr_ctree. + cbn -[CTree.branch CTree.bind]. rewrite bind_bind, bind_branch. + setoid_rewrite bind_ret_l. unshelve eapply step_ss'_br_l. apply equ_clos_sst'_ctx. intros. eapply ssim_br_l_inv in SIM. - step. rewrite bind_ret_l. apply step_ss'_guard_l. + fold (interp_state h u st). + step. apply step_ss'_guard_l. apply CH. apply SIM. Qed. @@ -882,16 +919,20 @@ Qed. (* The proof that interp preserves ssim reuses the interp_state proof. *) -#[global] Instance interp_ssim_eq {E F B C X} `{HasB: B -< C} : - forall (h : E ~> ctree F C) (Hh : forall X e, is_simple (h X e)), - Proper (ssim eq ==> ssim eq) (interp (B := B) h (T := X)). -Proof. - intros. cbn. intros. - rewrite !interp_lift_handler. - unfold CTree.map. apply ssim_clo_bind_eq. - refine (interp_state_ssim_eq _ _ _ _); auto. - reflexivity. -Qed. +#[global] Instance interp_ssim_eq@{d q d' q' +} + {E : Type -> Type} {F : Type -> Type} {B C : Type -> Type} {X : Type} `{HasB: B -< C} + (h : E ~> @ctree@{_ _ _ _ d' q'} F C) + (Hh : forall X (e : E X), is_simple (h _ e)) : + Proper (ssim eq ==> ssim eq) + (interp (B := B) (M := @ctree@{_ _ _ _ d' q'} F C) h (T := X) : + @ctree@{_ _ _ _ d q} E B X -> _). + Proof. + cbn. intros. + rewrite !interp_lift_handler. + unfold CTree.map. apply ssim_clo_bind_eq. + refine (interp_state_ssim_eq _ _ _ _); auto. + reflexivity. + Qed. (* Direct proof that interp_state preserves sbisim. *) @@ -979,11 +1020,12 @@ Proof. apply step_sb'_guard. apply CH. symmetry in SIM. step in SIM. apply SIM. * right; auto. - (* Br *) - unfold MonadBr_stateT, mbr, MonadBr_ctree. cbn -[RelProd]. rewrite bind_bind, bind_branch. + unfold MonadBr_stateT, mbr, MonadBr_ctree. + cbn -[RelProd CTree.branch CTree.bind]. rewrite bind_bind, bind_branch. apply step_sb'_true_br_l. intros. eapply ss_br_l_inv in SIM. - step. rewrite bind_ret_l. + step. rewrite !bind_ret_l. apply step_sb'_true_guard_l. cbn. apply CH. apply SIM. Unshelve. @@ -1026,16 +1068,20 @@ Qed. (* The proof that interp preserves sbisim reuses the interp_state proof. *) -#[global] Instance interp_sbisim_eq {E F B C X} `{HasB: B -< C} : - forall (h : E ~> ctree F C) (Hh : forall X e, is_simple (h X e)), - Proper (sbisim eq ==> sbisim eq) (interp (B := B) h (T := X)). -Proof. - intros. cbn. intros. - rewrite !interp_lift_handler. - unfold CTree.map. apply sbisim_clo_bind_eq. - refine (interp_state_sbisim_eq _ _ _ _); auto. - reflexivity. -Qed. +#[global] Instance interp_sbisim_eq@{d q d' q' +} + {E : Type -> Type} {F : Type -> Type} {B C : Type -> Type} {X : Type} `{HasB: B -< C} + (h : E ~> @ctree@{_ _ _ _ d' q'} F C) + (Hh : forall X (e : E X), is_simple (h _ e)) : + Proper (sbisim eq ==> sbisim eq) + (interp (B := B) (M := @ctree@{_ _ _ _ d' q'} F C) h (T := X) : + @ctree@{_ _ _ _ d q} E B X -> _). + Proof. + cbn. intros. + rewrite !interp_lift_handler. + unfold CTree.map. apply sbisim_clo_bind_eq. + refine (interp_state_sbisim_eq _ _ _ _); auto. + reflexivity. + Qed. Arguments get {S E C _}. Arguments put {S E C _}. diff --git a/theories/Interp/ITree.v b/theories/Interp/ITree.v index 985d08d3..98c84d64 100644 --- a/theories/Interp/ITree.v +++ b/theories/Interp/ITree.v @@ -1,16 +1,12 @@ -Unset Universe Checking. From Paco Require Import paco. From CTree Require Import CTree Eq Interp.Internalize Interp.FoldCTree. -(* Universe issue, TO FIX *) -Unset Universe Checking. -Unset Auto Template Polymorphism. From ITree Require Import - ITree Eq Interp InterpFacts. + ITree Eq Interp. From Stdlib Require Import Morphisms Program. @@ -18,13 +14,20 @@ Open Scope ctree. Set Implicit Arguments. Set Contextual Implicit. +Set Universe Polymorphism. -Definition h_embed {E C} : E ~> ctree E C := +Definition h_embed@{d q +} {E C} : E ~> @ctree@{_ _ _ _ d q} E C := fun _ e => CTree.trigger e. -Definition embed' {E} : itree E ~> ctree E (B01) := interp h_embed. -Definition embed {E C} : itree (C +' E) ~> ctree E (B01 +' C) := + +Definition embed'@{d q +} {E} : itree E ~> @ctree@{_ _ _ _ d q} E B01 := + interp h_embed. + +Definition embed@{d q +} {E C} : itree (C +' E) ~> @ctree@{_ _ _ _ d q} E (B01 +' C) := fun _ t => internalize (embed' t). +Arguments embed' {E} [T] _. +Arguments embed {E C} [T] _. + Notation "t '-' l '→' u" := (trans l t u) (at level 50, only printing, format "t '-' l '→' u"). @@ -45,16 +48,21 @@ Notation "t '-' l '→' u" := (transR l t u) #[local] Notation cVis e k := (CTreeDefinitions.Vis e k). (** Unfolding of [interp]. *) -Definition _interp {E F C R} (f : E ~> ctree F C) (ot : itreeF E R _) - : ctree F C R := +Section ITreeInterp. + Universes d q. +Definition _interp {E F C R} + (f : E ~> @ctree@{_ _ _ _ d q} F C) + (ot : itreeF E R _) : @ctree@{_ _ _ _ d q} F C R := match ot with | RetF r => CTreeDefinitions.Ret r | TauF t => cGuard (interp f t) | VisF e k => CTree.bind (f _ e) (fun x => cGuard (interp f (k x))) end. -Lemma unfold_interp_ctree {E F C X} (h: E ~> ctree F C) (t : itree E X): - (interp h t ≅ _interp h (iobserve t))%ctree. +Lemma unfold_interp_ctree {E F C X} + (f : E ~> @ctree@{_ _ _ _ d q} F C) + (t : itree E X) : + (interp f t ≅ _interp f (iobserve t))%ctree. Proof. revert t. coinduction R CIH. @@ -64,8 +72,7 @@ Proof. destruct (iobserve t) eqn:ot; try now cbn; auto. match goal with |- equb _ _ (_cobserve ?t) (_cobserve ?u) => - fold (cobserve t); - fold (cobserve u) + fold (cobserve t); fold (cobserve u) end. Transparent CTree.bind. cbn. @@ -74,25 +81,25 @@ Proof. intros ?. now constructor. Qed. +End ITreeInterp. #[global] Instance embed_eq {E C X}: Proper (eq_itree eq ==> equ eq) (@embed E C X). Proof. - unfold Proper, respectful. - coinduction r CIH. - intros t u bisim. unfold embed, embed', internalize. + unfold Proper, respectful. + coinduction r CIH. + intros t u bisim. unfold embed, embed', internalize. rewrite 2 unfold_interp_ctree. - rewrite 2 FoldCTree.unfold_interp. - punfold bisim. - inv bisim; pclearbot; try easy. - - cbn. + punfold bisim. + inv bisim; pclearbot; try discriminate; cbn [_interp h_embed]. + - reflexivity. + - rewrite 2 FoldCTree.interp_guard. constructor. now apply CIH. - - cbn. + - rewrite 2 FoldCTree.interp_bind. apply fequ_bind_chain_eq; intros. - rewrite 2 FoldCTree.unfold_interp. - cbn; constructor. - step; cbn; constructor. + setoid_rewrite FoldCTree.interp_guard. + constructor. apply CIH, REL. Qed. @@ -130,29 +137,18 @@ Notation embed_ t := Lemma unfold_embed {E C X} (t : itree (C +' E) X) : (embed t ≅ embed_ t)%ctree. Proof. unfold embed, embed', internalize at 1. - rewrite unfold_interp_ctree, FoldCTree.unfold_interp. - cbn. - destruct (iobserve t) eqn:EQ; cbn; auto. - - destruct e. - + cbn. - rewrite Equ.unfold_bind at 1. - cbn. - step; cbn; constructor; intros ?. - rewrite Equ.bind_step. - step; cbn; constructor. - rewrite Equ.bind_ret_l. - step; cbn; constructor. - step; cbn; constructor. - reflexivity. - + cbn. - rewrite Equ.unfold_bind at 1. - cbn. - step; cbn; constructor; intros ?. - rewrite Equ.bind_ret_l. - step; cbn; constructor. - rewrite FoldCTree.unfold_interp; cbn. - step; cbn; constructor. - reflexivity. + rewrite unfold_interp_ctree. + destruct (iobserve t) eqn:EQ; cbn [_interp h_embed]. + - rewrite FoldCTree.interp_ret; reflexivity. + - rewrite FoldCTree.interp_guard; reflexivity. + - rewrite FoldCTree.interp_bind, FoldCTree.interp_trigger, Equ.bind_bind. + setoid_rewrite Equ.bind_guard. + setoid_rewrite Equ.bind_ret_l. + setoid_rewrite FoldCTree.interp_guard. + destruct e; unfold internalize_h', internalize_h; + cbn -[CTree.trigger CTree.branchS CTree.bind]. + + rewrite Equ.bind_branchS; reflexivity. + + rewrite Equ.bind_trigger; reflexivity. Qed. (* TODO THIS IS REDUNDANT WITH THE DEF IN FOLDCTREE! *) diff --git a/theories/Interp/Internalize.v b/theories/Interp/Internalize.v index ce603ab5..5e208d58 100644 --- a/theories/Interp/Internalize.v +++ b/theories/Interp/Internalize.v @@ -1,32 +1,35 @@ -Unset Universe Checking. From CTree Require Import CTree Eq Interp.Fold Interp.FoldCTree. Set Implicit Arguments. Set Contextual Implicit. +Set Universe Polymorphism. Import CTreeNotations. Section Internalize. - Variable E C : Type -> Type. + Universes d q d' q'. + Variable E : Type -> Type. + Variable C : Type -> Type. Variable ExtChoice : Type -> Type. - Definition internalize_h : ExtChoice ~> ctree E (C +' ExtChoice) := + Definition internalize_h : ExtChoice ~> @ctree@{_ _ _ _ d' q'} E (C +' ExtChoice) := fun _ e => CTree.branchS (subevent _ e). - Definition internalize_h' : ExtChoice +' E ~> ctree E (C +' ExtChoice) := + Definition internalize_h' : ExtChoice +' E ~> @ctree@{_ _ _ _ d' q'} E (C +' ExtChoice) := fun _ e => match e with | inl1 e => internalize_h e | inr1 e => trigger e end. - Definition internalize : ctree (ExtChoice +' E) C ~> ctree E (C +' ExtChoice) := + Definition internalize : @ctree@{_ _ _ _ d q} (ExtChoice +' E) C ~> + @ctree@{_ _ _ _ d' q'} E (C +' ExtChoice) := interp internalize_h'. Lemma internalize_ret {R} (r : R) : internalize (Ret r) ≅ Ret r. Proof. unfold internalize. - rewrite interp_ret. + rewrite FoldCTree.interp_ret. reflexivity. Qed. @@ -34,7 +37,7 @@ Section Internalize. internalize (t >>= k) ≅ internalize t >>= (fun x => internalize (k x)). Proof. unfold internalize. - rewrite interp_bind. + rewrite FoldCTree.interp_bind. reflexivity. Qed. diff --git a/theories/Interp/Recursion.v b/theories/Interp/Recursion.v index d7a18709..ca2c3061 100644 --- a/theories/Interp/Recursion.v +++ b/theories/Interp/Recursion.v @@ -17,6 +17,8 @@ From CTree Require Import Misc.Pure Fold. +Set Universe Polymorphism. + Import CTreeNotations. Open Scope ctree_scope. @@ -77,10 +79,11 @@ Open Scope ctree_scope. (** 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 => +Definition interp_mrec@{d q d' q' +} {D E B} + (ctx : D ~> @ctree@{_ _ _ _ d q} (D +' E) B) : + @ctree@{_ _ _ _ d q} (D +' E) B ~> @ctree@{_ _ _ _ d' q'} E B := + fun T => + CTree.iter (fun t => match observe t with | RetF r => Ret (inr r) | StuckF => Stuck @@ -90,20 +93,24 @@ Definition interp_mrec {D E B : Type -> Type} | 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). + +Definition mrec@{d q d' q' +} {D E B} + (ctx : D ~> @ctree@{_ _ _ _ d q} (D +' E) B) : + D ~> @ctree@{_ _ _ _ d' q'} E B := + fun T d => interp_mrec ctx (ctx T 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). +Definition trigger_inl1@{d q +} {D E B} : + D ~> @ctree@{_ _ _ _ d q} (D +' E) B := + fun _ d => CTree.trigger (inl1 d). Arguments trigger_inl1 {D E B} [T]. @@ -125,7 +132,7 @@ Arguments trigger_inl1 {D E B} [T]. (** *** Simple recursion *) -Inductive callE (A B : Type) : Type -> Type := +Inductive callE (A : Type) (B : Type) : Type -> Type := | Call : A -> callE A B B. Arguments Call {A B}. @@ -137,35 +144,31 @@ Definition unCall {A B T} (e : callE A B T) : 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 := +Definition calling@{i +} {A B} {F : Type -> Type} + (f : A -> F B) : forall T : Type@{i}, callE A B T -> F T := 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. +(** Compatibility-specialized form of [calling]. *) +Definition calling'@{i d q +} {X Y F B} + (f : X -> @ctree@{_ _ _ _ d q} F B Y) : + forall T : Type@{i}, callE X Y T -> @ctree@{_ _ _ _ d q} F B T := + calling f. (* 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). +Definition rec@{d q +} {E B X Y} + (body : X -> ctree (callE X Y +' E) B Y) : X -> @ctree@{_ _ _ _ d q} 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 := +Definition call@{d q +} {E B X Y} (x:X) : + @ctree@{_ _ _ _ d q} (callE X Y +' E) B Y := CTree.trigger (inl1 (Call x)). (* (** Here's some syntactic sugar with a notation [mrec-fix]. *) *) diff --git a/theories/Interp/RecursionFacts.v b/theories/Interp/RecursionFacts.v index 203afbbf..04c93e3f 100644 --- a/theories/Interp/RecursionFacts.v +++ b/theories/Interp/RecursionFacts.v @@ -9,7 +9,6 @@ From ExtLib Require Import Structures.Functor Structures.Monad. -Unset Universe Checking. From CTree Require Import CTreeDefinitions Eq @@ -42,13 +41,16 @@ From ITree Require Import Import CoindNotations. -Section Facts. +Set Universe Polymorphism. -Context {D E B : Type -> Type} (ctx : D ~> ctree (D +' E) B). +Section Facts. +Universes d q d' q' d0 q0. +Context {D E B} (ctx : D ~> @ctree@{_ _ _ _ d q} (D +' E) B). (** Unfolding of [interp_mrec]. *) -Definition _interp_mrec {R : Type} (ot : ctreeF (D +' E) B R _) : ctree E B R := +Definition _interp_mrec@{d' q' +} {R : Type} (ot : ctreeF (D +' E) B R _) : + @ctree@{_ _ _ _ d' q'} E B R := match ot with | RetF r => Ret r | StuckF => Stuck @@ -88,9 +90,11 @@ 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. +Definition mrecursive@{d' q' +} (f : D ~> @ctree@{_ _ _ _ d q} (D +' E) B) : + (D +' E) ~> @ctree@{_ _ _ _ d' q'} E B := + case_sum1 (fun _ d => mrec f d) (fun _ e => CTree.trigger e). +Arguments mrecursive f [T] _. + Global Instance eq_itree_mrec {R} : Proper (equ eq ==> equ eq) (@interp_mrec _ _ _ ctx R). @@ -158,12 +162,12 @@ Qed. Theorem interp_mrec_trigger {U} (a : (D +' E) U) : interp_mrec ctx (CTree.trigger a) - ≲ mrecursive ctx _ 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. + rewrite Equ.unfold_trigger, unfold_interp_mrec; unfold mrecursive. + destruct a; cbn -[CTree.trigger]. + rewrite bind_ret_r. apply ssim_guard_l. reflexivity. + rewrite Equ.unfold_trigger. apply ssim_vis_id. intros. split; auto. apply ssim_guard_l. rewrite unfold_interp_mrec. cbn. reflexivity. @@ -180,6 +184,7 @@ Qed. + Theorem interp_mrec_as_interp {T} (c : ctree _ _ T) : interp_mrec ctx c ~ interp (mrecursive ctx) c. Proof. @@ -188,62 +193,44 @@ Proof. red. revert_until T. coinduction R CIH. intros. - rewrite unfold_interp_mrec. unfold _interp_mrec, fold. - unfold interp, fold. - setoid_rewrite unfold_iter. + rewrite unfold_interp_mrec. unfold _interp_mrec. + rewrite FoldCTree.unfold_interp. destruct (observe c). - - unfold ret, Monad_ctree. - apply step_sb'_guard_r. - rewrite bind_ret_l. + - apply step_sb'_guard_r. reflexivity. - - unfold mstuck, MonadStuck_ctree. rewrite bind_stuck. - apply step_sb'_guard_r. + - 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'_guard_r. 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 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. + + cbn. apply step_sb'_guard. - rewrite interp_mrec_bind. + change ((elem R) side (interp_mrec ctx (ctx _ d >>= k)) + (x <- mrec ctx d;; Guard (interp (mrecursive ctx) (k x)))). + setoid_rewrite (interp_mrec_bind (ctx _ d) k). 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. + + cbn -[CTree.trigger CTree.bind]. apply step_sb'_guard_r. + eapply (@equ_sb'_goal _ _ _ _ _ _ _ _ side); [reflexivity | |]. + { cbn -[CTree.trigger CTree.bind]; rewrite bind_trigger; reflexivity. } 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'. + eapply (@equ_sb'_goal _ _ _ _ _ _ _ _ side); [reflexivity | |]. + { unfold mbr, MonadBr_ctree; cbn -[CTree.branch CTree.bind]; apply Equ.bind_branch. } + apply step_sb'_br_id. intros. - apply CIH. - intros x. exists x. apply step_sb'_guard_l'. intros. apply CIH. @@ -264,12 +251,11 @@ 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). +Lemma interp_trigger {E' F' B' U} + (h : E' ~> @ctree@{_ _ _ _ d' q'} F' B') (e : E' U) : + interp h (CTree.trigger e : @ctree@{_ _ _ _ d0 q0} E' B' U) ~ Guard (h _ e). Proof. - unfold CTree.trigger. - rewrite interp_vis. - setoid_rewrite interp_ret. + rewrite FoldCTree.interp_trigger. setoid_rewrite sb_guard. rewrite bind_ret_r. reflexivity. @@ -278,7 +264,7 @@ 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. + unfold trigger_inl1. rewrite interp_trigger. cbn. setoid_rewrite sb_guard. @@ -334,25 +320,28 @@ 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. +Section RecursiveFacts. + Context {E : Type -> Type} {B : Type -> Type} {X Y : Type}. + Variable f : X -> ctree (callE X Y +' E) B Y. + + Definition recursive@{d q +} : (callE X Y +' E) ~> @ctree@{_ _ _ _ d q} E B := + case_sum1 (calling (rec f)) (fun _ e => CTree.trigger e). + Arguments recursive [T] _. + + (* SAZ: TODO - update this after the change to sbisim *) + Lemma rec_as_interp (x : X) : + rec f x ~ interp recursive (f x). + Admitted. + + Lemma interp_recursive_call (x : X) : + interp recursive (@call E B X Y x) ~ rec f x. + Proof. + unfold recursive, call. + rewrite interp_trigger. cbn [case_sum1 calling]. + setoid_rewrite sb_guard. + reflexivity. + Qed. +End RecursiveFacts. (* SAZ: TODO: Not sure what the appropriate analogue of this is for ctrees diff --git a/theories/Interp/Refine.v b/theories/Interp/Refine.v index b497392a..9e4239d7 100644 --- a/theories/Interp/Refine.v +++ b/theories/Interp/Refine.v @@ -1,10 +1,8 @@ -Unset Universe Checking. From ExtLib Require Import Structures.Functor Structures.Monad. -Unset Universe Checking. From CTree Require Import Eq Eq.Epsilon @@ -13,15 +11,17 @@ From CTree Require Import Interp.FoldCTree Interp.FoldStateT Misc.Pure. +Set Universe Polymorphism. + Import ITree.Basics.Basics.Monads. Import MonadNotation. Open Scope monad_scope. -Theorem ssim_pure {E F B C X} : forall (L : rel _ _) (t : ctree E B X), +Theorem ssim_pure@{d q +} {E F B C X} : forall (L : rel _ _) (t : ctree E B X), pure_finite t -> (forall x : X, L (val x) (val tt)) -> - ssim L t (Ret tt : ctree F C unit). + ssim L t (Ret tt : @ctree@{_ _ _ _ d q} F C unit). Proof. intros. induction H; subs. - now apply ssim_ret. @@ -30,7 +30,7 @@ Proof. - now apply ssim_guard_l. Qed. -Unset Universe Checking. + Theorem refine_ctree_ssim {E B B' X} : forall (t : ctree E B X) (h : B ~> ctree E B'), @@ -39,20 +39,23 @@ Theorem refine_ctree_ssim {E B B' X} : Proof. intros. rewrite ssim_ssim'. red. revert t. coinduction R CH. intros. rewrite (ctree_eta t) at 2. - setoid_rewrite unfold_refine. cbn. + setoid_rewrite unfold_refine. + cbn -[CTree.trigger]. destruct (observe t) eqn:?. - apply step_ssbt'_ret. reflexivity. - apply step_ss'_stuck. - apply step_ss'_step; auto. step. now apply step_ss'_guard_l. - now apply step_ss'_guard. - - setoid_rewrite bind_trigger. + - unfold mtrigger, MonadTrigger_ctree. + cbn -[CTree.trigger]. rewrite bind_trigger. apply step_ss'_vis_id. intros. split; [|auto]. step. apply step_ss'_guard_l. apply CH. - change (Br c k) with ((fun _ => Br c k) tt). setoid_rewrite <- bind_ret_l at 6. eapply ss'_clo_bind with (R0 := (fun _ _ => True)). - { apply ssim_pure. apply H. intros. now constructor. } + { eapply (@ssim_pure E E B' B X0 _ (h X0 c)). + apply H. intros. now constructor. } intros ? _ _. cbn. apply step_ss'_br_r with (x := x). apply step_ss'_guard_l. apply CH. @@ -68,7 +71,8 @@ Theorem refine_state_ssim {E B B' X St} : Proof. intros. rewrite ssim_ssim'. red. revert t s. coinduction R CH. intros. rewrite (ctree_eta t) at 2. - setoid_rewrite unfold_refine_state. cbn. + setoid_rewrite unfold_refine_state. + cbn -[CTree.trigger]. destruct (observe t) eqn:?. - apply step_ssbt'_ret. constructor. reflexivity. - apply step_ss'_stuck. @@ -77,7 +81,9 @@ Proof. step. apply step_ss'_guard_l. apply CH. - apply step_ss'_guard. apply CH. - - setoid_rewrite bind_trigger. + - unfold mtrigger, MonadTrigger_stateT, MonadTrigger_ctree. + cbn -[CTree.trigger]. + rewrite ?bind_bind, bind_trigger, ?bind_ret_l. cbn. apply step_ss'_vis_id. intros. split; [| constructor; etrans]. step. apply step_ss'_guard_l. apply CH. - change (Br c k) with ((fun _ => Br c k) tt). diff --git a/theories/Misc/Head.v b/theories/Misc/Head.v index 4af9bddc..c98d34e1 100644 --- a/theories/Misc/Head.v +++ b/theories/Misc/Head.v @@ -23,6 +23,7 @@ Open Scope ctree_scope. Set Implicit Arguments. Set Contextual Implicit. +Set Universe Polymorphism. (*| The [haction] computation is itself a tree. The values it computes is @@ -32,10 +33,17 @@ The [haction] data structure captures trivially this data. .. coq:: |*) -Variant haction {E B X} := +Section haction. + + Universe e. + Context {E : Type@{e} -> Type} {B : Type -> Type} {X : Type}. + +Variant haction := | ARet (r : X) | AStep (t : ctree E B X) - | AVis (Y : Type) (e : E Y) (k : Y -> ctree E B X). + | AVis (Y : Type@{e}) (e : E Y) (k : Y -> ctree E B X). + +End haction. (*| @@ -74,11 +82,11 @@ Proof. now step. Qed. -Unset Universe Checking. Section trans_head. -Context {E F B C : Type -> Type} {X : Type}. +Context {E : Type -> Type} {F : Type -> Type} + {B : Type -> Type} {C : Type -> Type} {X : Type}. Context `{B -< C}. (*| diff --git a/theories/Misc/Pure.v b/theories/Misc/Pure.v index 8bcee8b1..6bdee809 100644 --- a/theories/Misc/Pure.v +++ b/theories/Misc/Pure.v @@ -1,6 +1,8 @@ From CTree Require Import Eq Eq.Epsilon. +Set Universe Polymorphism. + Variant pureb {E C X} (rec : ctree E C X -> Prop) (t : ctree E C X) : Prop := | pureb_ret (v : X) (EQ : t ≅ Ret v) : pureb rec t | pureb_stuck (EQ : t ≅ Stuck) : pureb rec t @@ -15,7 +17,7 @@ Qed. Section pure. - Context {E C : Type -> Type} {X : Type}. + Context {E : Type -> Type} {C : Type -> Type} {X : Type}. Class pure (t : ctree E C X) := pure_ : gfp (@fpure E C X) t. @@ -144,7 +146,7 @@ Qed. Section pure_finite. - Context {E C : Type -> Type} {X : Type}. + Context {E : Type -> Type} {C : Type -> Type} {X : Type}. Inductive pure_finite_ : ctree E C X -> Prop := | puref_ret (v : X) t (EQ: t ≅ Ret v) : pure_finite_ t @@ -249,7 +251,7 @@ Class is_simple {E C X} (t : ctree E C X) := Section is_simple_theory. - Context {E C : Type -> Type} {X : Type}. + Context {E : Type -> Type} {C : Type -> Type} {X : Type}. #[global] Instance is_simple_equ : Proper (equ eq ==> iff) (@is_simple E C X). diff --git a/theories/dune b/theories/dune index 8165e1ab..586867fc 100644 --- a/theories/dune +++ b/theories/dune @@ -1,5 +1,6 @@ (include_subdirs qualified) -(coq.theory +(rocq.theory (name CTree) - (package rocq-ctree)) + (package rocq-ctree) + (theories Stdlib ExtLib Paco ITree Coinduction RelationAlgebra)) From 6f1c3d3db2d95ceaccd569a4a0fcdb539a318061 Mon Sep 17 00:00:00 2001 From: Lef Ioannidis Date: Mon, 12 Oct 2026 13:05:58 -0700 Subject: [PATCH 2/6] Fix CI toolchains and cross-version proof compatibility --- .github/workflows/coq.yml | 15 +++++++++++---- dune-project | 2 +- examples/Yield/Par.v | 7 +++---- flake.lock | 6 +++--- flake.nix | 9 +++++---- theories/Eq/SBisim.v | 9 +++++---- theories/Eq/SSimAlt.v | 2 +- theories/Eq/WBisim.v | 14 +++++++------- 8 files changed, 36 insertions(+), 28 deletions(-) diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml index 2cd7ea39..514c4df4 100644 --- a/.github/workflows/coq.yml +++ b/.github/workflows/coq.yml @@ -14,19 +14,26 @@ jobs: strategy: matrix: coq_version: - - '8.15.2' + - '9.2' ocaml_version: - - '4.14.0-flambda' + - '4.14-flambda' max-parallel: 4 fail-fast: false steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v4 - uses: coq-community/docker-coq-action@v1 with: - opam_file: 'coq-ctree.opam' + opam_file: 'rocq-ctree.opam' coq_version: ${{ matrix.coq_version }} ocaml_version: ${{ matrix.ocaml_version }} + before_install: | + opam pin remove -n -y dune + opam update -y + opam install -y dune.3.23.1 + dune build rocq-ctree.opam + cp _build/default/rocq-ctree.opam . + before_script: dune build -j 2 export: 'OPAMWITHTEST' env: OPAMWITHTEST: 'true' diff --git a/dune-project b/dune-project index b2163f43..e8512663 100644 --- a/dune-project +++ b/dune-project @@ -1,4 +1,4 @@ -(lang dune 3.24) +(lang dune 3.23) (using rocq 0.11) (name rocq-ctree) diff --git a/examples/Yield/Par.v b/examples/Yield/Par.v index dfaf25f4..0fdc93ef 100644 --- a/examples/Yield/Par.v +++ b/examples/Yield/Par.v @@ -297,8 +297,7 @@ Section parallel. invert. destruct n'; inv_equ. rewrite <- ctree_eta in Hequ. rewrite rewrite_schedule in Hequ. simp schedule_match in Hequ. - step in Hequ. inv Hequ. invert. exists n'. - dependent destruction H4. + step in Hequ. inv Hequ. repeat invert. exists n'. rewrite ctree_eta. rewrite <- Heq. rewrite <- H. rewrite REL. split; auto. } - destruct n'; inv_equ. @@ -632,7 +631,7 @@ Section parallel. rewrite rewrite_schedule at 1. simp schedule_match. econstructor. step. constructor. intros. apply equ_schedule. apply replace_vec_relation; repeat intro; auto. - invert; apply H. + all: invert; apply H. Qed. (** when the thread is a fork *) @@ -654,7 +653,7 @@ Section parallel. rewrite <- Heqc. constructor. rewrite <- (replace_vec_twice _ v i t (k false)). eapply IHvisible_; auto; rewrite replace_vec_eq; eauto. - - invert. invert. + - repeat invert. rewrite rewrite_schedule at 1. simp schedule_match. rewrite <- Heqc. econstructor. apply equ_schedule. apply cons_vec_relation; auto. diff --git a/flake.lock b/flake.lock index bbc2e751..04d42d4f 100644 --- a/flake.lock +++ b/flake.lock @@ -51,11 +51,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1762943920, - "narHash": "sha256-ITeH8GBpQTw9457ICZBddQEBjlXMmilML067q0e6vqY=", + "lastModified": 1791487292, + "narHash": "sha256-tqM7xDEsaeK1p6VvRygeZ9LkQRpUUkbRT02BHv6hnTM=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "91c9a64ce2a84e648d0cf9671274bb9c2fb9ba60", + "rev": "8edc0c72e3a38faf5434e40d1f19431125fe4b30", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 01e8f94a..2f63088a 100644 --- a/flake.nix +++ b/flake.nix @@ -20,9 +20,9 @@ let pkgs = import nixpkgs { inherit system; }; lib = pkgs.lib; - rocq = pkgs.rocq-core; rocqPkgs = pkgs.rocqPackages_9_0; coqPkgs = pkgs.coqPackages_9_0; + rocq = rocqPkgs.rocq-core; coinduction = rocqPkgs.callPackage ( { rocq, stdenv }: @@ -36,7 +36,7 @@ with rocqPkgs; with coqPkgs; with rocq.ocamlPackages; - [ ocaml camlp5 rocq pkgs.coq dune_3 stdlib rocq-core findlib ]; + [ ocaml camlp5 rocq coqPkgs.coq dune_3 stdlib rocq-core findlib ]; propagatedBuildInputs = with rocqPkgs; with coqPkgs; @@ -56,7 +56,7 @@ with rocqPkgs; with coqPkgs; with rocq.ocamlPackages; - [ ocaml camlp5 rocq pkgs.coq dune_3 stdlib rocq-core findlib ]; + [ ocaml camlp5 rocq coqPkgs.coq dune_3 stdlib rocq-core findlib ]; propagatedBuildInputs = with rocqPkgs; with coqPkgs; @@ -74,12 +74,13 @@ opam-name = "rocq-ctree"; useDune = true; src = ./.; + preBuild = "dune build rocq-ctree.opam && cp _build/default/rocq-ctree.opam ."; buildInputs = with rocqPkgs; with coqPkgs; with rocq.ocamlPackages; - [ ocaml camlp5 rocq pkgs.coq dune_3 ITree coinduction relation-algebra stdlib equations ExtLib zarith findlib ]; + [ ocaml camlp5 rocq coqPkgs.coq dune_3 ITree coinduction relation-algebra stdlib equations ExtLib zarith findlib ]; propagatedBuildInputs = [ rocq ]; }) { inherit rocq; }; diff --git a/theories/Eq/SBisim.v b/theories/Eq/SBisim.v index 233ecb6c..fc367d2f 100644 --- a/theories/Eq/SBisim.v +++ b/theories/Eq/SBisim.v @@ -1317,9 +1317,9 @@ produce any challenge for the other. intros R. coinduction S _; split; cbn. - intros * TR; exfalso. - exact (spinD_gen_is_stuck l (spin_gen c) t' c TR). + now apply spinD_gen_is_stuck in TR. - intros * TR; exfalso. - exact (spinD_gen_is_stuck l (spin_gen c') t' c' TR). + now apply spinD_gen_is_stuck in TR. Qed. (*| @@ -1380,7 +1380,8 @@ produce any challenge for the other. Lemma br2_spin_l {X} : forall (t : ctree E C X), br2 spin t ~ t. Proof. - intros; apply br2_is_stuck; exact (spin_is_stuck τ t t). + intros; apply br2_is_stuck. + red; intros l u TR; now apply spin_is_stuck in TR. Qed. Lemma br2_spin_r {X} : forall (t : ctree E C X), @@ -1548,7 +1549,7 @@ Not fond of this, need to give some thoughts about them do 2 eexists; intuition; eauto. apply trans_val_inv in TR0. rewrite TR0; eauto. - apply trans_ret. + all: apply trans_ret. Qed. End WithParams. diff --git a/theories/Eq/SSimAlt.v b/theories/Eq/SSimAlt.v index 15309b17..97335b40 100644 --- a/theories/Eq/SSimAlt.v +++ b/theories/Eq/SSimAlt.v @@ -500,7 +500,7 @@ Section Proof_Rules. split; [| split]; intros; inv_equ. inv_trans; subst. cbn; do 3 eexists; intuition; subs; eauto. - apply trans_step. + all: apply trans_step. Qed. Lemma step_ss'_step_l : diff --git a/theories/Eq/WBisim.v b/theories/Eq/WBisim.v index 6239f0f6..5d2c7033 100644 --- a/theories/Eq/WBisim.v +++ b/theories/Eq/WBisim.v @@ -378,24 +378,24 @@ on the setoid side. unfold wtrans, etrans. ka. Qed. - Lemma cnv_wt (R : Chain wb) : (elem R: hrel _ _)^° ≡ elem R. + Lemma cnv_wt (R : Chain wb) : cnv _ _ (elem R: hrel _ _) ≡ elem R. Proof. apply RelationAlgebra.lattice.antisym; intros ???; apply sym_t,H. Qed. - Lemma cnv_gfp: RelationAlgebra.lattice.weq ((gfp wb: hrel _ _)^°) (gfp wb). + Lemma cnv_gfp: RelationAlgebra.lattice.weq (cnv _ _ (gfp wb: hrel _ _)) (gfp wb). Proof. apply cnv_wt. Qed. - Lemma cnv_wbisim: wbisimT^° ≡ wbisimT. + Lemma cnv_wbisim: cnv _ _ wbisimT ≡ wbisimT. Proof. apply cnv_wt. Qed. - Lemma cnv_wbisim': wbisim^° ≡ wbisim. + Lemma cnv_wbisim': cnv _ _ wbisim ≡ wbisim. Proof. apply cnv_wt. Qed. (*| By symmetry, similar results for left-to-right game |*) - Lemma wbisim_trans_front l: (trans l)^° ⋅ wbisimT ≦ wbisimT ⋅ (wtrans l)^°. + Lemma wbisim_trans_front l: cnv _ _ (trans l) ⋅ wbisimT ≦ wbisimT ⋅ cnv _ _ (wtrans l). Proof. cnv_switch. rewrite 2cnvdot, cnv_invol, cnv_wbisim. apply wbisim_trans_back. Qed. - Lemma wbisim_etrans_front l: (etrans l)^° ⋅ wbisimT ≦ wbisimT ⋅ (wtrans l)^°. + Lemma wbisim_etrans_front l: cnv _ _ (etrans l) ⋅ wbisimT ≦ wbisimT ⋅ cnv _ _ (wtrans l). Proof. cnv_switch. rewrite 2cnvdot, cnv_invol, cnv_wbisim. apply wbisim_etrans_back. Qed. - Lemma wbisim_wtrans_front l: (wtrans l)^° ⋅ wbisimT ≦ wbisimT ⋅ (wtrans l)^°. + Lemma wbisim_wtrans_front l: cnv _ _ (wtrans l) ⋅ wbisimT ≦ wbisimT ⋅ cnv _ _ (wtrans l). Proof. cnv_switch. rewrite 2cnvdot, cnv_invol, cnv_wbisim. apply wbisim_wtrans_back. Qed. (*| From 7bb7681869962fce6e6b4825684926dbeb89d915 Mon Sep 17 00:00:00 2001 From: Lef Ioannidis Date: Mon, 12 Oct 2026 15:56:44 -0700 Subject: [PATCH 3/6] Fix Docker CI checkout ownership --- .github/workflows/coq.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml index 514c4df4..d827a39e 100644 --- a/.github/workflows/coq.yml +++ b/.github/workflows/coq.yml @@ -28,6 +28,7 @@ jobs: coq_version: ${{ matrix.coq_version }} ocaml_version: ${{ matrix.ocaml_version }} before_install: | + sudo chown -R "$(id -u):$(id -g)" . opam pin remove -n -y dune opam update -y opam install -y dune.3.23.1 From 1b688f3e8ebf686f008c0bfab33c33f299bf2800 Mon Sep 17 00:00:00 2001 From: Lef Ioannidis Date: Fri, 16 Oct 2026 15:41:54 -0700 Subject: [PATCH 4/6] Restore proofs and add strict universe regression coverage Keep required universe boundaries, restore existing proof structure, and retain only necessary polymorphism. Remove the unused trace instance and use native converse notation in WBisim. Validated on Rocq 9.3.0 with OCaml 5.4.1 and Dune 3.24.2: full build, UniverseCheck, kernel recheck, focused source probes, and ImpBr consumer. Rocq 9.0 and 9.2 CI remain required. --- examples/CCS/Denotation.v | 57 +++++++++++++++++++--------- examples/Coffee/coffeeCTree.v | 41 +++++++++++--------- examples/ImpBr/ImpBr.v | 39 +++++++++---------- examples/SimpleSim/SimExample.v | 4 +- examples/Yield/Lang.v | 38 ++++++++++--------- examples/Yield/Par.v | 2 +- tests/UniverseCheck/UniverseCheck.v | 54 +++++++++++++++++++++++++++ tests/UniverseCheck/dune | 3 ++ theories/Core/CTreeDefinitions.v | 8 ++-- theories/Core/Index.v | 2 - theories/Eq/Equ.v | 19 +--------- theories/Eq/Trace.v | 8 ---- theories/Eq/Trans.v | 49 ++++++++---------------- theories/Eq/WBisim.v | 15 ++++---- theories/Interp/FoldCTree.v | 8 ++-- theories/Interp/FoldStateT.v | 27 +++++--------- theories/Interp/ITree.v | 58 +++++++++++++++++------------ theories/Interp/Internalize.v | 4 +- theories/Interp/RecursionFacts.v | 54 ++++++++++++++++++--------- theories/Interp/Refine.v | 16 +++----- 20 files changed, 285 insertions(+), 221 deletions(-) create mode 100644 tests/UniverseCheck/UniverseCheck.v create mode 100644 tests/UniverseCheck/dune diff --git a/examples/CCS/Denotation.v b/examples/CCS/Denotation.v index 905b2ac0..b0de5141 100644 --- a/examples/CCS/Denotation.v +++ b/examples/CCS/Denotation.v @@ -53,8 +53,7 @@ Notation ccsE := ActionE. Notation ccsC := (B2 +' B3 +' B4). Universe ccs_u. -Definition ccsT (T : Type@{ccs_u}) : Type@{ccs_u} := - @ctree@{_ _ _ _ ccs_u ccs_u} ccsE ccsC T. +Definition ccsT := @ctree@{_ _ _ _ ccs_u ccs_u} ccsE ccsC. Definition ccsT' (T : Type@{ccs_u}) := ctreeF ccsE ccsC T (ccsT T). Definition ccs' := ccsT' void. @@ -72,7 +71,7 @@ Section Combinators. Definition plus (P Q : ccs) : ccs := br2 P Q. - Definition h_new (c : chan) : forall T, ActionE T -> ccsT T := + Definition h_new (c : chan) : ActionE ~> ccsT := fun _ e => let '(Act a) := e in match a with | Send c' @@ -250,15 +249,14 @@ Lemma trans_prefix_inv : forall l a p p', p' ≅ p /\ l = comm a. Proof. intros * tr. - unfold prefix in tr. - apply Trans.trans_trigger_inv in tr as (? & ? & ->). + apply trans_trigger_inv in tr as (? & ? & ->). destruct x; split; auto. Qed. Lemma trans_prefix : forall a p, trans (comm a) (prefix a p) p. Proof. - intros; unfold prefix; apply Trans.trans_trigger'. + intros; eapply trans_trigger. Qed. (* TO MOVE *) @@ -328,9 +326,12 @@ Proof. - edestruct IHtr as (q & tr' & eq); eauto. exists q; split; auto. unfold new; rewrite unfold_interp, <- Heqobsp. - cbn -[CTree.branch MonadBr_ctree]. - unfold Utils.mbr, MonadBr_ctree; rewrite bind_branch. - eapply trans_br with (x := x); [apply trans_guard; exact tr' | reflexivity]. + cbn; unfold Utils.mbr, MonadBr_ctree, branch. + eapply trans_bind_r with x. + eapply trans_br; [|reflexivity]. + apply trans_ret. + apply trans_guard. + apply tr'. - edestruct IHtr as (q & tr' & eq); eauto. exists q; split; auto. unfold new; rewrite unfold_interp, <- Heqobsp. @@ -343,14 +344,36 @@ Proof. rewrite <- H. apply observe_equ_eq in Heqop'. now rewrite Heqop'. - - destruct e as [a]; destruct a as [ch | ch]. - all: cbn [can_comm] in comm; - destruct (c =? ch) eqn:COMM; inv comm. - all: eexists; split. - all: try solve [unfold new; rewrite unfold_interp, <- Heqobsp; - cbn [h_new]; rewrite COMM; apply Trans.trans_trigger]. - all: rewrite sb_guard, H. - all: apply observe_equ_eq in Heqop'; rewrite Heqop'; reflexivity. + - destruct e, a. + all: cbn in *; destruct (c =? c0) eqn:comm'; inv comm. + + eexists; split. + unfold new; rewrite unfold_interp, <- Heqobsp. + cbn; unfold Utils.mbr, MonadBr_ctree, branch. + eapply trans_bind_l. + intros abs; inv abs. + rewrite comm'. + unfold trigger. + eapply trans_vis'. + reflexivity. + rewrite bind_ret_l, sb_guard, H. + unfold new. + rewrite unfold_interp. + rewrite <- Heqop', <- unfold_interp. + reflexivity. + + eexists; split. + unfold new; rewrite unfold_interp, <- Heqobsp. + cbn; unfold Utils.mbr, MonadBr_ctree, branch. + eapply trans_bind_l. + intros abs; inv abs. + rewrite comm'. + unfold trigger. + eapply trans_vis'. + reflexivity. + rewrite bind_ret_l, sb_guard, H. + unfold new. + rewrite unfold_interp. + rewrite <- Heqop', <- unfold_interp. + reflexivity. - tauto. Qed. diff --git a/examples/Coffee/coffeeCTree.v b/examples/Coffee/coffeeCTree.v index 30a07885..b1abb6b7 100644 --- a/examples/Coffee/coffeeCTree.v +++ b/examples/Coffee/coffeeCTree.v @@ -55,12 +55,10 @@ Proof. intros H. setoid_rewrite ctree_eta in H. play in H. setoid_rewrite bind_ret_l in EQ. - apply trans_br_inv in TR as (? & TR). destruct x1; - [| eapply ssim_br_l_inv with (x := true) in EQ]; play in EQ; - apply Trans.trans_trigger_inv in TR as ([] & EQt & _); - rewrite EQt in TR0; - apply Trans.trans_trigger_inv in TR0 as ([] & _ & BAD); inv BAD; auto. - all: match goal with H : obs _ _ = obs _ _ |- _ => inv H end. + apply trans_br_inv in TR as (? & TR). destruct x1. inv_trans. + - play in EQ. inv_trans. subst. discriminate. + - eapply ssim_br_l_inv with (x := true) in EQ. + play in EQ. inv_trans. subst; discriminate. Unshelve. all: auto. Qed. @@ -69,12 +67,18 @@ Proof. coinduction R CH. setoid_rewrite ctree_eta. cbn. setoid_rewrite bind_ret_l. apply step_ss_br_l. intros. - destruct x; rewrite !bind_trigger; - apply step_ss_vis; auto; intros []; exists tt; split; auto; step. - 1: apply step_ss_br_r with (x := true). - 2: apply step_ss_br_r with (x := false). - all: eapply ssim_bind_chain; [reflexivity | cbn; intros _]. - all: apply step_ss_vis_id; auto. + destruct x. + - rewrite bind_trigger. apply step_ss_vis; auto. intros []. + exists tt. split; auto. + step. apply step_ss_br_r with (x := true). + eapply ssim_bind_chain. reflexivity. cbn. intros _. + apply step_ss_vis_id. auto. + - rewrite bind_trigger. + apply step_ss_vis; auto; intros []; exists tt; split; auto. + step. + apply step_ss_br_r with (x := false). + apply ssim_bind_chain. reflexivity. intros _. + apply step_ss_vis_id. auto. Qed. Tactic Notation "play" "using" tactic(tac) := @@ -94,10 +98,13 @@ Proof. destruct s. 2: play; now step. setoid_rewrite bind_ret_l in H. - play in H. destruct x1; - [play using (apply trans_br21; etrans) | play using (apply trans_br22; etrans)]. - all: apply Trans.trans_trigger_inv in TR as ([] & EQt & EQl); subst l. - all: step; cbn; eexists; split; [apply Trans.trans_trigger' | ]. - all: rewrite EQt in H; step; destruct s; auto; play in H; play. + play in H. destruct x1; inv_trans; subst. + + play using (apply trans_br21; etrans). + step. play. + step. destruct s; auto. play in H. play. + + play using (apply trans_br22; etrans). + step. play. + step. destruct s; auto. + play in H. play. - pose proof (ssim_tracincl _ _ coffee_ssim); auto. Qed. diff --git a/examples/ImpBr/ImpBr.v b/examples/ImpBr/ImpBr.v index 232ac8dd..3015b79e 100755 --- a/examples/ImpBr/ImpBr.v +++ b/examples/ImpBr/ImpBr.v @@ -32,8 +32,8 @@ From CTree Require Import Interp.FoldStateT. Import ListNotations. -Import CTreeNotations. -Local Open Scope ctree_scope. +Import MonadNotation. +Local Open Scope monad_scope. Local Open Scope string_scope. (*| @@ -73,16 +73,15 @@ Variant MemE : Type -> Type := Section Semantics. Universe computation_u. - Definition computation (T : Type@{computation_u}) : Type@{computation_u} := - @ctree@{_ _ _ _ computation_u computation_u} MemE B2 T. + Notation computation := (@ctree@{_ _ _ _ computation_u computation_u} MemE B2). Fixpoint denote_expr (e : expr) : computation value := match e with - | Var v => trigger (rd v) - | Lit n => Ret n - | Plus a b => (l <- denote_expr a;; r <- denote_expr b;; Ret (l + r))%ctree - | Minus a b => (l <- denote_expr a;; r <- denote_expr b;; Ret (l - r))%ctree - | Mult a b => (l <- denote_expr a;; r <- denote_expr b;; Ret (l * r))%ctree + | Var v => trigger (rd v) + | Lit n => ret n + | Plus a b => l <- denote_expr a ;; r <- denote_expr b ;; ret (l + r) + | Minus a b => l <- denote_expr a ;; r <- denote_expr b ;; ret (l - r) + | Mult a b => l <- denote_expr a ;; r <- denote_expr b ;; ret (l * r) end. Definition while (step : computation (unit + unit)) : computation unit := @@ -92,20 +91,21 @@ Section Semantics. Fixpoint denote_imp (s : stmt) : computation unit := match s with - | Assign x e => (v <- denote_expr e;; trigger (wr x v))%ctree - | Seq a b => (denote_imp a;; denote_imp b)%ctree - | If i t e => (v <- denote_expr i;; - if is_true v then denote_imp t else denote_imp e)%ctree + | Assign x e => v <- denote_expr e ;; trigger (wr x v) + | Seq a b => denote_imp a ;; denote_imp b + | If i t e => + v <- denote_expr i ;; + if is_true v then denote_imp t else denote_imp e | While t b => - while (v <- denote_expr t;; - if is_true v - then denote_imp b;; Ret (inl tt) - else Ret (inr tt))%ctree + while (v <- denote_expr t ;; + if is_true v + then denote_imp b ;; ret (inl tt) + else ret (inr tt)) | Branch a b => br2 (denote_imp a) (denote_imp b) - | Skip => Ret tt + | Skip => ret tt | Block => Stuck @@ -233,8 +233,9 @@ from Section 2 are indeed equivalent. repeat setoid_rewrite sb_guard. cbn. rewrite interp_state_ret. - rewrite interp_state_trigger. + unfold trigger. rewrite interp_state_vis. cbn. rewrite bind_ret_l, sb_guard. + cbn. rewrite interp_state_ret. apply sb_ret. rewrite alist_add_alist_add; [reflexivity |]. apply RelDec_Correct_string. diff --git a/examples/SimpleSim/SimExample.v b/examples/SimpleSim/SimExample.v index 932e570c..2e09e1ee 100644 --- a/examples/SimpleSim/SimExample.v +++ b/examples/SimpleSim/SimExample.v @@ -58,11 +58,11 @@ Proof. unfold br2. rewrite bind_br. apply step_sb_br_id. intros. destruct x. - - rewrite !bind_trigger. + - rewrite bind_trigger. apply step_sb_vis_id. intros []. split; [| auto]. rewrite sb_guard. apply CH. - - rewrite !bind_trigger. + - rewrite bind_trigger. apply step_sb_vis_id. intros []. split; [| auto]. rewrite sb_guard. apply CH. diff --git a/examples/Yield/Lang.v b/examples/Yield/Lang.v index b6470994..8a322416 100644 --- a/examples/Yield/Lang.v +++ b/examples/Yield/Lang.v @@ -19,6 +19,7 @@ From ITree Require Import ITree Basics.CategoryKleisli Events.State + Events.StateFacts Events.MapDefault. From Coinduction Require Import all. @@ -70,7 +71,6 @@ Variant MemE : Type -> Type := | rd (x : var) : MemE value | wr (x : var) (v : value) : MemE unit. -Set Universe Polymorphism. Section Denote1. Universes d q sd sq yd yq md mq. Definition is_true (v : value) : bool := if (v =? 0)%nat then false else true. @@ -288,8 +288,12 @@ Section Denote1. Proof. unfold interp_concurrency. do 2 rewrite schedule_forks_equ. - repeat setoid_rewrite bind_trigger. - do 2 (apply sb_vis; intros []). + unfold trigger. + (* not sure why we can't just rewrite twice, but we can below *) + rewrite bind_vis. symmetry. rewrite bind_vis. + apply sb_vis. intros []. do 2 rewrite bind_ret_l. + do 2 rewrite bind_vis. + apply sb_vis. intros []. do 2 rewrite bind_ret_l. apply sb_guard_lr. do 2 rewrite rewrite_schedule. simp schedule_match. @@ -376,12 +380,17 @@ Section Denote1. interp_yield (interp_spawn (interp_concurrency (Fork s Skip))). Proof. rewrite yield_equ, fork_skip_equ. - setoid_rewrite (yield_equ s). unfold interp_yield, interp_spawn. - repeat (rewrite ?FoldCTree.interp_bind, ?FoldCTree.interp_trigger, - ?FoldCTree.interp_ret, ?FoldCTree.interp_guard, ?FoldCTree.interp_br', - ?bind_bind, ?bind_ret_l, ?bind_guard, ?sb_guard, - ?subevent_subevent, ?br1_guard; cbn -[schedule denote_imp]). + + repeat (unfold trigger; rewrite ?interp_bind, ?interp_vis, ?interp_ret, ?bind_ret_l, ?interp_guard, ?sb_guard; cbn). + rewrite ?interp_br', ?subevent_subevent, ?br1_guard. + repeat (unfold trigger; rewrite ?interp_bind, ?interp_vis, ?interp_ret, ?bind_ret_l, ?interp_guard, ?sb_guard; cbn). + rewrite yield_equ. + rewrite ?interp_guard, sb_guard. + repeat (unfold trigger; rewrite ?interp_bind, ?interp_vis, ?interp_ret, ?bind_ret_l, ?interp_guard, ?sb_guard; cbn). + rewrite ?interp_br', ?subevent_subevent, ?br1_guard. + repeat (unfold trigger; rewrite ?interp_bind, ?interp_vis, ?interp_ret, ?bind_ret_l, ?interp_guard, ?sb_guard; cbn). + unfold trigger. reflexivity. Qed. @@ -393,12 +402,8 @@ Section Denote1. Proof. rewrite yield_equ, fork_skip_equ. unfold interp_spawn. - repeat (rewrite ?FoldCTree.interp_bind, ?FoldCTree.interp_trigger, - ?FoldCTree.interp_ret, ?FoldCTree.interp_guard, - ?bind_bind, ?bind_ret_l, ?bind_guard, ?sb_guard; - cbn -[schedule denote_imp]). + repeat (unfold trigger; rewrite ?interp_bind, ?interp_vis, ?interp_ret, ?bind_ret_l, ?interp_guard, ?sb_guard; cbn). upto_bind_eq; intros []. - rewrite ?bind_ret_l, ?sb_guard. reflexivity. Qed. @@ -408,10 +413,9 @@ Section Denote1. Proof. rewrite fork_skip_equ. unfold interp_yield, interp_spawn. - repeat (rewrite ?FoldCTree.interp_bind, ?FoldCTree.interp_trigger, - ?FoldCTree.interp_ret, ?FoldCTree.interp_guard, ?FoldCTree.interp_br', - ?bind_bind, ?bind_ret_l, ?bind_guard, ?sb_guard, - ?subevent_subevent, ?br1_guard; cbn -[schedule denote_imp]). + repeat (unfold trigger; rewrite ?interp_bind, ?interp_vis, ?interp_ret, ?bind_ret_l, ?interp_guard, ?sb_guard; cbn). + rewrite ?interp_br', ?subevent_subevent, br1_guard. + repeat (unfold trigger; rewrite ?interp_bind, ?interp_vis, ?interp_ret, ?bind_ret_l, ?interp_guard, ?sb_guard; cbn). reflexivity. Qed. diff --git a/examples/Yield/Par.v b/examples/Yield/Par.v index 0fdc93ef..5b6a997c 100644 --- a/examples/Yield/Par.v +++ b/examples/Yield/Par.v @@ -217,7 +217,7 @@ Section parallel. induction H; intros n' ?t' v i x' Heql Heq Hequ; try inv Heql; subst. - rewrite <- ctree_eta in Hequ. destruct c. - exfalso; eapply (Br_schedule_inv n (branchn n) k n' v i); exact Hequ. + now exfalso; apply Br_schedule_inv in Hequ. - rewrite <- ctree_eta in Hequ. destruct n' as [| n]; [inv i |]. apply guard_schedule_inv in Hequ. diff --git a/tests/UniverseCheck/UniverseCheck.v b/tests/UniverseCheck/UniverseCheck.v new file mode 100644 index 00000000..2bb2434d --- /dev/null +++ b/tests/UniverseCheck/UniverseCheck.v @@ -0,0 +1,54 @@ +From CTree Require Import Core.Utils Core.CTreeDefinitions Eq.Equ Eq.Trans + Interp.FoldCTree Interp.FoldStateT Interp.Recursion Interp.ITree. +From ITree Require Import ITree InterpFacts Events.StateFacts. +From RelationAlgebra Require Import rel srel. +Import CTreeNotations EquNotations. +Local Open Scope ctree_scope. +Set Universe Checking. +Set Universe Polymorphism. + +Section IndependentBudgets. + Universes i ri qi ro qo. + Constraint i < ri. + Constraint ri < qi. + Constraint qi < ro. + Constraint ro < qo. + Context (E : Type@{i} -> Type) (B : Type@{i} -> Type). + Context (X : Type@{i}) (ev : E X) (choice : B X). + + Definition raised_trigger : @ctree@{i i _ _ ri qi} E B X := CTree.trigger ev. + Definition raised_branch : @ctree@{i i _ _ ri qi} E B X := CTree.branch choice. + Definition raised_branchS : @ctree@{i i _ _ ri qi} E B X := CTree.branchS choice. + Definition raised_monadic_trigger : @ctree@{i i _ _ ri qi} E B X := + @Utils.mtrigger E (@ctree@{i i _ _ ri qi} E B) _ X ev. + Definition raised_monadic_branch : @ctree@{i i _ _ ri qi} E B X := + @Utils.mbr B (@ctree@{i i _ _ ri qi} E B) _ X choice. + Definition continuation (x : X) : @ctree@{i i _ _ ro qo} E B X := + CTreeDefinitions.Ret x. + + Example bind_across_budgets : + CTree.bind raised_trigger continuation ≅ CTreeDefinitions.Vis ev continuation. + Proof. apply Equ.bind_trigger. Qed. + + Example algebra_across_budgets + (t u : @ctree@{i i _ _ ri qi} E B X) + (v w : @ctree@{i i _ _ ro qo} E B X) : + (trans τ t u -> etrans τ t u) /\ (trans τ v w -> etrans τ v w). + Proof. split; apply trans_etrans. Qed. +End IndependentBudgets. + +Section EventBelowBranch. + Universes e b. + Constraint e < b. + Context (E : Type@{e} -> Type) (B : Type@{b} -> Type). + Context (X : Type@{e}) (ev : E X). + Definition trigger_distinct_indices : ctree E B X := CTree.trigger ev. +End EventBelowBranch. + +Section BranchBelowEvent. + Universes e b. + Constraint b < e. + Context (E : Type@{e} -> Type) (B : Type@{b} -> Type). + Context (X : Type@{b}) (choice : B X). + Definition branch_distinct_indices : ctree E B X := CTree.branch choice. +End BranchBelowEvent. diff --git a/tests/UniverseCheck/dune b/tests/UniverseCheck/dune new file mode 100644 index 00000000..7842be8f --- /dev/null +++ b/tests/UniverseCheck/dune @@ -0,0 +1,3 @@ +(rocq.theory + (name CTreeUniverseCheck) + (theories CTree ITree RelationAlgebra)) diff --git a/theories/Core/CTreeDefinitions.v b/theories/Core/CTreeDefinitions.v index 53b78b68..b4f6da08 100644 --- a/theories/Core/CTreeDefinitions.v +++ b/theories/Core/CTreeDefinitions.v @@ -271,8 +271,8 @@ Functorial map ([fmap] in Haskell) Atomic itrees triggering a single event. |*) - Definition trigger (T : Type) (e : E T) : @ctree@{_ _ _ _ d q} E B T := - Vis e (fun x => Ret x). + Definition trigger : E ~> @ctree@{_ _ _ _ d q} E B := + fun T e => Vis e (fun x => Ret x). (*| Atomic ctrees with choice. @@ -415,11 +415,11 @@ Instances #[global] Instance MonadTrigger_ctree@{d q +} {E : Type -> Type} {F : Type -> Type} {B} `{E -< F} : MonadTrigger E (@ctree@{_ _ _ _ d q} F B) := - fun X e => (CTree.trigger (subevent _ e) : @ctree@{_ _ _ _ d q} F B X). + fun _ e => trigger e. #[global] Instance MonadBr_ctree@{d q +} {E} {C : Type -> Type} {D : Type -> Type} `{C -< D} : MonadBr C (@ctree@{_ _ _ _ d q} E D) := - fun X c => (CTree.branch (subevent _ c) : @ctree@{_ _ _ _ d q} E D X). + fun _ c => branch c. #[global] Instance MonadStuck_ctree {E C} : MonadStuck (ctree E C) := fun _ => Stuck. diff --git a/theories/Core/Index.v b/theories/Core/Index.v index 5cda1dec..b1993cc5 100644 --- a/theories/Core/Index.v +++ b/theories/Core/Index.v @@ -1,8 +1,6 @@ From ITree Require Import Basics Indexed.Sum. From CTree Require Import Core.Utils. -Set Universe Polymorphism. - Section Index. (*| diff --git a/theories/Eq/Equ.v b/theories/Eq/Equ.v index 57c6d2d1..f538d35d 100644 --- a/theories/Eq/Equ.v +++ b/theories/Eq/Equ.v @@ -266,16 +266,12 @@ Proof. cbn. rewrite <- x in EQu. dependent destruction EQu. - rewrite <- x. - constructor; intro z. - exact (CH _ _ (REL1 z) _ _ (REL z) (REL0 z)). + rewrite <- x. constructor; eauto. - dependent destruction EQ. cbn. rewrite <- x in EQu. dependent destruction EQu. - rewrite <- x. - constructor; intro z. - exact (CH _ _ (REL1 z) _ _ (REL z) (REL0 z)). + rewrite <- x. constructor; eauto. Qed. #[global] Instance equb_eq_equ {E B X} {Q : rel X X} : @@ -897,9 +893,6 @@ Lemma unfold_branch {X} (c : B X) : (CTree.branch c : @ctree@{_ _ _ _ d q} E B X) = Br c (fun x => Ret x). Proof. reflexivity. Qed. -Lemma unfold_branchS {X} (c : B X) : - (CTree.branchS c : @ctree@{_ _ _ _ d q} E B X) = BrS c (fun x => Ret x). -Proof. reflexivity. Qed. Lemma unfold_trigger {X} (e : E X) : (CTree.trigger e : @ctree@{_ _ _ _ d q} E B X) = Vis e (fun x => Ret x). @@ -952,14 +945,6 @@ Proof. reflexivity. Qed. -Lemma bind_branchS {X Y} - (c : C Y) (k : Y -> @ctree@{_ _ _ _ d' q'} E C X) : - (CTree.branchS c : @ctree@{_ _ _ _ d q} E C Y) >>= k ≅ BrS c k. -Proof. - rewrite unfold_branchS, bind_br; setoid_rewrite bind_step; - setoid_rewrite bind_ret_l. - reflexivity. -Qed. End BranchBindEquations. diff --git a/theories/Eq/Trace.v b/theories/Eq/Trace.v index c29693c2..a0ad256a 100644 --- a/theories/Eq/Trace.v +++ b/theories/Eq/Trace.v @@ -46,14 +46,6 @@ Definition traceq {E C D X Y} Instances |*) -#[global] Instance htr_equ {E C X} (R : trace -> ctree E C X -> Prop) s : - Proper (equ eq ==> impl) (@htr E C X R s). -Proof. - intros t u EQ H; destruct s; cbn in *; auto. - destruct H as (t' & TR & HR). - exists t'; split; [now rewrite <- EQ | exact HR]. -Qed. - #[global] Instance traceq_equ : forall {E C X} s, Proper (equ eq ==> impl) (@has_trace E C X s). Proof. diff --git a/theories/Eq/Trans.v b/theories/Eq/Trans.v index e3403a24..f2bae7de 100644 --- a/theories/Eq/Trans.v +++ b/theories/Eq/Trans.v @@ -300,27 +300,21 @@ Elimination rules for [trans] |*) Lemma trans_etrans l: trans l ≦ etrans l. Proof. - unfold etrans; destruct l; cbn; intros p q step; try exact step. - now left. + unfold etrans; case l; ka. Qed. Lemma etrans_wtrans l: etrans l ≦ wtrans l. Proof. - unfold wtrans. rewrite <- dot1x at 1; rewrite <- dotx1 at 1. - apply dot_leq; [apply dot_leq; [apply str_refl | reflexivity] | apply str_refl]. + unfold wtrans; ka. Qed. Lemma trans_wtrans l: trans l ≦ wtrans l. Proof. rewrite trans_etrans. apply etrans_wtrans. Qed. Lemma τtrans_wtrans : τtrans ≦ wtrans τ. Proof. - unfold τtrans, wtrans, etrans. rewrite itr_str_l. - etransitivity; [apply str_cons |]. - rewrite <- dotx1 at 1; rewrite <- dotx1 at 1. - apply dot_leq; [apply dot_leq; [reflexivity | apply leq_xcup; right; reflexivity] | apply str_refl]. + unfold τtrans, wtrans, etrans; ka. Qed. Lemma pwtrans_wtrans l : pwtrans l ≦ wtrans l. Proof. - unfold pwtrans, wtrans. - apply dot_leq; [apply dot_leq; [reflexivity | apply trans_etrans] | reflexivity]. + unfold pwtrans, wtrans, etrans; case l; ka. Qed. Lemma trans_etrans_ l: forall p p', trans l p p' -> etrans l p p'. @@ -342,45 +336,35 @@ Elimination rules for [trans] Lemma wcons l: forall p p' p'', trans τ p p' -> wtrans l p' p'' -> wtrans l p p''. Proof. assert ((trans τ: srel SS SS) ⋅ wtrans l ≦ wtrans l) as H - by (unfold wtrans; rewrite 2 dotA, str_cons; reflexivity). + by (unfold wtrans; ka). intros. apply H. eexists; eassumption. Qed. Lemma wsnoc l: forall p p' p'', wtrans l p p' -> trans τ p' p'' -> wtrans l p p''. Proof. assert (wtrans l ⋅ trans τ ≦ wtrans l) as H - by (unfold wtrans; rewrite <- dotA, str_snoc; reflexivity). + by (unfold wtrans; ka). intros. apply H. eexists; eassumption. Qed. - Lemma wtrans_τ: wtrans τ ≡ (trans τ)^*. - Proof. - unfold wtrans, etrans. - rewrite <- dotA, dotplsx, dot1x, - (proj1 (leq_iff_cup _ _) (str_cons (trans τ))), str_trans. - reflexivity. - Qed. Lemma wconss l: forall p p' p'', wtrans τ p p' -> wtrans l p' p'' -> wtrans l p p''. Proof. - assert (wtrans τ ⋅ wtrans l ≦ wtrans l) as H. - { rewrite wtrans_τ. apply str_ind_l. - unfold wtrans; rewrite 2 dotA, str_cons; reflexivity. } + assert (wtrans τ ⋅ wtrans l ≦ wtrans l) as H by (unfold wtrans, etrans; ka). intros. apply H. eexists; eassumption. Qed. Lemma wsnocs l: forall p p' p'', wtrans l p p' -> wtrans τ p' p'' -> wtrans l p p''. Proof. - assert (wtrans l ⋅ wtrans τ ≦ wtrans l) as H. - { rewrite wtrans_τ. apply str_ind_r. - unfold wtrans; rewrite <- dotA, str_snoc; reflexivity. } + assert (wtrans l ⋅ wtrans τ ≦ wtrans l) as H by (unfold wtrans, etrans; ka). intros. apply H. eexists; eassumption. Qed. + Lemma wtrans_τ: wtrans τ ≡ (trans τ)^*. + Proof. + unfold wtrans, etrans. ka. + Qed. Lemma pwtrans_τ: pwtrans τ ≡ (trans τ)^+. Proof. - unfold pwtrans. - rewrite <- itr_str_r. - rewrite !itr_str_l, <- dotA, str_trans. - reflexivity. + unfold pwtrans, etrans. ka. Qed. #[global] Instance PreOrder_wtrans_τ: PreOrder (wtrans τ). @@ -487,14 +471,11 @@ End backward. Section BackwardBounded. - Context {E : Type -> Type}. - Context {B : Type -> Type}. - Context {X : Type}. + Context {E B : Type -> Type} {X : Type}. Context `{B2 -< B}. Context `{B3 -< B}. Context `{B4 -< B}. - Variable (l : @label E). - Variable (t t' u u' v v' w w' : ctree E B X). + Variable (l : @label E) (t t' u u' v v' w w' : ctree E B X). Lemma trans_brS21 : trans τ (brS2 t u) t. diff --git a/theories/Eq/WBisim.v b/theories/Eq/WBisim.v index 5d2c7033..1ee732c2 100644 --- a/theories/Eq/WBisim.v +++ b/theories/Eq/WBisim.v @@ -59,7 +59,6 @@ Import CTree. Import CTreeNotations. Import EquNotations. Import SBisimNotations. -Set Universe Polymorphism. (*| Weak Bisimulation @@ -378,24 +377,24 @@ on the setoid side. unfold wtrans, etrans. ka. Qed. - Lemma cnv_wt (R : Chain wb) : cnv _ _ (elem R: hrel _ _) ≡ elem R. + Lemma cnv_wt (R : Chain wb) : (elem R: hrel _ _)^° ≡ elem R. Proof. apply RelationAlgebra.lattice.antisym; intros ???; apply sym_t,H. Qed. - Lemma cnv_gfp: RelationAlgebra.lattice.weq (cnv _ _ (gfp wb: hrel _ _)) (gfp wb). + Lemma cnv_gfp: RelationAlgebra.lattice.weq ((gfp wb: hrel _ _)^°) (gfp wb). Proof. apply cnv_wt. Qed. - Lemma cnv_wbisim: cnv _ _ wbisimT ≡ wbisimT. + Lemma cnv_wbisim: wbisimT^° ≡ wbisimT. Proof. apply cnv_wt. Qed. - Lemma cnv_wbisim': cnv _ _ wbisim ≡ wbisim. + Lemma cnv_wbisim': wbisim^° ≡ wbisim. Proof. apply cnv_wt. Qed. (*| By symmetry, similar results for left-to-right game |*) - Lemma wbisim_trans_front l: cnv _ _ (trans l) ⋅ wbisimT ≦ wbisimT ⋅ cnv _ _ (wtrans l). + Lemma wbisim_trans_front l: (trans l)^° ⋅ wbisimT ≦ wbisimT ⋅ (wtrans l)^°. Proof. cnv_switch. rewrite 2cnvdot, cnv_invol, cnv_wbisim. apply wbisim_trans_back. Qed. - Lemma wbisim_etrans_front l: cnv _ _ (etrans l) ⋅ wbisimT ≦ wbisimT ⋅ cnv _ _ (wtrans l). + Lemma wbisim_etrans_front l: (etrans l)^° ⋅ wbisimT ≦ wbisimT ⋅ (wtrans l)^°. Proof. cnv_switch. rewrite 2cnvdot, cnv_invol, cnv_wbisim. apply wbisim_etrans_back. Qed. - Lemma wbisim_wtrans_front l: cnv _ _ (wtrans l) ⋅ wbisimT ≦ wbisimT ⋅ cnv _ _ (wtrans l). + Lemma wbisim_wtrans_front l: (wtrans l)^° ⋅ wbisimT ≦ wbisimT ⋅ (wtrans l)^°. Proof. cnv_switch. rewrite 2cnvdot, cnv_invol, cnv_wbisim. apply wbisim_wtrans_back. Qed. (*| diff --git a/theories/Interp/FoldCTree.v b/theories/Interp/FoldCTree.v index 3b18138a..6068dc3c 100644 --- a/theories/Interp/FoldCTree.v +++ b/theories/Interp/FoldCTree.v @@ -43,9 +43,9 @@ Section FoldCTree. (** ** [interpE] and constructors *) - Definition fold_ctree : forall [T : Type], - @ctree@{_ _ _ _ d q} E C T -> - @ctree@{_ _ _ _ d' q'} F D T := fold h g. + Definition fold_ctree : + @ctree@{_ _ _ _ d q} E C ~> @ctree@{_ _ _ _ d' q'} F D := fold h g. + Arguments fold_ctree [T] _. (* fold (mstuck (M := ctree F D)) (mstep (M := ctree F D)) h (mbr (M := ctree F D)) g. *) (* fold (fun T => Stuck: ctree F D T) (Step (Ret tt)) h g. *) @@ -378,7 +378,7 @@ Module CounterExample. Section Handler. Universes d q. - #[local] Definition h : forall T, VoidE T -> @ctree@{_ _ _ _ d q} VoidE B2 T := + #[local] Definition h : VoidE ~> @ctree@{_ _ _ _ d q} VoidE B2 := fun _ e => match e with voidE => Step Stuck end. diff --git a/theories/Interp/FoldStateT.v b/theories/Interp/FoldStateT.v index d8706e9e..94f20d4d 100644 --- a/theories/Interp/FoldStateT.v +++ b/theories/Interp/FoldStateT.v @@ -90,9 +90,8 @@ Section State. fun _ c s => (x <- CTree.branch c;; Ret (s, x))%ctree. Definition run_state {E C} : - forall T : Type, - @ctree@{_ _ _ _ d q} (stateE +' E) C T -> - stateT S (@ctree@{_ _ _ _ d' q'} E C) T := + @ctree@{_ _ _ _ d q} (stateE +' E) C ~> + stateT S (@ctree@{_ _ _ _ d' q'} E C) := fold_state (case_sum1 h_state pure_state) pure_state_choice. End State. @@ -617,11 +616,9 @@ Proof. + red. reflexivity. + eapply weq_ssim. apply update_val_rel_update_val_rel. now apply Hh. + cbn. intros [] [] [? <-]. apply ssim_ret. constructor; cbn; auto. - - rewrite !bind_map, !bind_bind. - unfold mbr, MonadBr_stateT, MonadBr_ctree. - cbn -[CTree.branch CTree.bind]. - rewrite !bind_branch. - apply ssim_br_id; intros ?; rewrite !bind_ret_l; cbn. + - rewrite !bind_map, !bind_bind. setoid_rewrite bind_branch. + cbn. + apply ssim_br_id; intros ?; rewrite ?bind_ret_l. apply ssim_ret; constructor; cbn; auto. Qed. @@ -631,7 +628,7 @@ Context {E : Type -> Type} {F : Type -> Type} {C : Type -> Type}. Variable h : E ~> @ctree@{_ _ _ _ d q} F C. Definition lift_handler : - forall T, E T -> Monads.stateT unit (@ctree@{_ _ _ _ d q} F C) T := + E ~> Monads.stateT unit (@ctree@{_ _ _ _ d q} F C) := fun _ e s => CTree.map (fun x => (tt, x)) (h e). @@ -891,15 +888,12 @@ Proof. eauto. * constructor; auto. - (* Br *) - unfold MonadBr_stateT, mbr, MonadBr_ctree. - cbn -[CTree.branch CTree.bind]. rewrite bind_bind, bind_branch. - setoid_rewrite bind_ret_l. + unfold MonadBr_stateT, mbr, MonadBr_ctree. cbn. rewrite bind_bind, bind_branch. unshelve eapply step_ss'_br_l. apply equ_clos_sst'_ctx. intros. eapply ssim_br_l_inv in SIM. - fold (interp_state h u st). - step. apply step_ss'_guard_l. + step. rewrite bind_ret_l. apply step_ss'_guard_l. apply CH. apply SIM. Qed. @@ -1020,12 +1014,11 @@ Proof. apply step_sb'_guard. apply CH. symmetry in SIM. step in SIM. apply SIM. * right; auto. - (* Br *) - unfold MonadBr_stateT, mbr, MonadBr_ctree. - cbn -[RelProd CTree.branch CTree.bind]. rewrite bind_bind, bind_branch. + unfold MonadBr_stateT, mbr, MonadBr_ctree. cbn -[RelProd]. rewrite bind_bind, bind_branch. apply step_sb'_true_br_l. intros. eapply ss_br_l_inv in SIM. - step. rewrite !bind_ret_l. + step. rewrite bind_ret_l. apply step_sb'_true_guard_l. cbn. apply CH. apply SIM. Unshelve. diff --git a/theories/Interp/ITree.v b/theories/Interp/ITree.v index 98c84d64..08837c89 100644 --- a/theories/Interp/ITree.v +++ b/theories/Interp/ITree.v @@ -6,7 +6,7 @@ From CTree Require Import From ITree Require Import - ITree Eq Interp. + ITree Eq Interp InterpFacts. From Stdlib Require Import Morphisms Program. @@ -86,20 +86,21 @@ End ITreeInterp. #[global] Instance embed_eq {E C X}: Proper (eq_itree eq ==> equ eq) (@embed E C X). Proof. - unfold Proper, respectful. - coinduction r CIH. - intros t u bisim. unfold embed, embed', internalize. + unfold Proper, respectful. + coinduction r CIH. + intros t u bisim. unfold embed, embed', internalize. rewrite 2 unfold_interp_ctree. - punfold bisim. - inv bisim; pclearbot; try discriminate; cbn [_interp h_embed]. - - reflexivity. - - rewrite 2 FoldCTree.interp_guard. + rewrite 2 FoldCTree.unfold_interp. + punfold bisim. + inv bisim; pclearbot; try easy. + - cbn. constructor. now apply CIH. - - rewrite 2 FoldCTree.interp_bind. + - cbn. apply fequ_bind_chain_eq; intros. - setoid_rewrite FoldCTree.interp_guard. - constructor. + rewrite 2 FoldCTree.unfold_interp. + cbn; constructor. + step; cbn; constructor. apply CIH, REL. Qed. @@ -137,18 +138,29 @@ Notation embed_ t := Lemma unfold_embed {E C X} (t : itree (C +' E) X) : (embed t ≅ embed_ t)%ctree. Proof. unfold embed, embed', internalize at 1. - rewrite unfold_interp_ctree. - destruct (iobserve t) eqn:EQ; cbn [_interp h_embed]. - - rewrite FoldCTree.interp_ret; reflexivity. - - rewrite FoldCTree.interp_guard; reflexivity. - - rewrite FoldCTree.interp_bind, FoldCTree.interp_trigger, Equ.bind_bind. - setoid_rewrite Equ.bind_guard. - setoid_rewrite Equ.bind_ret_l. - setoid_rewrite FoldCTree.interp_guard. - destruct e; unfold internalize_h', internalize_h; - cbn -[CTree.trigger CTree.branchS CTree.bind]. - + rewrite Equ.bind_branchS; reflexivity. - + rewrite Equ.bind_trigger; reflexivity. + rewrite unfold_interp_ctree, FoldCTree.unfold_interp. + cbn. + destruct (iobserve t) eqn:EQ; cbn; auto. + - destruct e. + + cbn. + rewrite Equ.unfold_bind at 1. + cbn. + step; cbn; constructor; intros ?. + rewrite Equ.bind_step. + step; cbn; constructor. + rewrite Equ.bind_ret_l. + step; cbn; constructor. + step; cbn; constructor. + reflexivity. + + cbn. + rewrite Equ.unfold_bind at 1. + cbn. + step; cbn; constructor; intros ?. + rewrite Equ.bind_ret_l. + step; cbn; constructor. + rewrite FoldCTree.unfold_interp; cbn. + step; cbn; constructor. + reflexivity. Qed. (* TODO THIS IS REDUNDANT WITH THE DEF IN FOLDCTREE! *) diff --git a/theories/Interp/Internalize.v b/theories/Interp/Internalize.v index 5e208d58..729c6bff 100644 --- a/theories/Interp/Internalize.v +++ b/theories/Interp/Internalize.v @@ -29,7 +29,7 @@ Section Internalize. Lemma internalize_ret {R} (r : R) : internalize (Ret r) ≅ Ret r. Proof. unfold internalize. - rewrite FoldCTree.interp_ret. + rewrite interp_ret. reflexivity. Qed. @@ -37,7 +37,7 @@ Section Internalize. internalize (t >>= k) ≅ internalize t >>= (fun x => internalize (k x)). Proof. unfold internalize. - rewrite FoldCTree.interp_bind. + rewrite interp_bind. reflexivity. Qed. diff --git a/theories/Interp/RecursionFacts.v b/theories/Interp/RecursionFacts.v index 04c93e3f..8b19d39f 100644 --- a/theories/Interp/RecursionFacts.v +++ b/theories/Interp/RecursionFacts.v @@ -193,48 +193,66 @@ Proof. red. revert_until T. coinduction R CIH. intros. - rewrite unfold_interp_mrec. unfold _interp_mrec. - rewrite FoldCTree.unfold_interp. + rewrite unfold_interp_mrec. unfold _interp_mrec, fold. + unfold interp, fold. + setoid_rewrite unfold_iter. destruct (observe c). - - apply step_sb'_guard_r. + - unfold ret, Monad_ctree. + apply step_sb'_guard_r. + rewrite bind_ret_l. reflexivity. - - apply step_sb'_guard_r. + - unfold mstuck, MonadStuck_ctree. rewrite bind_stuck. + apply step_sb'_guard_r. reflexivity. - - apply step_sb'_guard_r. + - 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. - - apply step_sb'_guard. + - unfold ret, Monad_ctree. rewrite bind_ret_l. + apply step_sb'_guard. apply CIH. - destruct e. - + cbn. + + unfold mrecursive, case_, Case_sum1, case_sum1. + unfold fmap at 1, Functor_ctree at 1. + rewrite bind_map. apply step_sb'_guard. - change ((elem R) side (interp_mrec ctx (ctx _ d >>= k)) - (x <- mrec ctx d;; Guard (interp (mrecursive ctx) (k x)))). - setoid_rewrite (interp_mrec_bind (ctx _ d) k). + rewrite interp_mrec_bind. apply st'_clo_bind_eq. reflexivity. intros. apply CIH. - + cbn -[CTree.trigger CTree.bind]. + + 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. - eapply (@equ_sb'_goal _ _ _ _ _ _ _ _ side); [reflexivity | |]. - { cbn -[CTree.trigger CTree.bind]; rewrite bind_trigger; reflexivity. } apply step_sb'_vis_id. intros. split; auto. intros. apply step_sb'_guard_l'. intros. apply CIH. - apply step_sb'_guard_r. - eapply (@equ_sb'_goal _ _ _ _ _ _ _ _ side); [reflexivity | |]. - { unfold mbr, MonadBr_ctree; cbn -[CTree.branch CTree.bind]; apply Equ.bind_branch. } - apply step_sb'_br_id. + 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. +Qed. Theorem mrec_as_interp {T} (d : D T) : @@ -264,7 +282,7 @@ Qed. Lemma interp_mrecursive {T} (d : D T) : interp (mrecursive ctx) (@trigger_inl1 D E B _ d) ~ mrec ctx d. Proof. - unfold trigger_inl1. + unfold mrecursive. unfold trigger_inl1. rewrite interp_trigger. cbn. setoid_rewrite sb_guard. diff --git a/theories/Interp/Refine.v b/theories/Interp/Refine.v index 9e4239d7..f82cce60 100644 --- a/theories/Interp/Refine.v +++ b/theories/Interp/Refine.v @@ -39,23 +39,20 @@ Theorem refine_ctree_ssim {E B B' X} : Proof. intros. rewrite ssim_ssim'. red. revert t. coinduction R CH. intros. rewrite (ctree_eta t) at 2. - setoid_rewrite unfold_refine. - cbn -[CTree.trigger]. + setoid_rewrite unfold_refine. cbn. destruct (observe t) eqn:?. - apply step_ssbt'_ret. reflexivity. - apply step_ss'_stuck. - apply step_ss'_step; auto. step. now apply step_ss'_guard_l. - now apply step_ss'_guard. - - unfold mtrigger, MonadTrigger_ctree. - cbn -[CTree.trigger]. rewrite bind_trigger. + - setoid_rewrite bind_trigger. apply step_ss'_vis_id. intros. split; [|auto]. step. apply step_ss'_guard_l. apply CH. - change (Br c k) with ((fun _ => Br c k) tt). setoid_rewrite <- bind_ret_l at 6. eapply ss'_clo_bind with (R0 := (fun _ _ => True)). - { eapply (@ssim_pure E E B' B X0 _ (h X0 c)). - apply H. intros. now constructor. } + { apply ssim_pure. apply H. intros. now constructor. } intros ? _ _. cbn. apply step_ss'_br_r with (x := x). apply step_ss'_guard_l. apply CH. @@ -71,8 +68,7 @@ Theorem refine_state_ssim {E B B' X St} : Proof. intros. rewrite ssim_ssim'. red. revert t s. coinduction R CH. intros. rewrite (ctree_eta t) at 2. - setoid_rewrite unfold_refine_state. - cbn -[CTree.trigger]. + setoid_rewrite unfold_refine_state. cbn. destruct (observe t) eqn:?. - apply step_ssbt'_ret. constructor. reflexivity. - apply step_ss'_stuck. @@ -81,9 +77,7 @@ Proof. step. apply step_ss'_guard_l. apply CH. - apply step_ss'_guard. apply CH. - - unfold mtrigger, MonadTrigger_stateT, MonadTrigger_ctree. - cbn -[CTree.trigger]. - rewrite ?bind_bind, bind_trigger, ?bind_ret_l. cbn. + - setoid_rewrite bind_trigger. apply step_ss'_vis_id. intros. split; [| constructor; etrans]. step. apply step_ss'_guard_l. apply CH. - change (Br c k) with ((fun _ => Br c k) tt). From 85e732f80652db00a34de28dcf79fa08ae26dfc6 Mon Sep 17 00:00:00 2001 From: Lef Ioannidis Date: Fri, 16 Oct 2026 17:11:19 -0700 Subject: [PATCH 5/6] Fix Nix CI with supported Rocq 9.2 dependencies Align Nix with the passing Docker toolchain and pin coinduction v1.22 and relation-algebra v1.9.1. Update the declared compiler minimum and README to Rocq 9.2. The former Rocq 9.0 dependency combination fails a universe-checked RelationAlgebra/ITree facts import without loading any CTree code. The repaired dependency import and exact Nix package build pass locally; the Rocq 9.3 build, UniverseCheck, and ImpBr consumer also pass. --- README.md | 2 +- dune-project | 2 +- flake.lock | 14 ++++++++------ flake.nix | 12 ++++++------ 4 files changed, 16 insertions(+), 14 deletions(-) diff --git a/README.md b/README.md index d1277a8e..c3331b32 100644 --- a/README.md +++ b/README.md @@ -14,7 +14,7 @@ We develop a cousin of Interaction Trees, dubbed _Choice Trees_, with native sup - Yannick Zakowski - Steve Zdancewic - License: MIT License -- Compatible Rocq versions: 9.0 +- Compatible Rocq versions: 9.2 - Additional dependencies: - dune - [Extlib](https://github.com/coq-community/coq-ext-lib) diff --git a/dune-project b/dune-project index e8512663..af151e9d 100644 --- a/dune-project +++ b/dune-project @@ -15,7 +15,7 @@ (synopsis "Library for representing recursive, non-deterministic and impure programs with equational reasoning") (version 2.0-dev) (depends - (rocq-core (>= 9.0)) + (rocq-core (>= 9.2)) (rocq-stdlib (>= 9.0)) (coq-ext-lib (>= 0.11.3)) (rocq-coinduction (>= 1.21)) diff --git a/flake.lock b/flake.lock index 04d42d4f..5693948a 100644 --- a/flake.lock +++ b/flake.lock @@ -3,15 +3,16 @@ "coinduction-repo": { "flake": false, "locked": { - "lastModified": 1758090858, - "narHash": "sha256-S/stL5bpJsJt+bvOg4F2b/WaEt5IDOop3ruBIbde9GI=", + "lastModified": 1778079929, + "narHash": "sha256-ndGFgtFtqlfVpddyQDT9zSem218uJTqlLqI1wP38LSg=", "owner": "damien-pous", "repo": "coinduction", - "rev": "a88f0f4f170dcb9b24e3d470c76801a765423598", + "rev": "81ecd5f1ffa3e46b696d9461c88ad6ca9be5cfc7", "type": "github" }, "original": { "owner": "damien-pous", + "ref": "v1.22", "repo": "coinduction", "type": "github" } @@ -68,15 +69,16 @@ "relation-algebra-repo": { "flake": false, "locked": { - "lastModified": 1758092026, - "narHash": "sha256-RnY+a57KnStACteaT5dKQoCCH0qp7/W+4qoaApIilj0=", + "lastModified": 1789980351, + "narHash": "sha256-SnSEdPajAcIgUzL0VKERXg6i+Lg2yJbNQYoJGNyfVYE=", "owner": "damien-pous", "repo": "relation-algebra", - "rev": "062d5cf9468ce367fe11220b336dff254a51702b", + "rev": "a6eb2b0dd62f0df2d198159176e5b28aa9643dae", "type": "github" }, "original": { "owner": "damien-pous", + "ref": "v1.9.1", "repo": "relation-algebra", "type": "github" } diff --git a/flake.nix b/flake.nix index 2f63088a..a2906ebb 100644 --- a/flake.nix +++ b/flake.nix @@ -6,11 +6,11 @@ flake-utils.url = "github:numtide/flake-utils"; nix-filter.url = "github:numtide/nix-filter"; coinduction-repo = { - url = "github:damien-pous/coinduction"; + url = "github:damien-pous/coinduction/v1.22"; flake = false; }; relation-algebra-repo = { - url = "github:damien-pous/relation-algebra"; + url = "github:damien-pous/relation-algebra/v1.9.1"; flake = false; }; }; @@ -20,8 +20,8 @@ let pkgs = import nixpkgs { inherit system; }; lib = pkgs.lib; - rocqPkgs = pkgs.rocqPackages_9_0; - coqPkgs = pkgs.coqPackages_9_0; + rocqPkgs = pkgs.rocqPackages_9_2; + coqPkgs = pkgs.coqPackages_9_2; rocq = rocqPkgs.rocq-core; coinduction = rocqPkgs.callPackage @@ -29,7 +29,7 @@ rocqPkgs.mkRocqDerivation { owner = "damien-pous"; pname = "coinduction"; - version = "coinduction:master"; + version = "1.22"; src = coinduction-repo; buildInputs = @@ -49,7 +49,7 @@ rocqPkgs.mkRocqDerivation { owner = "damien-pous"; pname = "relation-algebra"; - version = "relation-algebra:master"; + version = "1.9.1"; src = relation-algebra-repo; buildInputs = From 748a4882e3d14d123c06094d06655fd1e369c659 Mon Sep 17 00:00:00 2001 From: Lef Ioannidis Date: Fri, 16 Oct 2026 17:59:30 -0700 Subject: [PATCH 6/6] Require RelationAlgebra 1.9.0 for converse notation --- dune-project | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dune-project b/dune-project index af151e9d..25a6fe5a 100644 --- a/dune-project +++ b/dune-project @@ -19,7 +19,7 @@ (rocq-stdlib (>= 9.0)) (coq-ext-lib (>= 0.11.3)) (rocq-coinduction (>= 1.21)) - (rocq-relation-algebra (>= 1.8.0)) + (rocq-relation-algebra (>= 1.9.0)) (rocq-equations (>= 1.3.1)) (coq-itree (>= 5.0))) (tags (