mathcomp 2.4 and rocq 9.0

Author: thery

.github/workflows/docker-action.yml

@@ -17,7 +17,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.3.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
       fail-fast: false
     steps:
       - uses: actions/checkout@v4

README.md

@@ -43,12 +43,11 @@ An interactive version of the library is available
 - Author(s):
   - Laurent Théry
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: 8.19 or later
+- Compatible Coq versions: 9.0 or later
 - Additional dependencies:
-  - [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)
+  - [MathComp ssreflect 2.4 or later](https://math-comp.github.io)
+  - [MathComp algebra 2.4 or later](https://math-comp.github.io)
+  - [MathComp finmap 2.2.1 or later](https://github.com/math-comp/finmap)
 - Coq namespace: `hanoi`
 - Related publication(s): none
 

coq-hanoi.opam

@@ -41,11 +41,10 @@ An interactive version of the library is available
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "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")}
+  "coq" {(>= "9.0")}
+  "coq-mathcomp-ssreflect" {(>= "2.4.0")}
+  "coq-mathcomp-algebra" {(>= "2.4.0")}
+  "coq-mathcomp-finmap" {(>= "2.2.1")}
 ]
 
 tags: [

extra.v

@@ -4,6 +4,7 @@
 (*                                                                            *)
 (******************************************************************************)
 
+From Stdlib Require Import ArithRing.
 From mathcomp Require Import all_ssreflect finmap.
 
 Set Implicit Arguments.
@@ -1018,44 +1019,55 @@ end.
 
 Ltac test t1 t2 := let xx := delta_lterm1 t1 t2 in pose kk := xx.
 
+
+Ltac ring_preprocess := rewrite -?mul2n -?[addn]/Nat.add -?[muln]/Nat.mul.
+Ltac ring_postprocess := 
+  rewrite ?[nat_of_bin _]/= -?[Nat.add]/addn -?[Nat.mul]/muln ?add1n ?add2n.
+Ltac hyp_ring_preprocess H := rewrite -?mul2n -?[addn]/Nat.add -?[muln]/Nat.mul in H |- *.
+Ltac hyp_ring_postprocess H := 
+  rewrite ?[nat_of_bin _]/= -?[Nat.add]/addn -?[Nat.mul]/muln ?add1n ?add2n in H |-*.
+  
+Ltac nat_ring := ring_preprocess; ring.
+
 Ltac applyr H :=
-  rewrite -?mul2n in H |- *;
+  hyp_ring_preprocess H;
   match goal with 
   H: is_true (leq _ ?X) |- is_true (leq _ ?Y) =>
     ring_simplify X Y in H;
     ring_simplify X Y; rewrite ?[nat_of_bin _]/= in H |- *
   end;
+  hyp_ring_postprocess H;
   let Z := fresh "Z" in
   match goal with 
   H: is_true (leq _ ?X1) |- is_true (leq _ ?Y1) =>
     let v := delta_lterm1 Y1 X1 in
     (try (rewrite [Z in _ <= Z](_ : _ = v + X1))); 
     [ apply: leq_trans (leq_add (leqnn _) H); rewrite {H}// ?(add0n,addn0) 
-     | ring]
+     | nat_ring]
   end.
 
 Ltac applyl H :=
-  rewrite -?mul2n in H |- *;
+  hyp_ring_preprocess H;
   match goal with 
   H: is_true (leq ?X _) |- is_true (leq ?Y _) =>
-    ring_simplify X Y; ring_simplify X Y in H;
-    rewrite ?[nat_of_bin _]/= in H |- *
+    ring_simplify X Y; ring_simplify X Y in H
   end;
+  hyp_ring_postprocess H;
   let Z := fresh "Z" in
   match goal with 
   H: is_true (leq ?X1 _) |- is_true (leq ?Y1 _) =>
     let v := delta_lterm1 Y1 X1 in
     (try rewrite [Z in Z <= _](_ : Y1 = v + X1));
     [apply: leq_trans (leq_add (leqnn _) H) _;
-     rewrite {H}// ?(add0n,addn0) | ring]
+     rewrite {H}// ?(add0n,addn0) | nat_ring]
   end.
 
 Ltac gsimpl :=
-  rewrite -?mul2n in |- *;
+  ring_preprocess;
   match goal with 
-  |- is_true (leq ?X ?Y) =>
-    ring_simplify X Y; rewrite ?[nat_of_bin _]/=
+  |- is_true (leq ?X ?Y) => ring_simplify X Y 
   end;
+  ring_postprocess;
   let Z := fresh "Z" in
   match goal with 
     |- is_true (leq ?X1 ?Y1) =>
@@ -1065,22 +1077,21 @@ Ltac gsimpl :=
     let v := delta_lterm1 X1 Y1 in
     let v1 := delta_lterm1 X1 v in
     let v2 := delta_lterm1 Y1 v1 in
-    (try (rewrite [Z in _ <= Z](_ : Y1 = v2 + v1); last by ring));
-    (try (rewrite [Z in Z <= _](_ : X1 = v + v1); last by ring));
+    (try (rewrite [Z in _ <= Z](_ : Y1 = v2 + v1); last by nat_ring));
+    (try (rewrite [Z in Z <= _](_ : X1 = v + v1); last by nat_ring));
     rewrite ?leq_add2r
     | _ => 
     let v1 := delta_lterm1 Y1 v in
     let v2 := delta_lterm1 X1 v1 in
-    (try (rewrite [Z in _ <= Z](_ : Y1 = v + v1); last by ring));
-    (try (rewrite [Z in Z <= _](_ : X1 = v2 + v1); last by ring));
+    (try (rewrite [Z in _ <= Z](_ : Y1 = v + v1); last by nat_ring));
+    (try (rewrite [Z in Z <= _](_ : X1 = v2 + v1); last by nat_ring));
     rewrite ?leq_add2r
   end
   end.
-  
-Ltac sring := rewrite -!mul2n; ring.
+
 Ltac changel t :=
   let X := fresh "X" in 
-  rewrite [X in X <= _](_ : _ = t); last by (ring || sring).
+  rewrite [X in X <= _](_ : _ = t); last by (ring || nat_ring).
 Ltac changer t := 
   let X := fresh "X" in 
-  rewrite [X in _ <= X](_ : _ = t); last by (ring || sring).
+  rewrite [X in _ <= X](_ : _ = t); last by (ring || nat_ring).

meta.yml

@@ -50,34 +50,29 @@ license:
   identifier: MIT
 
 supported_coq_versions:
-  text: '8.19 or later'
-  opam: '{(>= "8.19")}'
+  text: '9.0 or later'
+  opam: '{(>= "9.0")}'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "2.3.0")}'
+    version: '{(>= "2.4.0")}'
   description: |-
-    [MathComp ssreflect 2.3 or later](https://math-comp.github.io)
+    [MathComp ssreflect 2.4 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{(>= "2.3.0")}'
+    version: '{(>= "2.4.0")}'
   description: |-
-    [MathComp algebra 2.3 or later](https://math-comp.github.io)
+    [MathComp algebra 2.4 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-finmap
-    version: '{(>= "2.1.0")}'
+    version: '{(>= "2.2.1")}'
   description: |-
-    [MathComp finmap 2.1 or later](https://github.com/math-comp/finmap)
-- opam:
-    name: coq-mathcomp-bigenough
-    version: '{(>= "1.0.1")}'
-  description: |-
-    [MathComp bigenough 1.0.1 or later](https://github.com/math-comp/finmap)
+    [MathComp finmap 2.2.1 or later](https://github.com/math-comp/finmap)
 
 
 tested_coq_opam_versions:
-- version: '2.3.0-coq-8.19'
+- version: '2.4.0-rocq-prover-9.0'
   repo: 'mathcomp/mathcomp'
 
 namespace: hanoi

psi.v

@@ -897,7 +897,7 @@ Lemma phi_3_5_4_sum n :
 Proof.
 rewrite phiE.
 rewrite -(big_mkord xpredT (fun i => 2 ^ troot i)).
-rewrite (big_cat_nat _ _ _ (_ : 0 <= 1)) //=.
+rewrite (big_cat_nat (_ : 0 <= 1)) //=.
 by rewrite big_nat_recl //= big_mkord big_ord0 addn0 add1n.
 Qed.
 

shanoi4.v

@@ -1,3 +1,4 @@
+From Stdlib Require Import ArithRing.
 From mathcomp Require Import all_ssreflect finmap.
 From hanoi Require Import extra star gdist lhanoi3 ghanoi ghanoi4 shanoi.
 
@@ -612,7 +613,7 @@ have [/andP[a_gt1 aLlm1]|] := boolP (2 <= a <= l.-1).
       have F := big_mkord xpredT 
                     (fun i => `d[u (inord i), u (inord i.+1)]_smove).
       rewrite -{}[sd u]F.
-      rewrite (big_cat_nat _ _ _ (_ : _ <= (a.-1).+1)) //=; last first.
+      rewrite (big_cat_nat (_ : _ <= (a.-1).+1)) //=; last first.
          by rewrite prednK.
       rewrite big_mkord big_ord_recr /= prednK //.
       rewrite -{9}[a]add0n big_addn -/b big_mkord.
@@ -831,7 +832,6 @@ have [/andP[a_gt1 aLlm1]|] := boolP (2 <= a <= l.-1).
   have F9 : α_[1] (n.+2) <= (α_[1] n).*2.+2.
     apply: leq_trans (leqnSn _).
     by apply: alphaL_4_5.
-(* Lia should work now *)
   gsimpl.
   applyr P1.
   rewrite -(leq_add2r x1S); applyr P2.
@@ -846,7 +846,7 @@ have [/andP[a_gt1 aLlm1]|] := boolP (2 <= a <= l.-1).
   gsimpl.
   rewrite -(leq_add2r (S_[1] n.+1)); applyl F6n; gsimpl.
   rewrite F71; gsimpl.
-  rewrite !add1n {}F73; gsimpl.
+  rewrite ?add1n {}F73; gsimpl.
   rewrite -(leq_add2r (S_[1] n.+2 + S_[2] n.+2)).
   applyl  F6n1; gsimpl.
   rewrite {}F72 {}F721 {}F711 {}F71; gsimpl.
@@ -1131,7 +1131,7 @@ have [/andP[a_gt1 /eqP bE1]|] := boolP ((1 < a) && (b == 1)).
   rewrite lEa; applyr F6n.
   rewrite -(leq_add2r (S_[1] n.+2 + S_[3] n.+2)); applyr F6n1.
   rewrite {}F72 {}F711 {}F71; gsimpl.
-  rewrite !add1n -{}F8.
+  rewrite ?add1n -{}F8.
   by applyl F9; gsimpl.
 rewrite negb_and -leqNgt => o1H.
 have [/eqP aE1| aD1] := boolP (a == 1).
@@ -1243,7 +1243,7 @@ have [/eqP aE1| aD1] := boolP (a == 1).
       rewrite !alphaL_3E.
       have F := leq_dsum_alpha_2l_1 n.+1; applyr F.
       rewrite !dsum_alphaL_S; gsimpl.
-      rewrite !add1n.
+      rewrite ?add1n.
       by have F := alphaL_4_5 n; applyl F; gsimpl.
     rewrite (maxn_idPr _) //.
     changer (2 * (S_[3] (n.+1)).+1 +  2 * S_[b] (n.+1)).
@@ -2960,7 +2960,7 @@ move: c_gt0; rewrite leq_eqVlt eq_sym => /orP[/eqP cE1|c_gt1].
     set y3S := sp _ _ _ in P5; set y4S := \sum_(_ < _) _ in P5.
     rewrite /sd -(big_mkord xpredT 
                    (fun i => `d[u (inord i), u (inord i.+1)]_smove)).
-    rewrite (big_cat_nat _ _ _ (_ : 0 <= a1)) //=; last by apply: ltnW.
+    rewrite (big_cat_nat (_ : 0 <= a1)) //=; last by apply: ltnW.
     rewrite big_mkord -!addnA.
     apply: leq_trans (leq_add P1l1  (leqnn _)); rewrite -/x1S.
     rewrite -{P1l1}P2 -/x2S {1}lE2 !sum_beta_S //.
@@ -3331,7 +3331,7 @@ have [|b_gt0] := leqP b 0; last first.
     have F2 := dsum_alphaL_S 3 n; rewrite {1}F2.
     have F3 : S_[5] n.+2 <= S_[4] n.+1 + (α_[1] n.+1).*2.
       by apply: dsum_alphaL_alpha.
-    rewrite -[3 + 2]/5 -[2 + 2]/4; applyl F3.
+    rewrite -[3 + 2]/5; applyl F3.
     have F4 : S_[4] n.+1 <= S_[3] n + (α_[1] n).*2.
       by apply: dsum_alphaL_alpha.
     rewrite -leq_double in F4; applyl F4; gsimpl.
@@ -3569,7 +3569,7 @@ have [c_gt2|c_lt3] := leqP 3 c.
   rewrite -[_ <= _](leq_mul2l 3) mulnA.
   by apply: leq_trans F17 _; gsimpl.
 have cE2 : c = 2 by case: (c) c_gt1 c_lt3 => [|[|[|]]].
-rewrite cE2 (maxn_idPl _) // add1n -[2 * 2]/4 -[(3 * 2).-2]/4 -[2 + 4]/6.
+rewrite cE2 (maxn_idPl _) // -[2 * 2]/4 -[(3 * 2).-2]/4.
 rewrite [in X in _ <= X]mul2n -addnn.
 have F1 := dsum_alphaL_S 5 n; rewrite {1}F1.
 have F2 := dsum_alpha3_S n.+2.
@@ -3591,7 +3591,7 @@ have F9 : 3 * α_[1] n1.+1.+4 <= 4 * α_[1] n1.+4.
   by rewrite alpha_4_3.
 rewrite -[_ <= _]orFb  -(leq_mul2l 4) in F9.
 rewrite -[_ <= _](leq_mul2l 3).
-by rewrite add1n; applyl F9; gsimpl.
+by applyl F9; gsimpl.
 Qed.
 
 End Case3.