Commit 20cc2091 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Reorganize and start adding comments.

parent 863176c3
...@@ -12,9 +12,12 @@ theories/base.v ...@@ -12,9 +12,12 @@ theories/base.v
theories/types.v theories/types.v
theories/typing.v theories/typing.v
theories/sem_types.v theories/sem_types.v
theories/sem_type_formers.v
theories/sem_typing.v theories/sem_typing.v
theories/compatibility.v
theories/fundamental.v theories/fundamental.v
theories/safety.v theories/safety.v
theories/two_state_ghost.v
theories/symbol_ghost.v theories/symbol_ghost.v
theories/unsafe.v theories/unsafe.v
theories/exercises_answers.v theories/parametricity.v
From iris.algebra Require Export list gmap. From iris.algebra Require Export list gmap.
From iris.heap_lang Require Export lang notation metatheory. From iris.heap_lang Require Export lang notation metatheory.
From iris.heap_lang.lib Require Export assert.
(** We model type-level lambdas and applications as thunks since heap_lang does (** We model type-level lambdas and applications as thunks since heap_lang does
not have them. *) not have them. *)
......
From tutorial_popl20 Require Export sem_typing.
Section compatibility.
Context `{heapG Σ}.
Implicit Types A B : sem_ty Σ.
Implicit Types C : sem_ty Σ sem_ty Σ.
Lemma sem_typed_var Γ (x : string) A : Γ !! x = Some A Γ x : A.
Proof.
iIntros (HΓx vs) "!# #HΓ /=".
iDestruct (env_sem_typed_lookup with "HΓ") as (v ->) "HA"; first done.
by iApply wp_value.
Qed.
Lemma sem_typed_unit Γ : Γ #() : ().
Proof. iIntros (vs) "!# _ /=". by iApply wp_value. Qed.
Lemma sem_typed_bool Γ (b : bool) : Γ #b : sem_ty_bool.
Proof. iIntros (vs) "!# _ /=". iApply wp_value. rewrite /sem_ty_car /=. eauto. Qed.
Lemma sem_typed_int Γ (n : Z) : Γ #n : sem_ty_int.
Proof. iIntros (vs) "!# _ /=". iApply wp_value. rewrite /sem_ty_car /=. eauto. Qed.
Lemma sem_typed_pair Γ e1 e2 A1 A2 :
(Γ e1 : A1) - (Γ e2 : A2) - Γ (e1,e2) : A1 * A2.
Proof.
iIntros "#H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H2 [//])"); iIntros (w2) "#HA2".
wp_apply (wp_wand with "(H1 [//])"); iIntros (w1) "#HA1".
wp_pures. iExists w1, w2. auto.
Qed.
Lemma sem_typed_fst Γ e A1 A2 : (Γ e : A1 * A2) - Γ Fst e : A1.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w).
iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures.
Qed.
Lemma sem_typed_snd Γ e A1 A2 : (Γ e : A1 * A2) - Γ Snd e : A2.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w).
iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures.
Qed.
Lemma sem_typed_injl Γ e A1 A2 : (Γ e : A1) - Γ InjL e : A1 + A2.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HA".
wp_pures. iLeft. iExists w. auto.
Qed.
Lemma sem_typed_injr Γ e A1 A2 : (Γ e : A2) - Γ InjR e : A1 + A2.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HA".
wp_pures. iRight. iExists w. auto.
Qed.
Lemma sem_typed_case Γ e e1 e2 A1 A2 B :
(Γ e : A1 + A2) - (Γ e1 : A1 B) - (Γ e2 : A2 B) -
Γ Case e e1 e2 : B.
Proof.
iIntros "#H #H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#[HA|HA]".
- iDestruct "HA" as (w1 ->) "HA". wp_pures.
wp_apply (wp_wand with "(H1 [//])"); iIntros (v) "#HAB". by iApply "HAB".
- iDestruct "HA" as (w2 ->) "HA". wp_pures.
wp_apply (wp_wand with "(H2 [//])"); iIntros (v) "#HAB". by iApply "HAB".
Qed.
Lemma sem_typed_rec Γ f x e A1 A2 :
(binder_insert f (A1 A2)%sem_ty (binder_insert x A1 Γ) e : A2) -
Γ (rec: f x := e) : A1 A2.
Proof.
iIntros "#H" (vs) "!# #HΓ /=". wp_pures. iLöb as "IH".
iIntros "!#" (v) "#HA1". wp_pures. set (r := RecV f x _).
iSpecialize ("H" $! (binder_insert f r (binder_insert x v vs)) with "[#]").
{ iApply (env_sem_typed_insert with "IH"). by iApply env_sem_typed_insert. }
destruct x as [|x], f as [|f]; rewrite /= -?subst_map_insert //.
destruct (decide (x = f)) as [->|].
- by rewrite subst_subst delete_idemp insert_insert -subst_map_insert.
- rewrite subst_subst_ne // -subst_map_insert.
by rewrite -delete_insert_ne // -subst_map_insert.
Qed.
Lemma sem_typed_app Γ e1 e2 A1 A2 :
(Γ e1 : A1 A2) - (Γ e2 : A1) - Γ e1 e2 : A2.
Proof.
iIntros "#H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H2 [//])"); iIntros (w) "#HA1".
wp_apply (wp_wand with "(H1 [//])"); iIntros (v) "#HA". by iApply "HA".
Qed.
Lemma sem_typed_tlam Γ e C : ( A, Γ e : C A) - Γ (Λ: e) : A, C A.
Proof.
iIntros "#H" (vs) "!# #HΓ /=". wp_pures.
iIntros "!#" (A) "/=". wp_pures. by iApply ("H" $! A).
Qed.
Lemma sem_typed_tapp Γ e C A : (Γ e : A, C A) - Γ e ! : C A.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB". by iApply ("HB" $! A).
Qed.
Lemma sem_typed_pack Γ e C A : (Γ e : C A) - Γ e : A, C A.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB". by iExists A.
Qed.
Lemma sem_typed_unpack Γ x e1 e2 C B :
(Γ e1 : A, C A) - ( A, binder_insert x (C A) Γ e2 : B) -
Γ (unpack: x := e1 in e2) : B.
Proof.
iIntros "#H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H1 [//])"); iIntros (v); iDestruct 1 as (A) "#HC".
rewrite /exist_unpack; wp_pures. rewrite -subst_map_binder_insert.
wp_apply (wp_wand with "(H2 [])").
{ by iApply env_sem_typed_insert. }
auto.
Qed.
Lemma sem_typed_alloc Γ e A : (Γ e : A) - Γ ref e : ref A.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_bind (subst_map _ e). iApply (wp_wand with "(H [//])"); iIntros (w) "HA".
iApply wp_fupd. wp_alloc l as "Hl".
iMod (inv_alloc (tyN .@ l) _ ( v, l v A v)%I with "[Hl HA]") as "#?".
{ iExists w. iFrame. }
iModIntro. iExists l; auto.
Qed.
Lemma sem_typed_load Γ e A : (Γ e : ref A) - Γ ! e : A.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_bind (subst_map _ e). iApply (wp_wand with "(H [//])"); iIntros (w).
iDestruct 1 as (l ->) "#?".
iInv (tyN.@l) as (v) "[>Hl HA]". wp_load. eauto 10.
Qed.
Lemma sem_typed_store Γ e1 e2 A :
(Γ e1 : ref A) - (Γ e2 : A) - Γ (e1 <- e2) : ().
Proof.
iIntros "#H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H2 [//])"); iIntros (w2) "#HA".
wp_apply (wp_wand with "(H1 [//])"); iIntros (w1); iDestruct 1 as (l ->) "#?".
iInv (tyN.@l) as (v) "[>Hl _]". wp_store. eauto 10.
Qed.
Lemma sem_typed_faa Γ e1 e2 :
(Γ e1 : ref sem_ty_int) - (Γ e2 : sem_ty_int) - Γ FAA e1 e2 : sem_ty_int.
Proof.
iIntros "#H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H2 [//])"); iIntros (w2); iDestruct 1 as (n) "->".
wp_apply (wp_wand with "(H1 [//])"); iIntros (w1); iDestruct 1 as (l ->) "#?".
iInv (tyN.@l) as (v) "[>Hl Hv]"; iDestruct "Hv" as (n') "> ->".
wp_faa. iModIntro. eauto 10.
Qed.
Lemma sem_typed_cmpxchg Γ A e1 e2 e3 :
SemTyUnboxed A
(Γ e1 : ref A) - (Γ e2 : A) - (Γ e3 : A) - Γ CmpXchg e1 e2 e3 : A * sem_ty_bool.
Proof.
intros. iIntros "#H1 #H2 #H3" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H3 [//])"); iIntros (w3) "HA3".
wp_apply (wp_wand with "(H2 [//])"); iIntros (w2) "HA2".
iDestruct (sem_ty_unboxed with "HA2") as %?.
wp_apply (wp_wand with "(H1 [//])"); iIntros (w1); iDestruct 1 as (l ->) "#?".
iInv (tyN.@l) as (v) "[>Hl #Hv]". wp_cmpxchg as ?|?; iModIntro;
(iSplitL; [by eauto 12 with iFrame | iExists _, _; eauto]).
Qed.
Lemma sem_typed_un_op Γ e op A B :
SemTyUnOp op A B (Γ e : A) - Γ UnOp op e : B.
Proof.
intros ?. iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (v) "#HA".
iDestruct (sem_ty_un_op with "HA") as (w ?) "#HB". by wp_unop.
Qed.
Lemma sem_typed_bin_op Γ e1 e2 op A1 A2 B :
SemTyBinOp op A1 A2 B (Γ e1 : A1) - (Γ e2 : A2) - Γ BinOp op e1 e2 : B.
Proof.
intros. iIntros "#H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H2 [//])"); iIntros (v2) "#HA2".
wp_apply (wp_wand with "(H1 [//])"); iIntros (v1) "#HA1".
iDestruct (sem_ty_bin_op with "HA1 HA2") as (w ?) "#HB". by wp_binop.
Qed.
Lemma sem_typed_if Γ e e1 e2 B :
(Γ e : sem_ty_bool) - (Γ e1 : B) - (Γ e2 : B) -
Γ (if: e then e1 else e2) : B.
Proof.
iIntros "#H #H1 #H2" (vs) "!# #HΓ /=".
iSpecialize ("H1" with "HΓ"). iSpecialize ("H2" with "HΓ").
wp_apply (wp_wand with "(H [//])"); iIntros (w). iDestruct 1 as ([]) "->"; by wp_if.
Qed.
Lemma sem_typed_fork Γ e : (Γ e : ()) - Γ Fork e : ().
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply wp_fork; last done. by iApply (wp_wand with "(H [//])").
Qed.
End compatibility.
From iris.algebra Require Import auth.
From iris.base_logic Require Import lib.own.
From iris.heap_lang.lib Require Import assert.
From tutorial_popl20 Require Export sem_typing safety.
Section exercises.
Context `{heapG Σ}.
(* Easy *)
Definition exercise1_prog : val := λ: <>,
if: #true then #13 else #13 #37.
Lemma exercise1 : exercise1_prog : () sem_ty_int.
Proof.
iIntros (vs) "!# HΓ"; simpl.
iApply wp_value.
iIntros "!#" (? ->).
wp_lam.
wp_if.
rewrite /sem_ty_car /=.
by iExists 13.
Qed.
(* Easy *)
Definition exercise2_prog : val := λ: <>,
let: "l" := ref #0 in "l" <- #true;; !"l".
Lemma exercise2 : exercise2_prog : () sem_ty_bool.
Proof.
iIntros (vs) "!# HΓ"; simpl.
iApply wp_value.
iIntros "!#" (? ->).
wp_lam.
wp_alloc l as "Hl".
wp_let.
wp_store.
wp_load.
rewrite /sem_ty_car /=.
by iExists true.
Qed.
(* Moderate *)
Definition exercise3_prog : val := λ: <>,
let: "l" := ref #1 in
((λ: "x", if: "x" #0 then "l" <- "x" else #()),
(λ: <>, assert: !"l" #0)).
Lemma exercise3 : exercise3_prog : () (sem_ty_int ()) * (() ()).
Proof.
iIntros (vs) "!# HΓ"; simpl.
iApply wp_value.
iIntros "!#" (? ->).
wp_lam.
wp_alloc l as "Hl".
wp_let.
pose (I := ( n : Z, #n #0 l #n)%I).
iMod (inv_alloc (nroot .@ "exercise3") _ I with "[Hl]")%I as "#Hinv".
{ by iNext; iExists 1; iFrame. }
wp_pures.
iExists _, _. iSplit; first done.
iSplit.
- iIntros "!#" (? [n ->]).
wp_lam.
wp_op.
destruct (decide (n = 0%Z)); simplify_eq/=.
+ wp_op.
wp_if.
done.
+ rewrite bool_decide_eq_false_2; last congruence.
wp_op.
wp_if.
iInv (nroot .@ "exercise3") as (m) ">[% Hl]".
wp_store.
iModIntro. iSplit.
* iExists n; auto with congruence.
* done.
- iIntros "!#" (? ->).
wp_lam.
wp_pures.
iApply wp_assert.
(* Need because of atomic expression *)
wp_bind (! _)%E.
iInv (nroot .@ "exercise3") as (m) ">[% Hl]".
wp_load.
iModIntro. iSplitL "Hl".
{ iExists m; auto. }
wp_op.
rewrite bool_decide_eq_false_2; last done.
by wp_op.
Qed.
Definition exercise4_prog : val :=
λ: <>, let: "l" := ref #0 in λ: <>, "l" <- #true;; !"l".
Section exercise4.
Context `{!inG Σ (authUR (optionUR unitR))}.
Definition exercise4_auth (γ : gname) (b : bool) : iProp Σ :=
own γ ( (if b then Some () else None)).
Definition exercise4_final (γ : gname) : iProp Σ :=
own γ ( (Some ())).
Lemma exercise4_ghost_init : (|==> γ, exercise4_auth γ false)%I.
Proof. iApply own_alloc. by apply auth_auth_valid. Qed.
Lemma exercise4_ghost_update γ b :
exercise4_auth γ b ==
exercise4_auth γ true exercise4_final γ.
Proof.
iIntros "H".
iMod (own_update _ _ ( Some () Some ()) with "H") as "[$ $]"; last done.
apply auth_update_alloc. destruct b.
- by apply local_update_unital_discrete=> -[[]|].
- by apply alloc_option_local_update.
Qed.
Global Instance exercise4_auth_timeless γ b : Timeless (exercise4_auth γ b).
Proof. apply _. Qed.
Global Instance exercise4_final_timeless γ : Timeless (exercise4_final γ).
Proof. apply _. Qed.
Global Instance exercise4_final_persistent γ : Persistent (exercise4_final γ).
Proof. apply _. Qed.
Lemma exercise4_ghost_agree γ b :
exercise4_auth γ b - exercise4_final γ - b = true.
Proof.
iIntros "H1 H2".
iDestruct (own_valid_2 with "H1 H2") as %[Hinc _]%auth_both_valid.
apply option_included in Hinc as [|([]&[]&_&?&_)];
destruct b; naive_solver.
Qed.
Typeclasses Opaque exercise4_auth exercise4_final.
Lemma exercise4 :
exercise4_prog : sem_ty_unit (sem_ty_unit sem_ty_bool).
Proof.
iIntros (vs) "!# HΓ"; simpl.
iApply wp_value.
iIntros "!#" (? ->).
wp_lam.
wp_alloc l as "Hl".
iMod exercise4_ghost_init as (γ) "Ho".
pose (I := ( b, exercise4_auth γ b
l (if b then #true else #0))%I).
iMod (inv_alloc (nroot .@ "exercise4") _ I with "[Hl Ho]") as "#Hinv".
{ iNext. iExists false. iFrame. }
wp_pures.
iIntros "!#" (? ->).
wp_lam.
(* Need because of atomic expression *)
wp_bind (_ <- _)%E.
iInv (nroot .@ "exercise4") as (o) ">[Ho Hl]".
wp_store.
iMod (exercise4_ghost_update with "Ho") as "[Ho Hf]".
iModIntro. iSplitL "Hl Ho".
{ iNext. iExists true. iFrame. }
wp_pures.
iInv (nroot .@ "exercise4") as (o') ">[Ho Hl]".
iDestruct (exercise4_ghost_agree with "Ho Hf") as %->.
wp_load.
iModIntro. iSplitL "Hl Ho".
{ iNext. iExists true. iFrame. }
rewrite /sem_ty_car /=. by iExists _.
Qed.
End exercise4.
End exercises.
(* REMOVE *) Definition exercise5_sem_ty Σ (v : val) : sem_ty Σ :=
SemTy (λ w, w = v)%I.
Lemma exercise5 `{!heapPreG Σ} e (v : val) σ w es σ' :
( `{heapG Σ}, e : A, A A)
rtc erased_step ([e ! v]%E, σ) (of_val w :: es, σ') w = v.
(* REMOVE *) Proof.
intros He.
apply sem_gen_type_safety with (φ := λ u, u = v)=> ?.
exists (exercise5_sem_ty Σ v). split.
{ by iIntros (?) "?". }
iIntros (vs) "!# #Hvs".
iPoseProof (He with "Hvs") as "He /=".
wp_apply (wp_wand with "He").
iIntros (u) "#Hu".
iSpecialize ("Hu" $! (exercise5_sem_ty Σ v)).
wp_apply (wp_wand with "Hu"). iIntros (w') "Hw'". by iApply "Hw'".
Qed.
From tutorial_popl20 Require Export typing sem_typing. From tutorial_popl20 Require Export typing compatibility.
Reserved Notation "⟦ τ ⟧". Reserved Notation "⟦ τ ⟧".
Fixpoint interp `{heapG Σ} (τ : ty) (ρ : list (sem_ty Σ)) : sem_ty Σ := Fixpoint interp `{heapG Σ} (τ : ty) (ρ : list (sem_ty Σ)) : sem_ty Σ :=
......
From tutorial_popl20 Require Export safety.
Section parametricity.
Context `{heapG Σ}.
(* REMOVE *) Definition exercise5_sem_ty Σ (v : val) : sem_ty Σ :=
SemTy (λ w, w = v)%I.
Lemma exercise5 `{!heapPreG Σ} e (v : val) σ w es σ' :
( `{heapG Σ}, e : A, A A)
rtc erased_step ([e ! v]%E, σ) (of_val w :: es, σ') w = v.
(* REMOVE *) Proof.
intros He.
apply sem_gen_type_safety with (φ := λ u, u = v)=> ?.
exists (exercise5_sem_ty Σ v). split.
{ by iIntros (?) "?". }
iIntros (vs) "!# #Hvs".
iPoseProof (He with "Hvs") as "He /=".
wp_apply (wp_wand with "He").
iIntros (u) "#Hu".
iSpecialize ("Hu" $! (exercise5_sem_ty Σ v)).
wp_apply (wp_wand with "Hu"). iIntros (w') "Hw'". by iApply "Hw'".
Qed.
End parametricity.
\ No newline at end of file
From tutorial_popl20 Require Export fundamental.
From iris.heap_lang Require Export adequacy. From iris.heap_lang Require Export adequacy.
From tutorial_popl20 Require Export fundamental.
Lemma sem_gen_type_safety `{heapPreG Σ} e σ φ : Lemma sem_gen_type_safety `{heapPreG Σ} e σ φ :
( `{heapG Σ}, A : sem_ty Σ, ( v, A v - ⌜φ v) ( e : A)) ( `{heapG Σ}, A : sem_ty Σ, ( v, A v - ⌜φ v) ( e : A))
......
From tutorial_popl20 Require Export sem_types.
(** The definitions of the type formers *)
Section types.
Context `{heapG Σ}.
(** Let us start with the simplest types of our language: unit and Boolean.
The value interpretations of these types are as follows: *)
Definition sem_ty_unit : sem_ty Σ := SemTy (λ w, w = #() )%I.
Definition sem_ty_bool : sem_ty Σ := SemTy (λ w, b : bool, w = #b )%I.
(** These interpretations are exactly what you would expect: the only value
of the unit type is the unit value [()], the values of the Boolean type are
the elements of the Coq type [bool] (i.e. [true] and [false]). *)
(** Exercise. now define the value interpretation of the integer type. *)
(* REMOVE *) Definition sem_ty_int : sem_ty Σ := SemTy (λ w, n : Z, w = #n )%I.
(** The value interpretation for product type is as one would expect: *)
Definition sem_ty_prod (A1 A2 : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
w1 w2, w = PairV w1 w2 A1 w1 A2 w2)%I.
(** Values of the product type over [A1] and [A2] should be tuples [(w1, w2)],
where [w1] and [w2] should be in the interpretation of [A1] and [A2],
respectively. *)
(* REMOVE *) Definition sem_ty_sum (A1 A2 : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
( w1, w = InjLV w1 A1 w1) ( w2, w = InjRV w2 A2 w2))%I.
Definition sem_ty_arr (A1 A2 : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
v, A1 v - WP App w v {{ A2 }})%I.
Definition sem_ty_forall (C : sem_ty Σ sem_ty Σ) : sem_ty Σ := SemTy (λ w,
A : sem_ty Σ, WP w #() {{ w, C A w }})%I.
Definition sem_ty_exist (C : sem_ty Σ sem_ty Σ) : sem_ty Σ := SemTy (λ w,
A : sem_ty Σ, C A w)%I.
Definition tyN := nroot .@ "ty".
Definition sem_ty_ref (A : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
l : loc, w = #l inv (tyN .@ l) ( v, l v A v))%I.
End types.
(** We introduce nicely looking notations for our semantic types. This allows
us to write lemmas, for example, the compatibility lemmas, in a readable way. *)
Notation "()" := sem_ty_unit : sem_ty_scope.
Infix "*" := sem_ty_prod : sem_ty_scope.
Infix "+" := sem_ty_sum : sem_ty_scope.
Infix "→" := sem_ty_arr : sem_ty_scope.
Notation "∀ A1 .. An , C" :=
(sem_ty_forall (λ A1, .. (sem_ty_forall (λ An, C%sem_ty)) ..)) : sem_ty_scope.
Notation "∃ A1 .. An , C" :=
(sem_ty_exist (λ A1, .. (sem_ty_exist (λ An, C%sem_ty)) ..)) : sem_ty_scope.
Notation "'ref' A" := (sem_ty_ref A) : sem_ty_scope.
(** A [Params t n] instance tells Coq's setoid rewriting mechanism _not_ to
rewrite in the first [n] arguments of [t]. These instances tend to make the
setoid rewriting mechanism a lot faster. This code is mostly boilerplate. *)
Instance: Params (@sem_ty_arr) 1 := {}.
Instance: Params (@sem_ty_prod) 1 := {}.
Instance: Params (@sem_ty_sum) 1 := {}.
Instance: Params (@sem_ty_forall) 1 := {}.
Instance: Params (@sem_ty_exist) 1 := {}.
Instance: Params (@sem_ty_ref) 2 := {}.
(** We prove that all type formers are non-expansive and respect setoid
equality. This code is mostly boilerplate. *)
Section types_properties.
Context `{heapG Σ}.
Global Instance sem_ty_prod_ne : NonExpansive2 (@sem_ty_prod Σ).
Proof. solve_proper. Qed.
Global Instance sem_ty_sum_ne : NonExpansive2 (@sem_ty_sum Σ).
Proof. solve_proper. Qed.
Global Instance sem_ty_arr_ne : NonExpansive2 (@sem_ty_arr Σ _).
Proof. solve_proper. Qed.
Global Instance sem_ty_forall_ne n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@sem_ty_forall Σ _).
Proof. solve_proper. Qed.
Global Instance sem_ty_exist_ne n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@sem_ty_exist Σ).
Proof. solve_proper. Qed.
Global Instance sem_ty_ref_ne : NonExpansive2 (@sem_ty_ref Σ _).
Proof. solve_proper. Qed.