add Zmod, including Bits and minimal Zstar (#144)

Author: andres-erbsen

.nix/rocq-overlays/stdlib-subcomponents/default.nix

@@ -25,6 +25,7 @@ let
     "strings" = [ "arith" ];
     "lia" = [ "arith" "narith" ];
     "zarith" = [ "lia" ];
+    "zmod" = [ "zarith" "sorting" "field" ];
     "qarith-base" = [ "ring" ];
     "field" = [ "zarith" ];
     "lqa" = [ "field" "qarith-base" ];
@@ -47,7 +48,7 @@ let
     "wellfounded" = [ "lists" ];
     "streams" = [ "logic" ];
     "rtauto" = [ "positive" "lists" ];
-    "compat" = [ "rtauto" "fmaps-fsets-msets" "funind" "extraction" "reals" "wellfounded" "streams" ];
+    "compat" = [ "rtauto" "fmaps-fsets-msets" "funind" "extraction" "reals" "zmod" "wellfounded" "streams" ];
     "all" = [ "compat" ];
   };
 

doc/changelog/02-added/144-Zmod.rst

@@ -0,0 +1,8 @@
+- in `Zmod.v`
+
+  + Added theory of modular integer arithmetic, including machine words /
+    bitvectors and the multiplicative group of integers modulo another integer.
+    About 450 lemmas are provided
+    (`#144 <https://github.com/coq/stdlib/pull/144>`_,
+    by Andres Erbsen).
+

doc/stdlib/depends.dot

@@ -19,6 +19,9 @@ digraph stdlib_deps {
 	reals -> nsatz;
 	"arith-base" -> structures;
 	zarith -> lia;
+	zmod -> zarith;
+	zmod -> sorting;
+	zmod -> field;
 	qarith -> lqa;
 	positive -> "arith-base";
 	narith -> ring;
@@ -62,6 +65,7 @@ digraph stdlib_deps {
 	funind -> "arith-base";
 	rtauto -> positive;
 	rtauto -> lists;
+	compat -> zmod;
 	compat -> reals;
 	compat -> "fmaps-fsets-msets";
 	compat -> wellfounded;

doc/stdlib/index-list.html.template

@@ -307,6 +307,22 @@ through the <tt>From Stdlib Require Import</tt> command.</p>
     theories/Numbers/HexadecimalZ.v
   </dd>
 
+  <dt> <a name="zmod"></a><b>Zmod and Zstar</b>:
+    Modular arithmetic -- integers modulo another integer -- including machine
+    words (bitvectors) and the multiplicative group of integers modulo another
+    integer.
+  </dt>
+  <dd>
+    theories/Zmod/Zmod.v
+    theories/Zmod/Bits.v
+    theories/Zmod/Zstar.v
+    (theories/Zmod/ZmodDef.v)
+    (theories/Zmod/ZstarDef.v)
+    (theories/Zmod/ZmodBase.v)
+    (theories/Zmod/ZstarBase.v)
+    (theories/Zmod/ZmodInv.v)
+  </dd>
+
   <dt> <a name="unicode"></a><b>Unicode</b>:
     Unicode-based alternative notations
   </dt>

theories/All/All.v

@@ -567,3 +567,11 @@ From Stdlib Require Export Arith.PeanoNat.
 From Stdlib Require Export Arith.Peano_dec.
 From Stdlib Require Export Arith.Wf_nat.
 From Stdlib Require Export Arith.Zerob.
+From Stdlib Require Export Zmod.Zmod.
+From Stdlib Require Export Zmod.ZmodDef.
+From Stdlib Require Export Zmod.ZmodBase.
+From Stdlib Require Export Zmod.ZmodInv.
+From Stdlib Require Export Zmod.Zstar.
+From Stdlib Require Export Zmod.ZstarDef.
+From Stdlib Require Export Zmod.ZstarBase.
+From Stdlib Require Export Zmod.Bits.

theories/Make.zmod

@@ -0,0 +1,10 @@
+Zmod/Bits.v
+Zmod/Zmod.v
+Zmod/ZmodBase.v
+Zmod/ZmodDef.v
+Zmod/ZmodInv.v
+Zmod/Zstar.v
+Zmod/ZstarBase.v
+Zmod/ZstarDef.v
+
+-Q Zmod Stdlib.Zmod