add fingroup, switch to new namespaces

.github/workflows/docker-action.yml

@@ -28,6 +28,7 @@ jobs:
           opam_file: 'coq-htt.opam'
           custom_image: ${{ matrix.image }}
 
+
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
 # https://github.com/erikmd/docker-coq-github-action-demo

README.md

@@ -41,8 +41,9 @@ that HTT implements Separation logic as a shallow embedding in Coq.
 - Compatible Coq versions: Coq 8.14 to 8.16
 - Additional dependencies:
   - [MathComp ssreflect 1.13 to 1.15](https://math-comp.github.io)
+  - [MathComp fingroup](https://math-comp.github.io)
   - [FCSL-PCM 1.6](https://github.com/imdea-software/fcsl-pcm)
-- Coq namespace: `HTT`
+- Coq namespace: `htt`
 - Related publication(s):
   - [Structuring the verification of heap-manipulating programs](https://software.imdea.org/~aleks/papers/reflect/reflect.pdf) doi:[10.1145/1706299.1706331](https://doi.org/10.1145/1706299.1706331)
 

_CoqProject

@@ -1,11 +1,11 @@
--Q . HTT
+-Q . htt
 -arg "-w -notation-overridden,-local-declaration,-redundant-canonical-projection,-projection-no-head-constant"
 
 options.v
-core/interlude.v
-core/domain.v
-core/model.v
-core/heapauto.v
+htt/interlude.v
+htt/domain.v
+htt/model.v
+htt/heapauto.v
 examples/exploit.v
 examples/gcd.v
 examples/llist.v

coq-htt.opam

@@ -36,14 +36,15 @@ install: [make "install"]
 depends: [
   "coq" { (>= "8.14" & < "8.17~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.16~") | (= "dev") }
+  "coq-mathcomp-fingroup" 
   "coq-fcsl-pcm" { (>= "1.6.0" & < "1.7~") | (= "dev") }
 ]
 
 tags: [
   "category:Computer Science/Data Types and Data Structures"
   "keyword:partial commutative monoids"
   "keyword:separation logic"
-  "logpath:HTT"
+  "logpath:htt"
 ]
 authors: [
   "Aleksandar Nanevski"

examples/array.v

@@ -1,8 +1,8 @@
 From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq path fintype tuple finfun finset.
-From fcsl Require Import axioms prelude pred.
-From fcsl Require Import pcm unionmap heap.
-From HTT Require Import options model heapauto.
+From pcm Require Import options axioms prelude pred.
+From pcm Require Import pcm unionmap heap.
+From htt Require Import options model heapauto.
 
 Definition indx {I : finType} (x : I) := index x (enum I).
 

examples/bintree.v

@@ -1,10 +1,10 @@
 
 From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype seq ssrnat.
-From fcsl Require Import options axioms pred.
-From fcsl Require Import pcm unionmap heap autopcm automap.
-From HTT Require Import model heapauto.
-From HTT Require Import llist.
+From pcm Require Import options axioms pred.
+From pcm Require Import pcm unionmap heap autopcm automap.
+From htt Require Import options model heapauto.
+From htt Require Import llist.
 
 (* Binary tree specification *)
 

examples/bst.v

@@ -1,9 +1,9 @@
 From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype ssrnat seq path.
-From fcsl Require Import options axioms pred ordtype.
-From fcsl Require Import pcm unionmap heap autopcm automap.
-From HTT Require Import interlude model heapauto.
-From HTT Require Import bintree.
+From pcm Require Import options axioms pred ordtype.
+From pcm Require Import pcm unionmap heap autopcm automap.
+From htt Require Import interlude model heapauto.
+From htt Require Import bintree.
 
 Section BST.
 Context {T : ordType}.

examples/bubblesort.v

@@ -1,9 +1,9 @@
 From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq path fintype tuple finfun fingroup perm.
-From fcsl Require Import options axioms prelude pred ordtype.
-From fcsl Require Import pcm unionmap heap.
-From HTT Require Import interlude model heapauto.
-From HTT Require Import array.
+From pcm Require Import options axioms prelude pred ordtype.
+From pcm Require Import pcm unionmap heap.
+From htt Require Import options interlude model heapauto.
+From htt Require Import array.
 
 (* TODO use fintype.lift instead ? *)
 Section OrdArith.

examples/congmath.v

@@ -4,11 +4,8 @@
 
 From Coq Require Import Recdef ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype choice ssrnat seq bigop fintype finfun.
-From fcsl Require Import prelude ordtype finmap pred.
-From HTT Require Import interlude.
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
+From pcm Require Import options prelude ordtype finmap pred.
+From htt Require Import interlude.
 
 Ltac add_morphism_tactic := SetoidTactics.add_morphism_tactic.
 
@@ -529,9 +526,9 @@ Lemma join_use_metric (D : data) (a' b' : symb) :
         a' \notin reps D -> b' \in reps D -> a' != b' ->
           metric (join_use D a' b') = (metric D) + size (use D a').
 Proof.
-rewrite /join_use;  move E: (use D a')=>old_use.
+rewrite /join_use; move E: (use D a')=>old_use.
 elim: old_use D E=>[|[[c c1] c2] old_use IH] D E H1 H2 H3 /=; first by rewrite addn0.
-move: (mem_split_uniq H2 (uniq_reps D))=>[s1 [s2 [L1 [L2 L3]]]].
+move: (mem_split_uniq H2 (uniq_reps D))=>[s1][s2][L1 L2 L3].
 have L4 : undup (map (rep D) (enum predT)) = reps D by [].
 case: (fnd _ _)=>[[[d d1] d2]|]; last first.
 - rewrite IH //=; last by rewrite ffunE eq_refl E.

examples/cyclic.v

@@ -1,9 +1,9 @@
 From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype seq ssrnat.
-From fcsl Require Import options axioms pred.
-From fcsl Require Import pcm unionmap heap automap autopcm.
-From HTT Require Import interlude model heapauto.
-From HTT Require Import llist.
+From pcm Require Import options axioms pred.
+From pcm Require Import pcm unionmap heap automap autopcm.
+From htt Require Import options interlude model heapauto.
+From htt Require Import llist.
 
 (* a queue variant that has a fixed capacity and can overwrite data in a circular way *)
 

examples/dlist.v

@@ -1,9 +1,9 @@
 
 From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq.
-From fcsl Require Import axioms pred.
-From fcsl Require Import pcm unionmap heap autopcm.
-From HTT Require Import options model heapauto.
+From pcm Require Import options axioms pred.
+From pcm Require Import pcm unionmap heap autopcm.
+From htt Require Import options model heapauto.
 
 (* Doubly linked lists, follows the same structure as singly-linked *)
 (* ones, adding a second pointer pointing backwards. *)