mathcomp 2.3.0

Author: thery

.github/workflows/docker-action.yml

@@ -17,10 +17,10 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.1.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.19'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-hanoi.opam'

README.md

@@ -6,8 +6,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 [![Docker CI][docker-action-shield]][docker-action-link]
 
-[docker-action-shield]: https://github.com/thery/hanoi/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/thery/hanoi/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/thery/hanoi/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/thery/hanoi/actions/workflows/docker-action.yml
 
 
 
@@ -43,11 +43,11 @@ An interactive version of the library is available
 - Author(s):
   - Laurent Théry
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: 8.18 or later
+- Compatible Coq versions: 8.19 or later
 - Additional dependencies:
-  - [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
-  - [MathComp algebra 2.1 or later](https://math-comp.github.io)
-  - [MathComp finmap 2.0 or later](https://github.com/math-comp/finmap)
+  - [MathComp ssreflect 2.3 or later](https://math-comp.github.io)
+  - [MathComp algebra 2.3 or later](https://math-comp.github.io)
+  - [MathComp finmap 2.1 or later](https://github.com/math-comp/finmap)
   - [MathComp bigenough 1.0.1 or later](https://github.com/math-comp/finmap)
 - Coq namespace: `hanoi`
 - Related publication(s): none

coq-hanoi.opam

@@ -41,10 +41,10 @@ An interactive version of the library is available
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.18")}
-  "coq-mathcomp-ssreflect" {(>= "2.1.0")}
-  "coq-mathcomp-algebra" {(>= "2.1.0")}
-  "coq-mathcomp-finmap" {(>= "2.0.0")}
+  "coq" {(>= "8.19")}
+  "coq-mathcomp-ssreflect" {(>= "2.3.0")}
+  "coq-mathcomp-algebra" {(>= "2.3.0")}
+  "coq-mathcomp-finmap" {(>= "2.1.0")}
   "coq-mathcomp-bigenough" {(>= "1.0.1")}
 ]
 

extra.v

@@ -1,14 +1,15 @@
-From mathcomp Require Import all_ssreflect finmap.
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-
 (******************************************************************************)
 (*                                                                            *)
 (*   Extra theorems and definitions                                           *)
 (*                                                                            *)
 (******************************************************************************)
 
+From mathcomp Require Import all_ssreflect finmap.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+
 (******************************************************************************)
 (*                                                                            *)
 (*   Extra theorems about lists                                               *)
@@ -250,10 +251,9 @@ Lemma s2f_setT n : s2f (setT : {set 'I_n}) = sint 0 n.
 Proof.
 apply/fsetP => i; rewrite mem_sint /=.
 apply/imfsetP/idP => /= [[j _ -> //]| iLn].
-by exists (Ordinal iLn).
+by exists (Ordinal iLn); rewrite //= inE.
 Qed.
 
-
 Lemma s2fD n (s1 s2 : {set 'I_n}) : s2f (s1 :\: s2)  = s2f s1 `\` s2f s2.
 Proof.
 apply/fsetP => j; rewrite !inE.

meta.yml

@@ -50,25 +50,25 @@ license:
   identifier: MIT
 
 supported_coq_versions:
-  text: '8.18 or later'
-  opam: '{(>= "8.18")}'
+  text: '8.19 or later'
+  opam: '{(>= "8.19")}'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "2.1.0")}'
+    version: '{(>= "2.3.0")}'
   description: |-
-    [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
+    [MathComp ssreflect 2.3 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{(>= "2.1.0")}'
+    version: '{(>= "2.3.0")}'
   description: |-
-    [MathComp algebra 2.1 or later](https://math-comp.github.io)
+    [MathComp algebra 2.3 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-finmap
-    version: '{(>= "2.0.0")}'
+    version: '{(>= "2.1.0")}'
   description: |-
-    [MathComp finmap 2.0 or later](https://github.com/math-comp/finmap)
+    [MathComp finmap 2.1 or later](https://github.com/math-comp/finmap)
 - opam:
     name: coq-mathcomp-bigenough
     version: '{(>= "1.0.1")}'
@@ -77,7 +77,7 @@ dependencies:
 
 
 tested_coq_opam_versions:
-- version: '2.1.0-coq-8.18'
+- version: '2.3.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
 
 namespace: hanoi

phi.v

@@ -116,7 +116,7 @@ Lemma gminE n : n = gmin n + troot n.
 Proof.
 case: n => //= n.
 rewrite {1}[n.+1]tmodE /gmin.
-case: troot (troot_gt0 (isT : 0 < n.+1)) => //= t _.
+case: troot (troot_gt0 (isT : 0 < n.+1)) => // t _.
 by rewrite deltaS addnAC.
 Qed.
 
@@ -139,7 +139,7 @@ have mLt : tmod n < troot n by rewrite ltn_neqAle mDt tmod_le.
 rewrite subn1.
 apply/eqP; rewrite /gmin trootE.
 case: n {mDt}mLt => // [] [|] // n mLt.
-case: troot mLt => //= t mLt.
+case: troot mLt => // t mLt.
 by rewrite leq_addr deltaS ltn_add2l.
 Qed.
 
@@ -224,7 +224,7 @@ rewrite (leq_trans (_ : _ <= gmin n.+1 + troot m)) //.
 rewrite -ltnS -addnS.
 rewrite /gmin {3}[n.+1]tmodE addnAC leq_add2r.
 have : 0 < troot n.+1 by apply troot_gt0.
-case E : troot => [|t] _ //=.
+case E : troot => [|t] _ //; rewrite [X in X <= _]/=.
 rewrite deltaS -E leq_add2l.
 by apply: gmin_root_lt.
 Qed.

rhanoi4.v

@@ -984,10 +984,10 @@ have duz2_leq : psi (s2f E `&` `[T]) + psi (s2f A) + 2 ^ K.-1 < `d[u,z2]_rmove.
       rewrite -oprojE; case: (Hnz (z0 (oproj (enum_val i)))) => // /eqP.
       - rewrite -[_ == z0s N]negbK; case/negP.
         apply: (move_on_toplDr z0Mz0s) => //=.
-        by rewrite -{8}[n](subnK TLN) leq_add2r subnS ltnW.
+        by rewrite -[X in _ <= X](subnK TLN) leq_add2r subnS ltnW.
       - rewrite -[_ == p0]negbK; case/negP; rewrite -z0N0.
         apply: (move_on_toplDl z0Mz0s) => //=.
-        by rewrite -{8}[n](subnK TLN) ltn_add2r subnS.
+        by rewrite -[X in _ < X](subnK TLN) ltn_add2r subnS.
       rewrite -[_ == np3]negbK; case/negP.
       apply: memE''.
         have := mem_last u z0sb; rewrite -/z0 gE' !inE !mem_cat.

triangular.v

@@ -72,7 +72,7 @@ Proof. by case: n => // n _; rewrite deltaS addnS ltnS leq_addr. Qed.
 Lemma deltaE n : delta n = \sum_(i < n.+1) i.
 Proof.
 elim: n => [|n IH]; first by rewrite big_ord_recl big_ord0.
-by rewrite big_ord_recr /= -IH deltaS.
+by rewrite big_ord_recr -IH deltaS.
 Qed.
 
 Compute zip (iota 0 11) (map delta (iota 0 11)).
@@ -303,7 +303,7 @@ case: p => a b.
 rewrite /tpair /pairt /= /tmod.
 have ->: ∇(Δ(a + b) + b)  = a + b.
   apply/eqP.
-  rewrite trootE leq_addr /= deltaS.
+  rewrite trootE leq_addr deltaS.
   by rewrite addnS ltnS addnCA leq_addl.
 by rewrite [delta _ + _]addnC !addnK.
 Qed.