From 9b52923f32463d2a90f5bef75641c344f1fcfe7c Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Tue, 11 Jun 2019 12:02:12 +0200
Subject: [PATCH] Squashed commit of the following:
commit 32f5885b5083c6052251a266b0ec4b6f0cd01bcc
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Tue Jun 11 11:54:32 2019 +0200
Full bump
commit 3fdf913129ee6c1081e947de48e71ca6411f33da
Author: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue Jun 11 11:31:22 2019 +0200
More cleanup.
commit 46be8c0184d5a9e7de42022e389e23df99f73f6d
Author: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon Jun 10 22:50:02 2019 +0200
Some cleanup.
commit 2dc17e2cafc0b33e5ef0d2a6f6862b0938f68b18
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Mon Jun 10 16:33:46 2019 +0200
WIP
commit 9427aa2ddd4fecb49b8e1c02eccc954fdb8af554
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Mon Jun 10 15:02:21 2019 +0200
iRewrite Bug inspection
commit 40393f8800ab1a587f49f9ad479f5dc94b2bf2bc
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Mon Jun 10 14:56:08 2019 +0200
Bumped Iris
commit 660218ca36e148b7270fd0044a2401fa553373d1
Author: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon Jun 3 11:31:11 2019 +0200
Add type.
commit 54214779390c19b1f9c8b293ac26f36efda95f4d
Author: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri May 31 16:24:05 2019 +0200
Coinductive version of stype.
commit b0fe9afb62c21df3b320d7ca13b92b3d60149c3b
Author: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri May 31 13:19:13 2019 +0200
Bump Iris.
---
theories/encodings/auth_excl.v | 12 +-
theories/encodings/branching.v | 12 +-
theories/encodings/channel.v | 8 +-
theories/encodings/stype.v | 382 +++++++++++++--------------------
theories/encodings/stype_enc.v | 4 +-
theories/typing/stype.v | 222 +++++++++++--------
6 files changed, 310 insertions(+), 330 deletions(-)
diff --git a/theories/encodings/auth_excl.v b/theories/encodings/auth_excl.v
index 9aa43fe..1ad6b8a 100644
--- a/theories/encodings/auth_excl.v
+++ b/theories/encodings/auth_excl.v
@@ -12,7 +12,7 @@ Definition auth_exclΣ (F : cFunctor) `{!cFunctorContractive F} : gFunctors :=
#[GFunctor (authRF (optionURF (exclRF F)))].
Instance subG_auth_exclG (F : cFunctor) `{!cFunctorContractive F} {Σ} :
- subG (auth_exclΣ F) Σ → auth_exclG (F (iPreProp Σ)) Σ.
+ subG (auth_exclΣ F) Σ → auth_exclG (F (iPreProp Σ) _) Σ.
Proof. solve_inG. Qed.
Definition to_auth_excl {A : ofeT} (a : A) : option (excl A) :=
@@ -38,11 +38,11 @@ Section auth_excl.
✓ (◠to_auth_excl x ⋅ ◯ to_auth_excl y) -∗ (x ≡ y : iProp Σ).
Proof.
iIntros "Hvalid".
- iDestruct (auth_validI with "Hvalid") as "[Hy Hvalid]"; simpl.
- iDestruct "Hy" as ([z|]) "Hy"; last first.
- - by rewrite left_id right_id_L bi.option_equivI /= excl_equivI.
+ iDestruct (auth_both_validI with "Hvalid") as "[_ [Hle Hvalid]]"; simpl.
+ iDestruct "Hle" as ([z|]) "Hy"; last first.
+ - by rewrite bi.option_equivI /= excl_equivI.
- iRewrite "Hy" in "Hvalid".
- by rewrite left_id uPred.option_validI /= excl_validI /=.
+ by rewrite uPred.option_validI /= excl_validI /=.
Qed.
Lemma excl_eq γ x y :
@@ -64,4 +64,4 @@ Section auth_excl.
eapply exclusive_local_update. done. }
by rewrite own_op.
Qed.
-End auth_excl.
\ No newline at end of file
+End auth_excl.
diff --git a/theories/encodings/branching.v b/theories/encodings/branching.v
index 101b6b2..44a0eb4 100644
--- a/theories/encodings/branching.v
+++ b/theories/encodings/branching.v
@@ -22,20 +22,22 @@ Section DualBranch.
intros Ha Hst1 Hst2.
destruct a1.
- simpl.
- simpl in Ha. rewrite Ha.
+ simpl in Ha. rewrite -Ha.
+ rewrite -(stype_force_eq (dual_stype _)).
constructor.
f_equiv.
f_equiv.
destruct (decode a).
- by destruct b. done.
+ by destruct b. apply is_dual_end.
- simpl.
- simpl in Ha. rewrite Ha.
+ simpl in Ha. rewrite -Ha.
+ rewrite -(stype_force_eq (dual_stype _)).
constructor.
f_equiv.
f_equiv.
destruct (decode a).
- by destruct b.
- done.
+ by destruct b.
+ apply is_dual_end.
Qed.
End DualBranch.
Global Typeclasses Opaque TSB.
diff --git a/theories/encodings/channel.v b/theories/encodings/channel.v
index 5f9e8dd..fa0ed8a 100644
--- a/theories/encodings/channel.v
+++ b/theories/encodings/channel.v
@@ -121,10 +121,10 @@ Section channel.
wp_lam.
wp_apply (lnil_spec with "[//]"); iIntros (ls). wp_alloc l as "Hl".
wp_apply (lnil_spec with "[//]"); iIntros (rs). wp_alloc r as "Hr".
- iMod (own_alloc (â— (to_auth_excl []) â‹… â—¯ (to_auth_excl [])))
- as (lsγ) "[Hls Hls']"; first done.
- iMod (own_alloc (â— (to_auth_excl []) â‹… â—¯ (to_auth_excl [])))
- as (rsγ) "[Hrs Hrs']"; first done.
+ iMod (own_alloc (◠(to_auth_excl []) ⋅ ◯ (to_auth_excl []))) as (lsγ) "[Hls Hls']".
+ { by apply auth_both_valid. }
+ iMod (own_alloc (◠(to_auth_excl []) ⋅ ◯ (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
+ { by apply auth_both_valid. }
iAssert (is_list_ref #l []) with "[Hl]" as "Hl".
{ rewrite /is_list_ref; eauto. }
iAssert (is_list_ref #r []) with "[Hr]" as "Hr".
diff --git a/theories/encodings/stype.v b/theories/encodings/stype.v
index dd4528e..47b9288 100644
--- a/theories/encodings/stype.v
+++ b/theories/encodings/stype.v
@@ -20,28 +20,77 @@ Definition logrelΣ A :=
Instance subG_chanΣ {A Σ} : subG (logrelΣ A) Σ → logrelG A Σ.
Proof. intros [??%subG_auth_exclG]%subG_inv. constructor; apply _. Qed.
-Section stype_interp.
- Context `{!heapG Σ} (N : namespace).
- Context `{!logrelG val Σ}.
+Fixpoint st_eval `{!logrelG val Σ} (vs : list val) (st1 st2 : stype val (iProp Σ)) : iProp Σ :=
+ match vs with
+ | [] => st1 ≡ dual_stype st2
+ | v::vs => match st2 with
+ | TSR Receive P st2 => P v ∗ ▷ st_eval vs st1 (st2 v)
+ | _ => False
+ end
+ end%I.
+Arguments st_eval : simpl nomatch.
- Record st_name := SessionType_name {
- st_c_name : chan_name;
- st_l_name : gname;
- st_r_name : gname
- }.
+Record st_name := STName {
+ st_c_name : chan_name;
+ st_l_name : gname;
+ st_r_name : gname
+}.
+
+Definition to_stype_auth_excl `{!logrelG val Σ} (st : stype val (iProp Σ)) :=
+ to_auth_excl (Next (stype_map iProp_unfold st)).
+
+Definition st_own `{!logrelG val Σ} (γ : st_name) (s : side)
+ (st : stype val (iProp Σ)) : iProp Σ :=
+ own (side_elim s st_l_name st_r_name γ) (◯ to_stype_auth_excl st)%I.
- Definition to_stype_auth_excl (st : stype val (iProp Σ)) :=
- to_auth_excl (Next (stype_map iProp_unfold st)).
+Definition st_ctx `{!logrelG val Σ} (γ : st_name) (s : side)
+ (st : stype val (iProp Σ)) : iProp Σ :=
+ own (side_elim s st_l_name st_r_name γ) (◠to_stype_auth_excl st)%I.
- Definition st_own (γ : st_name) (s : side)
- (st : stype val (iProp Σ)) : iProp Σ :=
- own (side_elim s st_l_name st_r_name γ)
- (â—¯ to_stype_auth_excl st)%I.
+Definition inv_st `{!logrelG val Σ} (γ : st_name) (c : val) : iProp Σ :=
+ (∃ l r stl str,
+ chan_own (st_c_name γ) Left l ∗
+ chan_own (st_c_name γ) Right r ∗
+ st_ctx γ Left stl ∗
+ st_ctx γ Right str ∗
+ ▷ ((⌜r = []⌠∗ st_eval l stl str) ∨
+ (⌜l = []⌠∗ st_eval r str stl)))%I.
- Definition st_ctx (γ : st_name) (s : side)
- (st : stype val (iProp Σ)) : iProp Σ :=
- own (side_elim s st_l_name st_r_name γ)
- (â— to_stype_auth_excl st)%I.
+Definition interp_st `{!logrelG val Σ, !heapG Σ} (N : namespace) (γ : st_name)
+ (c : val) (s : side) (st : stype val (iProp Σ)) : iProp Σ :=
+ (st_own γ s st ∗ is_chan N (st_c_name γ) c ∗ inv N (inv_st γ c))%I.
+Instance: Params (@interp_st) 7.
+
+Notation "⟦ c @ s : st ⟧{ N , γ }" := (interp_st N γ c s st)
+ (at level 10, s at next level, st at next level, γ at next level,
+ format "⟦ c @ s : st ⟧{ N , γ }").
+
+Section stype.
+ Context `{!logrelG val Σ, !heapG Σ} (N : namespace).
+
+ Global Instance st_eval_ne : NonExpansive2 (st_eval vs).
+ Proof.
+ induction vs as [|v vs IH];
+ destruct 2 as [n|[] P1 P2 st1 st2|n [] P1 P2 st1 st2]=> //=.
+ - by repeat f_equiv.
+ - f_equiv. done. f_equiv. by constructor.
+ - f_equiv. done. f_equiv. by constructor.
+ - f_equiv. done. f_equiv. by constructor.
+ - f_equiv. done. f_equiv. by constructor.
+ - f_equiv. done. by f_contractive.
+ - f_equiv. done. f_contractive. apply IH. by apply dist_S. done.
+ Qed.
+ Global Instance st_eval_proper vs : Proper ((≡) ==> (≡) ==> (≡)) (st_eval vs).
+ Proof. apply (ne_proper_2 _). Qed.
+
+ Global Instance to_stype_auth_excl_ne : NonExpansive to_stype_auth_excl.
+ Proof. solve_proper. Qed.
+ Global Instance st_own_ne γ s : NonExpansive (st_own γ s).
+ Proof. solve_proper. Qed.
+ Global Instance interp_st_ne γ c s : NonExpansive (interp_st N γ c s).
+ Proof. solve_proper. Qed.
+ Global Instance interp_st_proper γ c s : Proper ((≡) ==> (≡)) (interp_st N γ c s).
+ Proof. apply (ne_proper _). Qed.
Lemma st_excl_eq γ s st st' :
st_ctx γ s st -∗ st_own γ s st' -∗ ▷ (st ≡ st').
@@ -58,8 +107,7 @@ Section stype_interp.
Qed.
Lemma st_excl_update γ s st st' st'' :
- st_ctx γ s st -∗ st_own γ s st' ==∗
- st_ctx γ s st'' ∗ st_own γ s st''.
+ st_ctx γ s st -∗ st_own γ s st' ==∗ st_ctx γ s st'' ∗ st_own γ s st''.
Proof.
iIntros "Hauth Hfrag".
iDestruct (own_update_2 with "Hauth Hfrag") as "H".
@@ -67,130 +115,43 @@ Section stype_interp.
(to_stype_auth_excl st'')).
eapply option_local_update.
eapply exclusive_local_update. done. }
- rewrite own_op.
- done.
- Qed.
-
- Fixpoint st_eval (vs : list val) (st1 st2 : stype val (iProp Σ)) : iProp Σ :=
- match vs with
- | [] => st1 ≡ dual_stype st2
- | v::vs => match st2 with
- | TSR Receive P st2 => P v ∗ st_eval vs st1 (st2 v)
- | _ => False
- end
- end%I.
- Global Arguments st_eval : simpl nomatch.
-
- Lemma st_later_eq a P2 (st : stype val (iProp Σ)) st2 :
- (▷ (st ≡ TSR a P2 st2) -∗
- ◇ (∃ P1 st1, st ≡ TSR a P1 st1 ∗
- ▷ ((∀ v, P1 v ≡ P2 v)) ∗
- ▷ ((∀ v, st1 v ≡ st2 v))) : iProp Σ).
- Proof.
- destruct st.
- - iIntros "Heq".
- iDestruct (stype_equivI with "Heq") as ">Heq".
- done.
- - iIntros "Heq".
- iDestruct (stype_equivI with "Heq") as "Heq".
- iDestruct ("Heq") as "[>Haeq [HPeq Hsteq]]".
- iDestruct "Haeq" as %Haeq.
- subst.
- iExists P, st.
- iSplit=> //.
- by iSplitL "HPeq".
+ by rewrite own_op.
Qed.
- Global Instance st_eval_ne : NonExpansive2 (st_eval vs).
- Proof.
- intros vs n. induction vs as [|v vs IH]; [solve_proper|].
- destruct 2 as [|[] ????? Hst]=> //=. f_equiv. solve_proper.
- by apply IH, Hst.
- Qed.
-
- Lemma st_eval_send (P : val -> iProp Σ) st l str v :
- P v -∗ st_eval l (TSR Send P st) str -∗ st_eval (l ++ [v]) (st v) str.
+ Lemma st_eval_send (P : val →iProp Σ) st vs v str :
+ P v -∗ st_eval vs (<!> @ P, st) str -∗ st_eval (vs ++ [v]) (st v) str.
Proof.
iIntros "HP".
iRevert (str).
- iInduction l as [|l] "IH"; iIntros (str) "Heval".
- - simpl.
- iDestruct (dual_stype_flip with "Heval") as "Heval".
- iRewrite -"Heval". simpl.
+ iInduction vs as [|v' vs] "IH"; iIntros (str) "Heval".
+ - iDestruct (dual_stype_flip with "Heval") as "Heval".
+ iRewrite -"Heval"; simpl.
rewrite dual_stype_involutive.
by iFrame.
- - simpl.
- destruct str; auto.
- destruct a; auto.
- iDestruct "Heval" as "[HP0 Heval]".
- iFrame.
+ - destruct str as [|[] P' str]=> //=.
+ iDestruct "Heval" as "[$ Heval]".
by iApply ("IH" with "HP").
Qed.
Lemma st_eval_recv (P : val → iProp Σ) st1 l st2 v :
- st_eval (v :: l) st1 (TSR Receive P st2) -∗ st_eval l st1 (st2 v) ∗ P v.
+ st_eval (v :: l) st1 (<?> @ P, st2) -∗ ▷ st_eval l st1 (st2 v) ∗ P v.
Proof. iDestruct 1 as "[HP Heval]". iFrame. Qed.
- Definition inv_st (γ : st_name) (c : val) : iProp Σ :=
- (∃ l r stl str,
- chan_own (st_c_name γ) Left l ∗
- chan_own (st_c_name γ) Right r ∗
- st_ctx γ Left stl ∗
- st_ctx γ Right str ∗
- ((⌜r = []⌠∗ st_eval l stl str) ∨
- (⌜l = []⌠∗ st_eval r str stl)))%I.
-
- Definition is_st (γ : st_name) (st : stype val (iProp Σ))
- (c : val) : iProp Σ :=
- (is_chan N (st_c_name γ) c ∗ inv N (inv_st γ c))%I.
-
- Definition interp_st (γ : st_name) (st : stype val (iProp Σ))
- (c : val) (s : side) : iProp Σ :=
- (st_own γ s st ∗ is_st γ st c)%I.
-
- Global Instance interp_st_proper γ :
- Proper ((≡) ==> (=) ==> (=) ==> (≡)) (interp_st γ).
- Proof.
- intros st1 st2 Heq v1 v2 <- s1 s2 <-.
- iSplit;
- iIntros "[Hown Hctx]";
- iFrame;
- unfold st_own;
- iApply (own_mono with "Hown");
- apply (auth_frag_mono);
- apply Some_included;
- left;
- f_equiv;
- f_equiv;
- apply stype_map_equiv=> //.
- Qed.
-End stype_interp.
-
-Notation "⟦ c @ s : st ⟧{ N , γ }" := (interp_st N γ st c s)
- (at level 10, s at next level, st at next level, γ at next level,
- format "⟦ c @ s : st ⟧{ N , γ }").
-
-Section stype_specs.
- Context `{!heapG Σ} (N : namespace).
- Context `{!logrelG val Σ}.
-
Lemma new_chan_vs st E c cγ :
is_chan N cγ c ∗
chan_own cγ Left [] ∗
- chan_own cγ Right []
- ={E}=∗
- ∃ lγ rγ,
- let γ := SessionType_name cγ lγ rγ in
- ⟦ c @ Left : st ⟧{N,γ} ∗ ⟦ c @ Right : dual_stype st ⟧{N,γ}.
+ chan_own cγ Right [] ={E}=∗ ∃ lγ rγ,
+ let γ := STName cγ lγ rγ in
+ ⟦ c @ Left : st ⟧{N,γ} ∗ ⟦ c @ Right : dual_stype st ⟧{N,γ}.
Proof.
iIntros "[#Hcctx [Hcol Hcor]]".
iMod (own_alloc (â— (to_stype_auth_excl st) â‹…
- â—¯ (to_stype_auth_excl st)))
- as (lγ) "[Hlsta Hlstf]"; first done.
+ ◯ (to_stype_auth_excl st))) as (lγ) "[Hlsta Hlstf]".
+ { by apply auth_both_valid_2. }
iMod (own_alloc (â— (to_stype_auth_excl (dual_stype st)) â‹…
- â—¯ (to_stype_auth_excl (dual_stype st))))
- as (rγ) "[Hrsta Hrstf]"; first done.
- pose (SessionType_name cγ lγ rγ) as stγ.
+ ◯ (to_stype_auth_excl (dual_stype st)))) as (rγ) "[Hrsta Hrstf]".
+ { by apply auth_both_valid_2. }
+ pose (STName cγ lγ rγ) as stγ.
iMod (inv_alloc N _ (inv_st stγ c) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
{ iNext. rewrite /inv_st. eauto 10 with iFrame. }
iModIntro.
@@ -202,8 +163,7 @@ Section stype_specs.
IsDualStype st1 st2 →
{{{ True }}}
new_chan #()
- {{{ c γ, RET c; ⟦ c @ Left : st1 ⟧{N,γ} ∗
- ⟦ c @ Right : st2 ⟧{N,γ} }}}.
+ {{{ c γ, RET c; ⟦ c @ Left : st1 ⟧{N,γ} ∗ ⟦ c @ Right : st2 ⟧{N,γ} }}}.
Proof.
rewrite /IsDualStype.
iIntros (Hst Φ _) "HΦ".
@@ -221,49 +181,41 @@ Section stype_specs.
Lemma send_vs c γ s (P : val → iProp Σ) st E :
↑N ⊆ E →
- ⟦ c @ s : TSR Send P st ⟧{N,γ} ={E,E∖↑N}=∗
- ∃ vs, chan_own (st_c_name γ) s vs ∗
- ▷ (∀ v, P v -∗
- chan_own (st_c_name γ) s (vs ++ [v])
- ={E∖ ↑N,E}=∗ ⟦ c @ s : st v ⟧{N,γ}).
+ ⟦ c @ s : TSR Send P st ⟧{N,γ} ={E,E∖↑N}=∗ ∃ vs,
+ chan_own (st_c_name γ) s vs ∗
+ ▷ ∀ v, P v -∗
+ chan_own (st_c_name γ) s (vs ++ [v]) ={E∖↑N,E}=∗
+ ⟦ c @ s : st v ⟧{N,γ}.
Proof.
iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
- iMod (inv_open with "Hinv") as "Hinv'"=> //.
- iDestruct "Hinv'" as "[Hinv' Hinvstep]".
- iDestruct "Hinv'" as
- (l r stl str) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')".
+ iInv N as (l r stl str) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
iModIntro.
destruct s.
- iExists _.
iIntros "{$Hclf} !>" (v) "HP Hclf".
iRename "Hstf" into "Hstlf".
iDestruct (st_excl_eq with "Hstla Hstlf") as "#Heq".
- iMod (st_excl_update _ _ _ _ (st v) with "Hstla Hstlf")
- as "[Hstla Hstlf]".
- iMod ("Hinvstep" with "[-Hstlf]") as "_".
- {
- iNext.
+ iMod (st_excl_update _ _ _ _ (st v) with "Hstla Hstlf") as "[Hstla Hstlf]".
+ iMod ("Hclose" with "[-Hstlf]") as "_".
+ { iNext.
iExists _,_,_,_. iFrame.
iLeft.
iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
- iSplit=> //.
iApply (st_eval_send with "HP").
- by iRewrite -"Heq".
- - iRewrite "Heq" in "Heval". destruct r as [|vr r]=> //.
- iSplit; first done. simpl.
- iRewrite "Heval". simpl. iFrame "HP". by rewrite involutive.
- }
- iModIntro. iFrame. rewrite /is_st. auto.
+ by iRewrite "Heq" in "Heval".
+ - iRewrite "Heq" in "Heval". destruct r as [|vr r]=> //=.
+ iSplit; first done.
+ iRewrite "Heval". simpl. iFrame "HP". by rewrite involutive. }
+ iModIntro. iFrame. auto.
- iExists _.
iIntros "{$Hcrf} !>" (v) "HP Hcrf".
iRename "Hstf" into "Hstrf".
iDestruct (st_excl_eq with "Hstra Hstrf") as "#Heq".
- iMod (st_excl_update _ _ _ _ (st v) with "Hstra Hstrf")
- as "[Hstra Hstrf]".
- iMod ("Hinvstep" with "[-Hstrf]") as "_".
- {
- iNext.
- iExists _,_,_,_. iFrame.
+ iMod (st_excl_update _ _ _ _ (st v) with "Hstra Hstrf") as "[Hstra Hstrf]".
+ iMod ("Hclose" with "[-Hstrf]") as "_".
+ { iNext.
+ iExists _, _, _, _. iFrame.
iRight.
iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
- iRewrite "Heq" in "Heval". destruct l as [|vl l]=> //.
@@ -271,9 +223,8 @@ Section stype_specs.
iRewrite "Heval". simpl. iFrame "HP". by rewrite involutive.
- iSplit=> //.
iApply (st_eval_send with "HP").
- by iRewrite -"Heq".
- }
- iModIntro. iFrame. rewrite /is_st. auto.
+ by iRewrite "Heq" in "Heval". }
+ iModIntro. iFrame. auto.
Qed.
Lemma send_st_spec st γ c s (P : val → iProp Σ) v :
@@ -292,75 +243,60 @@ Section stype_specs.
Lemma try_recv_vs c γ s (P : val → iProp Σ) st E :
↑N ⊆ E →
- ⟦ c @ s : TSR Receive P st ⟧{N,γ}
- ={E,E∖↑N}=∗
- ∃ vs, chan_own (st_c_name γ) (dual_side s) vs ∗
- (▷ ((⌜vs = []⌠-∗ chan_own (st_c_name γ) (dual_side s) vs ={E∖↑N,E}=∗
+ ⟦ c @ s : TSR Receive P st ⟧{N,γ} ={E,E∖↑N}=∗ ∃ vs,
+ chan_own (st_c_name γ) (dual_side s) vs ∗
+ ▷ ((⌜vs = []⌠-∗
+ chan_own (st_c_name γ) (dual_side s) vs ={E∖↑N,E}=∗
⟦ c @ s : TSR Receive P st ⟧{N,γ}) ∧
- (∀ v vs', ⌜vs = v :: vs'⌠-∗
- chan_own (st_c_name γ) (dual_side s) vs' -∗ |={E∖↑N,E}=>
- ⟦ c @ s : (st v) ⟧{N,γ} ∗ ▷ P v))).
+ (∀ v vs',
+ ⌜vs = v :: vs'⌠-∗
+ chan_own (st_c_name γ) (dual_side s) vs' ={E∖↑N,E}=∗
+ ⟦ c @ s : (st v) ⟧{N,γ} ∗ ▷ P v)).
Proof.
iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
- iMod (inv_open with "Hinv") as "Hinv'"=> //.
- iDestruct "Hinv'" as "[Hinv' Hinvstep]".
- iDestruct "Hinv'" as
- (l r stl str) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')".
+ iInv N as (l r stl str) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
iExists (side_elim s r l). iModIntro.
- destruct s.
- - simpl. iIntros "{$Hcrf} !>".
+ destruct s; simpl.
+ - iIntros "{$Hcrf} !>".
iRename "Hstf" into "Hstlf".
iDestruct (st_excl_eq with "Hstla Hstlf") as "#Heq".
- iSplit=> //.
- + iIntros "Hvs Hown".
- iMod ("Hinvstep" with "[-Hstlf]") as "_".
- { iNext. iExists l,r,_,_. iFrame. }
+ iSplit.
+ + iIntros (->) "Hown".
+ iMod ("Hclose" with "[-Hstlf]") as "_".
+ { iNext. iExists l, [], _, _. iFrame. }
iModIntro. iFrame "Hcctx ∗ Hinv".
- + iIntros (v vs Hvs) "Hown".
- iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]"; first inversion Hvs.
- iMod (st_excl_update _ _ _ _ (st v) with "Hstla Hstlf")
- as "[Hstla Hstlf]".
- subst.
- iDestruct (st_later_eq with "Heq") as ">Hleq".
- iDestruct "Hleq" as (P1 st1) "[Hsteq [HPeq Hsteq']]".
- iSpecialize ("HPeq" $!v).
- iSpecialize ("Hsteq'" $!v).
+ + iIntros (v vs ->) "Hown".
+ iDestruct "Hinv'" as "[[>% _]|[> -> Heval]]"; first done.
+ iMod (st_excl_update _ _ _ _ (st v) with "Hstla Hstlf") as "[Hstla Hstlf]".
+ iDestruct (stype_later_equiv with "Heq") as ">Hleq".
+ iDestruct "Hleq" as (P1 st1) "(Hsteq & HPeq & Hsteq')".
iRewrite "Hsteq" in "Heval".
- subst.
iDestruct (st_eval_recv with "Heval") as "[Heval HP]".
- iMod ("Hinvstep" with "[-Hstlf HP]") as "H".
- { iExists _,_,_,_. iFrame. iRight=> //.
- iNext. iSplit=> //. by iRewrite -"Hsteq'". }
- iModIntro.
- iSplitR "HP".
- * iFrame "Hstlf Hcctx Hinv".
- * iNext. by iRewrite -"HPeq".
- - simpl. iIntros "{$Hclf} !>".
+ iMod ("Hclose" with "[-Hstlf HP]") as "H".
+ { iExists _, _,_ ,_. iFrame. iRight.
+ iNext. iSplit=> //. iNext. by iRewrite -("Hsteq'" $! v). }
+ iModIntro. iFrame "Hstlf Hcctx Hinv".
+ iNext. by iRewrite -("HPeq" $! v).
+ - iIntros "{$Hclf} !>".
iRename "Hstf" into "Hstrf".
iDestruct (st_excl_eq with "Hstra Hstrf") as "#Heq".
iSplit=> //.
- + iIntros "Hvs Hown".
- iMod ("Hinvstep" with "[-Hstrf]") as "_".
- { iNext. iExists l,r,_,_. iFrame. }
+ + iIntros (->) "Hown".
+ iMod ("Hclose" with "[-Hstrf]") as "_".
+ { iNext. iExists [], r, _, _. iFrame. }
iModIntro. iFrame "Hcctx ∗ Hinv".
- + iIntros (v vs' Hvs) "Hown".
- iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]"; last inversion Hvs.
- iMod (st_excl_update _ _ _ _ (st v) with "Hstra Hstrf")
- as "[Hstra Hstrf]".
- subst.
- iDestruct (st_later_eq with "Heq") as ">Hleq".
- iDestruct "Hleq" as (P1 st1) "[Hsteq [HPeq Hsteq']]".
- iSpecialize ("HPeq" $!v).
- iSpecialize ("Hsteq'" $!v).
+ + iIntros (v vs' ->) "Hown".
+ iDestruct "Hinv'" as "[[>-> Heval]|[>% Heval]]"; last done.
+ iMod (st_excl_update _ _ _ _ (st v) with "Hstra Hstrf") as "[Hstra Hstrf]".
+ iDestruct (stype_later_equiv with "Heq") as ">Hleq".
+ iDestruct "Hleq" as (P1 st1) "(Hsteq & HPeq & Hsteq')".
iRewrite "Hsteq" in "Heval".
iDestruct (st_eval_recv with "Heval") as "[Heval HP]".
- iMod ("Hinvstep" with "[-Hstrf HP]") as "_".
- { iExists _,_,_,_. iFrame. iLeft=> //.
- iNext. iSplit=> //. by iRewrite -"Hsteq'". }
- iModIntro.
- iSplitR "HP".
- * iFrame "Hstrf Hcctx Hinv".
- * iNext. by iRewrite -"HPeq".
+ iMod ("Hclose" with "[-Hstrf HP]") as "_".
+ { iExists _, _, _, _. iFrame. iLeft.
+ iNext. iSplit=> //. iNext. by iRewrite -("Hsteq'" $! v). }
+ iModIntro. iFrame "Hstrf Hcctx Hinv".
+ iNext. by iRewrite -("HPeq" $! v).
Qed.
Lemma try_recv_st_spec st γ c s (P : val → iProp Σ) :
@@ -378,39 +314,29 @@ Section stype_specs.
iSplit.
- iIntros (Hvs) "Hown".
iDestruct "H" as "[H _]".
- iSpecialize ("H" $!Hvs).
- iMod ("H" with "Hown") as "H".
+ iMod ("H" $!Hvs with "Hown") as "H".
iModIntro.
iApply "HΦ"=> //.
eauto with iFrame.
- iIntros (v vs' Hvs) "Hown".
iDestruct "H" as "[_ H]".
- iSpecialize ("H" $!v vs' Hvs).
- iMod ("H" with "Hown") as "H".
+ iMod ("H" $!v vs' Hvs with "Hown") as "H".
iModIntro.
- iApply "HΦ"=> //.
- eauto with iFrame.
+ iApply "HΦ"; eauto with iFrame.
Qed.
Lemma recv_st_spec st γ c s (P : val → iProp Σ) :
{{{ ⟦ c @ s : <?> @ P , st ⟧{N,γ} }}}
recv c #s
- {{{ v, RET v; ⟦ c @ s : st v ⟧{N,γ} ∗ P v}}}.
+ {{{ v, RET v; ⟦ c @ s : st v ⟧{N,γ} ∗ P v }}}.
Proof.
iIntros (Φ) "Hrecv HΦ".
iLöb as "IH". wp_rec.
wp_apply (try_recv_st_spec with "Hrecv").
iIntros (v) "H".
- iDestruct "H" as "[H | H]".
- - iDestruct "H" as "[Hv H]".
- iDestruct "Hv" as %->.
- wp_pures.
- iApply ("IH" with "[H]")=> //.
- - iDestruct "H" as (w) "[Hv [H HP]]".
- iDestruct "Hv" as %->.
- wp_pures.
- iApply "HΦ".
- iFrame.
+ iDestruct "H" as "[[-> H]| H]".
+ - wp_pures. by iApply ("IH" with "[H]").
+ - iDestruct "H" as (w ->) "[H HP]".
+ wp_pures. iApply "HΦ". iFrame.
Qed.
-
-End stype_specs.
\ No newline at end of file
+End stype.
diff --git a/theories/encodings/stype_enc.v b/theories/encodings/stype_enc.v
index 3768474..2429c83 100644
--- a/theories/encodings/stype_enc.v
+++ b/theories/encodings/stype_enc.v
@@ -21,7 +21,9 @@ Section DualStypeEnc.
IsDualStype (TSR' a1 P st1) (TSR' a2 P st2).
Proof.
rewrite /IsDualAction /IsDualStype. intros <- Hst.
- constructor=> x. done. by destruct (decode x).
+ rewrite -(stype_force_eq (dual_stype _)).
+ constructor=> x. done. destruct (decode x)=> //.
+ apply is_dual_end.
Qed.
End DualStypeEnc.
diff --git a/theories/typing/stype.v b/theories/typing/stype.v
index ce4de20..edb21bd 100644
--- a/theories/typing/stype.v
+++ b/theories/typing/stype.v
@@ -14,7 +14,7 @@ Definition dual_action (a : action) : action :=
Instance dual_action_involutive : Involutive (=) dual_action.
Proof. by intros []. Qed.
-Inductive stype (V A : Type) :=
+CoInductive stype (V A : Type) :=
| TEnd
| TSR (a : action) (P : V → A) (st : V → stype V A).
Arguments TEnd {_ _}.
@@ -23,7 +23,7 @@ Instance: Params (@TSR) 3.
Instance stype_inhabited V A : Inhabited (stype V A) := populate TEnd.
-Fixpoint dual_stype {V A} (st : stype V A) :=
+CoFixpoint dual_stype {V A} (st : stype V A) : stype V A :=
match st with
| TEnd => TEnd
| TSR a P st => TSR (dual_action a) P (λ v, dual_stype (st v))
@@ -52,7 +52,7 @@ Section stype_ofe.
Context {V : Type}.
Context {A : ofeT}.
- Inductive stype_equiv : Equiv (stype V A) :=
+ CoInductive stype_equiv : Equiv (stype V A) :=
| TEnd_equiv : TEnd ≡ TEnd
| TSR_equiv a P1 P2 st1 st2 :
pointwise_relation V (≡) P1 P2 →
@@ -60,79 +60,119 @@ Section stype_ofe.
TSR a P1 st1 ≡ TSR a P2 st2.
Existing Instance stype_equiv.
- Inductive stype_dist' (n : nat) : relation (stype V A) :=
- | TEnd_dist : stype_dist' n TEnd TEnd
- | TSR_dist a P1 P2 st1 st2 :
- pointwise_relation V (dist n) P1 P2 →
- pointwise_relation V (stype_dist' n) st1 st2 →
- stype_dist' n (TSR a P1 st1) (TSR a P2 st2).
- Instance stype_dist : Dist (stype V A) := stype_dist'.
+ CoInductive stype_dist : Dist (stype V A) :=
+ | TEnd_dist n : TEnd ≡{n}≡ TEnd
+ | TSR_dist_0 a P1 P2 st1 st2 :
+ pointwise_relation V (dist 0) P1 P2 →
+ TSR a P1 st1 ≡{0}≡ TSR a P2 st2
+ | TSR_dist_S n a P1 P2 st1 st2 :
+ pointwise_relation V (dist (S n)) P1 P2 →
+ pointwise_relation V (dist n) st1 st2 →
+ TSR a P1 st1 ≡{S n}≡ TSR a P2 st2.
+ Existing Instance stype_dist.
+
+ Lemma TSR_dist n a P1 P2 st1 st2 :
+ pointwise_relation V (dist n) P1 P2 →
+ pointwise_relation V (dist_later n) st1 st2 →
+ TSR a P1 st1 ≡{n}≡ TSR a P2 st2.
+ Proof. destruct n; by constructor. Defined.
Definition stype_ofe_mixin : OfeMixin (stype V A).
Proof.
split.
- - intros st1 st2. rewrite /dist /stype_dist. split.
- + intros Hst n.
- induction Hst as [|a P1 P2 st1 st2 HP Hst IH]; constructor; intros v.
- * apply equiv_dist, HP.
- * apply IH.
- + revert st2. induction st1 as [|a P1 st1 IH]; intros [|a' P2 st2] Hst.
- * constructor.
- * feed inversion (Hst O).
- * feed inversion (Hst O).
- * feed inversion (Hst O); subst.
- constructor; intros v.
- ** apply equiv_dist=> n. feed inversion (Hst n); subst; auto.
- ** apply IH=> n. feed inversion (Hst n); subst; auto.
- - rewrite /dist /stype_dist. split.
- + intros st. induction st; constructor; repeat intro; auto.
- + intros st1 st2. induction 1; constructor; repeat intro; auto.
- symmetry; auto.
- + intros st1 st2 st3 H1 H2.
- revert H2. revert st3.
- induction H1 as [| a P1 P2 st1 st2 HP Hst12 IH]=> //.
- inversion 1. subst. constructor.
- ** by transitivity P2.
- ** intros v. by apply IH.
- - intros n st1 st2. induction 1; constructor.
- + intros v. apply dist_S. apply H.
- + intros v. apply H1.
+ - intros st1 st2. split.
+ + revert st1 st2. cofix IH; destruct 1 as [|a P1 P2 st1' st2' HP]=> n.
+ { constructor. }
+ destruct n as [|n].
+ * constructor=> v. apply equiv_dist, HP.
+ * constructor=> v. apply equiv_dist, HP. by apply IH.
+ + revert st1 st2. cofix IH=> -[|a1 P1 st1] -[|a2 P2 st2] Hst;
+ feed inversion (Hst O); subst; constructor=> v.
+ * apply equiv_dist=> n. feed inversion (Hst n); auto.
+ * apply IH=> n. feed inversion (Hst (S n)); auto.
+ - intros n. split.
+ + revert n. cofix IH=> -[|n] [|a P st]; constructor=> v; auto.
+ + revert n. cofix IH; destruct 1; constructor=> v; symmetry; auto.
+ + revert n. cofix IH; destruct 1; inversion 1; constructor=> v; etrans; eauto.
+ - cofix IH=> -[|n]; inversion 1; constructor=> v; try apply dist_S; auto.
Qed.
Canonical Structure stypeC : ofeT := OfeT (stype V A) stype_ofe_mixin.
+ Definition stype_head (d : V -c> A) (st : stype V A) : V -c> A :=
+ match st with TEnd => d | TSR a P st => P end.
+ Definition stype_tail (v : V) (st : stypeC) : later stypeC :=
+ match st with TEnd => Next TEnd | TSR a P st => Next (st v) end.
+ Global Instance stype_head_ne d : NonExpansive (stype_head d).
+ Proof. by destruct 1. Qed.
+ Global Instance stype_tail_ne v : NonExpansive (stype_tail v).
+ Proof. destruct 1; naive_solver. Qed.
+
+ Definition stype_force (st : stype V A) : stype V A :=
+ match st with
+ | TEnd => TEnd
+ | TSR a P st => TSR a P st
+ end.
+ Lemma stype_force_eq st : stype_force st = st.
+ Proof. by destruct st. Defined.
+
+ CoFixpoint stype_compl_go `{!Cofe A} (c : chain stypeC) : stypeC :=
+ match c O with
+ | TEnd => TEnd
+ | TSR a P st => TSR a
+ (compl (chain_map (stype_head P) c) : V → A)
+ (λ v, stype_compl_go (later_chain (chain_map (stype_tail v) c)))
+ end.
+
+ Global Program Instance stype_cofe `{!Cofe A} : Cofe stypeC :=
+ {| compl c := stype_compl_go c |}.
+ Next Obligation.
+ intros ? n c; rewrite /compl. revert c n. cofix IH=> c n.
+ rewrite -(stype_force_eq (stype_compl_go c)) /=.
+ destruct (c O) as [|a P st'] eqn:Hc0.
+ - assert (c n ≡{0}≡ TEnd) as Hcn.
+ { rewrite -Hc0 -(chain_cauchy c 0 n) //. lia. }
+ by inversion Hcn.
+ - assert (c n ≡{0}≡ TSR a P st') as Hcn.
+ { rewrite -Hc0 -(chain_cauchy c 0 n) //. lia. }
+ inversion Hcn as [|? P' ? st'' ? HP|]; subst.
+ destruct n as [|n]; constructor.
+ + intros v. by rewrite (conv_compl 0 (chain_map (stype_head P) c) v) /= -H.
+ + intros v. by rewrite (conv_compl _ (chain_map (stype_head P) c) v) /= -H.
+ + intros v. assert (st'' v = later_car (stype_tail v (c (S n)))) as ->.
+ { by rewrite -H /=. }
+ apply IH.
+ Qed.
+
+ Global Instance TSR_stype_contractive a n :
+ Proper (pointwise_relation _ (dist n) ==>
+ pointwise_relation _ (dist_later n) ==> dist n) (TSR a).
+ Proof. destruct n; by constructor. Qed.
Global Instance TSR_stype_ne a n :
Proper (pointwise_relation _ (dist n) ==>
pointwise_relation _ (dist n) ==> dist n) (TSR a).
Proof.
- intros P1 P2 HP st1 st2 Hst.
- constructor.
- - apply HP.
- - intros v. apply Hst.
+ intros P1 P2 HP st1 st2 Hst. apply TSR_stype_contractive=> //.
+ destruct n as [|n]=> // v /=. by apply dist_S.
Qed.
Global Instance TSR_stype_proper a :
Proper (pointwise_relation _ (≡) ==>
pointwise_relation _ (≡) ==> (≡)) (TSR a).
- Proof.
- intros P1 P2 HP st1 st2 Hst. apply equiv_dist=> n.
- by f_equiv; intros v; apply equiv_dist.
- Qed.
+ Proof. by constructor. Qed.
Global Instance dual_stype_ne : NonExpansive dual_stype.
Proof.
- intros n. induction 1 as [| a P1 P2 st1 st2 HP Hst IH].
- - constructor.
- - constructor. apply HP. intros v. apply IH.
+ cofix IH=> n st1 st2 Hst.
+ rewrite -(stype_force_eq (dual_stype st1)) -(stype_force_eq (dual_stype st2)).
+ destruct Hst; constructor=> v; auto; by apply IH.
Qed.
Global Instance dual_stype_proper : Proper ((≡) ==> (≡)) dual_stype.
Proof. apply (ne_proper _). Qed.
Global Instance dual_stype_involutive : Involutive (≡) dual_stype.
Proof.
- intros st.
- induction st.
- - constructor.
- - rewrite /= (involutive (f:=dual_action)).
- constructor. reflexivity. intros v. apply H.
+ cofix IH=> st. rewrite -(stype_force_eq (dual_stype (dual_stype _))).
+ destruct st as [|a P st]; first done.
+ rewrite /= involutive. constructor=> v; auto.
Qed.
Lemma stype_equivI {M} st1 st2 :
@@ -140,13 +180,25 @@ Section stype_ofe.
match st1, st2 with
| TEnd, TEnd => True
| TSR a1 P1 st1, TSR a2 P2 st2 =>
- ⌜ a1 = a2 ⌠∧ (∀ v, P1 v ≡ P2 v) ∧ (∀ v, st1 v ≡ st2 v)
+ ⌜ a1 = a2 ⌠∧ (∀ v, P1 v ≡ P2 v) ∧ ▷ (∀ v, st1 v ≡ st2 v)
| _, _ => False
end.
Proof.
uPred.unseal; constructor=> n x ?. split; first by destruct 1.
destruct st1, st2=> //=; [constructor|].
- by intros [[= ->] [??]]; constructor.
+ by intros [[= ->] [??]]; destruct n; constructor.
+ Qed.
+
+ Lemma stype_later_equiv M st a P2 st2 :
+ ▷ (st ≡ TSR a P2 st2) -∗
+ ◇ (∃ P1 st1, st ≡ TSR a P1 st1 ∗
+ ▷ (∀ v, P1 v ≡ P2 v) ∗
+ ▷ ▷ (∀ v, st1 v ≡ st2 v) : uPred M).
+ Proof.
+ iIntros "Heq". destruct st as [|a' P1 st1].
+ - iDestruct (stype_equivI with "Heq") as ">[]".
+ - iDestruct (stype_equivI with "Heq") as "(>-> & HPeq & Hsteq)".
+ iExists P1, st1. auto.
Qed.
Lemma dual_stype_flip {M} st1 st2 :
@@ -156,11 +208,11 @@ Section stype_ofe.
- iIntros "Heq". iRewrite -"Heq". by rewrite dual_stype_involutive.
- iIntros "Heq". iRewrite "Heq". by rewrite dual_stype_involutive.
Qed.
-
End stype_ofe.
+
Arguments stypeC : clear implicits.
-Fixpoint stype_map {V A B} (f : A → B) (st : stype V A) : stype V B :=
+CoFixpoint stype_map {V A B} (f : A → B) (st : stype V A) : stype V B :=
match st with
| TEnd => TEnd
| TSR a P st => TSR a (λ v, f (P v)) (λ v, stype_map f (st v))
@@ -168,42 +220,36 @@ Fixpoint stype_map {V A B} (f : A → B) (st : stype V A) : stype V B :=
Lemma stype_map_ext_ne {V A} {B : ofeT} (f g : A → B) (st : stype V A) n :
(∀ x, f x ≡{n}≡ g x) → stype_map f st ≡{n}≡ stype_map g st.
Proof.
- intros Hf. induction st as [| a P st IH]; constructor.
- - intros v. apply Hf.
- - intros v. apply IH.
+ revert n st. cofix IH=> n st Hf.
+ rewrite -(stype_force_eq (stype_map f st)) -(stype_force_eq (stype_map g st)).
+ destruct st as [|a P st], n as [|n]; constructor=> v //. apply IH; auto using dist_S.
Qed.
Lemma stype_map_ext {V A} {B : ofeT} (f g : A → B) (st : stype V A) :
(∀ x, f x ≡ g x) → stype_map f st ≡ stype_map g st.
Proof.
- intros Hf. apply equiv_dist.
- intros n. apply stype_map_ext_ne.
- intros x. apply equiv_dist.
- apply Hf.
+ intros Hf. apply equiv_dist=> n. apply stype_map_ext_ne=> v.
+ apply equiv_dist, Hf.
Qed.
Instance stype_map_ne {V : Type} {A B : ofeT} (f : A → B) n :
- Proper (dist n ==> dist n) f →
+ (∀ n, Proper (dist n ==> dist n) f) →
Proper (dist n ==> dist n) (@stype_map V _ _ f).
Proof.
- intros Hf st1 st2. induction 1 as [| a P1 P2 st1 st2 HP Hst IH]; constructor.
- - intros v. f_equiv. apply HP.
- - intros v. apply IH.
+ intros Hf. revert n. cofix IH=> n st1 st2 Hst.
+ rewrite -(stype_force_eq (stype_map _ st1)) -(stype_force_eq (stype_map _ st2)).
+ destruct Hst; constructor=> v; apply Hf || apply IH; auto.
Qed.
-Lemma stype_map_equiv {A B : ofeT} (f g : A -n> B) (st st' : stype val A) :
- (∀ x, f x ≡ g x) → st ≡ st' → stype_map f st ≡ stype_map g st'.
-Proof. intros Feq. induction 1=>//. constructor=>//. by repeat f_equiv. Qed.
Lemma stype_fmap_id {V : Type} {A : ofeT} (st : stype V A) :
stype_map id st ≡ st.
Proof.
- induction st as [| a P st IH]; constructor.
- - intros v. reflexivity.
- - intros v. apply IH.
+ revert st. cofix IH=> st. rewrite -(stype_force_eq (stype_map _ _)).
+ destruct st; constructor=> v; auto.
Qed.
Lemma stype_fmap_compose {V : Type} {A B C : ofeT} (f : A → B) (g : B → C) st :
stype_map (g ∘ f) st ≡ stype_map g (@stype_map V _ _ f st).
Proof.
- induction st as [| a P st IH]; constructor.
- - intros v. reflexivity.
- - intros v. apply IH.
+ revert st. cofix IH=> st.
+ rewrite -(stype_force_eq (stype_map _ _)) -(stype_force_eq (stype_map g _)).
+ destruct st; constructor=> v; auto.
Qed.
Definition stypeC_map {V A B} (f : A -n> B) : stypeC V A -n> stypeC V B :=
@@ -212,25 +258,29 @@ Instance stypeC_map_ne {V} A B : NonExpansive (@stypeC_map V A B).
Proof. intros n f g ? st. by apply stype_map_ext_ne. Qed.
Program Definition stypeCF {V} (F : cFunctor) : cFunctor := {|
- cFunctor_car A B := stypeC V (cFunctor_car F A B);
- cFunctor_map A1 A2 B1 B2 fg := stypeC_map (cFunctor_map F fg)
+ cFunctor_car A _ B _ := stypeC V (cFunctor_car F A _ B _);
+ cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := stypeC_map (cFunctor_map F fg)
|}.
+Next Obligation. done. Qed.
Next Obligation.
- by intros V F A1 A2 B1 B2 n f g Hfg; apply stypeC_map_ne, cFunctor_ne.
+ by intros V F A1 ? A2 ? B1 ? B2 ? n f g Hfg;
+ apply stypeC_map_ne, cFunctor_ne.
Qed.
Next Obligation.
- intros V F A B x. rewrite /= -{2}(stype_fmap_id x).
+ intros V F A ? B ? x. rewrite /= -{2}(stype_fmap_id x).
apply stype_map_ext=>y. apply cFunctor_id.
Qed.
Next Obligation.
- intros V F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -stype_fmap_compose.
+ intros V F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x.
+ rewrite /= -stype_fmap_compose.
apply stype_map_ext=>y; apply cFunctor_compose.
Qed.
Instance stypeCF_contractive {V} F :
cFunctorContractive F → cFunctorContractive (@stypeCF V F).
Proof.
- by intros ? A1 A2 B1 B2 n f g Hfg; apply stypeC_map_ne, cFunctor_contractive.
+ by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg;
+ apply stypeC_map_ne, cFunctor_contractive.
Qed.
Class IsDualAction (a1 a2 : action) :=
@@ -253,7 +303,7 @@ Section DualStype.
Proof. by rewrite /IsDualStype. Qed.
Global Instance is_dual_end : IsDualStype (TEnd : stype V A) TEnd.
- Proof. constructor. Qed.
+ Proof. by rewrite /IsDualStype -(stype_force_eq (dual_stype _)). Qed.
Global Instance is_dual_tsr a1 a2 P (st1 st2 : V → stype V A) :
IsDualAction a1 a2 →
@@ -261,7 +311,7 @@ Section DualStype.
IsDualStype (TSR a1 P st1) (TSR a2 P st2).
Proof.
rewrite /IsDualAction /IsDualStype. intros <- Hst.
- by constructor=> x.
+ rewrite /IsDualStype -(stype_force_eq (dual_stype _)) /=.
+ by constructor=> v.
Qed.
-
-End DualStype.
\ No newline at end of file
+End DualStype.
--
GitLab