update

.github/workflows/docker-action.yml

@@ -17,12 +17,18 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.15'
+          - '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'
       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.15
+- Compatible Coq versions: Coq 8.14 to Coq 8.18
 - Additional dependencies:
   - [MathComp ssreflect](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)

coq-robot.opam

@@ -19,13 +19,13 @@ Mathematical Components library."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.14" & < "8.16~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.16~") }
-  "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.16~") }
-  "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.16~") }
-  "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.16~") }
-  "coq-mathcomp-field" { (>= "1.13.0" & < "1.16~") }
-  "coq-mathcomp-analysis" { (>= "0.5.0" & < "0.6~") }
+  "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") }
 ]
 

derive_matrix.v

@@ -2,9 +2,9 @@
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum rat.
 From mathcomp Require Import closed_field polyrcf matrix mxalgebra mxpoly zmodp.
 From mathcomp Require Import realalg complex fingroup perm.
-From mathcomp.analysis Require Import boolp reals Rstruct classical_sets signed.
-From mathcomp.analysis Require Import topology normedtype landau forms derive.
-From mathcomp.analysis Require Import functions.
+From mathcomp Require Import boolp reals Rstruct classical_sets signed.
+From mathcomp Require Import topology normedtype landau forms derive.
+From mathcomp Require Import functions.
 Require Import ssr_ext euclidean rigid skew.
 
 (******************************************************************************)
@@ -22,19 +22,6 @@ Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 
 Local Open Scope ring_scope.
 
-(* NB: PR to analysis in progress *)
-Lemma derive1_cst (R : numFieldType) (V : normedModType R) (k : V) t :
-  (cst k)^`() t = 0.
-Proof. by rewrite derive1E derive_val. Qed.
-
-(* TODO: see coord_continuous in normedtype.v *)
-Lemma coord_continuous (R : numDomainType) (K : normedModType R) m n i j :
-  continuous (fun M : 'M[K]_(m, n) => M i j).
-Proof.
-move=> /= M s /= /nbhs_normP => -[e e0 es].
-by apply/nbhs_ballP; exists e => //= N MN; exact/es/MN.
-Qed.
-
 Lemma mx_lin1N (R : ringType) n (M : 'M[R]_n) :
   mx_lin1 (- M) = -1 \*: mx_lin1 M :> ( _ -> _).
 Proof. by rewrite funeqE => v /=; rewrite scaleN1r mulmxN. Qed.

differential_kinematics.v

@@ -2,8 +2,8 @@
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum rat.
 From mathcomp Require Import closed_field polyrcf matrix mxalgebra mxpoly zmodp.
 From mathcomp Require Import realalg complex fingroup perm.
-From mathcomp.analysis Require Import boolp reals Rstruct classical_sets signed.
-From mathcomp.analysis Require Import topology normedtype landau forms derive.
+From mathcomp Require Import boolp reals Rstruct classical_sets signed.
+From mathcomp Require Import topology normedtype landau forms derive.
 From mathcomp Require Import functions.
 Require Import ssr_ext derive_matrix euclidean frame rot skew rigid.
 

euclidean.v

@@ -652,14 +652,14 @@
   by rewrite -map_mxM mulmxE (eqP MSO) map_mx1.
 rewrite mul1mx -scalemxAr /= -scalemxAl scalerA => /eqP.
 rewrite -subr_eq0 -{1}(scale1r (v *m _)) -scalerBl scaler_eq0 => /orP [].
   by rewrite subr_eq0 mulrC -sqr_normc -{1}(expr1n _ 2) eqr_expn2 // ?ler01 // => /eqP.
 by rewrite dotmul_conjc_eq0 (negbTE v0).
 Qed.
 
 Lemma norm_row_of_O (T : rcfType) n M : M \is 'O[T]_n.+1 -> forall i, norm (row i M) = 1.
 Proof.
 move=> MSO i.
 apply/eqP; rewrite -(@eqr_expn2 _ 2) // ?norm_ge0 // expr1n; apply/eqP.
 rewrite -dotmulvv; move/orthogonalP : MSO => /(_ i i) ->; by rewrite eqxx.
 Qed.
 
@@ -1625,16 +1625,16 @@
 rewrite [X in X + _ + _](_ : _ = M 0 0 * (M 2%:R 2%:R + M 1 1) +
    (M 1 1 * M 2%:R 2%:R - M 2%:R 1 * M 1 2%:R)); last first.
   rewrite coefM sum2E coefD coefX add0r coefN coefC [- _]/=.
-  rewrite subn0 coefD.
+  rewrite subn0 coefD coefB.
   rewrite coefM sum2E subn0 coefD coefX add0r coefN (_ : _`_0 = M 1 1); last by rewrite coefC.
   rewrite coefD coefX coefN coefC subr0 mulr1.
   rewrite coefD coefN coefX coefN coefC subr0 mul1r.
   rewrite subnn coefD coefX add0r coefN coefC [in X in - M 1 1 - X]/=.
   rewrite coefM sum2E coefC coefC mulr0 add0r coefC mul0r subr0.
-  rewrite coefD coefX coefN coefC subr0 mul1r.
-  rewrite coefD coefM sum1E coefD coefX add0r coefN coefC [in X in - X * _`_ _]/=.
+  rewrite coefD coefN coefC subr0 mul1r.
+  rewrite coefM sum1E coefD coefX add0r coefN coefC [in X in - X * _`_ _]/=.
   rewrite coefD coefX add0r coefN coefC mulrN !mulNr opprK.
-  rewrite coefN coefM sum1E coefC coefC [in X in M 1 1 * _ - X]/=.
+  rewrite coefM sum1E coefC coefC [in X in M 1 1 * _ - X]/=.
   by rewrite -opprB mulrN 2!opprK.
 rewrite [X in _ + X + _](_ : _ = - M 0 1 * M 1 0); last first.
   rewrite coefN coefM sum2E coefC [in X in X * _]/= subnn.

meta.yml

@@ -30,52 +30,64 @@ license:
   file: LICENSE
 
 supported_coq_versions:
-  text: Coq 8.14 to Coq 8.15
-  opam: '{ (>= "8.14" & < "8.16~") | (= "dev") }'
+  text: Coq 8.14 to Coq 8.18
+  opam: '{ (>= "8.14" & < "8.19~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '1.13.0-coq-8.14'
+- version: '1.16.0-coq-8.14'
   repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.15'
+- version: '1.16.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.14'
+- version: '1.16.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.15'
+- version: '1.16.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.14'
+- version: '1.16.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.15'
+- version: '1.17.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
+- version: '1.17.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
+- version: '1.17.0-coq-8.17'
+  repo: 'mathcomp/mathcomp'
+- version: '1.17.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
+- version: '1.18.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
+- version: '1.18.0-coq-8.17'
+  repo: 'mathcomp/mathcomp'
+- version: '1.18.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.13.0" & < "1.16~") }'
+    version: '{ (>= "1.14.0" & < "1.19~") }'
   description: |-
     [MathComp ssreflect](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-fingroup
-    version: '{ (>= "1.13.0" & < "1.16~") }'
+    version: '{ (>= "1.14.0" & < "1.19~") }'
   description: |-
     [MathComp fingroup](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{ (>= "1.13.0" & < "1.16~") }'
+    version: '{ (>= "1.14.0" & < "1.19~") }'
   description: |-
     [MathComp algebra](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-solvable
-    version: '{ (>= "1.13.0" & < "1.16~") }'
+    version: '{ (>= "1.14.0" & < "1.19~") }'
   description: |-
     [MathComp solvable](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-field
-    version: '{ (>= "1.13.0" & < "1.16~") }'
+    version: '{ (>= "1.14.0" & < "1.19~") }'
   description: |-
     [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (>= "0.5.0" & < "0.6~") }'
+    version: '{ (>= "0.6.0" & < "0.7~") }'
   description: |-
     [MathComp analysis](https://github.com/math-comp/analysis)
 - opam:

skew.v

@@ -607,7 +607,7 @@ move=> u0 /= k.
 rewrite inE eigenvalue_root_char -map_char_poly char_poly_spin.
 apply/rootP.
 case: ifPn => [|Hk].
-- rewrite inE => /orP [/eqP ->|]; first by rewrite /= horner_map !hornerE.
+- rewrite inE => /orP [/eqP ->|]; first by rewrite /= horner_map/= !hornerE/= expr0n.
   rewrite inE => /orP [/eqP ->|].
     eigenvalue_spin_eval_poly.
     simpc.