Skip to content
Snippets Groups Projects
Commit 3a46d85b authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Hai Dang
Browse files

Bump Iris (transfinite algebra).

parent e7046bfb
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/typing/lib/rc/rc.v
+ 5
− 3
View file @ 3a46d85b
......@@ -300,7 +300,8 @@ Section code.
* iExists _. iFrame "Hl2". destruct weak.
-- iLeft. iSplit; first done. rewrite Hincls. iFrame "Hl†".
iMod (own_update_2 with "Hst Htok") as "Hst".
{ apply auth_update_dealloc. rewrite -{1}(right_id (None, 0%nat) _ (_, _)).
{ apply auth_update_dealloc.
rewrite -{1}(right_id ((None, 0%nat) : prodUR _ _) _ (_, _)).
apply cancel_local_update_unit, _. }
rewrite -[in (1).[ν]%I]Hqq' -[(|={lft_userE,⊤}=>_)%I]fupd_trans.
iApply step_fupd_mask_mono;
......@@ -362,7 +363,8 @@ Section code.
-- iLeft. iFrame. iSplitR; first done.
iApply ("Hclose" with "[>- $Hna]"). iExists (None, 0%nat).
iMod (own_update_2 with "Hst Htok") as "$"; last done.
apply auth_update_dealloc. rewrite -{1}(right_id (None, 0%nat) _ (_, _)).
apply auth_update_dealloc.
rewrite -{1}(right_id ((None, 0%nat) : prodUR _ _) _ (_, _)).
apply cancel_local_update_unit, _.
-- iRight. iSplitR; first by auto with lia. iIntros "!> Hl† Hl2 Hvl".
iApply ("Hclose" with "[>- $Hna]"). iExists (None, S weak).
......@@ -381,7 +383,7 @@ Section code.
iFrame. iExists _. iFrame. auto with iFrame.
* iMod (own_update_2 with "Hst Htok") as "Hst".
{ apply auth_update_dealloc.
rewrite pair_op Cinl_op Some_op -{1}(left_id 0%nat _ weak) pair_op.
rewrite pair_op Cinl_op Some_op -{1}(left_id (0%nat : natUR) _ weak) pair_op.
apply (cancel_local_update_unit _ (_, _)). }
iApply "Hclose". iFrame "Hna Hst". iExists (q+q'')%Qp. iFrame.
iSplitL; first last.
......
theories/typing/type.v
+ 96
− 59
View file @ 3a46d85b
......@@ -301,8 +301,8 @@ Section type_dist2.
Proof. intros EQ. split; intros; try apply dist_dist_later; apply EQ. Qed.
Lemma type_dist2_dist_later n ty1 ty2 : type_dist2 n ty1 ty2 → dist_later n ty1 ty2.
Proof.
intros EQ. eapply dist_later_fin_iff. destruct n; first done.
split; intros; try apply EQ; try si_solver.
intros EQ. dist_later_fin_intro.
split; intros; try apply EQ; eauto using SIdx.lt_succ_diag_r.
apply dist_S, EQ.
Qed.
Lemma type_later_dist2_later n ty1 ty2 : dist_later n ty1 ty2 → type_dist2_later n ty1 ty2.
......@@ -316,7 +316,7 @@ Section type_dist2.
Proof. intros ?? EQ. apply EQ. Qed.
Lemma ty_own_type_dist n:
Proper (type_dist2 (S n) ==> eq ==> eq ==> dist n) ty_own.
Proof. intros ?? EQ ??-> ??->. apply EQ. si_solver. Qed.
Proof. intros ?? EQ ??-> ??->. apply EQ, SIdx.lt_succ_diag_r. Qed.
Lemma ty_shr_type_dist n :
Proper (type_dist2 n ==> eq ==> eq ==> eq ==> dist n) ty_shr.
Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
......@@ -382,9 +382,7 @@ End type_contractive.
(* Tactic automation. *)
Ltac f_type_equiv :=
first [ ((eapply ty_size_type_dist || eapply ty_shr_type_dist || eapply ty_own_type_dist); try reflexivity) |
match goal with | |- @dist_later ?A _ ?n ?x ?y =>
eapply dist_later_fin_iff; destruct n as [|n]; [exact I|change (@dist A _ n x y)]
end ].
dist_later_fin_intro ].
Ltac solve_type_proper :=
constructor;
solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive_fin || f_equiv).
......@@ -484,7 +482,7 @@ Section type.
Global Instance copy_equiv : Proper (equiv ==> impl) Copy.
Proof.
intros ty1 ty2 [EQsz%leibniz_equiv EQown EQshr] Hty1. split.
intros ty1 ty2 [EQsz EQown EQshr] Hty1. split.
- intros. rewrite -EQown. apply _.
- intros *. rewrite -EQsz -EQshr. setoid_rewrite <-EQown.
apply copy_shr_acc.
......@@ -510,13 +508,13 @@ Section type.
(** Send and Sync types *)
Global Instance send_equiv : Proper (equiv ==> impl) Send.
Proof.
intros ty1 ty2 [EQsz%leibniz_equiv EQown EQshr] Hty1.
intros ty1 ty2 [EQsz EQown EQshr] Hty1.
rewrite /Send=>???. rewrite -!EQown. auto.
Qed.
Global Instance sync_equiv : Proper (equiv ==> impl) Sync.
Proof.
intros ty1 ty2 [EQsz%leibniz_equiv EQown EQshr] Hty1.
intros ty1 ty2 [EQsz EQown EQshr] Hty1.
rewrite /Send=>????. rewrite -!EQshr. auto.
Qed.
......@@ -552,26 +550,18 @@ Definition type_equal `{!typeG Σ} (ty1 ty2 : type) : vProp Σ :=
(□ ∀ κ tid l, ty1.(ty_shr) κ tid l ∗-∗ ty2.(ty_shr) κ tid l))%I.
Global Instance: Params (@type_equal) 2 := {}.
Definition subtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
∀ qmax qL, llctx_interp_noend qmax L qL ⊢ □ (elctx_interp E -∗ type_incl ty1 ty2).
Global Instance: Params (@subtype) 4 := {}.
(* TODO: The prelude should have a symmetric closure. *)
Definition eqtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
subtype E L ty1 ty2 ∧ subtype E L ty2 ty1.
Global Instance: Params (@eqtype) 4 := {}.
Section subtyping.
Section iprop_subtyping.
Context `{!typeG Σ}.
Global Instance type_incl_ne : NonExpansive2 type_incl.
Proof.
intros n ?? [EQsz1%leibniz_equiv EQown1 EQshr1] ?? [EQsz2%leibniz_equiv EQown2 EQshr2].
intros n ?? [EQsz1 EQown1 EQshr1] ?? [EQsz2 EQown2 EQshr2].
rewrite /type_incl. repeat ((by auto) || f_equiv).
Qed.
Global Instance type_incl_persistent ty1 ty2 : Persistent (type_incl ty1 ty2) := _.
Lemma type_incl_refl ty : ⊢ type_incl ty ty.
Proof. iSplit; first done. iSplit; iModIntro; iIntros; done. Qed.
......@@ -585,6 +575,92 @@ Section subtyping.
- iApply "Hs23". iApply "Hs12". done.
Qed.
Global Instance type_equal_ne : NonExpansive2 type_equal.
Proof.
intros n ?? [EQsz1 EQown1 EQshr1] ?? [EQsz2 EQown2 EQshr2].
rewrite /type_equal. repeat ((by auto) || f_equiv).
Qed.
Global Instance type_equal_proper :
Proper ((≡) ==> (≡) ==> (⊣⊢)) type_equal.
Proof. apply ne_proper_2, _. Qed.
Global Instance type_equal_persistent ty1 ty2 : Persistent (type_equal ty1 ty2) := _.
Lemma type_equal_incl ty1 ty2 :
type_equal ty1 ty2 ⊣⊢ type_incl ty1 ty2 ∗ type_incl ty2 ty1.
Proof.
iSplit.
- iIntros "#(% & Ho & Hs)".
iSplit; (iSplit; first done; iSplit; iModIntro).
+ iIntros (??) "?". by iApply "Ho".
+ iIntros (???) "?". by iApply "Hs".
+ iIntros (??) "?". by iApply "Ho".
+ iIntros (???) "?". by iApply "Hs".
- iIntros "#[(% & Ho1 & Hs1) (% & Ho2 & Hs2)]".
iSplit; first done. iSplit; iModIntro.
+ iIntros (??). iSplit; [iApply "Ho1"|iApply "Ho2"].
+ iIntros (???). iSplit; [iApply "Hs1"|iApply "Hs2"].
Qed.
Lemma type_equal_refl ty :
⊢ type_equal ty ty.
Proof.
iApply type_equal_incl. iSplit; iApply type_incl_refl.
Qed.
Lemma type_equal_trans ty1 ty2 ty3 :
type_equal ty1 ty2 -∗ type_equal ty2 ty3 -∗ type_equal ty1 ty3.
Proof.
rewrite !type_equal_incl. iIntros "#[??] #[??]". iSplit.
- iApply (type_incl_trans _ ty2); done.
- iApply (type_incl_trans _ ty2); done.
Qed.
Lemma type_incl_simple_type (st1 st2 : simple_type) :
□ (∀ tid vl, st1.(st_own) tid vl -∗ st2.(st_own) tid vl) -∗
type_incl st1 st2.
Proof.
iIntros "#Hst". iSplit; first done. iSplit; iModIntro.
- iIntros. iApply "Hst"; done.
- iIntros (???). iDestruct 1 as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
by iApply "Hst".
Qed.
Lemma type_equal_equiv ty1 ty2 :
(⊢ type_equal ty1 ty2) ↔ ty1 ≡ ty2.
Proof.
split.
- intros Heq. split.
+ eapply uPred.pure_soundness, embed_emp_valid_inj.
iDestruct Heq as "[%Hsz _]". done.
+ iDestruct Heq as "[_ [Hown _]]". done.
+ iDestruct Heq as "[_ [_ Hshr]]". done.
- intros ->. apply type_equal_refl.
Qed.
End iprop_subtyping.
(** Prop-level conditional type inclusion/equality
(may depend on assumptions in [E, L].) *)
Definition subtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
∀ qmax qL, llctx_interp_noend qmax L qL ⊢ □ (elctx_interp E -∗ type_incl ty1 ty2).
Global Instance: Params (@subtype) 4 := {}.
(* TODO: The prelude should have a symmetric closure. *)
Definition eqtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
subtype E L ty1 ty2 ∧ subtype E L ty2 ty1.
Global Instance: Params (@eqtype) 4 := {}.
Section subtyping.
Context `{!typeG Σ}.
Lemma type_incl_subtype ty1 ty2 E L :
(⊢ type_incl ty1 ty2) → subtype E L ty1 ty2.
Proof.
intros Heq. rewrite /subtype.
iIntros (??) "_ !> _". done.
Qed.
Lemma subtype_refl E L ty : subtype E L ty ty.
Proof. iIntros (??) "_ !> _". iApply type_incl_refl. Qed.
Global Instance subtype_preorder E L : PreOrder (subtype E L).
......@@ -635,35 +711,6 @@ Section subtyping.
iApply type_incl_refl.
Qed.
Lemma type_equal_incl ty1 ty2 :
type_equal ty1 ty2 ⊣⊢ type_incl ty1 ty2 ∗ type_incl ty2 ty1.
Proof.
iSplit.
- iIntros "#(% & Ho & Hs)".
iSplit; (iSplit; first done; iSplit; iModIntro).
+ iIntros (??) "?". by iApply "Ho".
+ iIntros (???) "?". by iApply "Hs".
+ iIntros (??) "?". by iApply "Ho".
+ iIntros (???) "?". by iApply "Hs".
- iIntros "#[(% & Ho1 & Hs1) (% & Ho2 & Hs2)]".
iSplit; first done. iSplit; iModIntro.
+ iIntros (??). iSplit; [iApply "Ho1"|iApply "Ho2"].
+ iIntros (???). iSplit; [iApply "Hs1"|iApply "Hs2"].
Qed.
Lemma type_equal_refl ty :
⊢ type_equal ty ty.
Proof.
iApply type_equal_incl. iSplit; iApply type_incl_refl.
Qed.
Lemma type_equal_trans ty1 ty2 ty3 :
type_equal ty1 ty2 -∗ type_equal ty2 ty3 -∗ type_equal ty1 ty3.
Proof.
rewrite !type_equal_incl. iIntros "#[??] #[??]". iSplit.
- iApply (type_incl_trans _ ty2); done.
- iApply (type_incl_trans _ ty2); done.
Qed.
Lemma lft_invariant_eqtype E L T :
Proper (lctx_lft_eq E L ==> eqtype E L) T.
Proof. split; by apply lft_invariant_subtype. Qed.
......@@ -717,16 +764,6 @@ Section subtyping.
- intros ??? H1 H2. split; etrans; (apply H1 || apply H2).
Qed.
Lemma type_incl_simple_type (st1 st2 : simple_type) :
□ (∀ tid vl, st1.(st_own) tid vl -∗ st2.(st_own) tid vl) -∗
type_incl st1 st2.
Proof.
iIntros "#Hst". iSplit; first done. iSplit; iModIntro.
- iIntros. iApply "Hst"; done.
- iIntros (???). iDestruct 1 as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
by iApply "Hst".
Qed.
Lemma subtype_simple_type E L (st1 st2 : simple_type) :
(∀ qmax qL, llctx_interp_noend qmax L qL -∗ □ (elctx_interp E -∗
∀ tid vl, st1.(st_own) tid vl -∗ st2.(st_own) tid vl)) →
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment