Adapt to math-comp/math-comp#1545 (#58)

* Adapt to math-comp/math-comp#1545

* added testing image 2.5.0-rocq-prover-9.1

* added docker image 2.5.0-rocq-prover-9.1

* adding docker image 2.5.0-rocq-prover-9.1

* adding docker image 2.5.0-rocq-prover-9.1

* adding docker image 2.5.0-rocq-prover-9.1

* relaxing hb bound

Author: aleksnanevski

.github/workflows/docker-action.yml

@@ -9,6 +9,7 @@ on:
   pull_request:
     branches:
       - '**'
+  workflow_dispatch:
 
 jobs:
   build:
@@ -18,6 +19,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

@@ -29,12 +29,12 @@ This library relies on propositional and functional extentionality axioms.
   - Anton Trunov
   - Alexander Gryzlov
 - License: [Apache-2.0](LICENSE)
-- Compatible Coq versions: 9.0 or later
+- Compatible Rocq/Coq versions: 9.0 or later
 - Additional dependencies:
   - [MathComp ssreflect 2.4 or later](https://math-comp.github.io)
   - [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder)
   - [MathComp algebra](https://math-comp.github.io)
-- Coq namespace: `pcm`
+- Rocq/Coq namespace: `pcm`
 - Related publication(s): none
 
 ## Building and installation instructions
@@ -43,15 +43,19 @@ The easiest way to install the latest released version of The PCM library
 is via [OPAM](https://opam.ocaml.org/doc/Install.html):
 
 ```shell
-opam repo add coq-released https://coq.inria.fr/opam/released
+opam repo add rocq-released https://rocq-prover.org/opam/released
 opam install coq-fcsl-pcm
 ```
 
-To instead build and install manually, do:
+To instead build and install manually, you need to make sure that all the
+libraries this development depends on are installed.  The easiest way to do that
+is still to rely on opam:
 
 ``` shell
 git clone https://github.com/imdea-software/fcsl-pcm.git
 cd fcsl-pcm
+opam repo add rocq-released https://rocq-prover.org/opam/released
+opam install --deps-only .
 make   # or make -j <number-of-cores-on-your-machine> 
 make install
 ```

coq-fcsl-pcm.opam

@@ -25,9 +25,9 @@ This library relies on propositional and functional extentionality axioms."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "9.0" & < "9.1~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.5~") | (= "dev") }
-  "coq-hierarchy-builder" { (>= "1.7.0" & < "1.10~") | (= "dev") }
+  "coq" { (>= "9.0" & < "9.2~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") }
+  "coq-hierarchy-builder" { (>= "1.7.0" & < "1.11~") | (= "dev") }
   "coq-mathcomp-algebra" 
 ]
 

core/finmap.v

@@ -22,6 +22,9 @@ From mathcomp Require Import ssrnat eqtype seq path.
 From pcm Require Export ordtype seqperm.
 From pcm Require Import options.
 
+(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Set SsrOldRewriteGoalsOrder.  
+
 Section Def.
 Variables (K : ordType) (V : Type).
 
@@ -416,7 +419,7 @@ case: (ordP k2 k3)=>H2 /=.
 - rewrite eq_sym H1 /=.
   case: (ordP k3 k1)=>H3 /=; case: (ordP k2 k3) (H2)=>//=.
   rewrite -(eqP H3) in H1 *.
-  rewrite -IH //; first by apply: path_sorted H.
+  rewrite -IH //; last by apply: path_sorted H.
   rewrite last_ins' /= 1?eq_sym ?H1 //.
   by apply: ord_path H.
 - by move: H1; rewrite (eqP H2) /= eq_sym => -> /=; rewrite irr eq_refl.
@@ -520,9 +523,9 @@ Lemma fmap_ind' (P : fmap -> Prop) :
         forall s, P s.
 Proof.
 move=>H1 H2; case; elim=>[|[k v] s IH] /= H.
-- by rewrite (_ : FinMap _ = nil); first by rewrite fmapE.
+- by rewrite (_ : FinMap _ = nil); last by rewrite fmapE.
 have S: sorted ord (map key s) by apply: path_sorted H.
-rewrite (_ : FinMap _ = ins k v (FinMap S)). 
+rewrite (_ : FinMap _ = ins k v (FinMap S)); last first.
 - by rewrite fmapE /= last_ins'.
 by apply: H2.
 Qed.
@@ -534,7 +537,7 @@ Lemma fmap_ind'' (P : fmap -> Prop) :
         forall s, P s.
 Proof.
 move=>H1 H2; case; elim/last_ind=>[|s [k v] IH] /= H.
-- by rewrite (_ : FinMap _ = nil); first by rewrite fmapE.
+- by rewrite (_ : FinMap _ = nil); last by rewrite fmapE.
 have Sb: subseq (map key s) (map key (rcons s (k, v))).
 - by elim: s {IH H}=>[|x s IH] //=; rewrite eq_refl.
 have S : sorted ord (map key s).
@@ -544,7 +547,7 @@ have T : forall x : K, x \in map key s -> ord x k.
   rewrite inE; case/orP; last by apply: IH; apply: path_sorted L.
   move/eqP=>->; elim: s {IH} L=>[|[x1 w1] s IH] /=; first by rewrite andbT.
   by case/andP=>O /(ord_path O) /IH.
-rewrite (_ : FinMap _ = ins k v (FinMap S)).
+rewrite (_ : FinMap _ = ins k v (FinMap S)); last first.
 - by rewrite fmapE /= first_ins'.
 by apply: H2 (IH _)=>x /T.
 Qed.
@@ -985,7 +988,7 @@ Lemma sorted_map_key (m : seq (K * U)) :
         sorted ord (map key m) -> sorted ord (map key (mapf' m)).
 Proof.
 elim: m=>[|[k v] m IH] //= H.
-rewrite path_min_sorted; last by apply: IH; apply: path_sorted H.
+rewrite path_min_sorted; first by apply: IH; apply: path_sorted H.
 rewrite map_key_mapf.
 by apply/(order_path_min _ H);apply/trans.
 Qed.
@@ -1099,7 +1102,7 @@ Lemma mapk_comp m:
 Proof.
 elim/fmap_ind': m  =>//= k v s P IH.
 rewrite [mapk (g \o f) _]mapk_ins //.
-rewrite mapk_ins // mapk_ins //; last by rewrite IH.
+rewrite mapk_ins // mapk_ins //; first by rewrite IH.
 exact: (path_mapk Hf P).
 Qed.
 End KeyMap.

core/pred.v

@@ -19,8 +19,10 @@ From Stdlib Require Import ssreflect ssrbool ssrfun Setoid Basics.
 From mathcomp Require Import ssrnat seq eqtype bigop.
 From pcm Require Import options.
 
-(* First some basic propositional equalities *)
+(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Set SsrOldRewriteGoalsOrder.  
 
+(* First some basic propositional equalities *)
 
 Lemma andTp p : True /\ p <-> p.      Proof. by intuition. Qed.
 Lemma andpT p : p /\ True <-> p.      Proof. by intuition. Qed.
@@ -867,7 +869,7 @@ Lemma eq_In_filter (T : Type) a1 a2 (s : seq T) :
         filter a1 s = filter a2 s.
 Proof.
 elim: s => //= x s IHs eq_a.
-rewrite eq_a; first by rewrite InE; left.
+rewrite eq_a; last by rewrite InE; left.
 rewrite IHs // => y s_y; apply: eq_a.
 by rewrite InE; right.
 Qed.

core/prelude.v

@@ -23,6 +23,9 @@ From mathcomp Require Import path fintype finset finfun tuple perm fingroup.
 From mathcomp Require Import ssralg.
 From pcm Require Import options axioms.
 
+(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Set SsrOldRewriteGoalsOrder.  
+
 (***********)
 (* Prelude *)
 (***********)
@@ -775,7 +778,7 @@ elim: (enum T) (enum_uniq T)=>[|x xs IH] //.
 set f := index^~(x :: xs)=>/= /andP [H1 H2].
 rewrite {1}/f /= eqxx; congr (0 :: _).
 case: (eq_in_map f (fun x=>(index x xs).+1) xs)=>E _. 
-rewrite E.
+rewrite E; last first.
 - by move=>z R; rewrite /f /=; case: (x =P z) R H1=>//= ->->.
 by rewrite -add1n iotaDl -IH // -map_comp. 
 Qed.

core/seqext.v

@@ -15,6 +15,9 @@ From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat seq eqtype path choice fintype bigop perm.
 From pcm Require Import options prelude pred seqperm.
 
+(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Set SsrOldRewriteGoalsOrder.  
+
 (*********************)
 (* Extensions to seq *)
 (*********************)
@@ -83,9 +86,9 @@ Lemma drop_take_mask {A} (s : seq A) x y :
         drop x (take y s) = mask (nseq x false ++ nseq (y-x) true) s.
 Proof.
 case: (ltnP x (size s))=>Hx; last first.
-- rewrite drop_oversize; first by rewrite size_take_min geq_min Hx orbT.
-  rewrite -{1}(subnKC Hx) nseqD -catA -{3}(cats0 s) mask_cat.
-  - by rewrite size_nseq.
+- rewrite drop_oversize; last by rewrite size_take_min geq_min Hx orbT.
+  rewrite -{1}(subnKC Hx) nseqD -catA -{3}(cats0 s) mask_cat;
+    last by rewrite size_nseq.
   by rewrite mask0 mask_false.
 have Hx': size (nseq x false) = size (take x s).
 - by rewrite size_nseq size_take_min; symmetry; apply/minn_idPl/ltnW.
@@ -400,7 +403,7 @@ case: m=>/=[|b m]; first by rewrite in_nil nth_nil andbF.
 case: b; rewrite !inE eq_sym; case: eqP=>//= _.
 - by rewrite add0n; apply: IHs.
 - rewrite -{2}(addn0 1%N) leq_add2l leqn0 => /eqP Hc.
-  rewrite IHs; first by rewrite Hc.
+  rewrite IHs; last by rewrite Hc.
   by move/count_memPn/negbTE: Hc=>->.
 by rewrite add0n; apply: IHs.
 Qed.
@@ -728,8 +731,8 @@ case/boolP: (has p s2)=>H2; last first.
   by rewrite addnC subnDl.
 have H2' : find p (rev s2) < size s2.
 - by rewrite -size_rev -has_find has_rev.
-rewrite /= orbT andbF -addnBA; first by apply: ltnW.
-rewrite -!subn1 -subnDA -addnBA; first by rewrite subn_gt0.
+rewrite /= orbT andbF -addnBA; last by apply: ltnW.
+rewrite -!subn1 -subnDA -addnBA; last by rewrite subn_gt0.
 by rewrite subnDA.
 Qed.
 
@@ -757,7 +760,7 @@ Lemma nth_findlast x0 p s :
         p (nth x0 s (findlast p s)).
 Proof.
 rewrite findlastE=>/[dup] E ->; rewrite -has_rev in E.
-rewrite -subnS -nth_rev; first by rewrite -size_rev -has_find.
+rewrite -subnS -nth_rev; last by rewrite -size_rev -has_find.
 by apply: nth_find.
 Qed.
 
@@ -771,7 +774,7 @@ have Hh: 0 < size s - find p (rev s).
 rewrite -size_rev; move/(has_take (size s - i)): (E).
 rewrite take_rev -subnS size_rev.
 case/boolP: (i < size s)=>[Hi|].
-- rewrite subnA //; first by apply: ltnW.
+- rewrite subnA //; last by apply: ltnW.
   rewrite subnn add0n has_rev=>->.
   rewrite ltn_subRL addnC -ltn_subRL subnS.
   by case: (size s - find p (rev s)) Hh.
@@ -799,7 +802,7 @@ elim: s=>//= h s IH.
 rewrite rev_cons -cats1 find_cat has_rev size_rev /=.
 case/orP; first by move=>->.
 move=>/[dup] H ->; case: ifP=>_ //.
-rewrite subSn /=.
+rewrite subSn /=; last first.
 - by rewrite -size_rev; apply: find_size.
 apply: (leq_ltn_trans (IH H)); rewrite ltn_predL subn_gt0.
 by rewrite -size_rev -has_find has_rev.
@@ -814,7 +817,7 @@ Lemma split_findlast_nth x0 p s (i := findlast p s) :
         split_findlast_nth_spec p s (take i s) (drop i.+1 s) (nth x0 s i).
 Proof.
 move=> p_s; rewrite -[X in split_findlast_nth_spec _ X](cat_take_drop i s).
-rewrite (drop_nth x0 _); first by rewrite -has_findlast.
+rewrite (drop_nth x0 _); last by rewrite -has_findlast.
 rewrite -cat_rcons; constructor; first by apply: nth_findlast.
 by rewrite has_drop // ltnn.
 Qed.
@@ -1004,11 +1007,11 @@ Lemma findall_cat p s1 s2 :
         findall p (s1 ++ s2) =
         findall p s1 ++ map (fun n => size s1 + n) (findall p s2).
 Proof.
-rewrite !findallE size_cat iotaD add0n zip_cat; first by rewrite size_iota.
+rewrite !findallE size_cat iotaD add0n zip_cat; last by rewrite size_iota.
 rewrite filter_cat {1}/unzip1 map_cat; congr (_ ++ _).
 set n := size s1.
 rewrite -{1}(addn0 n) iotaDl zip_mapl filter_map -!map_comp.
-rewrite (eq_filter (a2:=(p \o snd))); first by case.
+rewrite (eq_filter (a2:=(p \o snd))); last by case.
 by apply: eq_map; case.
 Qed.
 
@@ -1258,8 +1261,8 @@ Lemma filter_sub (p1 p2 : pred A) (s : seq A) :
         subpred p1 p2 -> 
         {subset filter p1 s <= filter p2 s}.
 Proof.
-move=>S; rewrite (_ : filter p1 s = filter p1 (filter p2 s)); 
-  last by apply: mem_subseq; apply: filter_subseq.
+move=>S; rewrite (_ : filter p1 s = filter p1 (filter p2 s)).
+- by apply: mem_subseq; apply: filter_subseq.
 rewrite -filter_predI; apply: eq_in_filter=>x X /=.
 by case E : (p1 x)=>//=; rewrite (S _ E).
 Qed.

core/slice.v

@@ -18,6 +18,9 @@ From pcm Require Import options prelude seqext.
 Open Scope order_scope.
 Import Order.Theory.
 
+(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Set SsrOldRewriteGoalsOrder.  
+
 Section BSimp_Extension.
 Context disp (T : porderType disp).
 Implicit Types (x y : T) (b c : bool).
@@ -222,7 +225,7 @@ by exact: geq_minl.
 Qed.
 
 Corollary slice_usize s : s = &:s `]-oo, size s[.
-Proof. by rewrite itv_overR /=; [rewrite addn0|rewrite slice_uu]. Qed.
+Proof. by rewrite itv_overR /=; [rewrite slice_uu|rewrite addn0]. Qed.
 
 (* slice size *)
 
@@ -367,7 +370,7 @@ move: (onth_size H)=>Hk; case: l; case: r=>/=;
 rewrite ?addn0 ?addn1.
 - by apply: drop_oversize; rewrite size_take Hk.
 - rewrite -addn1 addnC -take_drop.
-  rewrite (take_nth v); first by rewrite size_drop subn_gt0.
+  rewrite (take_nth v); last by rewrite size_drop subn_gt0.
   by rewrite take0 /= nth_drop addn0 nth_onth H.
 - by apply: drop_oversize; rewrite size_take Hk.
 apply: drop_oversize; rewrite size_take; case: ifP=>// /negbT.
@@ -441,7 +444,7 @@ Lemma slice_xR a x s :
                     (&:s (Interval a +oo))
              (onth s x).
 Proof.
-move=>Hax; rewrite (slice_split _ true (x:=x)) /=.
+move=>Hax; rewrite (slice_split _ true (x:=x)) /=; last first.
 - rewrite in_itv /= lexx andbT.
   by case: a Hax=>/=[ax av|ax]; case: ax.
 rewrite slice_kk /=; case: (onth_sizeP s x)=>[|v] H;
@@ -457,7 +460,7 @@ Lemma slice_xL b x s :
                      [::]
              (onth s x).
 Proof.
-move=>Hxb; rewrite (slice_split _ false (x:=x)) /=.
+move=>Hxb; rewrite (slice_split _ false (x:=x)) /=; last first.
 - rewrite in_itv /= lexx /=.
   by case: b Hxb=>/=[bx bv|bx]; case: bx.
 rewrite slice_kk /=; case: (onth_sizeP s x)=>[|v] H; rewrite H //=.
@@ -556,7 +559,7 @@ Lemma slice_cat_piecewise s1 s2 i :
 Proof.
 rewrite slice_cat; case: i=>i j /=; case: ifP.
 - rewrite in_itv; case/andP=>Hi Hj.
-  rewrite (itv_overR _ (j:=j)).
+  rewrite (itv_overR _ (j:=j)); last first.
   - case: j Hj=>[[] j|[]] //=.
     - by rewrite addn0; move/ltnW.
     by rewrite addn1 leEnat; move/(ltnW (n:=j.+1)).
@@ -566,7 +569,7 @@ rewrite slice_cat; case: i=>i j /=; case: ifP.
   by rewrite ltnn /= subnn.
 rewrite in_itv=>/negbT; rewrite negb_and=>H.
 case: ifP=>Hj.
-- rewrite (itv_underR (s:=s2)); last by rewrite cats0.
+- rewrite (itv_underR (s:=s2)); first by rewrite cats0.
   case: {H}j Hj=>[[] j|[]] //=.
   - rewrite addn0 leEnat leq_eqVlt; case/orP=>[/eqP->|->] //=.
     by rewrite ltnn /= subnn.
@@ -678,10 +681,10 @@ move=>x Hx.
 have Hij : i1 <= j1.
 - apply: contraLR Hx; rewrite -ltNge=>/ltW Hji.
   by rewrite itv_swapped_bnd.
-rewrite (@slice_split_bnd _ _ _ i1) /=.
+rewrite (@slice_split_bnd _ _ _ i1) /=; last first.
 - by rewrite Hi /=; apply/le_trans/Hj.
 rewrite mem_cat; apply/orP; right.
-rewrite (@slice_split_bnd _ _ _ j1) /=.
+rewrite (@slice_split_bnd _ _ _ j1) /=; last first.
 - by rewrite Hj andbT.
 by rewrite mem_cat Hx.
 Qed.