update to fcsl-pcm 1.6

.github/workflows/docker-action.yml

@@ -18,7 +18,7 @@ jobs:
  matrix:
  image:
  - 'mathcomp/mathcomp:1.13.0-coq-8.14'
- - 'mathcomp/mathcomp:1.15.0-coq-8.15'
+ - 'mathcomp/mathcomp:1.15.0-coq-8.16'
  - 'mathcomp/mathcomp-dev:coq-dev'
  fail-fast: false
  steps:

README.md

@@ -38,10 +38,10 @@ that HTT implements Separation logic as a shallow embedding in Coq.
  - Germán Andrés Delbianco
  - Alexander Gryzlov
 - License: [Apache-2.0](LICENSE)
-- Compatible Coq versions: Coq 8.14 to 8.15
+- Compatible Coq versions: Coq 8.14 to 8.16
 - Additional dependencies:
  - [MathComp ssreflect 1.13 to 1.15](https://math-comp.github.io)
- - [FCSL-PCM 1.5](https://github.com/imdea-software/fcsl-pcm)
+ - [FCSL-PCM 1.6](https://github.com/imdea-software/fcsl-pcm)
 - 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)

coq-htt.opam

@@ -34,9 +34,9 @@ that HTT implements Separation logic as a shallow embedding in Coq."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
- "coq" { (>= "8.14" & < "8.16~") | (= "dev") }
+ "coq" { (>= "8.14" & < "8.17~") | (= "dev") }
  "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.16~") | (= "dev") }
- "coq-fcsl-pcm" { (>= "1.5.0" & < "1.6~") | (= "dev") }
+ "coq-fcsl-pcm" { (>= "1.6.0" & < "1.7~") | (= "dev") }
 ]
 
 tags: [

core/interlude.v

@@ -1,6 +1,6 @@
 From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat seq eqtype path.
-From fcsl Require Import options axioms ordtype.
+From fcsl Require Import options prelude ordtype.
 
 Lemma rcons_nseq {A} n (x : A) :
  rcons (nseq n x) x = nseq n.+1 x.
@@ -63,18 +63,6 @@ Lemma path_all {S} (xs : seq S) x r :
  path r x xs -> all (r x) xs.
 Proof. by move=>Ht; rewrite path_sortedE; [case/andP | exact: Ht]. Qed.
 
-(* remove after fcsl-pcm update *)
-Lemma iffPb (b1 b2 : bool) : reflect (b1 <-> b2) (b1 == b2).
-Proof.
-case: eqP=>[->|N]; constructor=>//.
-case: b1 b2 N; case=>//= _.
-- by case=>/(_ erefl).
-by case=>_ /(_ erefl).
-Qed.
-
-Lemma iffE (b1 b2 : bool) : b1 = b2 <-> (b1 <-> b2).
-Proof. by split=>[->|] //; move/iffPb/eqP. Qed.
-
 Lemma all_notin {A : eqType} (p : pred A) xs y :
  all p xs -> ~~ p y -> y \notin xs.
 Proof. by move/allP=>Ha; apply/contra/Ha. Qed.
@@ -101,4 +89,4 @@ apply/iffE; split.
 case/andP=>/= + H; rewrite cats1.
 case: l=>//=a l; rewrite rcons_path=>/andP [H1 H2].
 by rewrite cat_path /= H1 H2.
-Qed.
+Qed.

examples/array.v

@@ -1,13 +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 options axioms prelude pred.
 From fcsl Require Import pcm unionmap heap.
 From HTT Require Import model heapauto.
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-Set Bullet Behavior "None".
-Obligation Tactic := auto.
 
 Definition indx {I : finType} (x : I) := index x (enum I).
 

examples/bintree.v

@@ -1,14 +1,10 @@
 
 From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype seq ssrnat.
-From fcsl Require Import axioms pred.
+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.
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-Obligation Tactic := auto.
 
 (* Binary tree specification *)
 
@@ -139,7 +135,7 @@ Program Definition treesize p :
  in len (p, 0)).
 Next Obligation.
 (* pull out ghost var + precondition, branch on null check *)
-move=>_ go _ p s /= _ [t][] i /= H; case: eqP H=>[{p}->|/eqP Ep] H.
+move=>_ go _ p s /= [t][] i /= H; case: eqP H=>[{p}->|/eqP Ep] H.
 - (* empty tree has size 0 *)
  by step=>V; case: (shape_null V H)=>->->/=; rewrite addn0.
 (* non-null pointer is a node, deconstruct it, read branch pointers *)
@@ -183,7 +179,7 @@ Program Definition inordertrav p :
  loop (p, n)).
 Next Obligation.
 (* pull out ghosts + precondition, deconstruct the heap, branch on null check *)
-move=>_ go _ p s _ /= [t][xs][] _ /= [h1][h2][-> H1 H2].
+move=>_ go _ p s /= [t][xs][] _ /= [h1][h2][-> H1 H2].
 case: eqP H1=>[{p}->|/eqP Ep] H1.
 - (* return the accumulated list - empty tree has no values *)
  by step=>V; case: (shape_null (validL V) H1)=>->->/=; vauto.

examples/bst.v

@@ -1,13 +1,9 @@
 From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype ssrnat seq path.
-From fcsl Require Import axioms pred ordtype.
+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.
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-Obligation Tactic := auto.
 
 Section BST.
 Context {T : ordType}.

examples/cyclic.v

@@ -1,13 +1,9 @@
 From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype seq ssrnat.
-From fcsl Require Import axioms pred.
+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.
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-Obligation Tactic := auto.
 
 (* a queue variant that has a fixed capacity and can overwrite data in a circular way *)
 
@@ -84,7 +80,7 @@ Program Definition new (n : nat) (init : T) :
 (* first the loop *)
 Next Obligation.
 (* pull out the ghost (the initial node) + preconditions, match on k *)
-move=>n init go [r k] _ _[->->][q []] i /= [Hk H]; case: ltnP=>Hk1.
+move=>n init go _ r k [q][] i /= [Hk H]; case: ltnP=>Hk1.
 - (* k < n.-1, allocate new node *)
  step=>p'; step; rewrite unitR.
  (* do the recursive call, both preconditions hold *)
@@ -283,7 +279,7 @@ Program Definition free (b : buffer) :
 (* first the loop *)
 Next Obligation.
 (* pull out ghosts, destructure the preconditions, match on k *)
-move=>b go [r k][_ _][->->][q][xs][] h /= [H Hs]; case: ltnP.
+move=>b go _ r k [q][xs][] h /= [H Hs]; case: ltnP.
 - (* k < capacity, so the spec is still non-empty *)
  move=>Hk; have {Hk}Hxs: 0 < size xs by rewrite Hs subn_gt0.
  (* unroll the heap *)

examples/dlist.v

@@ -1,13 +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 options axioms pred.
 From fcsl Require Import pcm unionmap heap autopcm.
 From HTT Require Import model heapauto.
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-Obligation Tactic := auto.
 
 (* Doubly linked lists, follows the same structure as singly-linked *)
 (* ones, adding a second pointer pointing backwards. *)
@@ -229,11 +225,11 @@ Program Definition traverse_back p q :
 (* first, the loop *)
 Next Obligation.
 (* pull out ghosts + precondition, branch *)
-move=>p _ go [r acc] _ _ [->->][l][nx][] i /= H; case: ifP H=>[/eqP->|/negbT].
+move=>p _ go _ r acc [l][nx][] i /= H; case: ifP H=>[/eqP->|/negbT].
 - (* remainder is empty, return accumulator *)
  by move/dseg_nullR=>H; step=>/H [->_->->].
 (* deconstruct non-empty remainder *)
-rewrite eq_sym=>Hr /(dseg_neqR Hr) [xs][x][z][h'][{l}-> {i}-> H'].
+rewrite eq_sym=>Hr /(dseg_neqR Hr) [xs][x][z][h'][{l}-> {i}-> H']{Hr}.
 (* run the rest, feed remainder, acc pointer and subheap to recursive call *)
 do 2!step; apply: [gX xs, r]@h'=>//= _ m [Hm ->] _ /=.
 (* simplify and restructure the goal *)

examples/gcd.v

@@ -1,11 +1,7 @@
 From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype div.
-From fcsl Require Import axioms pred pcm heap.
+From fcsl Require Import options axioms pred pcm heap.
 From HTT Require Import model heapauto.
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-Obligation Tactic := auto.
 
 (* classical mutable Euclid's algorithm for computing GCD with subtractions *)
 

examples/hashtab.v

@@ -1,13 +1,9 @@
 From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq fintype tuple finfun finset.
-From fcsl Require Import axioms prelude pred ordtype finmap.
+From fcsl Require Import options axioms prelude pred ordtype finmap.
 From fcsl Require Import pcm unionmap heap autopcm.
 From HTT Require Import model heapauto.
 From HTT Require Import array kvmaps.
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-Obligation Tactic := auto.
 
 Module HashTab.
 Section HashTab.

examples/kvmaps.v

@@ -4,13 +4,9 @@
 
 From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype seq path.
-From fcsl Require Import axioms pred ordtype finmap.
+From fcsl Require Import options axioms pred ordtype finmap.
 From fcsl Require Import pcm unionmap heap autopcm automap.
 From HTT Require Import interlude model heapauto.
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-Obligation Tactic := auto.
 
 (***********************)
 (* stateful KV map ADT *)
@@ -293,7 +289,7 @@ Program Definition remove x (k : K) :
 (* we don't return the pointer because it cannot change, as the head is fixed by fml *)
 Next Obligation.
 (* pull out ghost var, preconditions and heap validity *)
-move=>x k0 go _ prev cur _ [_][] _ /= [fml][fmr][k][v][-> [Ol Or][El E]][hl][_][-> Hl [_][hr][->->Hr]].
+move=>x k0 go _ prev cur [_][] _ /= [fml][fmr][k][v][-> [Ol Or][El E]][hl][_][-> Hl [_][hr][->->Hr]].
 (* branch on cur *)
 case: eqP=>[|/eqP] Ec.
 (* cur = null - nothing to left to process, i.e., fmr = [] *)
@@ -448,7 +444,7 @@ Program Definition insert x (k : K) (v : V) :
 (* we don't return the pointer because it cannot change, as the head is fixed by fml *)
 Next Obligation.
 (* pull out ghost var+preconditions *)
-move=>x k0 v0 loop _ prev cur _ [_][] _ /= [fml][fmr][k][v][-> [Ol Or][El Ho0]][hl][_][-> Hl [_][hr][->-> Hr]].
+move=>x k0 v0 loop _ prev cur [_][] _ /= [fml][fmr][k][v][-> [Ol Or][El Ho0]][hl][_][-> Hl [_][hr][->-> Hr]].
 (* branch on cur *)
 case: eqP=>[|/eqP] Ec.
 - (* cur = null, insert as the last element *)

examples/llist.v

@@ -1,12 +1,8 @@
 
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
-From fcsl Require Import axioms pred.
+From fcsl Require Import options axioms pred.
 From fcsl Require Import pcm unionmap heap autopcm automap.
 From HTT Require Import model heapauto.
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-Obligation Tactic := auto.
 
 (* Linked lists, storing a value and next pointer in consecutive locations. *)
 (* We start with a more general "segment" definition, where the last node's *)
@@ -233,7 +229,7 @@ Program Definition len p :
 (* first, the loop *)
 Next Obligation.
 (* pull out ghosts+precondition, branch *)
-move=>_ go _ p l /= _ [xs][] i /= H; case: eqP H=>[->|/eqP Ep] H.
+move=>_ go _ p l /= [xs][] i /= H; case: eqP H=>[->|/eqP Ep] H.
 - (* the end is reached *)
  by step=>V; case/(lseq_null V): H=>->->/=; rewrite addn0.
 (* deconstruct non-empty list, run one step *)
@@ -321,7 +317,7 @@ Program Definition reverse p :
 (* first, the loop *)
 Next Obligation.
 (* pull out ghosts + preconditions, branch *)
-move=>_ go _ i done _ [x1][x2][] _ /= [i1][i2][-> H1 H2].
+move=>_ go _ i done [x1][x2][] _ /= [i1][i2][-> H1 H2].
 case: eqP H1=>[->|/eqP E] H1.
 - (* nothing left to reverse, return the accumulator *)
  by step=>/validL V1; case/(lseq_null V1): H1=>->->/=; rewrite unitL.

examples/queue.v

@@ -1,13 +1,9 @@
 From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype seq.
-From fcsl Require Import axioms pred.
+From fcsl Require Import options axioms pred.
 From fcsl Require Import pcm unionmap heap automap.
 From HTT Require Import model heapauto.
 From HTT Require Import llist.
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-Obligation Tactic := auto.
 
 Record queue (T : Type) : Type := Queue {front: ptr; back: ptr}.
 Definition EmptyQueue : exn := exn_from_nat 100.

examples/stack.v

@@ -1,13 +1,9 @@
 From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype seq.
-From fcsl Require Import axioms pred.
+From fcsl Require Import options axioms pred.
 From fcsl Require Import pcm unionmap heap autopcm.
 From HTT Require Import model heapauto.
 From HTT Require Import llist.
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-Obligation Tactic := auto.
 
 Definition stack (T : Type) := ptr.
 Definition EmptyStack := exn_from_nat 25.

meta.yml

@@ -55,13 +55,13 @@ license:
  file: LICENSE
 
 supported_coq_versions:
- text: Coq 8.14 to 8.15
- opam: '{ (>= "8.14" & < "8.16~") | (= "dev") }'
+ text: Coq 8.14 to 8.16
+ opam: '{ (>= "8.14" & < "8.17~") | (= "dev") }'
 
 tested_coq_opam_versions:
 - version: '1.13.0-coq-8.14'
  repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.15'
+- version: '1.15.0-coq-8.16'
  repo: 'mathcomp/mathcomp'
 - version: 'coq-dev'
  repo: 'mathcomp/mathcomp-dev'
@@ -74,9 +74,9 @@ dependencies:
  [MathComp ssreflect 1.13 to 1.15](https://math-comp.github.io)
 - opam:
  name: coq-fcsl-pcm
- version: '{ (>= "1.5.0" & < "1.6~") | (= "dev") }'
+ version: '{ (>= "1.6.0" & < "1.7~") | (= "dev") }'
  description: |-
- [FCSL-PCM 1.5](https://github.com/imdea-software/fcsl-pcm)
+ [FCSL-PCM 1.6](https://github.com/imdea-software/fcsl-pcm)
 
 namespace: HTT