port to 8.17 and 8.18, refresh metadata

.github/workflows/docker-action.yml

@@ -18,15 +18,17 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
-          - 'coqorg/coq:8.16'
+          - 'coqorg/coq:8.18'
+          - 'coqorg/coq:8.17'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-buchberger.opam'
           custom_image: ${{ matrix.image }}
 
+
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
 # https://github.com/erikmd/docker-coq-github-action-demo

.github/workflows/nix-action.yml

@@ -32,15 +32,15 @@ jobs:
           else
             echo "tested_commit=${{ github.sha }}" >> $GITHUB_ENV
           fi
-      - uses: cachix/install-nix-action@v16
+      - uses: cachix/install-nix-action@v20
         with:
           nix_path: nixpkgs=channel:nixpkgs-unstable
-      - uses: cachix/cachix-action@v10
+      - uses: cachix/cachix-action@v12
         with:
           name: coq-community
           authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
           extraPullNames: coq, math-comp
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
         with:
           ref: ${{ env.tested_commit }}
       - run: >

README.md

@@ -39,7 +39,7 @@ Also includes a constructive proof of Dickson's lemma.
 - Coq-community maintainer(s):
   - Karl Palmskog ([**@palmskog**](https://github.com/palmskog))
 - License: [GNU Lesser General Public License v2.1 or later](LICENSE)
-- Compatible Coq versions: 8.16 or later
+- Compatible Coq versions: 8.17 or later
 - Additional dependencies: none
 - Coq namespace: `Buchberger`
 - Related publication(s):

coq-buchberger.opam

@@ -19,7 +19,7 @@ Also includes a constructive proof of Dickson's lemma."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.16" & < "8.17~") | (= "dev")}
+  "coq" {>= "8.17"}
 ]
 
 tags: [

meta.yml

@@ -43,15 +43,16 @@ license:
   identifier: LGPL-2.1-or-later
 
 supported_coq_versions:
-  text: 8.16 or later
-  opam: '{(>= "8.16" & < "8.17~") | (= "dev")}'
+  text: 8.17 or later
+  opam: '{>= "8.17"}'
 
 tested_coq_nix_versions:
 - coq_version: 'master'
 
 tested_coq_opam_versions:
 - version: dev
-- version: '8.16'
+- version: '8.18'
+- version: '8.17'
 
 namespace: Buchberger
 

theories/BuchRed.v

@@ -709,7 +709,7 @@ Proof.
 unfold Red in |- *.
 intros L p H'.
 generalize (redacc_cb L nil); simpl in |- *; auto.
-rewrite <- app_nil_end; auto.
+rewrite app_nil_r; auto.
 Qed.
 
 Theorem cb_redacc :
@@ -784,7 +784,7 @@ Proof.
 intros L p H'.
 lapply (cb_redacc L nil p); [ intros H'3; generalize H'3 | idtac ];
  simpl in |- *; auto.
-rewrite <- app_nil_end; auto.
+rewrite app_nil_r; auto.
 Qed.
 
 Theorem cb_Red_cb1 :
@@ -923,8 +923,8 @@ Proof.
 intros L p H' H'0.
 lapply (redacc_divp L nil p); auto.
 simpl in |- *; auto.
-rewrite <- app_nil_end; auto.
-rewrite <- app_nil_end; auto.
+rewrite app_nil_r; auto.
+rewrite app_nil_r; auto.
 Qed.
 
 Theorem Red_grobner :

theories/Fred.v

@@ -123,7 +123,7 @@ Proof.
 unfold red in |- *.
 intros L p H'.
 generalize (redacc_cb L nil); simpl in |- *; auto.
-rewrite <- app_nil_end; auto.
+rewrite app_nil_r; auto.
 Qed.
 
 Theorem cb_redacc :
@@ -164,7 +164,7 @@ Proof.
 intros L p H'.
 lapply (cb_redacc L nil p); [ intros H'3; generalize H'3 | idtac ];
  simpl in |- *; auto.
-rewrite <- app_nil_end; auto.
+rewrite app_nil_r; auto.
 Qed.
 
 Theorem cb_red_cb1 :
@@ -267,8 +267,8 @@ Proof.
 intros L p H' H'0.
 lapply (redacc_divp L nil p); auto.
 simpl in |- *; auto.
-rewrite <- app_nil_end; auto.
-rewrite <- app_nil_end; auto.
+rewrite app_nil_r; auto.
+rewrite app_nil_r; auto.
 Qed.
 
 Theorem red_grobner : forall L : list poly, grobner L -> grobner (red L).

theories/POrder.v

@@ -185,7 +185,6 @@ Local Hint Resolve olistOne : core.
 Theorem olistO : olist pO.
 Proof.
 unfold olist, ltT in |- *; simpl in |- *; auto.
-red in |- *; unfold nilA in |- *; apply d_nil.
 Qed.
 
 Lemma app2_inv :
@@ -249,7 +248,7 @@ intros H'2 H'3 H'4;
 generalize (olist_ltT (pX b0 (pX b l2))); unfold olist, ltT in |- *;
  intros H'5; apply H'5.
 rewrite (fP_app (pX b0 (pX b l2)) (pX x1 (pX x pO))); simpl in |- *; auto.
-generalize (app_ass (fP l2) (consA (T2M x1) nilA) (consA (T2M x) nilA));
+generalize (sym_eq (app_assoc (fP l2) (consA (T2M x1) nilA) (consA (T2M x) nilA)));
  simpl in |- *; auto; unfold consA in |- *.
 intros H'6; rewrite <- H'6; simpl in |- *; auto.
 simpl in |- *; apply H'3; auto; apply (desc_prefix _ ltM) with (a := T2M x);

theories/Pmults.v

@@ -428,24 +428,12 @@ intros p0; case p0; simpl in |- *; auto.
 intros q0 H' a H'0 H'1 H'2.
 apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := mults a q0); auto.
 apply mults_comp; auto.
-change
-  (eqP A eqA n
-     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
-        (pO A n) q0) q0) in |- *; auto.
-change
-  (eqP A eqA n (mults a q0)
-     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
-        (pO A n) (mults a q0))) in |- *; auto.
 apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto.
 intros a l q0.
 case q0; simpl in |- *; auto.
 intros H' a0 H'0 H'1 H'2.
 apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := mults a0 (pX a l)); auto.
 apply mults_comp; auto.
-change
-  (eqP A eqA n
-     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
-        (pX a l) (pO A n)) (pX a l)) in |- *; auto.
 change
   (eqP A eqA n (mults a0 (pX a l))
      (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec

theories/Preduceplus.v

@@ -884,17 +884,6 @@ apply
 apply reduce_imp_reduceplus; auto.
 apply reducetop with (b := b) (nZb := nZb) (q := q); auto.
 apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto.
-change
-  (eqP A eqA n
-     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
-        (pX a p) (pO A n)) (pX a p)) in |- *; auto.
-change
-  (reduceplus Q
-     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
-        (spminusf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec a
-           b nZb p q) (pO A n))
-     (spminusf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec a b
-        nZb p q)) in |- *; auto.
 clear r; intros c r H' H'0 a b nZb p q H'1 H'2 H'3.
 cut (canonical A0 eqA ltM p);
  [ intros C0 | apply canonical_imp_canonical with (a := a); auto ].
@@ -956,10 +945,6 @@ apply eqp_imp_canonical with (1 := cs) (p := pX c r); auto.
 apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto.
 apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pX c r); auto.
 apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto.
-change
-  (eqP A eqA n
-     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
-        (pO A n) (pX c r)) (pX c r)) in |- *; auto.
 intros t l H' H'5.
 change
   (reduceplus Q
@@ -1142,17 +1127,9 @@ elim r; auto.
 intros H'4; exists (pX a q); split; auto.
 apply reduceplus_eqp_com with (p := pX a p) (q := pX a q); auto.
 apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto.
-change
-  (eqP A eqA n
-     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
-        (pX a p) (pO A n)) (pX a p)) in |- *; auto.
 apply reduceplus_eqp_com with (p := pX a q) (q := pX a q); auto.
 apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pX b q); auto.
 apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto.
-change
-  (eqP A eqA n
-     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
-        (pX b q) (pO A n)) (pX b q)) in |- *; auto.
 clear r; intros c r H'4 H'5.
 cut (canonical A0 eqA ltM r);
  [ intros C3 | apply canonical_imp_canonical with (a := c); auto ].

theories/Relation_Operators_compat.v

@@ -197,7 +197,7 @@ Section Wf_Lexicographic_Exponentiation.
           Descl x0 /\ Descl y0).
 
     intro.
-    generalize (app_nil_end x1); simple induction 1; simple induction 1.
+    generalize (sym_eq (app_nil_r x1)); simple induction 1; simple induction 1.
     split. apply d_conc; auto with sets.
 
     apply d_nil.
@@ -219,15 +219,15 @@ Section Wf_Lexicographic_Exponentiation.
 
     apply d_one.
     do 5 intro.
-    generalize (app_ass x4 (l1 ++ Cons x2 Nil) (Cons x3 Nil)).
+    generalize (sym_eq (app_assoc x4 (l1 ++ Cons x2 Nil) (Cons x3 Nil))).
     simple induction 1.
-    generalize (app_ass x4 l1 (Cons x2 Nil)); simple induction 1.
+    generalize (sym_eq (app_assoc x4 l1 (Cons x2 Nil))); simple induction 1.
     intro E.
     generalize (app_inj_tail _ _ _ _ E).
     simple induction 1; intros.
     generalize (app_inj_tail _ _ _ _ H6); simple induction 1; intros.
     rewrite <- H7; rewrite <- H10; generalize H6.
-    generalize (app_ass x4 l1 (Cons x2 Nil)); intro E1.
+    generalize (sym_eq (app_assoc x4 l1 (Cons x2 Nil))); intro E1.
     rewrite E1.
     intro.
     generalize (Hind x4 (l1 ++ Cons x2 Nil) H11).
@@ -344,7 +344,7 @@ Section Wf_Lexicographic_Exponentiation.
         forall y1:Descl (l ++ x3),
           ltl x3 (Cons x1 Nil) -> Acc Lex_Exp << l ++ x3, y1 >>).
     intros.
-    generalize (app_nil_end l); intros Heq.
+    generalize (sym_eq (app_nil_r l)); intros Heq.
     generalize y1.
     clear y1.
     rewrite <- Heq.
@@ -361,7 +361,7 @@ Section Wf_Lexicographic_Exponentiation.
     intros.
     generalize (desc_end x4 x1 l0 (conj H8 H5)); intros.
     generalize y1.
-    rewrite <- (app_ass l l0 (Cons x4 Nil)); intro.
+    rewrite (app_assoc l l0 (Cons x4 Nil)); intro.
     generalize (HInd x4 H9 (l ++ l0)); intros HInd2.
     generalize (ltl_unit l0 x4 x1 H8 H5); intro.
     generalize (dist_Desc_concat (l ++ l0) (Cons x4 Nil) y2).

theories/WfR0.v

@@ -120,7 +120,7 @@ case H'2; auto.
 intros l H' H'0 bs Heq Hnz H'1; auto.
 apply Acc_intro; auto.
 intros y H'2; inversion H'2; auto.
-rewrite <- ass_app.
+rewrite <- app_assoc.
 change
   (Acc RO
      (cs1 ++