From 1076b6c9b44dcf54b6ce6881a5dba6e372aafca2 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 13 Mar 2017 14:35:48 +0100
Subject: [PATCH] Prove weakening lemmas for elctx_sat.
---
theories/typing/lft_contexts.v | 23 ++++++++++++++++++++++-
1 file changed, 22 insertions(+), 1 deletion(-)
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index dce104cb..1f273699 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -356,6 +356,26 @@ Arguments lctx_lft_eq {_ _ _} _%EL _%LL _ _.
Arguments lctx_lft_alive {_ _ _} _%EL _%LL _.
Arguments elctx_sat {_ _ _} _%EL _%LL _%EL.
+Lemma elctx_sat_cons_weaken `{invG Σ, lftG Σ} e0 E E' L :
+ elctx_sat E L E' → elctx_sat (e0 :: E) L E'.
+Proof.
+ iIntros (HE' ????). rewrite /elctx_interp. setoid_rewrite big_sepL_cons.
+ iIntros "[? HE] HL". iMod (HE' with "HE HL") as (?) "[H Hclose]". done.
+ auto 10 with iFrame.
+Qed.
+
+Lemma elctx_sat_app_weaken_l `{invG Σ, lftG Σ} E0 E E' L :
+ elctx_sat E L E' → elctx_sat (E0 ++ E) L E'.
+Proof. induction E0=>//= ?. auto using elctx_sat_cons_weaken. Qed.
+
+Lemma elctx_sat_app_weaken_r `{invG Σ, lftG Σ} E0 E E' L :
+ elctx_sat E L E' → elctx_sat (E ++ E0) L E'.
+Proof.
+ intros ?????. rewrite /elctx_sat /elctx_interp.
+ setoid_rewrite (big_opL_permutation _ (E++E0)); try apply Permutation_app_comm.
+ by apply elctx_sat_app_weaken_l.
+Qed.
+
Section elctx_incl.
(* External lifetime context inclusion, in a persistent context.
(Used for function types subtyping).
@@ -463,7 +483,8 @@ Hint Resolve
elctx_sat_nil elctx_sat_alive elctx_sat_lft_incl elctx_sat_app elctx_sat_refl
elctx_incl_refl elctx_incl_nil elctx_incl_lft_alive elctx_incl_lft_incl
: lrust_typing.
-Hint Resolve lctx_lft_alive_external' | 100 : lrust_typing.
+Hint Resolve elctx_sat_cons_weaken elctx_sat_app_weaken_l elctx_sat_app_weaken_r
+ lctx_lft_alive_external' | 100 : lrust_typing.
Hint Opaque elctx_incl elctx_sat lctx_lft_alive lctx_lft_incl : lrust_typing.
--
GitLab