From 345ff19caad1a8079cc9ff8660470c8863d29618 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <lepigre@mpi-sws.org>
Date: Fri, 29 Jan 2021 16:39:17 +0100
Subject: [PATCH] Infrastructure for [SimpleSubsumeVal].

---
 theories/typing/optional.v | 11 +++++++++++
 theories/typing/programs.v | 21 ++++++++++++---------
 2 files changed, 23 insertions(+), 9 deletions(-)

diff --git a/theories/typing/optional.v b/theories/typing/optional.v
index 0ba750c4..861f6b57 100644
--- a/theories/typing/optional.v
+++ b/theories/typing/optional.v
@@ -110,6 +110,17 @@ Section optional.
     iSplit => //. iApply (@simple_subsume_place with "HP Hl").
   Qed.
 
+  Global Instance simple_subsume_val_optional ty1 ty2 optty b1 b2 ot1 ot2
+       `{!Movable ty1} `{!Movable ty2} `{!Movable optty}
+       `{!Optionable ty1 optty ot1 ot2} `{!Optionable ty2 optty ot1 ot2}
+       `{!SimpleSubsumeVal ty1 ty2 P}:
+    SimpleSubsumeVal (b1 @ optional ty1 optty) (b2 @ optional ty2 optty) (⌜b1 ↔ b2⌝ ∗ P).
+  Proof.
+    iIntros (v) "[Heq P] H". rewrite /ty_own_val /=. iDestruct "Heq" as %->.
+    iDestruct "H" as "[[?H] | [??]]"; last (iRight; by iFrame).
+    iLeft. iFrame. iApply (simple_subsume_val with "P H").
+  Qed.
+
   Lemma subsume_optional_optty_ref b ty optty l β T:
     ⌜¬ b⌝ ∗ T -∗ subsume (l ◁ₗ{β} optty) (l ◁ₗ{β} b @ optional ty optty) T.
   Proof. iIntros "[Hb $] Hl". iRight. by iFrame. Qed.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index aad2f2e2..249f5d41 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -37,7 +37,9 @@ Section judgements.
     simple_subsume_place l β: P -∗ l ◁ₗ{β} ty1 -∗ l ◁ₗ{β} ty2.
   Class SimpleSubsumePlaceR (ty1 ty2 : rtype) (x1 : ty1.(rty_type)) (x2 : ty2.(rty_type)) (P : iProp Σ) : Prop :=
     simple_subsume_place_r l β: P -∗ l ◁ₗ{β} x1 @ ty1 -∗ l ◁ₗ{β} x2 @ ty2.
-  (* TODO: use SimpleSubsumeVal *)
+  (* TODO: add infrastructure like SimpleSubsumePlaceR to
+  SimpleSubsumeVal. Not sure if it would work because of the movable
+  instance. *)
   Class SimpleSubsumeVal (ty1 ty2 : type) `{!Movable ty1} `{!Movable ty2} (P : iProp Σ) : Prop :=
     simple_subsume_val v: P -∗ v ◁ᵥ ty1 -∗ v ◁ᵥ ty2.
 
@@ -530,6 +532,9 @@ Section typing.
   Proof. iIntros (??) "_ $". Qed.
   Global Instance simple_subsume_val_id ty `{!Movable ty} : SimpleSubsumeVal ty ty True | 1.
   Proof. iIntros (?) "_ $". Qed.
+  Global Instance simple_subsume_val_refinement_id ty x1 x2 `{!RMovable ty} :
+    SimpleSubsumeVal (x1 @ ty) (x2 @ ty) (⌜x1 = x2⌝) | 100.
+  Proof. iIntros (? ->) "$". Qed.
 
   Lemma simple_subsume_place_to_subsume l β ty1 ty2 P `{!SimpleSubsumePlace ty1 ty2 P} T:
     P ∗ T -∗ subsume (l ◁ₗ{β} ty1) (l ◁ₗ{β} ty2) T.
@@ -537,6 +542,12 @@ Section typing.
   Global Instance simple_subsume_place_to_subsume_inst l β ty1 ty2 P `{!SimpleSubsumePlace ty1 ty2 P}:
     SubsumePlace l β ty1 ty2 := λ T, i2p (simple_subsume_place_to_subsume l β ty1 ty2 P T).
 
+  Lemma simple_subsume_val_to_subsume v ty1 ty2 P `{!Movable ty1} `{!Movable ty2} `{!SimpleSubsumeVal ty1 ty2 P} T:
+    P ∗ T -∗ subsume (v ◁ᵥ ty1) (v ◁ᵥ ty2) T.
+  Proof. iIntros "[HP $] Hv". iApply (@simple_subsume_val with "HP Hv"). Qed.
+  Global Instance simple_subsume_val_to_subsume_inst v ty1 ty2 P `{!Movable ty1} `{!Movable ty2} `{!SimpleSubsumeVal ty1 ty2 P}:
+    SubsumeVal v ty1 ty2 := λ T, i2p (simple_subsume_val_to_subsume v ty1 ty2 P T).
+
   Import EqNotations.
   Lemma simple_subsume_place_refinement ty1 ty2 (x1 : ty1.(rty_type)) x2 P {Heq: ty1.(rty_type) = ty2.(rty_type)} `{!SimpleSubsumePlaceR ty1 ty2 x1 (rew [λ x : Type, x] Heq in x1) P} :
     SimpleSubsumePlace (x1 @ ty1) (x2 @ ty2) (⌜rew [λ x : Type, x] Heq in x1 = x2⌝ ∗ P).
@@ -561,14 +572,6 @@ Section typing.
   Proof. iIntros (l β) "HP Hl". iExists (rew [λ x : Type, x] Heq in x). iApply (@simple_subsume_place with "HP Hl"). Qed.
 
 
-  (* Doing the same trick as for subsume_place_refine seems hard because of the Movable instance *)
-  Lemma subsume_val_refinement_id v ty T x1 x2 `{!RMovable ty} :
-    ⌜x1 = x2⌝ ∗ T -∗ subsume (v ◁ᵥ x1 @ ty) (v ◁ᵥ x2 @ ty) T.
-  Proof. iIntros "[-> $] $". Qed.
-  Global Instance subsume_val_refinement_id_inst v ty x1 x2 `{!RMovable ty} :
-    SubsumeVal v (x1 @ ty)%I (x2 @ ty)%I | 2:=
-    λ T, i2p (subsume_val_refinement_id v ty T x1 x2).
-
   Lemma subtype_var {A} (ty : A → type) x y l β T:
     ⌜x = y⌝ ∗ T -∗
     subsume (l ◁ₗ{β} ty x) (l ◁ₗ{β} ty y) T.
-- 
GitLab