Skip to content
Snippets Groups Projects
Commit 39f06310 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Duplicable is defined as persistent in the model. This makes [ty_incl_fn] provable.

parent 152920f9
Branches
Tags
No related merge requests found
Hide whitespace changes
Inline Side-by-side
perm.v
+ 30
− 2
View file @ 39f06310
......@@ -5,14 +5,19 @@ From lrust Require Export type.
Delimit Scope perm_scope with P.
Bind Scope perm_scope with perm.
(* TODO : find a better place for this. *)
Definition valuable := option val.
Definition proj_valuable (n : Z) :=
(≫= λ v, match v with LitV (LitLoc l) => Some (shift_loc l n) | _ => None end).
Module Perm.
Section perm.
Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
Definition has_type (v : val) (ty : type) : perm :=
λ tid, ty.(ty_own) tid [v].
Definition has_type (v : valuable) (ty : type) : perm :=
λ tid, from_option (λ v, ty.(ty_own) tid [v]) False%I v.
Definition extract (κ : lifetime) (ρ : perm) : perm :=
λ tid, (κ ∋ ρ tid)%I.
......@@ -52,3 +57,26 @@ Notation "∃ x .. y , P" :=
(exist (λ x, .. (exist (λ y, P)) ..)) : perm_scope.
Infix "★" := sep (at level 80, right associativity) : perm_scope.
Section duplicable.
Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
Class Duplicable (ρ : @perm Σ) :=
duplicable_persistent tid : PersistentP (ρ tid).
Global Existing Instance duplicable_persistent.
Global Instance has_type_dup v ty : ty.(ty_dup) → Duplicable (v ◁ ty).
Proof. intros Hdup tid. apply _. Qed.
Global Instance lft_incl_dup κ κ' : Duplicable (κ ⊑ κ').
Proof. intros tid. apply _. Qed.
Global Instance sep_dup P Q :
Duplicable P → Duplicable Q → Duplicable (P ★ Q).
Proof. intros HP HQ tid. apply _. Qed.
Global Instance top_dup : Duplicable ⊤.
Proof. intros tid. apply _. Qed.
End duplicable.
\ No newline at end of file
perm_incl.v
+ 6
− 23
View file @ 39f06310
......@@ -15,9 +15,6 @@ Section defs.
Global Instance perm_equiv : Equiv perm :=
λ ρ1 ρ2, perm_incl ρ1 ρ2 ∧ perm_incl ρ2 ρ1.
Class Duplicable (ρ : @perm Σ) :=
perm_incl_duplicable : perm_incl ρ (ρ ★ ρ).
End defs.
Infix "⇒" := perm_incl (at level 95, no associativity) : C_scope.
......@@ -76,6 +73,9 @@ Section props.
Global Instance perm_top_left_id : LeftId (⇔) ⊤ sep.
Proof. intros ρ. by rewrite comm right_id. Qed.
Lemma perm_incl_duplicable ρ (_ : Duplicable ρ) : ρ ⇒ ρ ★ ρ.
Proof. iIntros (tid) "#H!==>". by iSplit. Qed.
Lemma perm_tok_plus κ q1 q2 :
tok κ q1 ★ tok κ q2 ⇔ tok κ (q1 + q2).
Proof.
......@@ -92,30 +92,13 @@ Section props.
Lemma perm_incl_share v κ ty :
v ◁ &uniq{κ} ty ⇒ v ◁ &shr{κ} ty.
Proof.
iIntros (tid) "Huniq". iDestruct "Huniq" as (l) "[% Hown]".
(* FIXME : we nee some tokens here. *)
iIntros (tid) "Huniq". destruct v; last done.
iDestruct "Huniq" as (l) "[% Hown]".
(* FIXME : we need some tokens here. *)
iAssert (∃ q, [κ]{q})%I as "Htok". admit.
iDestruct "Htok" as (q) "Htok".
iVs (ty.(ty_share) _ lrustN with "Hown Htok") as "[Hown _]".
admit. set_solver. iVsIntro. iExists _. iSplit. done. done.
Admitted.
Lemma has_type_dup v ty : ty.(ty_dup) → Duplicable (v ◁ ty).
Proof. iIntros (Hdup tid) "H". by iApply ty_dup_dup. Qed.
Global Instance lft_incl_dup κ κ' : Duplicable (κ ⊑ κ').
Proof. iIntros (tid) "#H!==>". by iSplit. Qed.
Global Instance sep_dup P Q :
Duplicable P → Duplicable Q → Duplicable (P ★ Q).
Proof.
iIntros (HP HQ tid) "[HP HQ]".
iVs (HP with "HP") as "[$$]". by iApply HQ.
Qed.
Global Instance top_dup : Duplicable ⊤.
Proof. iIntros (tid) "_!==>". by iSplit. Qed.
End props.
Hint Extern 0 (Duplicable (_ ◁ _)) => apply has_type_dup; exact I.
type.v
+ 23
− 34
View file @ 39f06310
......@@ -19,11 +19,10 @@ Section defs.
used with anything else than namespaces. *)
ty_shr : lifetime → thread_id → namespace → loc → iProp Σ;
ty_dup_persistent tid vl : ty_dup → PersistentP (ty_own tid vl);
ty_shr_persistent κ tid N l : PersistentP (ty_shr κ tid N l);
ty_size_eq tid vl : ty_own tid vl ⊢ length vl = ty_size;
ty_dup_dup tid vl E :
ty_dup → ty_own tid vl ={E}=> ty_own tid vl ★ ty_own tid vl;
(* The mask for starting the sharing does /not/ include the
namespace N, for allowing more flexibility for the user of
this type (typically for the [own] type). AFAIK, there is no
......@@ -43,7 +42,7 @@ Section defs.
[κ]{q} ★ tl_own tid N ={E}=> ∃ q', ▷l ↦★{q'}: ty_own tid ★
(▷l ↦★{q'}: ty_own tid ={E}=★ [κ]{q} ★ tl_own tid N)
}.
Global Existing Instance ty_shr_persistent.
Global Existing Instances ty_shr_persistent ty_dup_persistent.
Record simple_type :=
{ st_size : nat;
......@@ -60,7 +59,6 @@ Section defs.
(∃ vl, (&frac{κ} λ q, l ↦★{q} vl) ★ ▷ st.(st_own) tid vl)%I
|}.
Next Obligation. apply st_size_eq. Qed.
Next Obligation. iIntros (st tid vl E _) "H". eauto. Qed.
Next Obligation.
intros st E N κ l tid q ??. iIntros "Hmt Htok".
iVs (lft_borrow_exists with "Hmt Htok") as (vl) "[Hmt Htok]". set_solver.
......@@ -106,7 +104,6 @@ Section types.
{| ty_size := 0; ty_dup := true;
ty_own tid vl := False%I; ty_shr κ tid N l := False%I |}.
Next Obligation. iIntros (tid vl) "[]". Qed.
Next Obligation. iIntros (????) "[]". Qed.
Next Obligation.
iIntros (????????) "Hb Htok".
iVs (lft_borrow_exists with "Hb Htok") as (vl) "[Hb Htok]". set_solver.
......@@ -145,10 +142,10 @@ Section types.
(∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ★
∀ q', [κ]{q'} ={mgmtE ∪ N, mgmtE}▷=> ty.(ty_shr) κ tid N l' ★ [κ]{q'})%I
|}.
Next Obligation. done. Qed.
Next Obligation.
iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
Qed.
Next Obligation. done. Qed.
Next Obligation.
intros q ty E N κ l tid q' ?? =>/=. iIntros "Hshr Htok".
iVs (lft_borrow_exists with "Hshr Htok") as (vl) "[Hb Htok]". set_solver.
......@@ -197,10 +194,10 @@ Section types.
∀ q' κ'', κ'' ⊑ κ ★ κ'' ⊑ κ' ★ [κ'']{q'}
={mgmtE ∪ N, mgmtE}▷=> ty.(ty_shr) κ'' tid N l' ★ [κ'']{q'})%I
|}.
Next Obligation. done. Qed.
Next Obligation.
iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
Qed.
Next Obligation. done. Qed.
Next Obligation.
intros κ ty E N κ' l tid q' ?? =>/=. iIntros "Hshr Htok".
iVs (lft_borrow_exists with "Hshr Htok") as (vl) "[Hb Htok]". set_solver.
......@@ -338,23 +335,17 @@ Section types.
tyoffs.1.(ty_shr) κ tid (N .@ i) (shift_loc l (tyoffs.2)))%I
|}.
Next Obligation.
iIntros (tyl tid vl) "Hown". iDestruct "Hown" as (vll) "(%&%&Hown)".
subst. by iApply (list_ty_type_eq with "Hown").
intros tyl tid vl Hfa.
cut (∀ vll, PersistentP ([★ list] tyvl ∈ combine tyl vll,
ty_own (tyvl.1) tid (tyvl.2))). by apply _.
clear vl. induction tyl as [|ty tyl IH]=>[|[|vl vll]]; try by apply _.
edestruct andb_prop_elim as [Hduph Hdupq]. by apply Hfa.
rewrite /PersistentP /= big_sepL_cons.
iIntros "?". by iApply persistentP.
Qed.
Next Obligation.
induction tyl as [|ty tyq IH]; iIntros (tid vl E Hfa) "H";
iDestruct "H" as ([|vl0 vlq]) "(%&#Hlen&Hown)"; subst vl;
iDestruct "Hlen" as %Hlen; inversion Hlen; simpl in *.
- iIntros "!==>". iSplit; iExists []; by repeat iSplit.
- apply andb_prop_elim in Hfa. destruct Hfa as [Hfah Hfaq].
iDestruct (big_sepL_cons with "Hown") as "[Hh Hq]".
iVs (ty_dup_dup with "Hh") as "[Hh1 Hh2]". done.
iVs (IH tid (concat vlq) _ Hfaq with "[Hq]") as "[Hq1 Hq2]". by eauto.
iVsIntro. iSplitL "Hh1 Hq1".
+ iDestruct "Hq1" as (vllq) "(%&%&?)". iExists (vl0::vllq).
rewrite big_sepL_cons/=. iFrame. iSplit; iPureIntro; congruence.
+ iDestruct "Hq2" as (vllq) "(%&%&?)". iExists (vl0::vllq).
rewrite big_sepL_cons/=. iFrame. iSplit; iPureIntro; congruence.
iIntros (tyl tid vl) "Hown". iDestruct "Hown" as (vll) "(%&%&Hown)".
subst. by iApply (list_ty_type_eq with "Hown").
Qed.
Next Obligation.
intros tyl E N κ l tid q ??. rewrite split_prod_mt.
......@@ -385,7 +376,7 @@ Section types.
iIntros (q i offs) "#Hshr!#([Htokh Htokq]&Htlf&Htlh&Htlq)".
rewrite big_sepL_cons Nat.add_0_r.
iDestruct "Hshr" as "[Hshrh Hshrq]". setoid_rewrite <-Nat.add_succ_comm.
iVs (IH with "Hshrq [Htokq Htlf Htlq]") as (q'q) "[Hownq Hcloseq]". done. by iFrame.
iVs (IH with "Hshrq [Htokq Htlf Htlq]") as (q'q) "[Hownq Hcloseq]". by iFrame.
iVs (tyh.(ty_shr_acc) with "Hshrh [Htokh Htlh]") as (q'h) "[Hownh Hcloseh]"; try done.
by pose proof (nclose_subseteq N i); set_solver. by iFrame.
destruct (Qp_lower_bound q'h q'q) as (q' & q'0h & q'0q & -> & ->).
......@@ -440,16 +431,14 @@ Section types.
(nth i tyl bot).(ty_shr) κ tid N (shift_loc l 1))%I
|}.
Next Obligation.
iIntros (n tyl Hn tid vl) "Hown". iDestruct "Hown" as (i vl') "(%&Hown)". subst.
simpl. by iDestruct (sum_size_eq with "Hown") as %->.
intros n tyl Hn tid vl Hdup%Is_true_eq_true.
cut (∀ i vl', PersistentP (ty_own (nth i tyl bot) tid vl')). apply _.
intros. apply ty_dup_persistent. edestruct nth_in_or_default as [| ->]; last done.
rewrite ->forallb_forall in Hdup. auto using Is_true_eq_left.
Qed.
Next Obligation.
iIntros (n tyl Hn tid vl E Hdup%Is_true_eq_true) "Hown".
iDestruct "Hown" as (i vl') "[% Hown]". subst.
iVs ((nth i tyl bot).(ty_dup_dup) with "Hown") as "[Hown1 Hown2]".
- edestruct nth_in_or_default as [| ->]; last done.
rewrite ->forallb_forall in Hdup. auto using Is_true_eq_left.
- iSplitR "Hown1"; eauto.
iIntros (n tyl Hn tid vl) "Hown". iDestruct "Hown" as (i vl') "(%&Hown)". subst.
simpl. by iDestruct (sum_size_eq with "Hown") as %->.
Qed.
Next Obligation.
intros n tyl Hn E N κ l tid q ??. iIntros "Hown Htok". rewrite split_sum_mt.
......@@ -503,13 +492,13 @@ Section types.
Program Definition cont {n : nat} (ρ : vec val n → @perm Σ) :=
{| ty_size := 1; ty_dup := false;
ty_own tid vl := (∃ f, vl = [f] ★
∀ vl, ▷ ρ vl tid -★ tl_own tid ⊤
∀ vl, ρ vl tid -★ tl_own tid ⊤
-★ WP f (map of_val vl) {{λ _, False}})%I;
ty_shr κ tid N l := True%I |}.
Next Obligation. done. Qed.
Next Obligation.
iIntros (n ρ tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
Qed.
Next Obligation. done. Qed.
Next Obligation. intros. by iIntros "_ $". Qed.
Next Obligation. intros. by iIntros "_ _". Qed.
Next Obligation. done. Qed.
......@@ -517,7 +506,7 @@ Section types.
Program Definition fn {n : nat} (ρ : vec val n → @perm Σ):=
ty_of_st {| st_size := 1;
st_own tid vl := (∃ f, vl = [f] ★
∀ vl, {{ ▷ ρ vl tid ★ tl_own tid ⊤ }} f (map of_val vl) {{λ _, False}})%I |}.
∀ vl, {{ ρ vl tid ★ tl_own tid ⊤ }} f (map of_val vl) {{λ _, False}})%I |}.
Next Obligation.
iIntros (n ρ tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
Qed.
......
type_incl.v
+ 41
− 38
View file @ 39f06310
From iris.algebra Require Import upred_big_op.
From iris.program_logic Require Import thread_local.
From iris.program_logic Require Import thread_local hoare.
From lrust Require Export type perm_incl.
Import Types.
......@@ -40,9 +40,8 @@ Section ty_incl.
Global Instance ty_incl_preorder ρ: Duplicable ρ → PreOrder (ty_incl ρ).
Proof.
split.
- apply _.
- intros ?????. eauto using ty_incl_weaken, ty_incl_trans.
split. apply _.
eauto using ty_incl_weaken, ty_incl_trans, perm_incl_duplicable.
Qed.
Lemma ty_incl_bot ρ ty : ty_incl ρ ! ty.
......@@ -87,34 +86,37 @@ Section ty_incl.
by iApply (ty_shr_mono with "Hincl Hty").
Qed.
(* We have the additional hypothesis that ρ should be duplicable.
The only way I can see to circumvent this limitation is to deeply
embed permissions (and their inclusion). Not sure this is worth it. *)
Lemma ty_incl_prod ρ tyl1 tyl2 :
Duplicable ρ → Forall2 (ty_incl ρ) tyl1 tyl2 →
ty_incl ρ (product tyl1) (product tyl2).
Proof.
intros Hρ HFA. eapply ty_incl_weaken. apply Hρ.
iIntros (tid) "[Hρ1 Hρ2]". iSplitL "Hρ1".
intros Hρ HFA. iIntros (tid) "#Hρ". iSplitL "".
- assert (Himpl : ρ tid ={⊤}=>
□ (∀ vll, length tyl1 = length vll →
([★ list] tyvl ∈ combine tyl1 vll, ty_own (tyvl.1) tid (tyvl.2))
→ ([★ list] tyvl ∈ combine tyl2 vll, ty_own (tyvl.1) tid (tyvl.2)))).
{ induction HFA as [|ty1 ty2 tyl1 tyl2 Hincl HFA IH].
- iIntros "_!==>!#* _ _". by rewrite big_sepL_nil.
- iIntros "Hρ". iVs (Hρ with "Hρ") as "[Hρ1 Hρ2]".
iVs (IH with "Hρ1") as "#Hqimpl". iVs (Hincl with "Hρ2") as "[#Hhimpl _]".
iIntros "!==>!#*%". destruct vll as [|vlh vllq]. done. rewrite !big_sepL_cons.
- iIntros "#Hρ". iVs (IH with "Hρ") as "#Hqimpl".
iVs (Hincl with "Hρ") as "[#Hhimpl _]".
iIntros "!==>!#*%". destruct vll as [|vlh vllq]. done.
rewrite !big_sepL_cons.
iIntros "[Hh Hq]". iSplitL "Hh". by iApply "Hhimpl".
iApply ("Hqimpl" with "[] Hq"). iPureIntro. simpl in *. congruence. }
iVs (Himpl with "Hρ1") as "#Himpl". iIntros "!==>!#*H".
iVs (Himpl with "Hρ") as "#Himpl". iIntros "!==>!#*H".
iDestruct "H" as (vll) "(%&%&H)". iExists _. iSplit. done. iSplit.
by rewrite -(Forall2_length _ _ _ HFA). by iApply ("Himpl" with "[] H").
- rewrite /product /=. iRevert "Hρ2". generalize O.
- rewrite /product /=. iRevert "Hρ". generalize O.
change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). generalize O.
induction HFA as [|ty1 ty2 tyl1 tyl2 Hincl HFA IH].
+ iIntros (i offs) "_!==>!#*_/=". rewrite big_sepL_nil. eauto.
+ iIntros (i offs) "Hρ". iVs (Hρ with "Hρ") as "[Hρ1 Hρ2]".
iVs (IH with "[] Hρ1") as "#Hqimpl".
done. (* TODO : get rid of this done by doing induction in the proof mode. *)
iVs (Hincl with "Hρ2") as "[_ #Hhimpl]". iIntros "!==>!#*".
+ iIntros (i offs) "#Hρ". iVs (IH with "[] []") as "#Hqimpl".
by iClear "Hρ". (* TODO : get rid of this by doing induction in the proof mode. *)
done.
iVs (Hincl with "Hρ") as "[_ #Hhimpl]". iIntros "!==>!#*".
rewrite !big_sepL_cons. iIntros "[Hh Hq]".
setoid_rewrite <-Nat.add_succ_comm.
iDestruct ("Hhimpl" $! _ _ _ with "Hh") as "[$ %]".
......@@ -144,20 +146,18 @@ Section ty_incl.
Admitted.
Lemma ty_incl_sum ρ n tyl1 tyl2 (_ : LstTySize n tyl1) (_ : LstTySize n tyl2) :
Duplicable ρ →
Forall2 (ty_incl ρ) tyl1 tyl2 → ty_incl ρ (sum tyl1) (sum tyl2).
Duplicable ρ → Forall2 (ty_incl ρ) tyl1 tyl2 →
ty_incl ρ (sum tyl1) (sum tyl2).
Proof.
iIntros (DUP FA tid) "Hρ". rewrite /sum /=.
iVs (DUP with "Hρ") as "[Hρ1 Hρ2]". iSplitR "Hρ2".
iIntros (DUP FA tid) "#Hρ". rewrite /sum /=. iSplitR "".
- assert (Hincl : ρ tid ={⊤}=>
(□ ∀ i vl, (nth i tyl1 !%T).(ty_own) tid vl
→ (nth i tyl2 !%T).(ty_own) tid vl)).
{ clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
- iIntros "_!==>*!#". eauto.
- iIntros "Hρ". iVs (DUP with "Hρ") as "[Hρ1 Hρ2]".
iVs (IH with "Hρ1") as "#IH". iVs (Hincl with "Hρ2") as "[#Hh _]".
- iIntros "#Hρ". iVs (IH with "Hρ") as "#IH". iVs (Hincl with "Hρ") as "[#Hh _]".
iIntros "!==>*!#*Hown". destruct i as [|i]. by iApply "Hh". by iApply "IH". }
iVs (Hincl with "Hρ1") as "#Hincl". iIntros "!==>!#*H".
iVs (Hincl with "Hρ") as "#Hincl". iIntros "!==>!#*H".
iDestruct "H" as (i vl') "[% Hown]". subst. iExists _, _. iSplit. done.
by iApply "Hincl".
- assert (Hincl : ρ tid ={⊤}=>
......@@ -165,11 +165,11 @@ Section ty_incl.
→ (nth i tyl2 !%T).(ty_shr) κ tid E l)).
{ clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
- iIntros "_!==>*!#". eauto.
- iIntros "Hρ". iVs (DUP with "Hρ") as "[Hρ1 Hρ2]".
iVs (IH with "Hρ1") as "#IH". iVs (Hincl with "Hρ2") as "[_ #Hh]".
- iIntros "#Hρ".
iVs (IH with "Hρ") as "#IH". iVs (Hincl with "Hρ") as "[_ #Hh]".
iIntros "!==>*!#*Hown". destruct i as [|i]; last by iApply "IH".
by iDestruct ("Hh" $! _ _ _ with "Hown") as "[$ _]". }
iVs (Hincl with "Hρ2") as "#Hincl". iIntros "!==>!#*H". iSplit; last done.
iVs (Hincl with "Hρ") as "#Hincl". iIntros "!==>!#*H". iSplit; last done.
iDestruct "H" as (i) "[??]". iExists _. iSplit. done. by iApply "Hincl".
Qed.
......@@ -203,23 +203,26 @@ Section ty_incl.
Duplicable ρ → (∀ vl : vec val n, ρ ★ ρ2 vl ⇒ ρ1 vl) →
ty_incl ρ (cont ρ1) (cont ρ2).
Proof.
iIntros (? Hρ1ρ2 tid) "Hρ".
iVs (inv_alloc lrustN _ (ρ tid) with "[Hρ]") as "#INV". by auto.
iIntros "!==>". iSplit; iIntros "!#*H"; last by auto.
iIntros (? Hρ1ρ2 tid) "#Hρ!==>". iSplit; iIntros "!#*H"; last by auto.
iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
iIntros (vl) "Htl Hown".
iApply pvs_wp. iInv lrustN as "Hρ" "Hclose".
(* FIXME : we need some kind of "Invariant of duplicable
propositions" that we can open several times. *)
admit.
Admitted.
iIntros (vl) "Hρ2 Htl". iVs (Hρ1ρ2 with "[Hρ2]"). by iFrame.
by iApply ("Hwp" with "[-Htl] Htl").
Qed.
Lemma ty_incl_fn {n} ρ ρ1 ρ2 :
Duplicable ρ → (∀ vl : vec val n, ρ ★ ρ2 vl ⇒ ρ1 vl) →
ty_incl ρ (fn ρ1) (fn ρ2).
(* FIXME : idem. *)
admit.
Admitted.
Proof.
iIntros (? Hρ1ρ2 tid) "#Hρ!==>". iSplit; iIntros "!#*#H".
- iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
iIntros (vl) "!#[Hρ2 Htl]". iVs (Hρ1ρ2 with "[Hρ2]"). by iFrame.
iApply "Hwp". by iFrame.
- iSplit; last done. simpl. iDestruct "H" as (vl0) "[? Hvl]".
iExists vl0. iFrame "#". iNext. iDestruct "Hvl" as (f) "[% Hwp]".
iExists f. iSplit. done.
iIntros (vl) "!#[Hρ2 Htl]". iVs (Hρ1ρ2 with "[Hρ2]"). by iFrame.
iApply "Hwp". by iFrame.
Qed.
Lemma ty_incl_fn_cont {n} ρ ρf : ty_incl ρ (fn ρf) (cont (n:=n) ρf).
Proof.
......@@ -234,7 +237,7 @@ Section ty_incl.
ty_incl ρ ty1 ty2 → ρ ★ v ◁ ty1 ⇒ v ◁ ty2.
Proof.
iIntros (Hincl tid) "[Hρ Hty1]". iVs (Hincl with "Hρ") as "[#Hownincl _]".
by iApply "Hownincl".
destruct v; last done. by iApply "Hownincl".
Qed.
End ty_incl.
\ No newline at end of file
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment