better proofs of non-expansiveness of the lty2 constructors

+ better notation thanks to robbert

theories/logic/model.v

@@ -5,7 +5,7 @@
     - Basic monadic rules *)
 From iris.heap_lang Require Export lifting metatheory.
 From iris.base_logic.lib Require Import invariants.
-From iris.algebra Require Import list.
+From iris.algebra Require Import list gmap.
 From iris.heap_lang Require Import notation proofmode.
 From reloc Require Import logic.spec_rules prelude.ctx_subst.
 From reloc Require Export logic.spec_ra.
@@ -60,7 +60,7 @@ Section semtypes.
     ={E,⊤}=∗ WP e {{ v, ∃ v', j ⤇ fill K (of_val v') ∗ A v v' }})%I.
 
   Global Instance interp_expr_ne E n :
-    Proper ((=) ==> (=) ==> (dist n) ==> dist n) (interp_expr E).
+    Proper ((=) ==> (=) ==> dist n ==> dist n) (interp_expr E).
   Proof. solve_proper. Qed.
 
   Definition lty2_unit : lty2 := Lty2 (λ w1 w2, ⌜ w1 = #() ∧ w2 = #() ⌝%I).
@@ -95,6 +95,30 @@ Section semtypes.
 
   Definition lty2_rec (C : lty2C -n> lty2C) : lty2 := fixpoint (lty2_rec1 C).
 
+  Definition lty2_exists (C : lty2 → lty2) : lty2 := Lty2 (λ w1 w2,
+    ∃ A : lty2, C A w1 w2)%I.
+
+  (** The lty2 constructors are non-expansive *)
+  Instance lty2_prod_ne n : Proper (dist n ==> (dist n ==> dist n)) lty2_prod.
+  Proof. solve_proper. Qed.
+
+  Instance lty2_sum_ne n : Proper (dist n ==> (dist n ==> dist n)) lty2_sum.
+  Proof. solve_proper. Qed.
+
+  Instance lty2_arr_ne n : Proper (dist n ==> dist n ==> dist n) lty2_arr.
+  Proof. solve_proper. Qed.
+
+  Instance lty2_rec_ne n : Proper (dist n ==> dist n)
+                                   (lty2_rec : (lty2C -n> lty2C) -> lty2C).
+  Proof.
+    intros F F' HF.
+    unfold lty2_rec, lty2_car.
+    apply fixpoint_ne=> X w1 w2.
+    unfold lty2_rec1, lty2_car. cbn.
+    f_equiv.
+    apply lty2_car_ne; eauto.
+  Qed.
+
 End semtypes.
 
 (* Nice notations *)
@@ -108,6 +132,15 @@ Definition env_ltyped2 `{relocG Σ} (Γ : gmap string lty2)
   (⌜ ∀ x, is_Some (Γ !! x) ↔ is_Some (vs !! x) ⌝ ∧
   [∗ map] i ↦ Avv ∈ map_zip Γ vs, lty2_car Avv.1 Avv.2.1 Avv.2.2)%I.
 
+(* Instance env_ltyped2_ne `{relocG Σ} n : *)
+(*   Proper (dist n ==> (=) ==> dist n) env_ltyped2. *)
+(* Proof. *)
+(*   intros Δ Δ' HΔ ? vvs ->. *)
+(*   rewrite /env_ltyped2. *)
+(*   f_equiv. *)
+(*   - repeat f_equiv. admit. *)
+(*   - apply big_opM_ne. *)
+
 Section refinement.
   Context `{relocG Σ}.
 
@@ -124,6 +157,13 @@ Section refinement.
   Definition refines_eq : refines = refines_def :=
     seal_eq refines_aux.
 
+  (* Global Instance refines_ne E n : *)
+  (*   Proper ((dist n) ==> (=) ==> (=) ==> (dist n) ==> (dist n)) (refines E). *)
+  (* Proof. *)
+  (*   rewrite refines_eq /refines_def. *)
+  (*   intros Γ Γ' HΓ ? e -> ? e' -> A A' HA. *)
+  (*   repeat f_equiv. *)
+
 End refinement.
 
 Notation "⟦ A ⟧ₑ" := (λ e e', interp_expr ⊤ e e' A).
@@ -218,7 +258,7 @@ End environment_properties.
 
 Notation "'{' E ';' Γ '}' ⊨ e1 '<<' e2 : A" :=
   (refines E Γ e1%E e2%E (A)%lty2)
-  (at level 100, E at level 50, Γ at next level, e1, e2 at next level,
+  (at level 100, E at next level, Γ at next level, e1, e2 at next level,
    A at level 200,
    format "'[hv' '{' E ';' Γ '}'  ⊨  '/  ' e1  '/' '<<'  '/  ' e2  :  A ']'").
 Notation "Γ ⊨ e1 '<<' e2 : A" :=

theories/logic/proofmode/tactics.v

@@ -214,6 +214,7 @@ Lemma tac_rel_load_r `{relocG Σ} K ℶ1 ℶ2 E Γ i1 (l : loc) q e t tres A v :
   t = fill K (Load (# l)) →
   nclose specN ⊆ E →
   envs_lookup i1 ℶ1 = Some (false, l ↦ₛ{q} v)%I →
+  (* TODO: the line below is a detour! *)
   envs_simple_replace i1 false
     (Esnoc Enil i1 (l ↦ₛ{q} v)%I) ℶ1 = Some ℶ2 →
   tres = fill K (of_val v) →
@@ -247,7 +248,7 @@ Tactic Notation "rel_load_l" :=
 (* The structure for the tacticals on the right hand side is a bit
 different. Because there is only one type of rules, we can report
 errors in a more precise way. E.g. if we are executing !#l and l ↦ₛ is
-not found in the environmen, then we can immediately fail with an
+not found in the environment, then we can immediately fail with an
 error *)
 Tactic Notation "rel_load_r" :=
   let solve_mapsto _ :=

theories/typing/interp.v

@@ -10,12 +10,10 @@ Section semtypes.
 
   (** Type-level lambdas are interpreted as closures *)
 
+  (** DF: lty2_forall is defined here because it depends on TApp *)
   Definition lty2_forall (C : lty2 → lty2) : lty2 := Lty2 (λ w1 w2,
     □ ∀ A : lty2, interp_expr ⊤ (TApp w1) (TApp w2) (C A))%I.
 
-  Definition lty2_exists (C : lty2 → lty2) : lty2 := Lty2 (λ w1 w2,
-    ∃ A : lty2, C A w1 w2)%I.
-
   Definition lty2_true : lty2 := Lty2 (λ w1 w2, True)%I.
 
   Program Definition ctx_lookup (x : var) : listC lty2C -n> lty2C := λne Δ,
@@ -32,44 +30,6 @@ Section semtypes.
       rewrite HP in HP'. inversion HP'.
   Qed.
 
-  Instance lty2_prod_ne n : Proper (dist n ==> (dist n ==> dist n)) lty2_prod.
-  Proof.
-    intros A A' HA B B' HB.
-    intros w1 w2. cbn.
-    unfold lty2_prod, lty2_car. cbn.
-    (* TODO: why do we have to unfold lty2_car here? *)
-    repeat f_equiv; eauto.
-  Qed.
-
-  Instance lty2_sum_ne n : Proper (dist n ==> (dist n ==> dist n)) lty2_sum.
-  Proof.
-    intros A A' HA B B' HB.
-    intros w1 w2. cbn.
-    unfold lty2_sum, lty2_car. cbn.
-    (* TODO: why do we have to unfold lty2_car here? *)
-    repeat f_equiv; eauto.
-  Qed.
-
-  Instance lty2_arr_ne n : Proper (dist n ==> (dist n ==> dist n)) lty2_arr.
-  Proof.
-    intros A A' HA B B' HB.
-    intros w1 w2. cbn.
-    unfold lty2_sum, lty2_car. cbn.
-    (* TODO: why do we have to unfold lty2_car here? *)
-    repeat f_equiv; eauto.
-  Qed.
-
-  Instance lty2_rec_ne n : Proper (dist n ==> dist n)
-                                   (lty2_rec : (lty2C -n> lty2C) -> lty2C).
-  Proof.
-    intros F F' HF.
-    unfold lty2_rec, lty2_car.
-    apply fixpoint_ne=> X w1 w2.
-    unfold lty2_rec1, lty2_car. cbn.
-    f_equiv.
-    apply lty2_car_ne; eauto.
-  Qed.
-
   Program Fixpoint interp (τ : type) : listC lty2C -n> lty2C :=
     match τ as _ return _ with
     | TUnit => λne _, lty2_unit