start porting to MathComp 2

.github/workflows/docker-action.yml

@@ -17,18 +17,9 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.16.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.18'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.18'
-          - 'mathcomp/mathcomp:1.18.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.18.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.18.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

README.md

@@ -23,7 +23,7 @@ Mathematical Components library.
   - Cyril Cohen, Inria (initial)
   - Laurent Théry, Inria
 - License: [LGPL-2.1-or-later](LICENSE)
-- Compatible Coq versions: Coq 8.14 to Coq 8.18
+- Compatible Coq versions: Coq 8.18 to Coq 8.19
 - Additional dependencies:
   - [MathComp ssreflect](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)

angle.v

@@ -1,4 +1,5 @@
 (* coq-robot (c) 2017 AIST and INRIA. License: LGPL-2.1-or-later. *)
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrint.
 From mathcomp Require Import ssrnum rat poly closed_field polyrcf matrix.
 From mathcomp Require Import mxalgebra tuple mxpoly zmodp binomial realalg.
@@ -59,7 +60,7 @@
 have [->|n_gt0] := posnP n; first by rewrite muln0 root0C rootC0.
 have mn_gt0: (m * n > 0)%N by rewrite ?muln_gt0 ?m_gt0.
 wlog x_gt0 : x / x >= 0 => [hwlog_x_ge0|]; last first.
-  apply: (@pexpIrn _ (m * n)); rewrite // ?qualifE ?rootC_ge0 //.
+  apply: (@pexpIrn _ (m * n)) => //; rewrite ?nnegrE//= ?rootC_ge0 //.
   by rewrite rootCK // exprM !rootCK.
 wlog nx_eq1 : x / `|x| = 1 => [hwlog_nx_eq1|].
   have [->|x_neq0] := eqVneq x 0; first by rewrite !rootC0.
@@ -94,15 +95,15 @@
 Variable T : rcfType.
 
 Record angle := Angle {
-  expi : T[i];
+  expi :> T[i];
   _ : `| expi | == 1 }.
 
 Fact angle0_subproof : `| 1 / `| 1 | | == 1 :> T[i].
 Proof. by rewrite normr1 divr1 normr1. Qed.
 
 Definition angle0 := Angle angle0_subproof.
 
-Canonical angle_subType := [subType for expi].
+HB.instance Definition _ := [isSub for expi].
 
 Lemma normr_expi a : `|expi a| = 1.
 Proof. by case: a => x /= /eqP. Qed.
@@ -191,12 +192,10 @@
 by rewrite normrV ?expi_is_unit // normr_expi invr1.
 Qed.
 
-Definition angle_eqMixin := [eqMixin of angle by <:].
-Canonical angle_eqType := EqType angle angle_eqMixin.
-Definition angle_choiceMixin := [choiceMixin of angle by <:].
-Canonical angle_choiceType := ChoiceType angle angle_choiceMixin.
-Definition angle_ZmodMixin := ZmodMixin add_angleA add_angleC add_0angle add_Nangle.
-Canonical angle_ZmodType := ZmodType angle angle_ZmodMixin.
+HB.instance Definition _ := [Equality of angle by <:].
+HB.instance Definition _ := [Choice of angle by <:].
+HB.instance Definition _ :=
+  @GRing.isZmodule.Build angle _ opp_angle add_angle add_angleA add_angleC add_0angle add_Nangle.
 
 Lemma arg1 : arg 1 = 0.
 Proof. apply val_inj => /=; by rewrite argK // normr1. Qed.
@@ -917,24 +916,24 @@
   by rewrite normrM (eqP (norm_half_anglec (normr_expi _))) mulr1.
 rewrite /half_anglec. simpc. rewrite /=.
 case: ifPn => a0 /=.
-  rewrite mulrC -mulr2n -mulr_natl sqrtrM; last by rewrite subr_ge0 Im_half_anglec // normr_expi.
-  rewrite mulrAC sqrtrM; last by rewrite Re_half_anglec // normr_expi.
-  rewrite -!mulrA -sqrtrM; last by rewrite invr_ge0 ler0n.
-  rewrite -expr2 sqrtr_sqr !mulrA mulrC normrV ?unitfE ?pnatr_eq0 //.
-  rewrite normr_nat !mulrA mulVr ?mul1r ?unitfE ?pnatr_eq0 //.
-  rewrite -sqrtrM; last by rewrite subr_ge0 Im_half_anglec // normr_expi.
+  rewrite mulrC -mulr2n.
+  rewrite (@sqrtrM _ (1 - complex.Re a)); last by rewrite subr_ge0 Im_half_anglec // normr_expi.
+  rewrite (@sqrtrM _ (1 + complex.Re a)); last by rewrite Re_half_anglec // normr_expi.
+  rewrite mulrCA -mulrA -(sqrtrM 2^-1) ?invr_ge0//.
+  rewrite -expr2 sqrtr_sqr normfV ger0_norm// -mulr_natr -2!mulrA mulVf ?pnatr_eq0// mulr1.
+  rewrite mulrC -sqrtrM; last by rewrite subr_ge0 Im_half_anglec // normr_expi.
   rewrite -subr_sqr expr1n.
-  rewrite -(@eqr_expn2 _ 2%N) //; last by rewrite sqrtr_ge0.
+  rewrite -(@eqrXn2 _ 2%N) //; last by rewrite sqrtr_ge0.
   by rewrite -sin2cos2 sqr_sqrtr // sqr_ge0.
-rewrite mulrN mulNr -opprB opprK eqr_oppLR.
-rewrite mulrC -mulr2n -mulr_natl sqrtrM; last by rewrite Re_half_anglec // normr_expi.
-rewrite mulrAC sqrtrM; last by rewrite subr_ge0 Im_half_anglec // normr_expi.
-rewrite -!mulrA -sqrtrM; last by rewrite invr_ge0 ler0n.
-rewrite -expr2 sqrtr_sqr !mulrA mulrC normrV ?unitfE ?pnatr_eq0 //.
-rewrite normr_nat !mulrA mulVr ?mul1r ?unitfE ?pnatr_eq0 //.
-rewrite -sqrtrM; last by rewrite Re_half_anglec // normr_expi.
-rewrite mulrC -subr_sqr expr1n.
-rewrite -(@eqr_expn2 _ 2%N) //; last 2 first.
+rewrite mulrN mulNr -opprD eqr_oppLR.
+rewrite mulrC -mulr2n.
+rewrite (@sqrtrM _ (1 - complex.Re a)); last by rewrite subr_ge0 Im_half_anglec // normr_expi.
+rewrite (@sqrtrM _ (1 + complex.Re a)); last by rewrite Re_half_anglec // normr_expi.
+rewrite mulrAC -2!mulrA -sqrtrM ?invr_ge0//.
+rewrite -expr2 sqrtr_sqr normfV ger0_norm// mulrA -[eqbLHS]mulr_natr -!mulrA mulVf ?pnatr_eq0// mulr1.
+rewrite -sqrtrM; last by rewrite subr_ge0 Im_half_anglec // normr_expi.
+rewrite -subr_sqr expr1n.
+rewrite -(@eqrXn2 _ 2%N) //; last 2 first.
   by rewrite sqrtr_ge0.
   by rewrite ltW // oppr_gt0 ltNge.
 by rewrite -sin2cos2 sqrrN sqr_sqrtr // sqr_ge0.
@@ -967,7 +966,7 @@
 move: (cosD (half_angle a) (half_angle a)).
 rewrite halfP -2!expr2 cos2sin2 -addrA -opprD -mulr2n => /eqP.
 rewrite eq_sym subr_eq addrC -subr_eq eq_sym => /eqP/(congr1 (fun x => x / 2%:R)).
-rewrite -mulr_natl mulrC mulrA mulVr ?unitfE ?pnatr_eq0 // mul1r.
+rewrite -(mulr_natl (sin _ ^+ _)) mulrC mulrA mulVr ?unitfE ?pnatr_eq0 // mul1r.
 by move/(congr1 Num.sqrt); rewrite sqrtr_sqr.
 Qed.
 

coq-robot.opam

@@ -19,14 +19,14 @@ Mathematical Components library."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.14" & < "8.19~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.14.0" & < "1.19~") }
-  "coq-mathcomp-fingroup" { (>= "1.14.0" & < "1.19~") }
-  "coq-mathcomp-algebra" { (>= "1.14.0" & < "1.19~") }
-  "coq-mathcomp-solvable" { (>= "1.14.0" & < "1.19~") }
-  "coq-mathcomp-field" { (>= "1.14.0" & < "1.19~") }
-  "coq-mathcomp-analysis" { (>= "0.6.0" & < "0.7~") }
-  "coq-mathcomp-real-closed" { (>= "1.1.3") }
+  "coq" { (>= "8.16" & < "8.20~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.2.0") }
+  "coq-mathcomp-fingroup" { (>= "2.2.0") }
+  "coq-mathcomp-algebra" { (>= "2.2.0") }
+  "coq-mathcomp-solvable" { (>= "2.2.0") }
+  "coq-mathcomp-field" { (>= "2.2.0") }
+  "coq-mathcomp-analysis" { (>= "1.0.0") }
+  "coq-mathcomp-real-closed" { (>= "2.0.0") }
 ]
 
 tags: [

derive_matrix.v

@@ -170,8 +170,8 @@ Qed.
 
 Lemma derive1mx_SE : (forall t, M t \in 'SE3[R]) ->
   forall t, derive1mx M t = block_mx
-    (derive1mx (@rot_of_hom [rcfType of R^o] \o M) t) 0
-    (derive1mx (@trans_of_hom [rcfType of R^o] \o M) t) 0.
+    (derive1mx (@rot_of_hom R^o \o M) t) 0
+    (derive1mx (@trans_of_hom R^o \o M) t) 0.
 Proof.
 move=> MSE t.
 rewrite block_mxEh.
@@ -313,7 +313,7 @@ rewrite (_ : (fun x => _) =
 rewrite (derive1mx_dotmul (derivable_mx_row HM) (derivable_mx_col HN)).
 by rewrite [in RHS]mxE; congr (_  + _); rewrite [in RHS]mxE dotmulE;
    apply/eq_bigr => /= k _; rewrite !mxE; apply: f_equal2;
-   try by congr (@derive1 _ [normedModType R of R^o] _ t);
+   try by congr (@derive1 _ R^o _ t);
           rewrite funeqE => z; rewrite !mxE.
 Qed.
 
@@ -338,14 +338,13 @@ Qed.
 End product_rules.
 
 Section cross_product_matrix.
-Import rv3LieAlgebra.Exports.
 
 Lemma differential_cross_product (R : realFieldType) (v : 'rV[R^o]_3) y :
   'd (crossmul v) y = mx_lin1 \S( v ) :> (_ -> _).
 Proof.
 rewrite (_ : crossmul v = (fun x => x *m \S( v ))); last first.
   by rewrite funeqE => ?; rewrite -spinE.
-rewrite (_ : mulmx^~ \S(v) = mulmxr_linear 1 \S(v)); last by rewrite funeqE.
+rewrite (_ : mulmx^~ \S(v) = @mulmxr _ 1 _ _ \S(v)); last by rewrite funeqE.
 rewrite diff_lin //= => x.
 suff : differentiable (mulmxr \S(v)) (x : 'rV[R^o]_3).
   by move/differentiable_continuous.
@@ -363,7 +362,7 @@ Proof.
 transitivity ('d (crossmul (- v)) y); last first.
   by rewrite differential_cross_product spinN mx_lin1N.
 congr diff.
-by rewrite funeqE => /= u; rewrite lieC linearNl.
+by rewrite funeqE => /= u; rewrite (@lieC _ (vec3 R)) linearNl.
 Qed.
 
 End cross_product_matrix.

dh.v

@@ -52,7 +52,6 @@ Coercion plucker_array_mx (T : ringType) (p : Plucker.array T) :=
 Section plucker_of_line.
 Variable T : rcfType.
 Implicit Types l : Line.t T.
-Import rv3LieAlgebra.Exports.
 
 Definition normalized_plucker_direction l :=
   let p1 := \pt( l ) in let p2 := \pt2( l ) in
@@ -75,8 +74,8 @@ Lemma normalized_plucker_positionP l :
   normalized_plucker_position l *d normalized_plucker_direction l == 0.
 Proof.
 rewrite /normalized_plucker_position /normalized_plucker_direction -Line.vectorE.
-rewrite (linearZr_LR (crossmul_bilinear _)) /=.
-by rewrite dotmulvZ dotmulZv -dot_crossmulC liexx dotmulv0 2!mulr0.
+rewrite (linearZr_LR crossmul) /=.
+by rewrite dotmulvZ dotmulZv -dot_crossmulC (@liexx _ (vec3 T)) dotmulv0 2!mulr0.
 Qed.
 
 Definition normalized_plucker l : 'rV[T]_6 :=
@@ -94,7 +93,7 @@ Lemma normalized_pluckerP l :
 Proof.
 move=> p1 p2 l0.
 rewrite /normalized_plucker /normalized_plucker_direction /normalized_plucker_position.
-rewrite -/p1 -/p2 (linearZr_LR (crossmul_bilinear _)) -scale_row_mx scalerA.
+rewrite -/p1 -/p2 (linearZr_LR crossmul) -scale_row_mx scalerA.
 by rewrite divrr ?scale1r // unitfE norm_eq0 /p2 -Line.vectorE.
 Qed.
 
@@ -104,7 +103,7 @@ Lemma plucker_of_lineE l (l0 : \vec( l ) != 0) :
 Proof.
 rewrite /plucker_of_line /plucker_array_mx /=.
 rewrite /normalized_plucker_direction /normalized_plucker_position.
-rewrite (linearZr_LR (crossmul_bilinear _)) -scale_row_mx.
+rewrite (linearZr_LR crossmul) -scale_row_mx.
 by rewrite scalerA divrr ?scale1r // unitfE norm_eq0 -Line.vectorE.
 Qed.
 
@@ -120,14 +119,14 @@ Qed.
 
 Lemma plucker_eqn_self l : plucker_eqn \pt( l ) l = 0.
 Proof.
-rewrite /plucker_eqn -spinN -spinD spinE lieC addrC.
+rewrite /plucker_eqn -spinN -spinD spinE (@lieC _ (vec3 T)) addrC.
 by rewrite -linearBl /= subrr linear0l.
 Qed.
 
 Lemma in_plucker p l : p \in (l : pred _) -> plucker_eqn p l = 0.
 Proof.
 rewrite inE => /orP[/eqP ->|/andP[l0 H]]; first by rewrite plucker_eqn_self.
-rewrite /plucker_eqn -spinN -spinD spinE lieC addrC -linearBl.
+rewrite /plucker_eqn -spinN -spinD spinE (@lieC _ (vec3 T)) addrC -linearBl.
 apply/eqP.
 rewrite -/(colinear _ _) -colinearNv opprB colinear_sym.
 apply: (colinear_trans l0 _ H).
@@ -265,7 +264,8 @@ rewrite [_ 0 1]mxE [_ 1 1]mxE [_ 0 2%:R]mxE [_ 1 2%:R]mxE.
 move/eqP. rewrite -addrA eq_sym addrC -subr_eq -cos2sin2. move/eqP.
 move/(congr1 (fun x => (sin alpha)^+2 * x)).
 rewrite mulrDr -(@exprMn _ _ (sin alpha) (_ 1 1)) (mulrC _ (_ 1 1)) H11_H21.
-rewrite sqrrN exprMn (mulrC _ (_ ^+ 2)) -mulrDl cos2Dsin2 mul1r => /esym sqr_H21.
+rewrite sqrrN exprMn [in X in _ = X -> _](mulrC (sin alpha ^+ 2)).
+rewrite -mulrDr cos2Dsin2 mulr1 => /esym sqr_H21.
 
 move: (norm_col_of_O (FromTo_is_O F1 F0) 0) => /= /(congr1 (fun x => x ^+ 2)).
 rewrite sqr_norm sum3E 2![_ 0 0]mxE.
@@ -380,8 +380,14 @@ have H4 : From1To0 = dh_rot theta alpha.
     move: Hrot.
     rewrite H11 (eqP H21) H10 !mulNr opprK H20 -(mulrA (cos theta)) -expr2 mulrAC.
     rewrite -expr2 -opprD (mulrC (cos theta) (_ ^+ 2)) -mulrDl cos2Dsin2 mul1r.
-    rewrite mulrN -expr2 -mulrA mulrCA -expr2 -mulrA mulrCA -expr2 -mulrDr (addrC (_ ^+ 2)).
-    rewrite cos2Dsin2 mulr1 -expr2 sin2cos2 addrCA -opprD -mulr2n => /eqP.
+    rewrite [in LHS]mulrN -expr2.
+    rewrite mulrAC -expr2.
+    rewrite (mulrAC (cos alpha)) -expr2.
+    rewrite -mulrDl.
+    rewrite (addrC (_ ^+ 2)).
+    rewrite cos2Dsin2 mul1r.
+    rewrite -expr2.
+    rewrite (sin2cos2 theta) addrCA -opprD -mulr2n => /eqP.
     rewrite subr_eq addrC -subr_eq subrr eq_sym mulrn_eq0 /= sqrf_eq0 => ct0.
     rewrite {1}/From1To0 -lock H11 {1}/From1To0 -lock (eqP H21).
     by rewrite (eqP ct0) !(mulr0,mul0r) oppr0.
@@ -401,8 +407,9 @@ have H4 : From1To0 = dh_rot theta alpha.
     move: Hrot.
     rewrite H11 H21 H10 !mulNr opprK (eqP H20) -(mulrA (cos theta)) -expr2 mulrAC.
     rewrite -expr2 (mulrC (cos theta) (_ ^+ 2)) -mulrDl cos2Dsin2 mul1r.
-    rewrite mulNr mulrAC -!expr2 (mulrAC (cos alpha)) -expr2 -opprD -mulrDl.
-    rewrite (addrC _ (cos _ ^+ 2)) cos2Dsin2 mul1r mulrN -expr2 cos2sin2 -addrA -opprD.
+    rewrite mulNr mulrAC -2!expr2.
+    rewrite (mulrAC (cos alpha)) -expr2 -opprD -mulrDl.
+    rewrite (addrC (sin alpha ^+ 2)) cos2Dsin2 mul1r mulrN -expr2 cos2sin2 -addrA -opprD.
     rewrite -mulr2n => /eqP; rewrite subr_eq addrC -subr_eq subrr eq_sym mulrn_eq0 /=.
     rewrite sqrf_eq0 => /eqP st0.
     by rewrite st0 !(mulr0,oppr0) (mulrC (cos theta)).

differential_kinematics.v

@@ -740,8 +740,6 @@ Hypothesis o4E : forall t, \o{Fmax t} = \o{Fim1 3%:R t} + d4 *: 'e_2.
 Lemma scale_realType (K : realType) (k1 : K) (k2 : K^o) : k1 *: k2 = k1 * k2.
 Proof. by []. Qed.
 
-Import rv3LieAlgebra.Exports.
-
 Lemma scara_geometric_jacobian t :
   derivable (theta1 : R^o -> R^o) t 1 ->
   derivable (theta2 : R^o -> R^o) t 1 ->
@@ -772,7 +770,7 @@ rewrite (mul_mx_row _ a) {}/a; congr (@row_mx _ _ 3 3 _ _).
   rewrite {1}o4E.
   rewrite linearDr /=.
   rewrite (linearZr_LR _ _ _ 'e_2)
-   /= {2}Hzvec (linearZl_LR _ _ _ 'e_2) /= liexx 2!{1}scaler0 addr0.
+   /= {2}Hzvec (linearZl_LR _ _ _ 'e_2) /= (@liexx _ (vec3 R)) 2!{1}scaler0 addr0.
   rewrite (_ : \o{Fmax t} - \o{Fim1 1 t} =
     (a2 * cos (theta1 t + theta2 t) *: 'e_0 +
     (a1 * sin (theta1 t) + a2 * sin (theta1 t + theta2 t) - a1 * sin (theta1 t)) *: 'e_1 +
@@ -784,16 +782,16 @@ rewrite (mul_mx_row _ a) {}/a; congr (@row_mx _ _ 3 3 _ _).
     rewrite addrC -[in RHS]addrA; congr (_ + _).
     by rewrite -addrA -scalerDl.
   rewrite linearDr /=.
-  rewrite (linearZr_LR _ _ _ 'e_2) /= (linearZl_LR (crossmul_bilinear _) 'e_2)
-          {2}(Hzvec t 1) /= liexx 2!{1}scaler0 addr0.
+  rewrite (linearZr_LR _ _ _ 'e_2) /= (linearZl_LR crossmul 'e_2)
+          {2}(Hzvec t 1) /= (@liexx _ (vec3 R)) 2!{1}scaler0 addr0.
   rewrite (addrC (a1 * sin _)) addrK.
   rewrite (_ : \o{Fmax t} - \o{Fim1 3%:R t} = d4 *: 'e_2%:R); last first.
     by rewrite o4E -addrA addrC subrK.
-  rewrite (linearZr_LR _ _ _ 'e_2) /= (linearZl_LR (crossmul_bilinear _) 'e_2)
-          {1}(Hzvec t 3%:R) /= liexx 2!scaler0 addr0.
+  rewrite (linearZr_LR _ _ _ 'e_2) /= (linearZl_LR crossmul 'e_2)
+          {1}(Hzvec t 3%:R) /= (@liexx _ (vec3 R)) 2!scaler0 addr0.
   rewrite o3E.
   rewrite linearDr /= (linearZr_LR _ _ _ 'e_2) (linearZl_LR _ 'e_2)
-          {2}(Hzvec t 0) /= liexx 2!scaler0 addr0.
+          {2}(Hzvec t 0) /= (@liexx _ (vec3 R)) 2!scaler0 addr0.
   rewrite {1}o2E {1}o1E.
   rewrite (_ : (fun _ => _) =
                 (a2 \*: (cos \o (theta2 + theta1) : R^o -> R^o)) +
@@ -806,8 +804,8 @@ rewrite (mul_mx_row _ a) {}/a; congr (@row_mx _ _ 3 3 _ _).
       exact: ex_derive.
       exact: H3.
     by rewrite deriveE // diff_cst add0r derive1E.
-  - rewrite !linearDr /= !(linearZr_LR (crossmul_bilinear _))
-            !(linearZl_LR (crossmul_bilinear _)) /= !Hzvec veckj vecki
+  - rewrite !linearDr /= !(linearZr_LR crossmul)
+            !(linearZl_LR crossmul) /= !Hzvec veckj vecki
             !{1}scalerN.
     rewrite -!addrA addrCA addrC -!addrA (addrCA (- _)) !addrA.
     rewrite -2!addrA [in RHS]addrC; congr (_ + _).