Skip to content

Commit

Permalink
Merge pull request #20 from coq-community/hierarchy-builder
Browse files Browse the repository at this point in the history
Port to Hierarchy Builder
  • Loading branch information
proux01 authored Dec 7, 2023
2 parents acaa128 + da24ef2 commit 64ae535
Show file tree
Hide file tree
Showing 5 changed files with 44 additions and 46 deletions.
12 changes: 6 additions & 6 deletions .github/workflows/docker-action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand Down
9 changes: 4 additions & 5 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)
Expand Down
5 changes: 2 additions & 3 deletions coq-bits.opam
Original file line number Diff line number Diff line change
Expand Up @@ -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: [
Expand Down
26 changes: 9 additions & 17 deletions meta.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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

Expand Down
38 changes: 23 additions & 15 deletions src/spec/operations/properties.v
Original file line number Diff line number Diff line change
@@ -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.
Expand Down Expand Up @@ -1196,22 +1197,27 @@ specialize (IHn true p1 p2).
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 *)
Expand All @@ -1222,26 +1228,30 @@ 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.
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.
Expand Down Expand Up @@ -1962,13 +1972,11 @@ Section Structures.

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].

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18)

Notation "[ finType of _ ]" is deprecated since mathcomp 2.0.0.

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18)

Ignoring canonical projection to isCountable.pickleK by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18)

Ignoring canonical projection to isCountable.unpickle by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18)

Ignoring canonical projection to isCountable.pickle by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18)

Ignoring canonical projection to inj_eqAxiom by hasDecEq.eqP in

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18)

Ignoring canonical projection to eq_op by hasDecEq.eq_op in

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18)

Ignoring canonical projection to FinTuple.enumP by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18)

Ignoring canonical projection to FinTuple.enum by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.18)

Notation "[ finType of _ ]" is deprecated since mathcomp 2.0.0.

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.18)

Ignoring canonical projection to isCountable.pickleK by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.18)

Ignoring canonical projection to isCountable.unpickle by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.18)

Ignoring canonical projection to isCountable.pickle by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.18)

Ignoring canonical projection to inj_eqAxiom by hasDecEq.eqP in

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.18)

Ignoring canonical projection to eq_op by hasDecEq.eq_op in

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.18)

Ignoring canonical projection to FinTuple.enumP by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.18)

Ignoring canonical projection to FinTuple.enum by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.17)

Notation "[ finType of _ ]" is deprecated since mathcomp 2.0.0.

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.17)

Ignoring canonical projection to isCountable.pickleK by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.17)

Ignoring canonical projection to isCountable.unpickle by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.17)

Ignoring canonical projection to isCountable.pickle by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.17)

Ignoring canonical projection to inj_eqAxiom by hasDecEq.eqP in

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.17)

Ignoring canonical projection to eq_op by hasDecEq.eq_op in

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.17)

Ignoring canonical projection to FinTuple.enumP by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.17)

Ignoring canonical projection to FinTuple.enum by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.16)

Notation "[ finType of _ ]" is deprecated since mathcomp 2.0.0.

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.16)

Ignoring canonical projection to isCountable.pickleK by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.16)

Ignoring canonical projection to isCountable.unpickle by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.16)

Ignoring canonical projection to isCountable.pickle by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.16)

Ignoring canonical projection to inj_eqAxiom by hasDecEq.eqP in

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.16)

Ignoring canonical projection to eq_op by hasDecEq.eq_op in

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.16)

Ignoring canonical projection to FinTuple.enumP by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.16)

Ignoring canonical projection to FinTuple.enum by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.16)

Notation "[ finType of _ ]" is deprecated since mathcomp 2.0.0.

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.16)

Ignoring canonical projection to isCountable.pickleK by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.16)

Ignoring canonical projection to isCountable.unpickle by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.16)

Ignoring canonical projection to isCountable.pickle by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.16)

Ignoring canonical projection to inj_eqAxiom by hasDecEq.eqP in

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.16)

Ignoring canonical projection to eq_op by hasDecEq.eq_op in

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.16)

Ignoring canonical projection to FinTuple.enumP by

Check warning on line 1975 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.16)

Ignoring canonical projection to FinTuple.enum by
HB.instance Definition _ := GRing.isZmodule.Build (BITS n)

Check warning on line 1976 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.17)

Ignoring canonical projection to GRing.isZmodule.addNr by

Check warning on line 1976 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.17)

Ignoring canonical projection to GRing.isZmodule.opp by

Check warning on line 1976 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.16)

Ignoring canonical projection to GRing.isZmodule.addNr by

Check warning on line 1976 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.16)

Ignoring canonical projection to GRing.isZmodule.opp by

Check warning on line 1976 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.16)

Ignoring canonical projection to GRing.isZmodule.addNr by

Check warning on line 1976 in src/spec/operations/properties.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.16)

Ignoring canonical projection to GRing.isZmodule.opp by
(@addBA n) (@addBC n) (@add0B n) (@addBN n).
HB.instance Definition _ := isMulGroup.Build (BITS n)
(@addBA n) (@add0B n) (@addBN n).

End Structures.

Expand Down

0 comments on commit 64ae535

Please sign in to comment.