Adapting to math-comp/math-comp#1545.

.github/workflows/docker-action.yml

@@ -18,6 +18,7 @@ jobs:
       matrix:
         image:
           - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
+          - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.1'
           - 'mathcomp/mathcomp-dev:rocq-prover-dev'
       fail-fast: false
     steps:

README.md

@@ -10,8 +10,6 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [docker-action-link]: https://github.com/imdea-software/htt/actions/workflows/docker-action.yml
 
 
-
-
 Hoare Type Theory (HTT) is a verification system for reasoning about sequential heap-manipulating
 programs based on Separation logic.
 
@@ -130,3 +128,10 @@ The original version of HTT can be found [here](https://software.imdea.org/~alek
   Kasper Svendsen, Lars Birkedal and Aleksandar Nanevski. TLCA 2011.
 
   A semantic model for HTT, with large sigma types.
+
+* [Verifying Graph Algorithms in Separation Logic: A Case for an
+  Algebraic Approach](https://software.imdea.org/~aleks/icfp25/paper-sub.pdf)
+
+  Marcos Grandury, Aleksandar Nanevski and Alexander Gryzlov. ICFP 2025.
+
+  The paper on verifying graphs algorithms using PCMs and their morphism.

coq-htt-core.opam

@@ -35,9 +35,9 @@ build: [make "-C" "htt" "-j%{jobs}%"]
 install: [make "-C" "htt" "install"]
 depends: [
   "dune" {>= "3.6"}
-  "coq" { (>= "9.0" & < "9.1~") | (= "dev") }
-  "coq-hierarchy-builder" { (>= "1.7.0" & < "1.10~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.5~") | (= "dev") }
+  "coq" { (>= "9.0" & < "9.2~") | (= "dev") }
+  "coq-hierarchy-builder" { (>= "1.7.0" & < "1.11~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
   "coq-fcsl-pcm" { (>= "2.2.0" & < "2.3~") | (= "dev") }

coq-htt.opam

@@ -32,8 +32,8 @@ build: [make "-C" "examples" "-j%{jobs}%"]
 install: [make "-C" "examples" "install"]
 depends: [
   "dune" {>= "3.6"}
-  "coq" { (>= "9.0" & < "9.1~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.5~") | (= "dev") }
+  "coq" { (>= "9.0" & < "9.2~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
   "coq-fcsl-pcm" { (>= "2.2.0" & < "2.3~") | (= "dev") }

examples/array.v

@@ -27,7 +27,7 @@ From htt Require Import options model heapauto.
 Record array (I : finType) (T : Type) : Set := Array {orig :> ptr}.
 Arguments Array {I T}.
 
-Definition array_for (I : finType) (T : Type) of phant (I -> T) := array I T.
+Definition array_for (I : finType) (T : Type) & phant (I -> T) := array I T.
 Identity Coercion array_for_array : array_for >-> array.
 Notation "{ 'array' aT }" := (array_for (Phant aT))
   (at level 0, format "{ 'array'  '[hv' aT ']' }") : type_scope.

examples/bubblesort.v

@@ -22,6 +22,9 @@ Import Order.NatOrder Order.TTheory.
 Local Open Scope order_scope.
 Local Open Scope nat_scope.
 
+(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Set SsrOldRewriteGoalsOrder.  
+
 (* Brief mathematics of (bubble) array sorting: *)
 (* Theory of permutations built out of (adjacent-element) swaps acting on *)
 (* finite functions from bounded nats to ordered values. *)

examples/congmath.v

@@ -16,6 +16,9 @@ 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.
 
+(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Set SsrOldRewriteGoalsOrder.  
+
 (**********************)
 (* Congruence closure *)
 (**********************)

examples/congprog.v

@@ -19,6 +19,9 @@ From pcm Require Import unionmap heap autopcm automap.
 From htt Require Import options model heapauto llist array.
 From htt Require Import kvmaps hashtab congmath.
 
+(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Set SsrOldRewriteGoalsOrder.  
+
 (***********************************)
 (* Congruence closure verification *)
 (***********************************)

examples/hashtab.v

@@ -19,6 +19,9 @@ From pcm Require Import pcm unionmap heap autopcm.
 From htt Require Import options model heapauto.
 From htt Require Import array kvmaps.
 
+(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Set SsrOldRewriteGoalsOrder.  
+
 (* hash table is array of buckets, i.e. KV maps *)
 (* bucket indices are provided by the hash function *)
 (* using dynaming kv-maps for buckets *)

examples/kvmaps.v

@@ -22,6 +22,9 @@ From pcm Require Import options axioms pred ordtype finmap seqext.
 From pcm Require Import pcm unionmap heap autopcm automap.
 From htt Require Import options model heapauto.
 
+(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Set SsrOldRewriteGoalsOrder.  
+
 (* Dynamic KV map is determined by its root pointer(s). *)
 (* Functions such insert and remove may modify *)
 (* the root, and will correspondingly return the new one. *)

examples/quicksort.v

@@ -21,6 +21,9 @@ Import Order.NatOrder Order.TTheory.
 Local Open Scope order_scope.
 Local Open Scope nat_scope.
 
+(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Set SsrOldRewriteGoalsOrder.  
+
 (* Brief mathematics of quickorting *)
 (* There is some overlap with mathematics developed for bubblesort *)
 (* but the development is repeated here to make the files *)

examples/union_find.v

@@ -17,6 +17,9 @@ From pcm Require Import options axioms pred seqext.
 From pcm Require Import prelude pcm unionmap natmap heap autopcm automap.
 From htt Require Import options model heapauto tree.
 
+(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Set SsrOldRewriteGoalsOrder.  
+
 (**************)
 (**************)
 (* Union-find *)

htt/domain.v

@@ -16,6 +16,9 @@ From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype.
 From pcm Require Import options axioms pred prelude.
 
+(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Set SsrOldRewriteGoalsOrder.  
+
 (**************************************************)
 (* This file develops some basic domain theory of *)
 (* posets, complete lattices, complete partial    *)
@@ -208,7 +211,7 @@ Definition lattice_axiom (T : poset) (sup : Pred T -> T) :=
       forall (s : Pred T) x,
         (forall y, y \In s -> y <== x) -> sup s <== x].  
 
-HB.mixin Record isLattice T of Poset T := {
+HB.mixin Record isLattice T & Poset T := {
   sup : Pred T -> T; 
   lattice_subproof : lattice_axiom sup}.
 
@@ -602,15 +605,15 @@ Definition cpo_axiom (T : poset) (bot : T) (lim : chain T -> T) :=
       forall (s : chain T) x,
         (forall y, y \In s -> y <== x) -> lim s <== x].
 
-HB.mixin Record isCPO T of Poset T := {
+HB.mixin Record isCPO T & Poset T := {
   bot : T; 
   lim_op : chain T -> T; 
   cpo_subproof: cpo_axiom bot lim_op}.
 
 #[short(type="cpo")]
 HB.structure Definition CPO := {T of Poset T & isCPO T}.
 
-Definition limx (D : cpo) (s : chain D) of phantom (Pred _) s := lim_op s.
+Definition limx (D : cpo) (s : chain D) & phantom (Pred _) s := lim_op s.
 Notation lim s := (limx (Phantom (Pred _) s)).
 
 Section Repack.
@@ -854,7 +857,7 @@ Definition contfun_axiom (D1 D2 : cpo) (f : mono_fun D1 D2) :=
   forall s : chain D1, f (lim s) <== lim (Image f s).  
 
 HB.mixin Record isContFun (D1 D2 : cpo) (f : D1 -> D2) 
-  of @MonoFun D1 D2 f := {contfun_subproof : contfun_axiom f}.
+  & @MonoFun D1 D2 f := {contfun_subproof : contfun_axiom f}.
 
 #[short(type="cont_fun")]
 HB.structure Definition ContFun (D1 D2 : cpo) := 

meta.yml

@@ -81,24 +81,26 @@ license:
 
 supported_coq_versions:
   text: 9.0 or later
-  opam: '{ (>= "9.0" & < "9.1~") | (= "dev") }'
+  opam: '{ (>= "9.0" & < "9.2~") | (= "dev") }'
 
 tested_coq_opam_versions:
 - version: '2.4.0-rocq-prover-9.0'
   repo: 'mathcomp/mathcomp'
+- version: '2.5.0-rocq-prover-9.1'
+  repo: 'mathcomp/mathcomp'
 - version: 'rocq-prover-dev'
   repo: 'mathcomp/mathcomp-dev'
 
 
 dependencies:
 - opam:
     name: coq-hierarchy-builder
-    version: '{ (>= "1.7.0" & < "1.10~") | (= "dev") }'
+    version: '{ (>= "1.7.0" & < "1.11~") | (= "dev") }'
   description: |-
     [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder)
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "2.4.0" & < "2.5~") | (= "dev") }'
+    version: '{ (>= "2.4.0" & < "2.6~") | (= "dev") }'
   description: |-
     [MathComp ssreflect 2.4 or later](https://math-comp.github.io)
 - opam: