From 9418275e0cc22f7bfc840a94e0e64b175268225f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 15 May 2020 14:17:47 +0200
Subject: [PATCH] mark a stronger-than-on-paper rule as such
---
theories/typing/cont_context.v | 9 +++++----
theories/typing/function.v | 2 +-
2 files changed, 6 insertions(+), 5 deletions(-)
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index c29c7315..f4f3051d 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -82,7 +82,7 @@ Section cont_context.
iApply ("H" with "[%]"). by apply HC1C2.
Qed.
- Lemma cctx_incl_cons_match E k L n (T1 T2 : vec val n → tctx) C1 C2 :
+ Lemma cctx_incl_cons E k L n (T1 T2 : vec val n → tctx) C1 C2 :
cctx_incl E C1 C2 → (∀ args, tctx_incl E L (T2 args) (T1 args)) →
cctx_incl E (k â—cont(L, T1) :: C1) (k â—cont(L, T2) :: C2).
Proof.
@@ -99,14 +99,15 @@ Section cont_context.
Lemma cctx_incl_nil E C : cctx_incl E C [].
Proof. apply incl_cctx_incl. by set_unfold. Qed.
- Lemma cctx_incl_cons E k L n (T1 T2 : vec val n → tctx) C1 C2 :
+ (* Extra strong cctx inclusion rule that we do not have on paper. *)
+ Lemma cctx_incl_cons_dup E k L n (T1 T2 : vec val n → tctx) C1 C2 :
k â—cont(L, T1) ∈ C1 →
(∀ args, tctx_incl E L (T2 args) (T1 args)) →
cctx_incl E C1 C2 →
cctx_incl E C1 (k â—cont(L, T2) :: C2).
Proof.
- intros Hin ??. rewrite <-cctx_incl_cons_match; try done.
- iIntros (?) "_ #HE HC".
+ intros Hin ??. rewrite <-cctx_incl_cons; try done.
+ clear -Hin. iIntros (?) "_ #HE HC".
rewrite cctx_interp_cons. iSplit; last done. clear -Hin.
iInduction Hin as [] "IH"; rewrite cctx_interp_cons;
[iDestruct "HC" as "[$ _]" | iApply "IH"; iDestruct "HC" as "[_ $]"].
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 5d7513fe..0f7e78ac 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -349,7 +349,7 @@ Section typing.
intros Hfn HL HE HTT' HC HT'T''.
rewrite -typed_body_mono /flip; last done; first by eapply type_call'.
- etrans. eapply (incl_cctx_incl _ [_]); first by intros ? ->%stdpp.list.elem_of_list_singleton.
- apply cctx_incl_cons_match; first done. intros args. by inv_vec args.
+ apply cctx_incl_cons; first done. intros args. by inv_vec args.
- etrans; last by apply (tctx_incl_frame_l [_]).
apply copy_elem_of_tctx_incl; last done. apply _.
Qed.
--
GitLab