Merge pull request #25 from Tragicus/pr2216

apply val_inj early

.github/workflows/docker-action.yml

@@ -24,7 +24,6 @@ jobs:
           - 'mathcomp/mathcomp:2.2.0-coq-8.16'
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.2.0-coq-dev'
-          - 'mathcomp/mathcomp-dev:coq-8.17'
           - 'mathcomp/mathcomp-dev:coq-8.19'
           - 'mathcomp/mathcomp-dev:coq-dev'
       fail-fast: false

coq-bits.opam

@@ -18,9 +18,9 @@ axiomatization and extraction to OCaml native integers."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.16" & < "8.20~") | (= "dev")}
+  "coq" {>= "8.16"}
   "ocamlbuild" 
-  "coq-mathcomp-algebra" {(>= "2.0" & < "2.3~") | (= "dev")}
+  "coq-mathcomp-algebra" {>= "2.0"}
 ]
 
 tags: [

meta.yml

@@ -48,7 +48,7 @@ license:
 
 supported_coq_versions:
   text: 8.16 or later (use releases for other Coq versions)
-  opam: '{(>= "8.16" & < "8.20~") | (= "dev")}'
+  opam: '{>= "8.16"}'
 
 tested_coq_opam_versions:
 - version: '2.0.0-coq-8.16'
@@ -65,8 +65,6 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-dev'
   repo: 'mathcomp/mathcomp'
-- version: 'coq-8.17'
-  repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.19'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-dev'
@@ -78,7 +76,7 @@ dependencies:
   description: OCamlbuild
 - opam:
     name: coq-mathcomp-algebra
-    version: '{(>= "2.0" & < "2.3~") | (= "dev")}'
+    version: '{>= "2.0"}'
   description: |-
     [MathComp](https://math-comp.github.io) 2.0 or later (`algebra` suffices)
 

src/spec/operations/properties.v

@@ -1455,8 +1455,8 @@ by rewrite -C splitmsbK.
 Qed.
 
 Lemma toZp_shlBaux n (p: BITS n) : toZp (shlBaux p) = (toZpAux p * 2%:R)%R.
-Proof. destruct n. by rewrite (tuple0 p).
-apply val_inj.
+Proof.
+apply/val_inj; destruct n. by rewrite (tuple0 p).
 rewrite /toZp toNat_shlBaux. rewrite /=Zp_cast; last apply pow2_gt1.
 rewrite modn_small.
 rewrite (@modn_small 1); last apply pow2_gt1.
@@ -1473,15 +1473,15 @@ rewrite expnS mul2n. rewrite ltn_double. apply toNatBounded.
 Qed.
 
 Lemma toZp_shlB n (p: BITS n) : toZp (shlB p) = (toZp p * 2%:R)%R.
-Proof. destruct n. by rewrite (tuple0 p).
+Proof. apply/val_inj; destruct n. by rewrite (tuple0 p).
 
 destruct n.
 case/tupleP: p => [b p].
 rewrite (tuple0 p). by destruct b.
 
 rewrite /shlB.  rewrite toZp_dropmsb /toZpAux.
 rewrite toNat_shlBaux. rewrite /toZp.
-apply val_inj. rewrite /=Zp_cast.
+rewrite /=Zp_cast.
 rewrite (@modn_small 1); last apply pow2_gt1.
 rewrite (@modn_small (toNat p)); last apply toNatBounded.
 rewrite addnn.
@@ -1810,7 +1810,8 @@ done. apply expn_gt0.
 Qed.
 
 Lemma toZp_mulB n (p1 p2: BITS n) : toZp (mulB p1 p2) = (toZp p1 * toZp p2)%R.
-Proof. destruct n. by rewrite (tuple0 p1) (tuple0 p2).
+Proof.
+destruct n; first by rewrite (tuple0 p1) (tuple0 p2); apply/val_inj.
 rewrite /mulB/toZp. rewrite toNat_low. rewrite toNat_fullmulB.
 rewrite modZp_pow. rewrite -!Zp_nat. by rewrite !natrM.
 Qed.