Splitting system calls into two transitions

.gitignore

@@ -4,3 +4,4 @@ _build
 *~
 .lia.cache
 .aux
+rocq-ctree.opam

examples/AltBisim/BisimExample.v

@@ -1,4 +1,4 @@
-From CTree Require Import CTree Eq Eq.SBisimAlt Eq.IterFacts.
+From CTree Require Import CTree Eq Eq.SBisimAlt Eq.OldAltEquiv.TransEquiv Eq.OldAltEquiv.SBisimEquiv Eq.IterFacts.
 
 Import CoindNotations.
 Import CTreeNotations.
@@ -18,37 +18,36 @@ Proof. step. cbn. reflexivity. Qed.
 Lemma unfold_u : u ≅ br2 (trigger (print true);; u) u.
 Proof. step. cbn. reflexivity. Qed.
 
-Theorem bisim_t_u : t ~ u.
+Theorem bisim_t_u : t ≃ u.
 Proof.
   coinduction R CH.
   rewrite unfold_t, unfold_u.
-  apply step_sb_br; intros [].
+  apply sb_br; intros [].
   2: {
     exists true.
     rewrite !bind_trigger.
-    apply step_sb_vis_id. intros [].
-    split; [| auto].
-    apply CH.
+    apply sb_vis_id; [constructor |]. intros [].
+    split; [apply CH | constructor].
   }
   {
     exists false.
-    Fail apply CH.
+    Fail apply CH. 
 Abort.
 
-Theorem bisim_t_u : t ~ u.
+Theorem bisim_t_u : t ≃ u.
 Proof.
   (* We switch to the alternative characterization of bisimulation. *)
-  rewrite sbisim_sbisim'.
+  unfold sbisimT; rewrite sbisim_sbisim'.
   (* The rest of the proof proceeds as before, but this time it succeeds. *)
   coinduction R CH. intros.
-  rewrite unfold_t, unfold_u.
+  cbn [TransEquiv.o2n_S]. rewrite unfold_t, unfold_u.
   apply step_sb'_br; intros [].
   (* Notice that unlike step_sb_br, step_sb'_br has unlocked the coinduction hypothesis. *)
   2: {
     exists true.
     rewrite !bind_trigger.
-    step. apply step_sb'_vis_id. intros [].
-    split; [| auto].
+    step. apply step_sb'_vis_id; [| constructor; constructor]. intros.
+    apply (b_chain R). apply step_sb'_passive_id; [| constructor; constructor]. intros ? [].
     apply CH.
   }
   {
@@ -59,8 +58,8 @@ Proof.
   {
     exists false.
     rewrite !bind_trigger.
-    step. apply step_sb'_vis_id. intros [].
-    split; [| auto].
+    step. apply step_sb'_vis_id; [| constructor; constructor]. intros.
+    apply (b_chain R). apply step_sb'_passive_id; [| constructor; constructor]. intros ? [].
     apply CH.
   }
   {
@@ -78,7 +77,7 @@ Definition t' : ctree PrintE B2 void :=
 Definition u' : ctree PrintE B2 void :=
   CTree.iter (fun _ => br2 (trigger (print true);; Ret (inl tt)) (Ret (inl tt))) tt.
 
-Theorem bisim_t'_u'_simple : t' ~ u'.
+Theorem bisim_t'_u'_simple : t' ≃ u'.
 Proof.
   unfold t', u'.
   apply sbisim_eq_iter. intros _.

examples/CCS/Denotation.v

@@ -1063,25 +1063,25 @@ Qed.
 
 Section Theory.
 
-  Lemma plsC: forall (p q : ccs), p+q ~ q+p.
+  Lemma plsC: forall (p q : ccs), p+q ≃ q+p.
   Proof.
     apply br2_commut.
   Qed.
 
-  Lemma plsA (p q r : ccs): p+(q+r) ~ (p+q)+r.
+  Lemma plsA (p q r : ccs): p+(q+r) ≃ (p+q)+r.
   Proof.
     symmetry; apply br2_assoc.
   Qed.
 
-  Lemma pls0p (p : ccs) : 0 + p ~ p.
+  Lemma pls0p (p : ccs) : 0 + p ≃ p.
   Proof.
     apply br2_stuck_l.
   Qed.
 
-  Lemma plsp0 (p : ccs) : p + 0 ~ p.
+  Lemma plsp0 (p : ccs) : p + 0 ≃ p.
   Proof. now rewrite plsC, pls0p. Qed.
 
-  Lemma plsidem (p : ccs) : p + p ~ p.
+  Lemma plsidem (p : ccs) : p + p ≃ p.
   Proof.
     apply br2_idem.
   Qed.
@@ -1093,7 +1093,7 @@ Section Theory.
     all:rewrite eqb_sym; auto.
   Qed.
 
-  Lemma paraC: forall (p q : ccs), p ∥ q ~ q ∥ p.
+  Lemma paraC: forall (p q : ccs), p ∥ q ≃ q ∥ p.
   Proof.
     coinduction r CIH; symmetric.
     intros p q ? ? tr.
@@ -1113,7 +1113,7 @@ Section Theory.
       reflexivity.
   Qed.
 
-  Lemma para0p : forall (p : ccs), 0 ∥ p ~ p.
+  Lemma para0p : forall (p : ccs), 0 ∥ p ≃ p.
   Proof.
     coinduction R CIH.
     intros.
@@ -1130,12 +1130,12 @@ Section Theory.
       cbn; auto.
   Qed.
 
-  Lemma parap0 : forall (p : ccs), p ∥ 0 ~ p.
+  Lemma parap0 : forall (p : ccs), p ∥ 0 ≃ p.
   Proof.
     intros; rewrite paraC; apply para0p.
   Qed.
 
-  Lemma paraA : forall (p q r : ccs), p ∥ (q ∥ r) ~ (p ∥ q) ∥ r.
+  Lemma paraA : forall (p q r : ccs), p ∥ (q ∥ r) ≃ (p ∥ q) ∥ r.
   Proof.
     coinduction r CIH; intros.
     split.
@@ -1194,7 +1194,7 @@ Section Theory.
 End Theory.
 
 Lemma para_parabang : forall p q r,
-    parabang (p ∥ q) r ~ p ∥ parabang q r.
+    parabang (p ∥ q) r ≃ p ∥ parabang q r.
 Proof.
   coinduction R CIH.
   intros; split.
@@ -1310,7 +1310,7 @@ Proof.
 Qed.
 
 Lemma parabang_aux : forall p q,
-    parabang (p ∥ q) q ~ parabang p q.
+    parabang (p ∥ q) q ≃ parabang p q.
 Proof.
   coinduction R CIH.
   split.
@@ -1381,7 +1381,7 @@ Proof.
 Qed.
 
 Lemma parabang_eq : forall p q,
-    parabang p q ~ p ∥ !q.
+    parabang p q ≃ p ∥ !q.
 Proof.
   coinduction R CIH.
   intros p q; split.
@@ -1451,7 +1451,7 @@ Proof.
 Qed.
 
 Lemma unfold_bang' : forall p,
-    !p ~ !p ∥ p.
+    !p ≃ !p ∥ p.
 Proof.
   intros; unfold bang at 1.
   rewrite parabang_eq. rewrite paraC; reflexivity.

examples/CCS/OpDenot.v

@@ -103,7 +103,7 @@ Proof.
     exists R; split; auto.
 Qed.
 
-Definition bisim_model := fun P (q: ccs) => ⟦P⟧ ~ q.
+Definition bisim_model := fun P (q: ccs) => ⟦P⟧ ≃ q.
 
 Lemma complete : forward bisim_model.
 Proof.
@@ -321,7 +321,7 @@ Lemma cross_model_compose : forall T t u U,
     bisimilar t T ->
     Operational.bisim t u ->
     bisimilar u U ->
-    T ~ U.
+    T ≃ U.
 Proof.
   coinduction r cih.
   intros * EQtT EQtu EQuU.
@@ -343,7 +343,7 @@ Qed.
 
 Lemma cross_model_compose' : forall T t u U,
     bisimilar t T ->
-    T ~ U ->
+    T ≃ U ->
     bisimilar u U ->
     Operational.bisim t u.
 Proof.
@@ -373,7 +373,7 @@ Proof.
   red; intros; edestruct F; eauto.
 Qed.
 
-Lemma embed_sound : forall t u, Operational.bisim t u -> ⟦t⟧ ~ ⟦u⟧.
+Lemma embed_sound : forall t u, Operational.bisim t u -> ⟦t⟧ ≃ ⟦u⟧.
 Proof.
   intros * BIS.
   apply (gfp_fp b t u) in BIS; destruct BIS as [F B]; cbn in *.
@@ -402,7 +402,7 @@ Proof.
     eapply cross_model_compose; eauto.
 Qed.
 
-Lemma embed_complete : forall t u, ⟦t⟧ ~ ⟦u⟧ -> Operational.bisim t u.
+Lemma embed_complete : forall t u, ⟦t⟧ ≃ ⟦u⟧ -> Operational.bisim t u.
 Proof.
   intros * BIS.
   step in BIS; destruct BIS as [F B]; cbn in *.
@@ -431,7 +431,7 @@ Proof.
     eapply cross_model_compose'; eauto.
 Qed.
 
-Theorem equiv_bisims : forall t u, ⟦t⟧ ~ ⟦u⟧ <-> Operational.bisim t u.
+Theorem equiv_bisims : forall t u, ⟦t⟧ ≃ ⟦u⟧ <-> Operational.bisim t u.
 Proof.
   intros; split; eauto using embed_complete, embed_sound.
 Qed.

examples/ImpBr/ImpBr.v

@@ -137,41 +137,41 @@ Section Theory.
   at the level of uninterpreted ctrees.
 |*)
   Lemma branch_commut : forall (a b : stmt),
-      ⟦Branch a b⟧ ~ ⟦Branch b a⟧.
+      ⟦Branch a b⟧ ≃ ⟦Branch b a⟧.
   Proof.
     intros; apply br2_commut.
   Qed.
 
   Lemma branch_assoc : forall (a b c : stmt),
-      ⟦Branch a (Branch b c)⟧ ~ ⟦Branch (Branch a b) c⟧.
+      ⟦Branch a (Branch b c)⟧ ≃ ⟦Branch (Branch a b) c⟧.
   Proof.
     intros; cbn.
     now rewrite br2_assoc.
   Qed.
 
   Lemma branch_idem : forall a : stmt,
-      ⟦Branch a a⟧ ~ ⟦a⟧.
+      ⟦Branch a a⟧ ≃ ⟦a⟧.
   Proof.
     intros; apply br2_idem.
   Qed.
 
   Lemma branch_congr : forall a a' b b',
-      ⟦a⟧ ~ ⟦a'⟧ ->
-      ⟦b⟧ ~ ⟦b'⟧ ->
-      ⟦Branch a b⟧ ~ ⟦Branch a' b'⟧.
+      ⟦a⟧ ≃ ⟦a'⟧ ->
+      ⟦b⟧ ≃ ⟦b'⟧ ->
+      ⟦Branch a b⟧ ≃ ⟦Branch a' b'⟧.
   Proof.
-    intros. cbn. apply sb_br_id.
+    intros. cbn. apply sbisim_br_id.
     intro; destruct x; rewrite ?H, ?H0; reflexivity.
   Qed.
 
   Lemma branch_block_l : forall a : stmt,
-      ⟦Branch Block a⟧ ~ ⟦a⟧.
+      ⟦Branch Block a⟧ ≃ ⟦a⟧.
   Proof.
     intros; apply br2_stuck_l.
   Qed.
 
   Lemma branch_block_r : forall a : stmt,
-      ⟦Branch a Block⟧ ~ ⟦a⟧.
+      ⟦Branch a Block⟧ ≃ ⟦a⟧.
   Proof.
     intros; apply br2_stuck_r.
   Qed.
@@ -189,7 +189,7 @@ Section Theory.
   Qed.
 
   Lemma branch_block_r_interp : forall (a : stmt) s,
-    ℑ (Branch a Block) s ~
+    ℑ (Branch a Block) s ≃
     ℑ a s.
   Proof.
     intros.
@@ -222,7 +222,7 @@ from Section 2 are indeed equivalent.
            (Seq
               (Assign "x" (Lit 0))
               (Assign "x" (Lit 1)))
-           Block) s ~
+           Block) s ≃
         ℑ (Assign "x" (Lit 1)) s.
   Proof with (unfold interp_imp).
     intros...

examples/SimpleSim/SimExample.v

@@ -43,27 +43,27 @@ Theorem sim_t_u : t ≲ u.
 Proof.
   coinduction R CH.
   rewrite unfold_t, unfold_u.
-  apply step_ss_br_r with (x := true).
-  apply step_ss_vis_id. intros []. split; auto.
+  apply ss_br_r with (x := true).
+  apply ss_vis_eq. intros [].
   rewrite unfold_u.
-  step. apply step_ss_br_r with (x := false).
-  apply step_ss_vis_id. intros []. split; [| auto].
+  step. apply ss_br_r with (x := false).
+  apply ss_vis_eq. intros [].
   apply CH.
 Qed.
 
-Theorem bisim_u_u' : u ~ u'.
+Theorem bisim_u_u' : u ≃ u'.
 Proof.
   coinduction R CH.
   rewrite unfold_u, unfold_u'.
   unfold br2. rewrite bind_br.
-  apply step_sb_br_id. intros.
+  apply sb_br_id. intros.
   destruct x.
   - rewrite bind_trigger.
-    apply step_sb_vis_id. intros []. split; [| auto].
-    rewrite sb_guard.
+    apply sb_vis_eq. intros [].
+    rewrite sbisim_guard.
     apply CH.
   - rewrite bind_trigger.
-    apply step_sb_vis_id. intros []. split; [| auto].
-    rewrite sb_guard.
+    apply sb_vis_eq. intros [].
+    rewrite sbisim_guard.
     apply CH.
 Qed.