preparing v2.2.0 release

.github/workflows/docker-action.yml

@@ -17,8 +17,6 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
-          - 'mathcomp/mathcomp:2.3.0-coq-8.20'
           - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
           - 'mathcomp/mathcomp-dev:rocq-prover-dev'
       fail-fast: false

README.md

@@ -39,13 +39,13 @@ that HTT implements Separation logic as a shallow embedding in Coq.
   - Alexander Gryzlov
   - Marcos Grandury
 - License: [Apache-2.0](LICENSE)
-- Compatible Coq versions: 8.19 or later
+- Compatible Coq versions: 9.0 or later
 - Additional dependencies:
   - [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder)
   - [MathComp ssreflect 2.2 or later](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)
-  - [FCSL-PCM 2.1](https://github.com/imdea-software/fcsl-pcm)
+  - [FCSL-PCM 2.2](https://github.com/imdea-software/fcsl-pcm)
   - [Dune](https://dune.build) 3.6 or later
 - Coq namespace: `htt`
 - Related publication(s):

coq-htt-core.opam

@@ -3,7 +3,7 @@
 
 opam-version: "2.0"
 maintainer: "[email protected]"
-version: "2.1.0"
+version: "2.2.0"
 
 homepage: "https://github.com/imdea-software/htt"
 dev-repo: "git+https://github.com/imdea-software/htt.git"
@@ -31,16 +31,15 @@ variables). The connection reconciles dependent types with effects of state and
 establishes Separation logic as a type theory for such effects. In implementation terms, it means
 that HTT implements Separation logic as a shallow embedding in Coq."""
 
-build: [make "-C" "htt" "-j%{jobs}%"]
-install: [make "-C" "htt" "install"]
+build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "3.6"}
-  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
+  "coq" { (>= "9.0" & < "9.1~") | (= "dev") }
   "coq-hierarchy-builder" { (>= "1.7.0" & < "1.10~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.5~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.5~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
-  "coq-fcsl-pcm" { (>= "2.1.0" & < "2.2~") | (= "dev") }
+  "coq-fcsl-pcm" { (>= "2.2.0" & < "2.3~") | (= "dev") }
 ]
 
 tags: [

coq-htt.opam

@@ -1,6 +1,6 @@
 opam-version: "2.0"
 maintainer: "[email protected]"
-version: "2.1.0"
+version: "2.2.0"
 
 homepage: "https://github.com/imdea-software/htt"
 dev-repo: "git+https://github.com/imdea-software/htt.git"
@@ -32,11 +32,11 @@ build: [make "-C" "examples" "-j%{jobs}%"]
 install: [make "-C" "examples" "install"]
 depends: [
   "dune" {>= "3.6"}
-  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.5~") | (= "dev") }
+  "coq" { (>= "9.0" & < "9.1~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.5~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
-  "coq-fcsl-pcm" { (>= "2.1.0" & < "2.2~") | (= "dev") }
+  "coq-fcsl-pcm" { (>= "2.2.0" & < "2.3~") | (= "dev") }
   "coq-htt-core" {= version}
 ]
 

examples/array.v

@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq path fintype tuple finfun finset.
 From pcm Require Import options axioms prelude pred.
 From pcm Require Import pcm unionmap heap.

examples/bintree.v

@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype seq ssrnat.
 From pcm Require Import options axioms pred.
 From pcm Require Import pcm unionmap heap autopcm automap.

examples/bst.v

@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype ssrnat seq path.
 From pcm Require Import options axioms pred ordtype seqext.
 From pcm Require Import pcm unionmap heap autopcm automap.

examples/bubblesort.v

@@ -16,7 +16,8 @@ From mathcomp Require Import ssrnat eqtype seq path fintype tuple.
 From mathcomp Require Import finfun fingroup perm order interval.
 From pcm Require Import options axioms prelude pred ordtype slice.
 From pcm Require Import seqext pcm unionmap heap.
-From htt Require Import options model heapauto array.
+From htt Require Import options model heapauto.
+From htt Require Import array.
 Import Order.NatOrder Order.TTheory.
 Local Open Scope order_scope.
 Local Open Scope nat_scope.

examples/congmath.v

@@ -12,7 +12,7 @@ limitations under the License.
 *)
 
 From HB Require Import structures.
-From Coq Require Import Recdef Setoid ssreflect ssrbool ssrfun.
+From Stdlib Require Import Recdef Setoid ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype choice ssrnat seq bigop fintype finfun.
 From pcm Require Import options prelude ordtype finmap pred seqext.
 

examples/cyclic.v

@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype seq ssrnat.
 From pcm Require Import options axioms pred seqext.
 From pcm Require Import pcm unionmap heap auto automap autopcm.

examples/dlist.v

@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq.
 From pcm Require Import options axioms pred.
 From pcm Require Import pcm unionmap heap autopcm.

examples/exploit.v

@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool Logic.Hurkens.
+From Stdlib Require Import ssreflect ssrbool Logic.Hurkens.
 
 (* This file shows the unsoundness of the axiom pack_injective assumed in *)
 (* the implementation of Ynot2.0. The proof relies on the lemma of        *)

examples/gcd.v

@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype div.
 From pcm Require Import axioms pred ordtype pcm heap.
 From htt Require Import options model heapauto.

examples/hashtab.v

@@ -12,7 +12,7 @@ limitations under the License.
 *)
 
 From HB Require Import structures.
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq fintype tuple finfun finset.
 From pcm Require Import options axioms prelude pred ordtype finmap.
 From pcm Require Import pcm unionmap heap autopcm.

examples/kvmaps.v

@@ -16,7 +16,7 @@ limitations under the License.
 (******************)
 
 From HB Require Import structures.
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype seq path ssrnat.
 From pcm Require Import options axioms pred ordtype finmap seqext.
 From pcm Require Import pcm unionmap heap autopcm automap.

examples/queue.v

@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype ssrnat seq.
 From pcm Require Import options axioms pred.
 From pcm Require Import pcm unionmap heap automap.

examples/quicksort.v

@@ -303,8 +303,8 @@ case: oleqP=>Hfp.
   - step=>_; split.
     - rewrite Sbo_eq; apply/andP; split=>//.
       by apply/leq_ltn_trans/Hj.
-    exists (tperm i j); rewrite Sbo_eq; split=>//.
-    - rewrite -(eqP Hj1).
+    exists (tperm i j); rewrite Sbo_eq; split=>//.  
+    - rewrite -(eqP Hj1).      
       apply/(subset_trans (tperm_on i j))/subsetP=>/= x; rewrite !inE ltnS.
       by case/orP=>/eqP->; rewrite leqnn // andbT.
     - rewrite slice_oSR slice_xR; last by rewrite bnd_simp.

examples/stack.v

@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype seq.
 From pcm Require Import options axioms pred.
 From pcm Require Import pcm unionmap heap autopcm.

htt/domain.v

@@ -12,7 +12,7 @@ limitations under the License.
 *)
 
 From HB Require Import structures.
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype.
 From pcm Require Import options axioms pred prelude.
 

htt/model.v

@@ -1292,13 +1292,33 @@ move=>Hp Hv Hx; apply/vrf_bnd/(gU _ Hp).
 by move=>ex m H V _; apply: Hx.
 Qed.
 
+(* variant of stepU that adds the new heap to the right *)
+Lemma stepV G A B (pq : spec G A) (e : STspec G pq) (e2 : A -> ST B)
+             i (Q : post B) g :
+        (pq g).1 Unit ->
+        (forall x m, (pq g).2 (Val x) m -> vrf (i \+ m) (e2 x) Q) ->
+        (forall x m, (pq g).2 (Exn x) m ->
+           valid (i \+ m) -> Q (Exn x) (i \+ m)) ->
+        vrf i (bnd e e2) Q.
+Proof.
+move=>H1 H2 H3; apply: stepU H1 _ _ =>x m H1; rewrite !(joinC m).
+- by apply: H2.
+by apply: H3.
+Qed.
+
 Arguments stepU {G A B pq e e2 i Q}. 
+Arguments stepV {G A B pq e e2 i Q}. 
 
 Notation "[stepU]" := (stepU tt) (at level 0).
 Notation "[ 'stepU' x1 , .. , xn ]" :=
   (stepU (existT _ x1 .. (existT _ xn tt) ..))
   (at level 0, format "[ 'stepU'  x1 ,  .. ,  xn ]").
 
+Notation "[stepV]" := (stepV tt) (at level 0).
+Notation "[ 'stepV' x1 , .. , xn ]" :=
+  (stepU (existT _ x1 .. (existT _ xn tt) ..))
+  (at level 0, format "[ 'stepV'  x1 ,  .. ,  xn ]").
+
 (* combination of gU + vrf_try *)
 Lemma tryU G A B (pq : spec G A) (e : STspec G pq)
              (e1 : A -> ST B) (e2 : exn -> ST B) i (Q : post B) g :

meta.yml

@@ -72,22 +72,18 @@ maintainers:
 
 opam-file-maintainer: [email protected]
 
-opam-file-version: 2.1.0
+opam-file-version: 2.2.0
 
 license:
   fullname: Apache-2.0
   identifier: Apache-2.0
   file: LICENSE
 
 supported_coq_versions:
-  text: 8.19 or later
-  opam: '{ (>= "8.19" & < "9.1~") | (= "dev") }'
+  text: 9.0 or later
+  opam: '{ (>= "9.0" & < "9.1~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '2.2.0-coq-8.19'
-  repo: 'mathcomp/mathcomp'
-- version: '2.3.0-coq-8.20'
-  repo: 'mathcomp/mathcomp'
 - version: '2.4.0-rocq-prover-9.0'
   repo: 'mathcomp/mathcomp'
 - version: 'rocq-prover-dev'
@@ -102,7 +98,7 @@ dependencies:
     [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder)
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "2.2.0" & < "2.5~") | (= "dev") }'
+    version: '{ (>= "2.4.0" & < "2.5~") | (= "dev") }'
   description: |-
     [MathComp ssreflect 2.2 or later](https://math-comp.github.io)
 - opam:
@@ -115,9 +111,9 @@ dependencies:
     [MathComp fingroup](https://math-comp.github.io)
 - opam:
     name: coq-fcsl-pcm
-    version: '{ (>= "2.1.0" & < "2.2~") | (= "dev") }'
+    version: '{ (>= "2.2.0" & < "2.3~") | (= "dev") }'
   description: |-
-    [FCSL-PCM 2.1](https://github.com/imdea-software/fcsl-pcm)
+    [FCSL-PCM 2.2](https://github.com/imdea-software/fcsl-pcm)
 
 namespace: htt