From f4d2aa124c4a26a0894ffdaa60081165449815de Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <gaeher@mpi-sws.org>
Date: Wed, 4 Oct 2023 08:25:04 +0200
Subject: [PATCH] bump
---
semantics.opam | 8 ++++----
theories/program_logics/heap_lang/primitive_laws.v | 5 +++--
theories/program_logics/resource_algebras.v | 4 ++--
theories/type_systems/systemf/binary_logrel.v | 2 +-
4 files changed, 10 insertions(+), 9 deletions(-)
diff --git a/semantics.opam b/semantics.opam
index 627e21e..fe4d8e4 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -9,10 +9,10 @@ bug-reports: "https://gitlab.mpi-sws.org/FP/semantics-course/issues"
version: "dev"
depends: [
- "coq" { (>= "8.14" & < "8.18~") | (= "dev") }
- "coq-iris-heap-lang" { (= "dev.2023-05-19.0.89b39c82") | (= "dev") }
- "coq-equations" { (= "1.2.4+8.13") | (= "1.3+8.14") | (= "1.3+8.15") | (= "1.3+8.16") | (= "1.3+8.17") }
- "coq-autosubst" { (= "1.7") | (= "dev") }
+ "coq" { (>= "8.18" & < "8.19~") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2023-10-03.0.70b30af7") | (= "dev") }
+ "coq-equations" { (= "1.3+8.18") }
+ "coq-autosubst" { (= "1.8") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/program_logics/heap_lang/primitive_laws.v b/theories/program_logics/heap_lang/primitive_laws.v
index 6ce0ff7..e31f12f 100644
--- a/theories/program_logics/heap_lang/primitive_laws.v
+++ b/theories/program_logics/heap_lang/primitive_laws.v
@@ -68,10 +68,11 @@ Proof. apply mapsto_valid. Qed.
Lemma mapsto_valid_2 l dq1 dq2 v1 v2 :
l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
Proof.
- iIntros "H1 H2". iDestruct (mapsto_valid_2 with "H1 H2") as %[? [=?]]. done.
+ iIntros "H1 H2".
+ iDestruct (mapsto_valid_2 with "H1 H2") as %[? [=]]. done.
Qed.
Lemma mapsto_agree l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2⌝.
-Proof. iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %[=?]. done. Qed.
+Proof. iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %[=]. done. Qed.
Lemma mapsto_combine l dq1 dq2 v1 v2 :
l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{dq1 ⋅ dq2} v1 ∗ ⌜v1 = v2⌝.
diff --git a/theories/program_logics/resource_algebras.v b/theories/program_logics/resource_algebras.v
index 381ea9a..66fa150 100644
--- a/theories/program_logics/resource_algebras.v
+++ b/theories/program_logics/resource_algebras.v
@@ -675,9 +675,9 @@ Section sum.
f_equiv. eauto using lra_pcore_l.
- intros [a|b|] ? [= Ha]; subst; auto; rewrite csum_pcore in Ha.
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
- feed inversion (lra_pcore_idemp a ca); auto; rewrite csum_pcore; by simplify_option_eq.
+ oinversion (lra_pcore_idemp a ca); auto; rewrite csum_pcore; by simplify_option_eq.
+ destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
- feed inversion (lra_pcore_idemp b cb); auto; rewrite csum_pcore; by simplify_option_eq.
+ oinversion (lra_pcore_idemp b cb); auto; rewrite csum_pcore; by simplify_option_eq.
- intros x y ? [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]%csum_included [= Ha].
+ exists CsumBot. rewrite csum_included; eauto.
+ destruct (pcore a) as [ca|] eqn:?; rewrite csum_pcore; rewrite csum_pcore in Ha; simplify_option_eq.
diff --git a/theories/type_systems/systemf/binary_logrel.v b/theories/type_systems/systemf/binary_logrel.v
index 4717a13..01d568a 100644
--- a/theories/type_systems/systemf/binary_logrel.v
+++ b/theories/type_systems/systemf/binary_logrel.v
@@ -1051,7 +1051,7 @@ Lemma sem_typing_ctx_equiv Δ Γ e1 e2 A :
Proof.
intros Hsem ? ? C Hty. eapply sem_typed_congruence in Hty; last done.
all: try done.
- feed pose proof (Hty ∅ ∅ δ_any) as He; first constructor.
+ opose proof* (Hty ∅ ∅ δ_any) as He; first constructor.
revert He. rewrite !subst_map_empty.
simp type_interp. destruct 1 as (v1 & v2 & Hbs1 & Hbs2 & Hv).
simp type_interp in Hv. destruct Hv as (z & -> & ->). eauto.
--
GitLab