Misc changes.

theories/fundamental.v

@@ -19,8 +19,6 @@ Section fundamental.
   Implicit Types τ : ty.
   Implicit Types ρ : list (sem_ty Σ).
 
-  (* I'm not sure where I should move the following but they don't
-  seem to belong here! *)
   Instance ty_unboxed_sound τ ρ : ty_unboxed τ → SemTyUnboxed (⟦ τ ⟧ ρ).
   Proof. destruct 1; simpl; apply _. Qed.
   Instance ty_un_op_sound op τ σ ρ :

theories/parametricity.v

@@ -71,7 +71,7 @@ Section parametricity.
   Lemma nat_param `{!heapPreG Σ} e σ w es σ' :
     (∀ `{heapG Σ}, ∅ ⊨ e : ∀ A, (A → A) → A → A) →
     rtc erased_step ([e <_> (λ: "n", "n" + #1)%V #0]%E, σ)
-        (of_val w :: es, σ') → ∃ n : nat, w = #n.
+      (of_val w :: es, σ') → ∃ n : nat, w = #n.
   (* REMOVE *) Proof.
     intros He.
     apply sem_gen_type_safety with (φ := λ w, ∃ n : nat, w = #n)=> ?.
@@ -95,50 +95,43 @@ Section parametricity.
     by iExists 0%nat.
   Qed.
 
-  (* REMOVE *) Definition strong_nat_param_sem_ty Σ (ψ : nat → val → Prop) : sem_ty Σ :=
-    SemTy (λ w, ∃ n : nat, ⌜ψ n w⌝)%I.
+  (* REMOVE *) Definition strong_nat_param_sem_ty {A Σ} (Ψ : A → sem_ty Σ) : sem_ty Σ :=
+    SemTy (λ w, ∃ x : A, Ψ x w)%I.
 
-  Definition strong_nat_param_semtyp_family
-             {A Σ} (Ψ : A → sem_ty Σ) : sem_ty Σ :=
-    SemTy (λ w, ∃ n, Ψ n w)%I.
-
-  Lemma strong_nat_param `{!heapPreG Σ} e σ w es σ' (f z : val) ψ:
-    (∀ `{heapG Σ}, ∅ ⊨ e : ∀ A, (A → A) → A → A) →
-    (∀ `{heapG Σ},
-        ∃ (Ψ : nat → sem_ty Σ),
-          (∀ n w, Ψ n w -∗ ⌜ψ n w⌝) ∧
-          (∀ n w, {{{Ψ n w}}} f w {{{w', RET w'; Ψ (S n) w'}}}) ∧
-          (Ψ 0%nat z)%I) →
-    rtc erased_step ([e <_> f z]%E, σ) (of_val w :: es, σ') → ∃ n : nat, ψ n w.
+  Lemma strong_nat_param `{!heapPreG Σ} e σ w es σ' (vf vz : val) ψ:
+    (∀ `{heapG Σ}, ∃ (Ψ : nat → sem_ty Σ),
+      (∅ ⊨ e : ∀ A, (A → A) → A → A) ∧
+      (∀ n w, {{{ Ψ n w }}} vf w {{{ w', RET w'; Ψ (S n) w' }}}) ∧
+      (Ψ 0%nat vz) ∧
+      (∀ n w, Ψ n w -∗ ⌜ψ n w⌝)) →
+    rtc erased_step ([e <_> vf vz]%E, σ) (of_val w :: es, σ') → ∃ n : nat, ψ n w.
   (* REMOVE *) Proof.
-    intros He Hfz.
+    intros He.
     apply sem_gen_type_safety with (φ := λ w, ∃ n, ψ n w)=> ?.
-    exists (strong_nat_param_sem_ty Σ ψ). split.
-    { iIntros (?). iDestruct 1 as (?) "%". eauto. }
-    specialize (Hfz _) as (Ψ & HΨ & Hf & Hz).
+    exists (strong_nat_param_sem_ty (λ n : nat, SemTy (λ w, ⌜ψ n w⌝)%I)). split.
+    { iIntros (v [n ?]); eauto. }
+    specialize (He _) as (Ψ & He & Hvf & Hvz & Hψ).
     iIntros (vs) "!# #Hvs".
     iPoseProof (He with "Hvs") as "He /=".
     wp_apply (wp_wand with "He").
     iIntros (u) "#Hu".
-    iSpecialize ("Hu" $! (strong_nat_param_semtyp_family Ψ)).
+    iSpecialize ("Hu" $! (strong_nat_param_sem_ty Ψ)).
     wp_apply (wp_wand with "Hu"). iIntros (w') "#Hw'".
-    iSpecialize ("Hw'" $! f with "[]").
+    iSpecialize ("Hw'" $! vf with "[]").
     { iIntros "!#" (u') "Hu'".
       iDestruct "Hu'"as (k) "Hu'".
-      iApply (Hf with "Hu'").
-      iNext.
-      iIntros (u'') "Hu''".
+      iApply (Hvf with "Hu'").
+      iIntros "!>" (u'') "Hu''".
       by iExists _. }
     wp_apply (wp_wand with "Hw'").
     iIntros (w'') "#Hw''".
     iApply wp_wand.
-    { iApply ("Hw''" $! z with "[]"); eauto.
+    { iApply ("Hw''" $! vz with "[]"); eauto.
       iExists 0%nat.
-      iApply Hz. }
+      iApply Hvz. }
     iIntros (v).
     iDestruct 1 as (k) "Hv".
     iExists k.
-    by iApply HΨ.
+    by iApply Hψ.
   Qed.
-
 End parametricity.

theories/sem_type_formers.v

@@ -99,8 +99,8 @@ Section types.
    types. However, for the sake of simplicity we did not consider
    recursive types for this tutorial. In particular, to give the
    semantics of recursive types one needs to use Iris's guarded
-   fixpoints which in turn requires us to enforce that semantics types,
-   in addition to being persistent, are also non-expansive. *)
+   fixpoints, which require some additional bookkeeping related to
+   contractiveness. *)
 End types.
 
 (** We introduce nicely looking notations for our semantic types. This allows

theories/sem_typed.v

@@ -43,10 +43,15 @@ Section sem_typed.
 
   Global Instance env_sem_typed_ne n :
     Proper (dist n ==> (=) ==> dist n) (@env_sem_typed Σ _).
-  Proof. Admitted.
+  Proof.
+    intros Γ1 Γ2 HΓ ρ ? <-.
+    apply big_sepM2_ne_2=> // k A1 v1 A2 v2 _ _ HA _ _ /discrete_iff / leibniz_equiv_iff ->.
+    by apply HA.
+  Qed.
   Global Instance env_sem_typed_proper :
     Proper ((≡) ==> (=) ==> (≡)) (@env_sem_typed Σ _).
-  Proof. intros ??????. subst. rewrite /env_sem_typed. Admitted.
+  Proof. intros Γ1 Γ2 HΓ ρ ? <-. apply equiv_dist=> n. f_equiv. by rewrite HΓ. Qed.
+
   Global Instance sem_typed_ne n :
     Proper (dist n ==> (=) ==> dist n ==> dist n) (@sem_typed Σ _).
   Proof. solve_proper. Qed.

theories/sem_types.v

@@ -3,22 +3,25 @@ From iris.heap_lang Require Export proofmode.
 From iris.base_logic.lib Require Export invariants.
 
 (** * The domain of semantics types. *)
-(** Here we define the domain of semantics types as persistent iris
+(** Here we define the domain of semantics types as persistent Iris
     predicates over values. That is, to capture the semantics of a
-    type [τ], we need to define what programs are belong to the
+    type [τ], we need to define what expressions belong to the
     semantics of [τ]. We do this in two steps:
 
-      - We define what values semantically belong to type [τ]
+      - We define what values semantically belong to type [τ]. We do
+        this in the file [sem_type_formers].
       - We define the expressions that semantically belong to [τ]. An
         expression [e] semantically belongs to type [τ] if [e] is
         _safe_, and whenever it evaluates to a value [v], [v]
-        semantically belongs to [τ].
+        semantically belongs to [τ]. We do this in the file [sem_typed].
 
-    Here we use iris predicates as value semantics of types. The power
-    iris's logic then allows us to define many semantic types
+    Here we use Iris predicates as value semantics of types. The power
+    of Iris's logic then allows us to define many semantic types
     including those that we need to interpret syntactic types for
     heap_lang, e.g., higher-order references, parametric polymorphism,
-    etc. It is crucial for value semantics of types to be persistent
+    etc.
+
+    It is crucial for value semantics of types to be persistent
     predicates. This is due to the fact that our type system (as
     opposed to substructural type systems, e.g., affine type systems)
     allows values to be used multiple times. Hence, the fact that a