Library iris.chan_lang.simple_types
From iris.chan_lang Require Export lang protocol notation.
From iris.prelude Require Import gmap stringmap mapset list.
Inductive typ :=
| Tensor: typ → typ → typ
| Lolli: typ → typ → typ
| Unit: typ
| Int: typ
| Bool: typ
| Sum: typ → typ → typ
| Styp: protocol typ → typ.
Definition typ_ctx := gmap string typ.
Module examples.
CoFixpoint IntStream : protocol typ :=
prot_send Int IntStream.
Definition IntStreamTyp : typ := Styp IntStream.
End examples.
Import chan_lang.
Import iris.chan_lang.derived.
Import iris.chan_lang.notation.
Inductive has_typ (Γ: typ_ctx): chan_lang.expr → typ → Prop :=
| var_typ x ty:
Γ !! x = Some ty →
has_typ Γ (Var x) ty
| bool_typ b:
has_typ Γ (Lit (LitBool b)) Bool
| int_typ n:
has_typ Γ (Lit (LitInt n)) Int
| unit_typ:
has_typ Γ (Lit (LitUnit)) Unit
| pair_intro_typ Γ1 e1 ty1 Γ2 e2 ty2:
has_typ Γ1 e1 ty1 →
has_typ Γ2 e2 ty2 →
dom (gset string) Γ1 ∩ dom (gset string) Γ2 ≡ ∅ →
Γ1 ⊆ Γ →
Γ2 ⊆ Γ →
has_typ Γ (Pair e1 e2) (Tensor ty1 ty2)
| pair_elim_typ (x y: string) Γ1 e ty1 ty2 Γ2 eb ty:
has_typ Γ1 e (Tensor ty1 ty2) →
has_typ (<[x := ty1]>(<[y := ty2]>Γ2)) eb ty →
x ≠ y → Γ2 !! x = None → Γ2 !! y = None →
dom (gset string) Γ1 ∩ dom (gset string) Γ2 ≡ ∅ →
Γ1 ⊆ Γ →
Γ2 ⊆ Γ →
has_typ Γ (Letp x y e eb) ty
| seq_typ Γ1 e1 Γ2 e2 ty1 ty2:
has_typ Γ1 e1 ty1 →
has_typ Γ2 e2 ty2 →
dom (gset string) Γ1 ∩ dom (gset string) Γ2 ≡ ∅ →
Γ1 ⊆ Γ →
Γ2 ⊆ Γ →
has_typ Γ (App (Lam BAnon e1) e2) ty1
| fork_typ e ty:
has_typ Γ e ty →
has_typ Γ (Fork e) Unit
| lolli_intro_typ x ty1 e ty2 :
has_typ (<[x := ty1]>Γ) e ty2 →
has_typ Γ (Rec BAnon (BNamed x) e) (Lolli ty1 ty2)
| lolli_elim_typ Γ1 e1 ty1 ty2 Γ2 e2 :
has_typ Γ1 e1 (Lolli ty1 ty2) →
has_typ Γ2 e2 ty1 →
dom (gset string) Γ1 ∩ dom (gset string) Γ2 ≡ ∅ →
Γ1 ⊆ Γ →
Γ2 ⊆ Γ →
has_typ Γ (App e1 e2) ty2
| session_intro_typ p :
has_typ Γ Alloc (Tensor (Styp p) (Styp (dual p)))
| send_typ Γ1 e ty p Γ2 ev :
has_typ Γ1 e (Styp (prot_send ty p)) →
has_typ Γ2 ev ty →
dom (gset string) Γ1 ∩ dom (gset string) Γ2 ≡ ∅ →
Γ1 ⊆ Γ →
Γ2 ⊆ Γ →
has_typ Γ (Send e ev) (Styp p)
| recv_typ e ty p :
has_typ Γ e (Styp (prot_recv ty p)) →
has_typ Γ (Recv e) (Tensor (Styp p) ty)
| session_equiv p p' e :
p ≡ p' →
has_typ Γ e (Styp p) →
has_typ Γ e (Styp p').
Hint Constructors has_typ.
Section tests.
Goal has_typ {["x" := Unit]} (chan_lang.Var "x") Unit.
Proof. eauto. Qed.
Remark ht_id1: has_typ ∅ (Lam "x" "x") (Lolli Int Int).
Proof.
eapply lolli_intro_typ; eauto.
Qed.
Goal has_typ ∅ (Pair (Lam "x" "x") #3) (Tensor (Lolli Int Int) Int).
Proof.
eapply pair_intro_typ; eauto.
- eauto.
- rewrite dom_empty; set_solver.
Qed.
Goal has_typ ∅ (letp: "x" "y" := newch in
Fork(Send "x" #3) ;;
letp: "y'" "res" := Recv "y" in
"res")%C Int.
eapply pair_elim_typ; eauto.
- eapply (seq_typ _ (<["y":= Styp (dual (prot_send Int prot_end))]>∅) _
(<["x":= Styp (prot_send Int prot_end)]>∅)).
× eapply (pair_elim_typ _ _ _ (<["y":=Styp (dual (prot_send Int prot_end))]>∅) _ _ _ ∅).
** eapply recv_typ. eapply session_equiv; last first; eauto.
rewrite (unfold_prot (dual _)) //=.
** eapply var_typ; eauto.
** auto.
** set_solver.
** set_solver.
** rewrite dom_empty. set_solver.
** set_solver.
** eapply insert_subseteq; set_solver.
× eapply fork_typ. eapply (send_typ _ _ _ _ _ ∅); eauto.
** eapply var_typ; eauto.
** rewrite dom_empty. set_solver.
** eapply insert_subseteq. set_solver.
× rewrite ?dom_insert ?dom_empty. set_solver.
× eapply insert_subseteq. set_solver.
× rewrite insert_commute; auto.
eapply insert_subseteq. auto.
- eauto.
- eauto.
- rewrite dom_empty; set_solver.
Qed.
End tests.
Section type_lemmas.
Lemma cons_included {A} (a: A) l1 l2:
l1 `included` l2 → a :: l1 `included` a :: l2.
Proof. set_unfold=>?? [?|?]; naive_solver. Qed.
Instance included_permutation {A} : Proper (Permutation ==> Permutation ==> iff) (@list.included A).
Proof.
intros l1 l2 Hperm l1' l2' Hperm'.
split; intros Hin ?.
- rewrite -Hperm' -Hperm; eauto.
- rewrite Hperm' Hperm; eauto.
Qed.
Lemma typ_context_closed_1 Γ l e ty:
has_typ Γ e ty → (∀ x, x ∈ dom (gset string) Γ → x ∈ l) → Closed l e.
Proof.
intros Htyp; revert l; induction Htyp⇒l; try done;
rewrite /Closed⇒Hin; simplify_eq/=;
repeat (match goal with
| [ H: ?Γ' ⊆ ?Γ |- _ ] ⇒
match type of Γ with
typ_ctx ⇒ eapply subseteq_dom in H; eauto
end
| [ |- context [is_closed ?l1 ?e1 && is_closed ?l2 ?e2] ] ⇒
apply andb_prop_intro; split
| [ H: ∀ l : list string, ?P → Closed l ?e |- context [is_closed ?l' ?e]] ⇒
eapply H; intros x'; rewrite ?dom_insert; set_unfold; naive_solver
end).
rewrite bool_decide_spec. apply Hin, elem_of_dom; eauto.
Qed.
Lemma typ_context_closed_2 Γ e ty:
has_typ Γ e ty → Closed (map_to_list Γ.*1) e.
Proof.
intros ?%typ_context_closed_1; eauto.
intros x. rewrite elem_of_dom. intros [ty' Heq].
rewrite elem_of_list_fmap. ∃ (x, ty'); split; auto.
by apply elem_of_map_to_list.
Qed.
Lemma typ_weaken Γ Γ' e ty:
has_typ Γ e ty →
Γ ⊆ Γ' →
has_typ Γ' e ty.
Proof.
intros Htyp Hsub. revert Γ' Hsub.
induction Htyp⇒Γ' Hsub; eauto;
try (econstructor; eauto; etransitivity; eauto; done).
- econstructor. eapply lookup_weaken; eauto.
- econstructor; eauto.
× apply IHHtyp. apply map_subseteq_spec⇒ x' ty'.
case (decide (x' = x)).
** intros →. rewrite ?lookup_insert //=.
** intros ?. rewrite ?lookup_insert_ne //. intros ?%map_subseteq_spec; eauto.
Qed.
Ltac lookup_functional :=
match goal with
[ H1: ?Γ !! ?x = Some ?t1 ∨ ?Γ !! ?x = None,
H2: ?Γ !! ?x = Some ?t2 |- _ ] ⇒
assert (t1 = t2) by (destruct H1 as [H1|H1]; rewrite H1 in H2; congruence); subst
end.
Ltac lookup_subseteq :=
match goal with
[ H1: ?Γ !! ?x = Some ?t1 ∨ ?Γ !! ?x = None,
H2: ?Γ' !! ?x = Some ?t2,
H3: ?Γ' ⊆ ?Γ |- _ ] ⇒
assert (Γ !! x = Some t2) by
(eapply map_subseteq_spec in H2; eauto)
end.
Lemma lookup_subseteq_same_or_none (Γ1 Γ2: typ_ctx) x ty:
Γ2 !! x = Some ty ∨ Γ2 !! x = None →
Γ1 ⊆ Γ2 →
Γ1 !! x = Some ty ∨ Γ1 !! x = None.
Proof.
intros.
remember (Γ1 !! x) as mty eqn:Heq; symmetry in Heq.
destruct mty as [ty''|]; subst; eauto.
lookup_subseteq. lookup_functional. eauto.
Qed.
Lemma typ_subst Γ x es e ty1 ty2:
has_typ Γ e ty2 →
has_typ ∅ es ty1 →
(Γ !! x = Some ty1 ∨ Γ !! x = None) →
has_typ (delete x Γ) (subst x es e) ty2.
Proof.
intros Htyp_e. revert es ty1. induction Htyp_e⇒es ty'; try (econstructor; done).
- simpl. case_decide. intros; subst.
× lookup_functional.
eapply typ_weaken; eauto.
apply map_subseteq_spec. inversion 1.
× intros. econstructor. rewrite lookup_delete_ne //.
- simplify_eq/=.
intros. eapply (pair_intro_typ _ (delete x Γ1) _ _ (delete x Γ2)).
× eapply IHHtyp_e1; eauto using lookup_subseteq_same_or_none.
× eapply IHHtyp_e2; eauto using lookup_subseteq_same_or_none.
× rewrite ?dom_delete. set_solver.
× by apply delete_subseteq_compat.
× by apply delete_subseteq_compat.
- simplify_eq/=.
intros. eapply (pair_elim_typ _ _ _ (delete x Γ1) _ _ _ (delete x Γ2)); auto.
× eapply IHHtyp_e1; eauto using lookup_subseteq_same_or_none.
× case_decide as Hdec.
** rewrite -delete_insert_ne; last naive_solver.
rewrite -delete_insert_ne; last naive_solver.
eapply IHHtyp_e2; eauto.
rewrite ?lookup_insert_ne; [|naive_solver|naive_solver].
eauto using lookup_subseteq_same_or_none.
** rewrite not_and_l in Hdec *=>Hcase.
destruct Hcase as [Heq%dec_stable|Heq%dec_stable]; inversion Heq; subst.
*** rewrite -delete_insert_ne; last naive_solver.
by rewrite insert_delete.
*** by rewrite insert_delete.
× apply lookup_delete_None; auto.
× apply lookup_delete_None; auto.
× rewrite ?dom_delete. set_solver.
× by apply delete_subseteq_compat.
× by apply delete_subseteq_compat.
- simplify_eq/=.
intros; eapply (seq_typ _ (delete x Γ1) _ (delete x Γ2)).
× eapply IHHtyp_e1; eauto using lookup_subseteq_same_or_none.
× eapply IHHtyp_e2; eauto using lookup_subseteq_same_or_none.
× rewrite ?dom_delete. set_solver.
× by apply delete_subseteq_compat.
× by apply delete_subseteq_compat.
- intros; eapply (fork_typ); eauto.
- simplify_eq/=.
intros. eapply (lolli_intro_typ); auto.
× case_decide as Hdec.
** rewrite -delete_insert_ne; last naive_solver.
eapply IHHtyp_e; eauto.
rewrite ?lookup_insert_ne; [|naive_solver].
eauto using lookup_subseteq_same_or_none.
** rewrite not_and_l in Hdec *=>Hcase.
destruct Hcase as [Heq%dec_stable|Heq%dec_stable]; inversion Heq; subst.
by rewrite insert_delete.
- simplify_eq/=.
intros. eapply (lolli_elim_typ _ (delete x Γ1) _ _ _ (delete x Γ2)); auto.
× eapply IHHtyp_e1; eauto using lookup_subseteq_same_or_none.
× eapply IHHtyp_e2; eauto using lookup_subseteq_same_or_none.
× rewrite ?dom_delete. set_solver.
× by apply delete_subseteq_compat.
× by apply delete_subseteq_compat.
- simplify_eq/=.
intros. eapply (send_typ _ (delete x Γ1) _ _ _ (delete x Γ2)); auto.
× eapply IHHtyp_e1; eauto using lookup_subseteq_same_or_none.
× eapply IHHtyp_e2; eauto using lookup_subseteq_same_or_none.
× rewrite ?dom_delete. set_solver.
× by apply delete_subseteq_compat.
× by apply delete_subseteq_compat.
- simplify_eq/=.
intros. eapply (recv_typ); eauto.
- eauto.
Qed.
End type_lemmas.
From iris.prelude Require Import gmap stringmap mapset list.
Inductive typ :=
| Tensor: typ → typ → typ
| Lolli: typ → typ → typ
| Unit: typ
| Int: typ
| Bool: typ
| Sum: typ → typ → typ
| Styp: protocol typ → typ.
Definition typ_ctx := gmap string typ.
Module examples.
CoFixpoint IntStream : protocol typ :=
prot_send Int IntStream.
Definition IntStreamTyp : typ := Styp IntStream.
End examples.
Import chan_lang.
Import iris.chan_lang.derived.
Import iris.chan_lang.notation.
Inductive has_typ (Γ: typ_ctx): chan_lang.expr → typ → Prop :=
| var_typ x ty:
Γ !! x = Some ty →
has_typ Γ (Var x) ty
| bool_typ b:
has_typ Γ (Lit (LitBool b)) Bool
| int_typ n:
has_typ Γ (Lit (LitInt n)) Int
| unit_typ:
has_typ Γ (Lit (LitUnit)) Unit
| pair_intro_typ Γ1 e1 ty1 Γ2 e2 ty2:
has_typ Γ1 e1 ty1 →
has_typ Γ2 e2 ty2 →
dom (gset string) Γ1 ∩ dom (gset string) Γ2 ≡ ∅ →
Γ1 ⊆ Γ →
Γ2 ⊆ Γ →
has_typ Γ (Pair e1 e2) (Tensor ty1 ty2)
| pair_elim_typ (x y: string) Γ1 e ty1 ty2 Γ2 eb ty:
has_typ Γ1 e (Tensor ty1 ty2) →
has_typ (<[x := ty1]>(<[y := ty2]>Γ2)) eb ty →
x ≠ y → Γ2 !! x = None → Γ2 !! y = None →
dom (gset string) Γ1 ∩ dom (gset string) Γ2 ≡ ∅ →
Γ1 ⊆ Γ →
Γ2 ⊆ Γ →
has_typ Γ (Letp x y e eb) ty
| seq_typ Γ1 e1 Γ2 e2 ty1 ty2:
has_typ Γ1 e1 ty1 →
has_typ Γ2 e2 ty2 →
dom (gset string) Γ1 ∩ dom (gset string) Γ2 ≡ ∅ →
Γ1 ⊆ Γ →
Γ2 ⊆ Γ →
has_typ Γ (App (Lam BAnon e1) e2) ty1
| fork_typ e ty:
has_typ Γ e ty →
has_typ Γ (Fork e) Unit
| lolli_intro_typ x ty1 e ty2 :
has_typ (<[x := ty1]>Γ) e ty2 →
has_typ Γ (Rec BAnon (BNamed x) e) (Lolli ty1 ty2)
| lolli_elim_typ Γ1 e1 ty1 ty2 Γ2 e2 :
has_typ Γ1 e1 (Lolli ty1 ty2) →
has_typ Γ2 e2 ty1 →
dom (gset string) Γ1 ∩ dom (gset string) Γ2 ≡ ∅ →
Γ1 ⊆ Γ →
Γ2 ⊆ Γ →
has_typ Γ (App e1 e2) ty2
| session_intro_typ p :
has_typ Γ Alloc (Tensor (Styp p) (Styp (dual p)))
| send_typ Γ1 e ty p Γ2 ev :
has_typ Γ1 e (Styp (prot_send ty p)) →
has_typ Γ2 ev ty →
dom (gset string) Γ1 ∩ dom (gset string) Γ2 ≡ ∅ →
Γ1 ⊆ Γ →
Γ2 ⊆ Γ →
has_typ Γ (Send e ev) (Styp p)
| recv_typ e ty p :
has_typ Γ e (Styp (prot_recv ty p)) →
has_typ Γ (Recv e) (Tensor (Styp p) ty)
| session_equiv p p' e :
p ≡ p' →
has_typ Γ e (Styp p) →
has_typ Γ e (Styp p').
Hint Constructors has_typ.
Section tests.
Goal has_typ {["x" := Unit]} (chan_lang.Var "x") Unit.
Proof. eauto. Qed.
Remark ht_id1: has_typ ∅ (Lam "x" "x") (Lolli Int Int).
Proof.
eapply lolli_intro_typ; eauto.
Qed.
Goal has_typ ∅ (Pair (Lam "x" "x") #3) (Tensor (Lolli Int Int) Int).
Proof.
eapply pair_intro_typ; eauto.
- eauto.
- rewrite dom_empty; set_solver.
Qed.
Goal has_typ ∅ (letp: "x" "y" := newch in
Fork(Send "x" #3) ;;
letp: "y'" "res" := Recv "y" in
"res")%C Int.
eapply pair_elim_typ; eauto.
- eapply (seq_typ _ (<["y":= Styp (dual (prot_send Int prot_end))]>∅) _
(<["x":= Styp (prot_send Int prot_end)]>∅)).
× eapply (pair_elim_typ _ _ _ (<["y":=Styp (dual (prot_send Int prot_end))]>∅) _ _ _ ∅).
** eapply recv_typ. eapply session_equiv; last first; eauto.
rewrite (unfold_prot (dual _)) //=.
** eapply var_typ; eauto.
** auto.
** set_solver.
** set_solver.
** rewrite dom_empty. set_solver.
** set_solver.
** eapply insert_subseteq; set_solver.
× eapply fork_typ. eapply (send_typ _ _ _ _ _ ∅); eauto.
** eapply var_typ; eauto.
** rewrite dom_empty. set_solver.
** eapply insert_subseteq. set_solver.
× rewrite ?dom_insert ?dom_empty. set_solver.
× eapply insert_subseteq. set_solver.
× rewrite insert_commute; auto.
eapply insert_subseteq. auto.
- eauto.
- eauto.
- rewrite dom_empty; set_solver.
Qed.
End tests.
Section type_lemmas.
Lemma cons_included {A} (a: A) l1 l2:
l1 `included` l2 → a :: l1 `included` a :: l2.
Proof. set_unfold=>?? [?|?]; naive_solver. Qed.
Instance included_permutation {A} : Proper (Permutation ==> Permutation ==> iff) (@list.included A).
Proof.
intros l1 l2 Hperm l1' l2' Hperm'.
split; intros Hin ?.
- rewrite -Hperm' -Hperm; eauto.
- rewrite Hperm' Hperm; eauto.
Qed.
Lemma typ_context_closed_1 Γ l e ty:
has_typ Γ e ty → (∀ x, x ∈ dom (gset string) Γ → x ∈ l) → Closed l e.
Proof.
intros Htyp; revert l; induction Htyp⇒l; try done;
rewrite /Closed⇒Hin; simplify_eq/=;
repeat (match goal with
| [ H: ?Γ' ⊆ ?Γ |- _ ] ⇒
match type of Γ with
typ_ctx ⇒ eapply subseteq_dom in H; eauto
end
| [ |- context [is_closed ?l1 ?e1 && is_closed ?l2 ?e2] ] ⇒
apply andb_prop_intro; split
| [ H: ∀ l : list string, ?P → Closed l ?e |- context [is_closed ?l' ?e]] ⇒
eapply H; intros x'; rewrite ?dom_insert; set_unfold; naive_solver
end).
rewrite bool_decide_spec. apply Hin, elem_of_dom; eauto.
Qed.
Lemma typ_context_closed_2 Γ e ty:
has_typ Γ e ty → Closed (map_to_list Γ.*1) e.
Proof.
intros ?%typ_context_closed_1; eauto.
intros x. rewrite elem_of_dom. intros [ty' Heq].
rewrite elem_of_list_fmap. ∃ (x, ty'); split; auto.
by apply elem_of_map_to_list.
Qed.
Lemma typ_weaken Γ Γ' e ty:
has_typ Γ e ty →
Γ ⊆ Γ' →
has_typ Γ' e ty.
Proof.
intros Htyp Hsub. revert Γ' Hsub.
induction Htyp⇒Γ' Hsub; eauto;
try (econstructor; eauto; etransitivity; eauto; done).
- econstructor. eapply lookup_weaken; eauto.
- econstructor; eauto.
× apply IHHtyp. apply map_subseteq_spec⇒ x' ty'.
case (decide (x' = x)).
** intros →. rewrite ?lookup_insert //=.
** intros ?. rewrite ?lookup_insert_ne //. intros ?%map_subseteq_spec; eauto.
Qed.
Ltac lookup_functional :=
match goal with
[ H1: ?Γ !! ?x = Some ?t1 ∨ ?Γ !! ?x = None,
H2: ?Γ !! ?x = Some ?t2 |- _ ] ⇒
assert (t1 = t2) by (destruct H1 as [H1|H1]; rewrite H1 in H2; congruence); subst
end.
Ltac lookup_subseteq :=
match goal with
[ H1: ?Γ !! ?x = Some ?t1 ∨ ?Γ !! ?x = None,
H2: ?Γ' !! ?x = Some ?t2,
H3: ?Γ' ⊆ ?Γ |- _ ] ⇒
assert (Γ !! x = Some t2) by
(eapply map_subseteq_spec in H2; eauto)
end.
Lemma lookup_subseteq_same_or_none (Γ1 Γ2: typ_ctx) x ty:
Γ2 !! x = Some ty ∨ Γ2 !! x = None →
Γ1 ⊆ Γ2 →
Γ1 !! x = Some ty ∨ Γ1 !! x = None.
Proof.
intros.
remember (Γ1 !! x) as mty eqn:Heq; symmetry in Heq.
destruct mty as [ty''|]; subst; eauto.
lookup_subseteq. lookup_functional. eauto.
Qed.
Lemma typ_subst Γ x es e ty1 ty2:
has_typ Γ e ty2 →
has_typ ∅ es ty1 →
(Γ !! x = Some ty1 ∨ Γ !! x = None) →
has_typ (delete x Γ) (subst x es e) ty2.
Proof.
intros Htyp_e. revert es ty1. induction Htyp_e⇒es ty'; try (econstructor; done).
- simpl. case_decide. intros; subst.
× lookup_functional.
eapply typ_weaken; eauto.
apply map_subseteq_spec. inversion 1.
× intros. econstructor. rewrite lookup_delete_ne //.
- simplify_eq/=.
intros. eapply (pair_intro_typ _ (delete x Γ1) _ _ (delete x Γ2)).
× eapply IHHtyp_e1; eauto using lookup_subseteq_same_or_none.
× eapply IHHtyp_e2; eauto using lookup_subseteq_same_or_none.
× rewrite ?dom_delete. set_solver.
× by apply delete_subseteq_compat.
× by apply delete_subseteq_compat.
- simplify_eq/=.
intros. eapply (pair_elim_typ _ _ _ (delete x Γ1) _ _ _ (delete x Γ2)); auto.
× eapply IHHtyp_e1; eauto using lookup_subseteq_same_or_none.
× case_decide as Hdec.
** rewrite -delete_insert_ne; last naive_solver.
rewrite -delete_insert_ne; last naive_solver.
eapply IHHtyp_e2; eauto.
rewrite ?lookup_insert_ne; [|naive_solver|naive_solver].
eauto using lookup_subseteq_same_or_none.
** rewrite not_and_l in Hdec *=>Hcase.
destruct Hcase as [Heq%dec_stable|Heq%dec_stable]; inversion Heq; subst.
*** rewrite -delete_insert_ne; last naive_solver.
by rewrite insert_delete.
*** by rewrite insert_delete.
× apply lookup_delete_None; auto.
× apply lookup_delete_None; auto.
× rewrite ?dom_delete. set_solver.
× by apply delete_subseteq_compat.
× by apply delete_subseteq_compat.
- simplify_eq/=.
intros; eapply (seq_typ _ (delete x Γ1) _ (delete x Γ2)).
× eapply IHHtyp_e1; eauto using lookup_subseteq_same_or_none.
× eapply IHHtyp_e2; eauto using lookup_subseteq_same_or_none.
× rewrite ?dom_delete. set_solver.
× by apply delete_subseteq_compat.
× by apply delete_subseteq_compat.
- intros; eapply (fork_typ); eauto.
- simplify_eq/=.
intros. eapply (lolli_intro_typ); auto.
× case_decide as Hdec.
** rewrite -delete_insert_ne; last naive_solver.
eapply IHHtyp_e; eauto.
rewrite ?lookup_insert_ne; [|naive_solver].
eauto using lookup_subseteq_same_or_none.
** rewrite not_and_l in Hdec *=>Hcase.
destruct Hcase as [Heq%dec_stable|Heq%dec_stable]; inversion Heq; subst.
by rewrite insert_delete.
- simplify_eq/=.
intros. eapply (lolli_elim_typ _ (delete x Γ1) _ _ _ (delete x Γ2)); auto.
× eapply IHHtyp_e1; eauto using lookup_subseteq_same_or_none.
× eapply IHHtyp_e2; eauto using lookup_subseteq_same_or_none.
× rewrite ?dom_delete. set_solver.
× by apply delete_subseteq_compat.
× by apply delete_subseteq_compat.
- simplify_eq/=.
intros. eapply (send_typ _ (delete x Γ1) _ _ _ (delete x Γ2)); auto.
× eapply IHHtyp_e1; eauto using lookup_subseteq_same_or_none.
× eapply IHHtyp_e2; eauto using lookup_subseteq_same_or_none.
× rewrite ?dom_delete. set_solver.
× by apply delete_subseteq_compat.
× by apply delete_subseteq_compat.
- simplify_eq/=.
intros. eapply (recv_typ); eauto.
- eauto.
Qed.
End type_lemmas.