port to stdpp 1.6.0 and later (#13)

runtimeverification · Feb 18, 2022 · 6c24ee5 · 6c24ee5
1 parent d5595fe
commit 6c24ee5
Show file tree

Hide file tree

Showing 10 changed files with 22 additions and 22 deletions.
diff --git a/Dockerfile b/Dockerfile
@@ -50,7 +50,7 @@ RUN    opam init --auto-setup --yes --jobs=${NJOBS} --compiler=${COMPILER} --dis
 # From: https://github.com/coq-community/docker-coq/blob/master/Dockerfile
 
 ENV COQ_VERSION="8.13.2"
-ENV STDPP_VERSION="1.5.0"
+ENV STDPP_VERSION="1.6.0"
 ENV COQ_OPAM="coq coq-stdpp"
 
 RUN    eval $(opam env --switch=${COMPILER} --set-switch)                          \

diff --git a/README.md b/README.md
@@ -9,20 +9,20 @@ contains a formalization of VLSMs and their theory in the Coq proof assistant.
 - License: [BSD 3-Clause "New" or "Revised" License](LICENSE.md)
 - Compatible Coq versions: 8.13
 - Additional dependencies:
-  - [Coq-std++](https://gitlab.mpi-sws.org/iris/stdpp/) 1.5.0
+  - [Coq-std++](https://gitlab.mpi-sws.org/iris/stdpp/) 1.6.0 or later
 - Coq namespace: `VLSM`
 
 ## Building instructions
 
-The project is compatible with the 2021.09 package pick for Coq 8.13 of
-[Coq Platform release 2021.09.0](https://github.com/coq/platform/releases/tag/2021.09.0),
+The project is compatible with the Jan 2022 package pick for Coq 8.13 of
+[Coq Platform release 2022.01.0](https://github.com/coq/platform/releases/tag/2022.01.0),
 so you can obtain all dependencies by installing that Coq Platform variant.
 
 To instead install dependencies manually via [opam](https://opam.ocaml.org/doc/Install.html), do:
 
 ```shell
 opam repo add coq-released https://coq.inria.fr/opam/released
-opam install coq.8.13.2 coq-stdpp.1.5.0
+opam install coq.8.13.2 coq-stdpp.1.6.0
 ```
 
 To build the project when you have all dependencies installed, do:

diff --git a/coq-vlsm.opam b/coq-vlsm.opam
@@ -17,7 +17,7 @@ build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
   "coq" {>= "8.13" & < "8.14~"}
-  "coq-stdpp" {= "1.5.0"}
+  "coq-stdpp" {>= "1.6.0"}
 ]
 
 tags: [

diff --git a/meta.yml b/meta.yml
@@ -44,9 +44,9 @@ supported_coq_versions:
 dependencies:
 - opam:
     name: coq-stdpp
-    version: '{= "1.5.0"}'
+    version: '{>= "1.6.0"}'
   description: |-
-    [Coq-std++](https://gitlab.mpi-sws.org/iris/stdpp/) 1.5.0
+    [Coq-std++](https://gitlab.mpi-sws.org/iris/stdpp/) 1.6.0 or later
 
 namespace: VLSM
 
@@ -60,15 +60,15 @@ categories:
 build: |-
   ## Building instructions
 
-  The project is compatible with the 2021.09 package pick for Coq 8.13 of
-  [Coq Platform release 2021.09.0](https://github.com/coq/platform/releases/tag/2021.09.0),
+  The project is compatible with the Jan 2022 package pick for Coq 8.13 of
+  [Coq Platform release 2022.01.0](https://github.com/coq/platform/releases/tag/2022.01.0),
   so you can obtain all dependencies by installing that Coq Platform variant.
 
   To instead install dependencies manually via [opam](https://opam.ocaml.org/doc/Install.html), do:
 
   ```shell
   opam repo add coq-released https://coq.inria.fr/opam/released
-  opam install coq.8.13.2 coq-stdpp.1.5.0
+  opam install coq.8.13.2 coq-stdpp.1.6.0
   ```
 
   To build the project when you have all dependencies installed, do:

diff --git a/theories/VLSM/Core/Equivocation/MsgDepFixedSetEquivocation.v b/theories/VLSM/Core/Equivocation/MsgDepFixedSetEquivocation.v
@@ -155,7 +155,7 @@ Proof.
           (single_equivocator_projection s i Hi)) with (lY := li) in HtX
   ; [eexists _,_,_; eassumption |].
   unfold sub_label_element_project; cbn.
-  rewrite decide_left with eq_refl; cbn.
+  rewrite (decide_True_pi eq_refl).
   reflexivity.
 Qed.
 
@@ -218,7 +218,7 @@ Proof.
       eapply (VLSM_projection_input_valid_transition (single_equivocator_projection s i Hi))
       ; [| eassumption].
       unfold sub_label_element_project; cbn.
-      rewrite decide_left with eq_refl; reflexivity.
+      rewrite (decide_True_pi eq_refl); reflexivity.
 Qed.
 
 Lemma strong_fixed_equivocation_msg_dep_constraint_subsumption

diff --git a/theories/VLSM/Core/ProjectionTraces.v b/theories/VLSM/Core/ProjectionTraces.v
@@ -259,7 +259,7 @@ Lemma composite_project_label_eq lj
   : composite_project_label (existT j lj) = Some lj.
 Proof.
   unfold composite_project_label; cbn.
-  rewrite decide_left with eq_refl; cbn.
+  rewrite (decide_True_pi eq_refl).
   reflexivity.
 Qed.
 

diff --git a/theories/VLSM/Core/SubProjectionTraces.v b/theories/VLSM/Core/SubProjectionTraces.v
@@ -1655,7 +1655,7 @@ Lemma sub_element_state_eq s H_j
   : sub_element_state s (dexist j H_j) = s.
 Proof.
   unfold sub_element_state; cbn.
-  rewrite decide_left with (HP := eq_refl); cbn.
+  rewrite (decide_True_pi eq_refl).
   reflexivity.
 Qed.
 
@@ -1760,7 +1760,7 @@ Lemma sub_element_label_project
 Proof.
   intros lY.
   unfold sub_element_label, sub_label_element_project; cbn.
-  rewrite decide_left with (HP := eq_refl); cbn.
+  rewrite (decide_True_pi eq_refl).
   reflexivity.
 Qed.
 
@@ -1769,7 +1769,7 @@ Lemma sub_element_state_project
 Proof.
   intros sY.
   unfold sub_element_state, sub_state_element_project; cbn.
-  rewrite decide_left with (HP := eq_refl); cbn.
+  rewrite (decide_True_pi eq_refl).
   reflexivity.
 Qed.
 

diff --git a/theories/VLSM/Core/Validator.v b/theories/VLSM/Core/Validator.v
@@ -14,7 +14,7 @@ Section projection_validator.
 Context
   {message : Type}
   {X Y : VLSM message}
-  {label_project : vlabel X -> option (vlabel Y)}
+  {label_project : vlabel X -> option (vlabel Y)} 
   {state_project : vstate X -> vstate Y}
   (PreY := pre_loaded_with_all_messages_vlsm Y)
   (Hproj : VLSM_projection X PreY label_project state_project)
@@ -355,7 +355,7 @@ Proof.
     apply Hvalidator in Hiv as (sX & <- & HivX).
     exists (existT i li), sX; intuition.
     unfold composite_project_label; cbn.
-    rewrite decide_left with eq_refl; reflexivity.
+    rewrite (decide_True_pi eq_refl); reflexivity.
 Qed.
 
 Definition pre_loaded_with_all_messages_validator_component_proj_incl

diff --git a/theories/VLSM/Lib/FinSetExtras.v b/theories/VLSM/Lib/FinSetExtras.v
@@ -75,7 +75,7 @@ Section general.
   Lemma difference_size_subset
     (X Y : C)
     (Hsub : Y ⊆ X) :
-    (Z.of_nat (size (X ∖ Y)) = size X - size Y)%Z.
+    (Z.of_nat (size (X ∖ Y)) = Z.of_nat (size X) - Z.of_nat (size Y))%Z.
   Proof.
     assert (Htemp : Y ∪ (X ∖ Y) ≡ X). {
       apply set_equiv_equivalence.
@@ -110,7 +110,7 @@ Section general.
 
   Lemma difference_size
     (X Y : C) :
-    (Z.of_nat (size (X ∖ Y)) = size X - size (X ∩ Y))%Z.
+    (Z.of_nat (size (X ∖ Y)) = Z.of_nat (size X) - Z.of_nat (size (X ∩ Y)))%Z.
   Proof.
     rewrite difference_with_intersection.
     specialize (difference_size_subset X (X ∩ Y)) as Hdif.

diff --git a/theories/VLSM/Lib/StdppExtras.v b/theories/VLSM/Lib/StdppExtras.v
@@ -81,7 +81,7 @@ Qed.
 Lemma last_last_error {A : Type} (l : list A) :
  last_error l = last l.
 Proof.
- induction l; [reflexivity|]; simpl.
+ induction l; [reflexivity|]; rewrite last_cons.
  rewrite <- IHl; clear IHl.
  destruct l; [reflexivity|]; simpl.
  f_equal.