Merge branch 'master' of gitlab.mpi-sws.org:iris/tutorial-popl20

_CoqProject

@@ -10,10 +10,11 @@
 
 theories/base.v
 theories/types.v
-theories/typing.v
+theories/typed.v
 theories/sem_types.v
 theories/sem_type_formers.v
-theories/sem_typing.v
+theories/sem_typed.v
+theories/sem_operators.v
 theories/compatibility.v
 theories/fundamental.v
 theories/safety.v

theories/compatibility.v

-From tutorial_popl20 Require Export sem_typing.
+From tutorial_popl20 Require Export sem_typed sem_operators.
 
 Section compatibility.
   Context `{heapG Σ}.

theories/fundamental.v

-From tutorial_popl20 Require Export typing compatibility interp.
+From tutorial_popl20 Require Export typed compatibility interp.
 
 Definition interp_env `{heapG Σ} (Γ : gmap string ty)
   (ρ : list (sem_ty Σ)) : gmap string (sem_ty Σ) := flip interp ρ <$> Γ.

theories/parametricity.v

@@ -3,13 +3,13 @@ From tutorial_popl20 Require Export safety.
 Section parametricity.
   Context `{heapG Σ}.
 
-  (* REMOVE *) Definition identity_param_sem_ty Σ (v : val) : sem_ty Σ :=
+  Definition identity_param_sem_ty Σ (v : val) : sem_ty Σ :=
     SemTy (λ w, ⌜w = v⌝)%I.
 
   Lemma identity_param `{!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.
+  Proof.
     intros He.
     apply sem_gen_type_safety with (φ := λ u, u = v)=> ?.
     exists (identity_param_sem_ty Σ v). split.

theories/sem_typing.v → theories/sem_operators.v

-From tutorial_popl20 Require Export sem_type_formers.
+From tutorial_popl20 Require Export sem_typed.
 
 (* Typing for operators *)
 Class SemTyUnboxed `{heapG Σ} (A : sem_ty Σ) :=
@@ -10,57 +10,9 @@ Class SemTyUnOp `{heapG Σ} (op : un_op) (A B : sem_ty Σ) :=
 Class SemTyBinOp `{heapG Σ} (op : bin_op) (A1 A2 B : sem_ty Σ) :=
   sem_ty_bin_op v1 v2 : A1 v1 -∗ A2 v2 -∗ ∃ w, ⌜ bin_op_eval op v1 v2 = Some w ⌝ ∧ B w.
 
-(* The semantic typing judgment *)
-Definition env_sem_typed `{heapG Σ} (Γ : gmap string (sem_ty Σ))
-    (vs : gmap string val) : iProp Σ :=
-  ([∗ map] i ↦ A;v ∈ Γ; vs, sem_ty_car A v)%I.
-Instance: Params (@env_sem_typed) 2 := {}.
-Definition sem_typed `{heapG Σ}
-    (Γ : gmap string (sem_ty Σ)) (e : expr) (A : sem_ty Σ) : iProp Σ :=
-  tc_opaque (□ ∀ vs, env_sem_typed Γ vs -∗ WP subst_map vs e {{ A }})%I.
-Instance: Params (@sem_typed) 2 := {}.
-Notation "Γ ⊨ e : A" := (sem_typed Γ e A)
-  (at level 100, e at next level, A at level 200).
-
-Section typed_properties.
+Section sem_operators.
   Context `{heapG Σ}.
   Implicit Types A B : sem_ty Σ.
-  Implicit Types C : sem_ty Σ → sem_ty Σ.
-
-  Global Instance env_sem_typed_ne n :
-    Proper (dist n ==> (=) ==> dist n) (@env_sem_typed Σ _).
-  Proof. Admitted.
-  Global Instance env_sem_typed_proper :
-    Proper ((≡) ==> (=) ==> (≡)) (@env_sem_typed Σ _).
-  Proof. intros ??????. subst. rewrite /env_sem_typed. Admitted.
-  Global Instance sem_typed_ne n :
-    Proper (dist n ==> (=) ==> dist n ==> dist n) (@sem_typed Σ _).
-  Proof. solve_proper. Qed.
-  Global Instance sem_typed_proper :
-    Proper ((≡) ==> (=) ==> (≡) ==> (≡)) (@sem_typed Σ _).
-  Proof. solve_proper. Qed.
-
-  Global Instance sem_typed_persistent Γ e A : Persistent (Γ ⊨ e : A).
-  Proof. rewrite /sem_typed /=. apply _. Qed.
-
-  (* Environments *)
-  Lemma env_sem_typed_lookup Γ vs x A :
-    Γ !! x = Some A →
-    env_sem_typed Γ vs -∗ ∃ v, ⌜ vs !! x = Some v ⌝ ∧ A v.
-  Proof.
-    iIntros (HΓx) "HΓ". rewrite /env_sem_typed.
-    by iApply (big_sepM2_lookup_1 with "HΓ").
-  Qed.
-  Lemma env_sem_typed_insert Γ vs x A v :
-    A v -∗ env_sem_typed Γ vs -∗
-    env_sem_typed (binder_insert x A Γ) (binder_insert x v vs).
-  Proof.
-    destruct x as [|x]=> /=; first by auto. rewrite /env_sem_typed.
-    iIntros "#HA #HΓ". by iApply (big_sepM2_insert_2 with "[] HΓ").
-  Qed.
-
-  Lemma env_sem_typed_empty vs : env_sem_typed ∅ vs -∗ ⌜vs = ∅⌝.
-  Proof. by iIntros "?"; iApply big_sepM2_empty_r. Qed.
 
   (* Unboxed types *)
   Global Instance sem_ty_unit_unboxed : SemTyUnboxed ().
@@ -110,4 +62,4 @@ Section typed_properties.
     repeat match goal with H : TCElemOf _ _ |- _ => inversion_clear H end;
       rewrite /sem_ty_car /=; eauto.
   Qed.
-End typed_properties.
+End sem_operators.

theories/sem_typed.v

+From tutorial_popl20 Require Export sem_type_formers.
+
+(* The semantic typing judgment *)
+Definition env_sem_typed `{heapG Σ} (Γ : gmap string (sem_ty Σ))
+    (vs : gmap string val) : iProp Σ :=
+  ([∗ map] i ↦ A;v ∈ Γ; vs, sem_ty_car A v)%I.
+Instance: Params (@env_sem_typed) 2 := {}.
+Definition sem_typed `{heapG Σ}
+    (Γ : gmap string (sem_ty Σ)) (e : expr) (A : sem_ty Σ) : iProp Σ :=
+  tc_opaque (□ ∀ vs, env_sem_typed Γ vs -∗ WP subst_map vs e {{ A }})%I.
+Instance: Params (@sem_typed) 2 := {}.
+Notation "Γ ⊨ e : A" := (sem_typed Γ e A)
+  (at level 100, e at next level, A at level 200).
+
+Section sem_typed.
+  Context `{heapG Σ}.
+  Implicit Types A B : sem_ty Σ.
+  Implicit Types C : sem_ty Σ → sem_ty Σ.
+
+  Global Instance env_sem_typed_ne n :
+    Proper (dist n ==> (=) ==> dist n) (@env_sem_typed Σ _).
+  Proof. Admitted.
+  Global Instance env_sem_typed_proper :
+    Proper ((≡) ==> (=) ==> (≡)) (@env_sem_typed Σ _).
+  Proof. intros ??????. subst. rewrite /env_sem_typed. Admitted.
+  Global Instance sem_typed_ne n :
+    Proper (dist n ==> (=) ==> dist n ==> dist n) (@sem_typed Σ _).
+  Proof. solve_proper. Qed.
+  Global Instance sem_typed_proper :
+    Proper ((≡) ==> (=) ==> (≡) ==> (≡)) (@sem_typed Σ _).
+  Proof. solve_proper. Qed.
+
+  Global Instance sem_typed_persistent Γ e A : Persistent (Γ ⊨ e : A).
+  Proof. rewrite /sem_typed /=. apply _. Qed.
+
+  (* Environments *)
+  Lemma env_sem_typed_lookup Γ vs x A :
+    Γ !! x = Some A →
+    env_sem_typed Γ vs -∗ ∃ v, ⌜ vs !! x = Some v ⌝ ∧ A v.
+  Proof.
+    iIntros (HΓx) "HΓ". rewrite /env_sem_typed.
+    by iApply (big_sepM2_lookup_1 with "HΓ").
+  Qed.
+  Lemma env_sem_typed_insert Γ vs x A v :
+    A v -∗ env_sem_typed Γ vs -∗
+    env_sem_typed (binder_insert x A Γ) (binder_insert x v vs).
+  Proof.
+    destruct x as [|x]=> /=; first by auto. rewrite /env_sem_typed.
+    iIntros "#HA #HΓ". by iApply (big_sepM2_insert_2 with "[] HΓ").
+  Qed.
+
+  Lemma env_sem_typed_empty vs : env_sem_typed ∅ vs -∗ ⌜vs = ∅⌝.
+  Proof. by iIntros "?"; iApply big_sepM2_empty_r. Qed.
+End sem_typed.

theories/unsafe.v

-From tutorial_popl20 Require Export sem_typing.
+From tutorial_popl20 Require Export sem_typed.
 From tutorial_popl20 Require Import symbol_ghost two_state_ghost.
 
 Section unsafe.
@@ -53,7 +53,7 @@ Section unsafe.
     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".
+    iMod (inv_alloc (nroot .@ "inv") _ I with "[Hl]")%I as "#Hinv".
     { by iNext; iExists 1; iFrame. }
     wp_pures.
     iExists _, _. iSplit; first done.
@@ -68,7 +68,7 @@ Section unsafe.
       + rewrite bool_decide_eq_false_2; last congruence.
         wp_op.
         wp_if.
-        iInv (nroot .@ "exercise3") as (m) ">[% Hl]".
+        iInv (nroot .@ "inv") as (m) ">[% Hl]".
         wp_store.
         iModIntro. iSplit.
         * iExists n; auto with congruence.
@@ -79,7 +79,7 @@ Section unsafe.
       iApply wp_assert.
       (* Need because of atomic expression *)
       wp_bind (! _)%E.
-      iInv (nroot .@ "exercise3") as (m) ">[% Hl]".
+      iInv (nroot .@ "inv") as (m) ">[% Hl]".
       wp_load.
       iModIntro. iSplitL "Hl".
       { iExists m; auto. }
@@ -102,20 +102,20 @@ Section unsafe.
     wp_alloc l as "Hl".
     iMod two_state_init as (γ) "Ho".
     pose (I := (∃ b, two_state_auth γ b ∗ l ↦ (if b then #true else #0))%I).
-    iMod (inv_alloc (nroot .@ "exercise4") _ I with "[Hl Ho]") as "#Hinv".
+    iMod (inv_alloc (nroot .@ "inv") _ 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]".
+    iInv (nroot .@ "inv") as (o) ">[Ho Hl]".
     wp_store.
     iMod (two_state_update with "Ho") as "[Ho Hf]".
     iModIntro. iSplitL "Hl Ho".
     { iNext. iExists true. iFrame. }
     wp_pures.
-    iInv (nroot .@ "exercise4") as (o') ">[Ho Hl]".
+    iInv (nroot .@ "inv") as (o') ">[Ho Hl]".
     iDestruct (two_state_agree with "Ho Hf") as %->.
     wp_load.
     iModIntro. iSplitL "Hl Ho".