Port to Hierarchy Builder

.github/workflows/docker-action.yml

@@ -17,14 +17,14 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.16.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.14'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.16'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-bits.opam'

README.md

@@ -10,8 +10,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![Zulip][zulip-shield]][zulip-link]
 [![DOI][doi-shield]][doi-link]
 
-[docker-action-shield]: https://github.com/coq-community/bits/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/coq-community/bits/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/bits/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/bits/actions/workflows/docker-action.yml
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
@@ -38,11 +38,10 @@ axiomatization and extraction to OCaml native integers.
 - Coq-community maintainer(s):
   - Anton Trunov ([**@anton-trunov**](https://github.com/anton-trunov))
 - License: [Apache License 2.0](LICENSE)
-- Compatible Coq versions: 8.10 or later (use releases for other Coq versions)
-- Compatible OCaml versions: 4.05 or later (not tested on previous versions)
+- Compatible Coq versions: 8.16 or later (use releases for other Coq versions)
 - Additional dependencies:
   - OCamlbuild
-  - [MathComp](https://math-comp.github.io) 1.12.0 or later (`algebra` suffices)
+  - [MathComp](https://math-comp.github.io) 2.0 or later (`algebra` suffices)
 - Coq namespace: `Bits`
 - Related publication(s):
   - [From Sets to Bits in Coq](https://hal.archives-ouvertes.fr/hal-01251943/document) doi:[10.1007/978-3-319-29604-3_2](https://doi.org/10.1007/978-3-319-29604-3_2)

coq-bits.opam

@@ -18,10 +18,9 @@ axiomatization and extraction to OCaml native integers."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "ocaml" {(>= "4.05" & < "4.15~")}
-  "coq" {(>= "8.14" & < "8.18~")}
+  "coq" {(>= "8.16" & < "8.19~")}
   "ocamlbuild" 
-  "coq-mathcomp-algebra" {(>= "1.12" & < "1.17~")}
+  "coq-mathcomp-algebra" {(>= "2.0" & < "2.2~")}
 ]
 
 tags: [

meta.yml

@@ -46,28 +46,20 @@ license:
   identifier: Apache-2.0
   file: LICENSE
 
-supported_ocaml_versions:
-  text: 4.05 or later (not tested on previous versions)
-  opam: '{(>= "4.05" & < "4.15~")}'
-
 supported_coq_versions:
-  text: 8.10 or later (use releases for other Coq versions)
-  opam: '{(>= "8.10" & < "8.17~")}'
+  text: 8.16 or later (use releases for other Coq versions)
+  opam: '{(>= "8.16" & < "8.19~")}'
 
 tested_coq_opam_versions:
-- version: '1.15.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.15'
-  repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.14'
+- version: '2.1.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-8.13'
+- version: '2.0.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-8.12'
+- version: '2.1.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-8.11'
+- version: '2.1.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-8.10'
+- version: '2.0.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
 
 dependencies:
@@ -76,9 +68,9 @@ dependencies:
   description: OCamlbuild
 - opam:
     name: coq-mathcomp-algebra
-    version: '{(>= "1.12" & < "1.16~")}'
+    version: '{(>= "2.0" & < "2.2~")}'
   description: |-
-    [MathComp](https://math-comp.github.io) 1.12.0 or later (`algebra` suffices)
+    [MathComp](https://math-comp.github.io) 2.0 or later (`algebra` suffices)
 
 namespace: Bits
 

src/spec/operations/properties.v

@@ -1,6 +1,7 @@
  (*===========================================================================
   Proofs of properties of arithmetic and logical operations on n-bit words
   ===========================================================================*)
+From HB Require Import structures.
 Require Import mathcomp.ssreflect.ssreflect.
 
 From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div.
@@ -1196,22 +1197,27 @@
 case E: (splitmsb (adcBmain true p1 p2)) => [carry' p'].
 destruct b2.
 (* b2 = true *)
-rewrite beheadCons theadCons E in H. inversion H. apply val_inj in H3. subst.
+rewrite beheadCons theadCons E in H. inversion H.
+rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst.
 rewrite IHn; first by rewrite orTb. done.
 (* b2 = false *)
-rewrite beheadCons E in H. inversion H. apply val_inj in H3. subst.
+rewrite beheadCons E in H. inversion H.
+rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst.
 rewrite IHn; first by rewrite orTb. done.
 (* b1 = false *)
 destruct b2.
 (* b2 = true *)
 specialize (IHn true p1 p2).
 case E: (splitmsb (adcBmain true p1 p2)) => [carry' p'].
-rewrite beheadCons E in H. inversion H. apply val_inj in H3. subst.
+rewrite beheadCons E in H. inversion H.
+rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst.
 rewrite IHn; first by rewrite orTb. done.
 (* b2 = false *)
 specialize (IHn false p1 p2).
 case E: (splitmsb (adcBmain false p1 p2)) => [carry' p'].
-rewrite beheadCons E in H. inversion H. apply val_inj in H3. subst. simpl.
+rewrite beheadCons E in H. inversion H.
+rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3.
+subst. simpl.
 rewrite /leB in IHn. rewrite !andbT. by rewrite IHn.
 
 (* c = false *)
@@ -1222,26 +1228,30 @@
 (* b2 = true *)
 specialize (IHn true p1 p2).
 case E: (splitmsb (adcBmain true p1 p2)) => [carry' p'].
-rewrite beheadCons E in H. inversion H. apply val_inj in H3. subst.
+rewrite beheadCons E in H. inversion H.
+rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst.
 specialize (IHn _ E). rewrite /leB. simpl. rewrite !beheadCons. by rewrite IHn.
 (* b2 = false *)
 specialize (IHn false p1 p2).
 case E: (splitmsb (adcBmain false p1 p2)) => [carry' p'].
-rewrite beheadCons E in H. inversion H. apply val_inj in H3. subst.
+rewrite beheadCons E in H. inversion H.
+rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst.
 rewrite /leB. simpl. rewrite !beheadCons. specialize (IHn _ E).
 rewrite /leB in IHn. rewrite andbF. rewrite orbF. done.
 (* b1 = false *)
 specialize (IHn false p1 p2). destruct b2.
 (* b2 = true *)
 case E: (splitmsb (adcBmain false p1 p2)) => [carry' p'].
-rewrite beheadCons E in H. inversion H. apply val_inj in H3. subst.
+rewrite beheadCons E in H. inversion H.
+rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst.
 rewrite /leB.
 simpl. rewrite !beheadCons !theadCons.
 rewrite /leB in IHn. specialize (IHn _ E). rewrite orbA. rewrite orbF.
 rewrite orbA. rewrite orbF. rewrite IHn. done.
 (* b2 = false *)
 case E: (splitmsb (adcBmain false p1 p2)) => [carry' p'].
-rewrite beheadCons E in H. inversion H. apply val_inj in H3. subst.
+rewrite beheadCons E in H. inversion H.
+rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst.
 rewrite /leB. simpl.
 rewrite !beheadCons !theadCons. specialize (IHn _ E).
 rewrite /leB in IHn. rewrite andbT. rewrite andbF. rewrite orbF.
@@ -1962,13 +1972,11 @@
 
 Variable n:nat.
 
-Definition BITS_zmodMixin := ZmodMixin (@addBA n) (@addBC n) (@add0B n) (@addBN n).
-Canonical Structure BITS_zmodType := Eval hnf in ZmodType (BITS n) BITS_zmodMixin.
-Canonical Structure BITS_finZmodType := Eval hnf in [finZmodType of BITS n].
-Canonical Structure BITS_baseFinGroupType :=
-  Eval hnf in [baseFinGroupType of (BITS n) for +%R].
-Canonical Structure BITS_finGroupType :=
-  Eval hnf in [finGroupType of  (BITS n) for +%R].
+HB.instance Definition _ := Finite.copy (BITS n) [finType of BITS n].
+HB.instance Definition _ := GRing.isZmodule.Build (BITS n)
+  (@addBA n) (@addBC n) (@add0B n) (@addBN n).
+HB.instance Definition _ := isMulGroup.Build (BITS n)
+  (@addBA n) (@add0B n) (@addBN n).
 
 End Structures.