From 2d2e9d45de9f13021a687d68cbf1005f022c92d3 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Tue, 29 Jan 2019 13:29:13 +0100
Subject: [PATCH] better proofs of non-expansiveness of the lty2 constructors
+ better notation thanks to robbert
---
theories/logic/model.v | 46 ++++++++++++++++++++++++++++--
theories/logic/proofmode/tactics.v | 3 +-
theories/typing/interp.v | 42 +--------------------------
3 files changed, 46 insertions(+), 45 deletions(-)
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 29f9539..cc5c936 100644
--- a/theories/logic/model.v
+++ b/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" :=
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index b88fe4d..a38a0fb 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/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 _ :=
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 2890756..84539f0 100644
--- a/theories/typing/interp.v
+++ b/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
--
GitLab