Mathcomp 2.x

.github/workflows/docker-action.yml

@@ -17,12 +17,9 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.19.0-coq-8.20'
-          - 'mathcomp/mathcomp:1.19.0-coq-8.19'
-          - 'mathcomp/mathcomp:1.18.0-coq-8.18'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.15'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.20'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.18'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3

README.md

@@ -34,9 +34,9 @@ The book was previously called "Functional Algorithms Verified", hence the FAV a
 - Coq-community maintainer(s):
   - Alex Gryzlov ([**@clayrat**](https://github.com/clayrat))
 - License: [MIT license](LICENSE)
-- Compatible Coq versions: 8.15 to 8.19
+- Compatible Coq versions: 8.18 to 8.20
 - Additional dependencies:
-  - [MathComp ssreflect](https://math-comp.github.io) 1.17.0 to 1.19.0
+  - [MathComp ssreflect](https://math-comp.github.io) 2.3
   - [MathComp algebra](https://math-comp.github.io)
   - [Equations](https://github.com/mattam82/Coq-Equations) 1.3 or later
 - Coq namespace: `favssr`

coq-fav-ssr.opam

@@ -19,8 +19,8 @@ The book was previously called "Functional Algorithms Verified", hence the FAV a
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.15" & < "8.21"}
-  "coq-mathcomp-ssreflect" {>= "1.17" & < "2.0"}
+  "coq" {>= "8.18" & < "8.21"}
+  "coq-mathcomp-ssreflect" {>= "2.3" & < "2.4"}
   "coq-mathcomp-algebra" 
   "coq-equations" {>= "1.3"}
 ]

meta.yml

@@ -32,27 +32,23 @@ license:
   identifier: MIT
 
 supported_coq_versions:
-  text: 8.15 to 8.20
-  opam: '{>= "8.15" & < "8.21"}'
+  text: 8.18 to 8.20
+  opam: '{>= "8.18" & < "8.21"}'
 
 tested_coq_opam_versions:
-- version: '1.19.0-coq-8.19'
+- version: '2.3.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
-- version: '1.18.0-coq-8.18'
+- version: '2.3.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.15'
+- version: '2.3.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{>= "1.17" & < "2.0"}'
+    version: '{>= "2.3" & < "2.4"}'
   description: |-
-    [MathComp ssreflect](https://math-comp.github.io) 1.17.0 to 1.19.0
+    [MathComp ssreflect](https://math-comp.github.io) 2.3.0
 - opam:
     name: coq-mathcomp-algebra
   description: |-

src/adt.v

@@ -37,7 +37,7 @@ Structure ASetM (T : eqType): Type :=
 End ASetM.
 
 Section Specification.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Corollary inorder_empty_pred : inorder (@Leaf T) =i pred0.
 Proof. by []. Qed.
@@ -187,7 +187,7 @@ End ASetI.
 (* Exercise 6.3 *)
 
 Section MapUnbalanced.
-Context {disp : unit} {K : orderType disp} {V : Type}.
+Context {disp : Order.disp_t} {K : orderType disp} {V : Type}.
 
 Notation kvtree := (tree (K*V)).
 

src/avl.v

@@ -1,5 +1,6 @@
 From Equations Require Import Equations.
 From Coq Require Import ssreflect ssrbool ssrfun.
+From HB Require Import structures.
 From mathcomp Require Import eqtype ssrnat ssrint ssralg ssrnum order seq path.
 From favssr Require Import prelude bintree bst adt.
 Set Implicit Arguments.
@@ -149,15 +150,15 @@ Lemma fib_bound n : phi ^+ n <= (fib (n + 2)) %:R.
 Proof.
 funelim (fib n); simp fib=>//.
 - rewrite add0n; simp fib=>//; rewrite addn0 expr1 addn1 /phi.
-  rewrite -(@ler_pmul2r _ 2%:R) // mulfVK; last by rewrite pnatr_eq0.
-  rewrite -natrM (_ : (2*2 = 1+3)%N) // natrD mulr1n ler_add2l.
-  rewrite -(@ler_pexpn2r _ 2) //; first last.
+  rewrite -(@ler_pM2r _ 2%:R) // mulfVK; last by rewrite pnatr_eq0.
+  rewrite -natrM (_ : (2*2 = 1+3)%N) // natrD mulr1n lerD2l.
+  rewrite -(@ler_pXn2r _ 2) //; first last.
   - by rewrite nnegrE.
   - by rewrite nnegrE sqrtC_ge0; apply: ler0n.
   by rewrite sqrtCK expr2 -natrM ler_nat.
 rewrite -addn2 (addn2 (n + 2)); simp fib.
 rewrite exprD phi_sq mulrDr mulr1 natrD.
-by apply: ler_add=>//; move: H; rewrite exprD expr1 -!addnA.
+by apply: lerD=>//; move: H; rewrite exprD expr1 -!addnA.
 Qed.
 
 Corollary height_bound (t : tree_ht A) : avl t -> phi ^+ (height t) <= (size1_tree t)%:R.
@@ -174,7 +175,7 @@ Qed.
 End LogarithmicHeight.
 
 Section SetImplementation.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 (* rebalancing *)
 
@@ -741,7 +742,7 @@ Admitted.
 End Exercises.
 
 Section Optimization.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Variant bal := Lh | Bal | Rh.
 
@@ -756,8 +757,7 @@ Definition eqbal (b1 b2 : bal) :=
 Lemma eqbalP : Equality.axiom eqbal.
 Proof. by move; case; case; constructor. Qed.
 
-Canonical bal_eqMixin := EqMixin eqbalP.
-Canonical bal_eqType := Eval hnf in EqType bal bal_eqMixin.
+HB.instance Definition _ := hasDecEq.Build bal eqbalP.
 
 Definition tree_bal A := tree (A * bal).
 
@@ -1135,7 +1135,7 @@ Admitted.
 
 (* Exercise 9.7 *)
 
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Inductive tree4 A := Leaf
                    | Lh4 of (tree4 A) & A & (tree4 A)

src/beyond.v

@@ -13,7 +13,7 @@ Open Scope order_scope.
 
 (* TODO switch to packed structures to reuse ASetM *)
 Module ASetM2.
-Structure ASetM2 (disp : unit) (T : orderType disp): Type :=
+Structure ASetM2 (disp : Order.disp_t) (T : orderType disp): Type :=
   make {tp :> Type;
         empty : tp;
         insert : T -> tp -> tp;
@@ -54,7 +54,7 @@ Structure ASetM2 (disp : unit) (T : orderType disp): Type :=
 End ASetM2.
 
 (* TODO use a canonical structure? *)
-Structure JoinSig (disp : unit) (X : orderType disp) (Y : Type) : Type :=
+Structure JoinSig (disp : Order.disp_t) (X : orderType disp) (Y : Type) : Type :=
   mkjoin {
     join : tree (X*Y) -> X -> tree (X*Y) -> tree (X*Y);
     inv : tree (X*Y) -> bool;
@@ -70,7 +70,7 @@ Structure JoinSig (disp : unit) (X : orderType disp) (Y : Type) : Type :=
 }.
 
 Section JustJoin.
-Context {disp : unit} {X : orderType disp} {Y : Type} {j : JoinSig X Y}.
+Context {disp : Order.disp_t} {X : orderType disp} {Y : Type} {j : JoinSig X Y}.
 
 Fixpoint split (t : tree (X*Y)) (x : X) : (tree (X*Y) * bool * tree (X*Y)) :=
   if t is Node l (a,_) r then
@@ -465,7 +465,7 @@ Admitted.
 End JustJoin.
 
 Section JoiningRedBlackTrees.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Lemma ne_bhgt (t1 t2 : rbt T) : non_empty_if (bh t1 < bh t2)%N t2.
 Proof.
@@ -773,7 +773,7 @@ Definition JoinRBT :=
 End JoiningRedBlackTrees.
 
 Section RBTSetJoin.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Definition invariant' (t : rbt T) := bst_list_a t && invch t.
 
@@ -888,7 +888,7 @@ End RBTSetJoin.
 From favssr Require Import twothree.
 
 Section Joining23Trees.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Equations? join23L (l : tree23 T) (x : T) (r : tree23 T) : upI T by wf (size23 r) lt :=
 join23L l x r => TI l. (* FIXME *)

src/binom_heap.v

@@ -1,5 +1,6 @@
 From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype order seq path bigop prime binomial.
+From HB Require Import structures.
 From favssr Require Import prelude basics priority.
 
 Set Implicit Arguments.
@@ -68,8 +69,7 @@ rewrite {}H12; case: H2.
 by move=>H12; apply: ReflectF; case=>E; rewrite E in H12.
 Qed.
 
-Canonical tree_eqMixin := EqMixin eqtreeP.
-Canonical tree_eqType := Eval hnf in EqType (tree A) tree_eqMixin.
+HB.instance Definition _ := hasDecEq.Build (tree A) eqtreeP.
 
 Lemma tree_ind_eq (P : tree A -> Prop) :
   (forall r a l, (forall x, x \in l -> P x) -> P (Node r a l)) ->
@@ -83,7 +83,7 @@ Qed.
 End TreeEq.
 
 Section TreeOrd.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Fixpoint invar_btree (t : tree T) : bool :=
   let: Node r _ ts := t in
@@ -116,7 +116,7 @@ Qed.
 End TreeOrd.
 
 Section Size.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Fixpoint mset_tree (t : tree T) : seq T :=
   let: Node _ a ts := t in
@@ -226,7 +226,7 @@ Qed.
 End Size.
 
 Section PriorityQueueImplementation.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 (* insert *)
 
@@ -431,7 +431,7 @@ elim: h t=>/=.
 - move=>t Ht _ _; rewrite mset_heap_nil in_nil orbF=>Hx.
   by apply: invar_tree_root_min.
 move=>t1 ts IH t Ht _.
-rewrite invar_cons; case/and3P=>Ht1 Ha1 Hs; rewrite le_minl; case/orP.
+rewrite invar_cons; case/and3P=>Ht1 Ha1 Hs; rewrite ge_min; case/orP.
 - by move=>Hx; rewrite invar_tree_root_min.
 rewrite mset_heap_cons mem_cat=>Hx.
 by rewrite IH // orbT.
@@ -597,7 +597,7 @@ Definition BHeapPQM :=
 End PriorityQueueImplementation.
 
 Section RunningTimeAnalysis.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Definition T_link (t1 t2 : tree T) : nat := 1.
 
@@ -749,7 +749,7 @@ Qed.
 End RunningTimeAnalysis.
 
 Section Exercises.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 (* Exercise 17.1 *)
 

src/bintree.v

@@ -1,5 +1,6 @@
 From Equations Require Import Equations.
 From Coq Require Import ssreflect ssrbool ssrfun.
+From HB Require Import structures.
 From mathcomp Require Import eqtype ssrnat seq prime.
 From favssr Require Import prelude.
 Set Implicit Arguments.
@@ -130,7 +131,7 @@
 
 (* Exercise 4.1 *)
 
 Fixpoint inorder2 (t : tree A) (acc : seq A) : seq A := [::]. (* FIXME *)
 
 Lemma inorder2_correct t xs : inorder2 t xs = inorder t ++ xs.
 Proof.
@@ -157,8 +158,10 @@
 by case=><-<-; split; [apply/IHl|apply/IHr].
 Qed.
 
-Canonical tree_eqMixin := EqMixin eqtreeP.
-Canonical tree_eqType := Eval hnf in EqType (tree T) tree_eqMixin.
+HB.instance Definition _ := hasDecEq.Build (tree T) eqtreeP.
+
+(* Canonical tree_eqMixin := EqMixin eqtreeP.
+Canonical tree_eqType := Eval hnf in EqType (tree T) tree_eqMixin. *)
 
 Lemma perm_pre_in (t : tree T) : perm_eq (inorder t) (preorder t).
 Proof.
@@ -267,7 +270,7 @@
 
 (* Exercise 4.2 *)
 
 Fixpoint mcs (t : tree A) : tree A := t. (* FIXME *)
 
 Lemma complete_mcs t : complete (mcs t).
 Proof.
@@ -470,7 +473,7 @@
 
 (* Exercise 4.3 *)
 
 Fixpoint acomplete_rec (t : tree A) : bool :=
   if t is Node l x r then
     false (* FIXME *)
   else true.
@@ -609,13 +612,13 @@
 
 (* Exercise 4.6 *)
 
-Context {disp : unit} {P : orderType disp}.
+Context {disp : Order.disp_t} {P : orderType disp}.
 Variable (x0 : P) (lmin : left_id x0 Order.max).
 
 Lemma rmin : right_id x0 Order.max.
 Proof. by move=>x; rewrite maxC lmin. Qed.
 
-Canonical max_monoid := Monoid.Law maxA lmin rmin.
+HB.instance Definition _ := Monoid.isLaw.Build P x0 Order.max maxA lmin rmin.
 
 Definition max_seq (xs : seq P) : P :=
   \big[Order.max/x0]_(x<-xs) x.
@@ -626,7 +629,7 @@
 Definition node_mx (l : tree (P*P)) (a : P) (r : tree (P*P)) : tree (P*P) :=
   @Leaf (P*P).   (* FIXME *)
 
 Fixpoint invar_mx (t : tree (P*P)) : bool :=
   true.  (* FIXME *)
 
 Lemma max_invar t :

src/braun_queue.v

@@ -12,7 +12,7 @@ Import Order.TotalTheory.
 Open Scope order_scope.
 
 Section Implementation.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Fixpoint insert (a : T) (t : tree T) : tree T :=
   if t is Node l x r then
@@ -59,7 +59,7 @@ Definition del_min (t : tree T) : tree T :=
 End Implementation.
 
 Section Correctness.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Lemma size_insert (x : T) t : size_tree (insert x t) = size_tree t + 1.
 Proof.