From ba92121550d9f031e572b1e63655d8d9778220b4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 6 Jan 2017 20:28:10 +0100
Subject: [PATCH] update Iris
For some reason I have to fix some diverging proof scripts
---
opam.pins | 2 +-
theories/typing/function.v | 4 ++--
theories/typing/product_split.v | 4 ++--
theories/typing/programs.v | 9 +++++++--
theories/typing/type.v | 6 +++---
theories/typing/type_context.v | 12 ++++++------
6 files changed, 21 insertions(+), 16 deletions(-)
diff --git a/opam.pins b/opam.pins
index 425ba64c..16be4581 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 05b530001f48a4544a9aaee7b8ff1a2abbe14e14
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 587cde167492b4b25f1d11ca7797c2087527abd6
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 16d30054..9a63ce18 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -117,8 +117,8 @@ Section typing.
Proof.
intros tys1 tys2 Htys ty1 ty2 Hty. apply fn_subtype_ty.
- intros. eapply Forall2_impl; first eapply Htys. intros ??.
- eapply subtype_weaken; last done. by apply contains_inserts_r.
- - intros. eapply subtype_weaken, Hty; last done. by apply contains_inserts_r.
+ eapply subtype_weaken; last done. by apply submseteq_inserts_r.
+ - intros. eapply subtype_weaken, Hty; last done. by apply submseteq_inserts_r.
Qed.
Global Instance fn_eqtype_ty' {A n} E0 L0 E :
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 5911d74c..0553b61c 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -293,7 +293,7 @@ Section product_split.
rewrite !tctx_extract_hasty_unfold=>?. apply (tctx_incl_frame_r _ [_] [_;_]).
rewrite {1}copy_tctx_incl. apply (tctx_incl_frame_r _ [_] [_]).
rewrite tctx_split_shr_prod2 -(contains_tctx_incl _ _ [p' â— ty]%TC) //.
- apply contains_skip, contains_nil_l.
+ apply submseteq_skip, submseteq_nil_l.
Qed.
Lemma tctx_extract_split_own_prod E L p p' n ty tyl T T' :
@@ -319,7 +319,7 @@ Section product_split.
rewrite !tctx_extract_hasty_unfold=>?. apply (tctx_incl_frame_r _ [_] [_;_]).
rewrite {1}copy_tctx_incl. apply (tctx_incl_frame_r _ [_] [_]).
rewrite tctx_split_shr_prod -(contains_tctx_incl _ _ [p' â— ty]%TC) //.
- apply contains_skip, contains_nil_l.
+ apply submseteq_skip, submseteq_nil_l.
Qed.
(* Merging with [tctx_extract]. *)
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 5ba09002..68b0a6d9 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -130,7 +130,11 @@ Section typing_rules.
tctx_extract_ctx E L T1 T T' →
(typed_body E L C (T2 ++ T') e') →
typed_body E L C T (e ;; e').
- Proof. intros. by eapply type_let. Qed.
+ Proof.
+ intros ? Hinst ? Hbody. eapply type_let; [done| |done|].
+ (* FIXME: done divergese on the remaining goals. *)
+ exact Hinst. intros. exact Hbody.
+ Qed.
Lemma typed_newlft E L C T κs e :
Closed [] e →
@@ -265,6 +269,7 @@ Section typing_rules.
typed_body E L C ((p1 ◠ty1') :: (p2 ◠ty2') :: T') e →
typed_body E L C T (p1 <⋯ !{n}p2;; e).
Proof.
- intros. eapply type_seq; [done|by eapply type_memcpy_instr|done|by simpl].
+ intros ?? Hwr Hrd ??. eapply type_seq; [done|eapply type_memcpy_instr| |by simpl]; first done.
+ exact Hwr. exact Hrd. done.
Qed.
End typing_rules.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 5e0d853a..89ffb4c6 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -434,13 +434,13 @@ Section weakening.
Context `{typeG Σ}.
Lemma subtype_weaken E1 E2 L1 L2 ty1 ty2 :
- E1 `contains` E2 → L1 `contains` L2 →
+ E1 ⊆+ E2 → L1 ⊆+ L2 →
subtype E1 L1 ty1 ty2 → subtype E2 L2 ty1 ty2.
Proof.
(* TODO: There's no lemma relating `contains` to membership (∈)...?? *)
- iIntros (HE12 [L' HL12]%contains_Permutation Hsub) "#LFT HE HL".
+ iIntros (HE12 [L' HL12]%submseteq_Permutation Hsub) "#LFT HE HL".
iApply (Hsub with "LFT [HE] [HL]").
- - rewrite /elctx_interp_0. by iApply big_sepL_contains.
+ - rewrite /elctx_interp_0. by iApply big_sepL_submseteq.
- iDestruct "HL" as %HL. iPureIntro. intros ??. apply HL.
rewrite HL12. set_solver.
Qed.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index ec4bceff..bfa53826 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -197,9 +197,9 @@ Section type_context.
by iMod (H2 with "LFT HE HL H") as "($ & $ & $)".
Qed.
- Lemma contains_tctx_incl E L T1 T2 : T1 `contains` T2 → tctx_incl E L T2 T1.
+ Lemma contains_tctx_incl E L T1 T2 : T1 ⊆+ T2 → tctx_incl E L T2 T1.
Proof.
- rewrite /tctx_incl. iIntros (Hc ???) "_ $ $ H". by iApply big_sepL_contains.
+ rewrite /tctx_incl. iIntros (Hc ???) "_ $ $ H". by iApply big_sepL_submseteq.
Qed.
Global Instance tctx_incl_app E L :
@@ -234,7 +234,7 @@ Section type_context.
remember (p â— ty)%TC. induction 1 as [|???? IH]; subst.
- apply (tctx_incl_frame_r _ [_] [_;_]), copy_tctx_incl, _.
- etrans. by apply (tctx_incl_frame_l [_]), IH, reflexivity.
- apply contains_tctx_incl, contains_swap.
+ apply contains_tctx_incl, submseteq_swap.
Qed.
Lemma subtype_tctx_incl E L p ty1 ty2 :
@@ -258,7 +258,7 @@ Section type_context.
Lemma tctx_extract_hasty_cons E L p ty T T' x :
tctx_extract_hasty E L p ty T T' →
tctx_extract_hasty E L p ty (x::T) (x::T').
- Proof. unfold tctx_extract_hasty=>->. apply contains_tctx_incl, contains_swap. Qed.
+ Proof. unfold tctx_extract_hasty=>->. apply contains_tctx_incl, submseteq_swap. Qed.
Lemma tctx_extract_hasty_here_copy E L p ty ty' T `{!Copy ty} :
subtype E L ty ty' →
tctx_extract_hasty E L p ty' ((p â— ty)::T) ((p â— ty)::T).
@@ -281,7 +281,7 @@ Section type_context.
tctx_extract_blocked E L p κ ty (x::T) (x::T').
Proof.
move=> /(tctx_incl_frame_l [x]) /= Hincl. rewrite /tctx_extract_blocked.
- etrans; first done. apply contains_tctx_incl, contains_swap.
+ etrans; first done. apply contains_tctx_incl, submseteq_swap.
Qed.
Lemma tctx_extract_blocked_here E L p κ ty T :
tctx_extract_blocked E L p κ ty ((p â—{κ} ty)::T) T.
@@ -309,7 +309,7 @@ Section type_context.
tctx_incl E L T T'.
Proof.
unfold tctx_extract_ctx=>->.
- by apply contains_tctx_incl, contains_inserts_r.
+ by apply contains_tctx_incl, submseteq_inserts_r.
Qed.
(* Unblocking a type context. *)
--
GitLab