From f9b4c7533d0e95f8936cf62004366ce613c65f64 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Thu, 22 Sep 2022 18:42:48 +0200
Subject: [PATCH] adapt for Coq 8.16
---
semantics.opam | 2 +-
theories/program_logics/concurrency.v | 8 ++++----
theories/type_systems/systemf/types.v | 6 +++---
theories/type_systems/systemf_mu/types.v | 8 ++++----
theories/type_systems/systemf_mu_state/logrel.v | 2 +-
theories/type_systems/systemf_mu_state/types.v | 8 ++++----
6 files changed, 17 insertions(+), 17 deletions(-)
diff --git a/semantics.opam b/semantics.opam
index 90fbb39..b263766 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -12,7 +12,7 @@ depends: [
"coq" { (>= "8.13" & < "8.17~") | (= "dev") }
"coq-iris-heap-lang" { (= "dev.2022-09-21.1.291dc89e") | (= "dev") }
"coq-equations" { (= "1.2.4+8.13") | (= "1.3+8.14") | (= "1.3+8.15") | (= "1.3+8.16") }
- "coq-autosubst" { = "1.7" }
+ "coq-autosubst" { (= "1.7") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/program_logics/concurrency.v b/theories/program_logics/concurrency.v
index 435a834..1c30fb7 100644
--- a/theories/program_logics/concurrency.v
+++ b/theories/program_logics/concurrency.v
@@ -153,9 +153,9 @@ Section spin_lock.
(** Lock specification *)
Definition lockN : namespace := nroot .@ "lock".
- Definition lock_inv l (P : iProp Σ) :=
+ Definition lock_inv (l : loc) (P : iProp Σ) : iProp Σ :=
((l ↦ #false ∗ P) ∨ (l ↦ #true))%I.
- Definition is_lock v P :=
+ Definition is_lock (v : val) (P : iProp Σ) : iProp Σ :=
(∃ l : loc, ⌜v = #l⌝ ∗ inv lockN (lock_inv l P))%I.
Instance is_lock_pers v P : Persistent (is_lock v P).
@@ -262,8 +262,8 @@ End lock_lemmas.
Section excl_spin_lock.
Context `{heapGS Σ} `{lockG Σ}.
- Definition is_excl_lock v γ P :=
- is_lock v P
+ Definition is_excl_lock (v : val) (γ : gname) (P : iProp Σ) : iProp Σ :=
+ is_lock v P (* TODO *)
.
Instance is_excl_lock_pers v γ P : Persistent (is_excl_lock v γ P).
diff --git a/theories/type_systems/systemf/types.v b/theories/type_systems/systemf/types.v
index 7346fad..d6ffb7e 100644
--- a/theories/type_systems/systemf/types.v
+++ b/theories/type_systems/systemf/types.v
@@ -275,7 +275,7 @@ Proof.
induction 1 in δ |-*; intros Hmon; simpl; eauto.
all: econstructor; eapply type_wf_mono; first eapply IHtype_wf; last done.
all: intros i j Hlt; destruct i, j; simpl; try lia.
- all: by eapply lt_n_S, Hmon, lt_S_n.
+ all: rewrite -Nat.succ_lt_mono; eapply Hmon; lia.
Qed.
(** [A.[σ]], i.e. [A] with the substitution [σ] applied to it, is well-formed under [m] if
@@ -290,12 +290,12 @@ Proof.
+ econstructor; eapply IHtype_wf.
intros [|x]; rewrite /up //=.
- econstructor. lia.
- - intros Hlt % lt_S_n. eapply type_wf_rename; eauto.
+ - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
intros i j Hlt'; simpl; lia.
+ econstructor; eapply IHtype_wf.
intros [|x]; rewrite /up //=.
- econstructor. lia.
- - intros Hlt % lt_S_n. eapply type_wf_rename; eauto.
+ - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
intros i j Hlt'; simpl; lia.
Qed.
diff --git a/theories/type_systems/systemf_mu/types.v b/theories/type_systems/systemf_mu/types.v
index a8e88e6..eaca72d 100644
--- a/theories/type_systems/systemf_mu/types.v
+++ b/theories/type_systems/systemf_mu/types.v
@@ -288,7 +288,7 @@ Proof.
induction 1 in δ |-*; intros Hmon; simpl; eauto.
all: econstructor; eapply type_wf_mono; first eapply IHtype_wf; last done.
all: intros i j Hlt; destruct i, j; simpl; try lia.
- all: by eapply lt_n_S, Hmon, lt_S_n.
+ all: rewrite -Nat.succ_lt_mono; eapply Hmon; lia.
Qed.
(** [A.[σ]], i.e. [A] with the substitution [σ] applied to it, is well-formed under [m] if
@@ -303,17 +303,17 @@ Proof.
+ econstructor; eapply IHtype_wf.
intros [|x]; rewrite /up //=.
- econstructor. lia.
- - intros Hlt % lt_S_n. eapply type_wf_rename; eauto.
+ - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
intros i j Hlt'; simpl; lia.
+ econstructor; eapply IHtype_wf.
intros [|x]; rewrite /up //=.
- econstructor. lia.
- - intros Hlt % lt_S_n. eapply type_wf_rename; eauto.
+ - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
intros i j Hlt'; simpl; lia.
+ econstructor. eapply IHtype_wf.
intros [|x]; rewrite /up //=.
- econstructor. lia.
- - intros Hlt % lt_S_n. eapply type_wf_rename; eauto.
+ - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
intros ???. simpl; lia.
Qed.
diff --git a/theories/type_systems/systemf_mu_state/logrel.v b/theories/type_systems/systemf_mu_state/logrel.v
index fccf98b..bc3afd7 100644
--- a/theories/type_systems/systemf_mu_state/logrel.v
+++ b/theories/type_systems/systemf_mu_state/logrel.v
@@ -346,7 +346,7 @@ Proof.
destruct Hincl as (W''& ->).
exists (length W'' + i).
rewrite lookup_app_r; last lia.
- by rewrite minus_plus.
+ by rewrite Nat.add_comm Nat.add_sub.
Qed.
Lemma wsat_merge σ1 σ2 W1 W2 :
diff --git a/theories/type_systems/systemf_mu_state/types.v b/theories/type_systems/systemf_mu_state/types.v
index d1f982d..3f73707 100644
--- a/theories/type_systems/systemf_mu_state/types.v
+++ b/theories/type_systems/systemf_mu_state/types.v
@@ -309,7 +309,7 @@ Proof.
induction 1 in δ |-*; intros Hmon; simpl; eauto.
all: econstructor; eapply type_wf_mono; first eapply IHtype_wf; last done.
all: intros i j Hlt; destruct i, j; simpl; try lia.
- all: by eapply lt_n_S, Hmon, lt_S_n.
+ all: rewrite -Nat.succ_lt_mono; eapply Hmon; lia.
Qed.
(** [A.[σ]], i.e. [A] with the substitution [σ] applied to it, is well-formed under [m] if
@@ -324,17 +324,17 @@ Proof.
+ econstructor; eapply IHtype_wf.
intros [|x]; rewrite /up //=.
- econstructor. lia.
- - intros Hlt % lt_S_n. eapply type_wf_rename; eauto.
+ - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
intros i j Hlt'; simpl; lia.
+ econstructor; eapply IHtype_wf.
intros [|x]; rewrite /up //=.
- econstructor. lia.
- - intros Hlt % lt_S_n. eapply type_wf_rename; eauto.
+ - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
intros i j Hlt'; simpl; lia.
+ econstructor. eapply IHtype_wf.
intros [|x]; rewrite /up //=.
- econstructor. lia.
- - intros Hlt % lt_S_n. eapply type_wf_rename; eauto.
+ - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
intros ???. simpl; lia.
Qed.
--
GitLab