[RFC WIP] define modular arithmetic in theories/Numbers/Zmod.v

doc/stdlib/index-list.html.template

@@ -241,6 +241,22 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/HexadecimalString.v
     </dd>
 
+    <dt> <b>&nbsp;&nbsp;Zmod</b>:
+       Modular arithmetic.
+    </dt>
+    <dd>
+    theories/Numbers/Zmod.v
+    (theories/Numbers/Zmod/Base.v)
+    (theories/Numbers/Zmod/FastPow2.v)
+    (theories/Numbers/Zmod/Inverse.v)
+    (theories/Numbers/Zmod/LittleEndian.v)
+    (theories/Numbers/Zmod/Mask.v)
+    (theories/Numbers/Zmod/NonuniformDependent.v)
+    (theories/Numbers/Zmod/TODO_MOVE.v)
+    (theories/Numbers/Zstar/Base.v)
+    (theories/Numbers/Zstar/Fermat.v)
+    </dd>
+
     <dt> <b>&nbsp;&nbsp;NatInt</b>:
        Abstract mixed natural/integer/cyclic arithmetic
     </dt>

theories/Bool/Bool.v

@@ -8,6 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+Require Import Coq.Logic.HLevelsDef.
 Require Import DecidableClass.
 
 (** The type [bool] is defined in the prelude as
@@ -31,6 +32,15 @@ Definition Is_true (b:bool) :=
     | false => False
   end.
 
+Lemma Is_true_hprop b : IsHProp (Is_true b).
+Proof. destruct b; auto using true_hprop, false_hprop. Qed.
+
+Definition transparent_true (b : bool) : (True -> Is_true b) -> Is_true b :=
+  match b with
+  | true => fun _ => I
+  | false => fun H => False_rect _ (H I)
+  end.
+
 (*******************)
 (** * Decidability *)
 (*******************)

theories/Lists/List.v

@@ -360,6 +360,8 @@ Section Facts.
       right; unfold not; intros [Hc1| Hc2]; auto.
   Defined.
 
+  Lemma tl_length l : length (@tl A l) = pred (length l).
+  Proof. case l; trivial. Qed.
 End Facts.
 
 #[global]
@@ -1161,6 +1163,9 @@ Section Map.
     intros n l d H. now rewrite nth_error_map, H.
   Qed.
 
+  Lemma tl_map l : tl (map l) = map (tl l).
+  Proof. case l; trivial. Qed.
+
   Lemma map_app : forall l l',
     map (l++l') = (map l)++(map l').
   Proof.
@@ -1644,8 +1649,19 @@ End Fold_Right_Recursor.
   (*******************************)
 
   Section Filtering.
+
+    Lemma filter_map_comm A B f g l :
+      filter f (@map A B g l) = @map A B g (filter (fun a => f (g a)) l).
+    Proof. induction l; cbn [map filter]; auto. rewrite IHl; case f; auto. Qed.
+
     Variables (A : Type).
 
+    Lemma filter_true l : filter (fun _ : A => true) l = l.
+    Proof. induction l; cbn [filter]; congruence. Qed.
+
+    Lemma filter_false l : filter (fun _ : A => false) l = nil.
+    Proof. induction l; cbn [filter]; congruence. Qed.
+
     Lemma filter_ext_in : forall (f g : A -> bool) (l : list A),
       (forall a, In a l -> f a = g a) -> filter f l = filter g l.
     Proof.
@@ -2212,6 +2228,9 @@ Section Cutting.
   Lemma skipn_cons n a l: skipn (S n) (a::l) = skipn n l.
   Proof. reflexivity. Qed.
 
+  Lemma hd_error_skipn n : forall xs, hd_error (skipn n xs) = nth_error xs n.
+  Proof. induction n, xs; cbn [hd_error skipn nth_error]; auto. Qed.
+
   Lemma skipn_all : forall l, skipn (length l) l = nil.
   Proof. now intro l; induction l. Qed.
 
@@ -2777,6 +2796,22 @@ Section NatSeq.
    rewrite Nat.add_succ_r, Nat.add_0_r; reflexivity.
   Qed.
 
+  Lemma skipn_seq n start len : skipn n (seq start len) = seq (start+n) (len-n).
+  Proof.
+    revert len; revert start; induction n, len;
+      cbn [skipn seq]; rewrite ?Nat.add_0_r, ?IHn; cbn [Nat.add]; auto.
+  Qed.
+
+  Lemma nth_error_seq n start len : nth_error (seq start len) n =
+    if Nat.ltb n len then Some (Nat.add start n) else None.
+  Proof.
+    rewrite <-hd_error_skipn, skipn_seq.
+    destruct (Nat.sub len n) eqn:?, (Nat.ltb_spec n len);
+    cbn [nth_error seq]; trivial (*; lia *).
+    { apply Nat.sub_0_le, Nat.le_ngt in Heqn0; intuition idtac. }
+    { apply Nat.sub_0_le in H; congruence. }
+  Qed.
+
 End NatSeq.
 
 Section Exists_Forall.

theories/Logic/FinFun.v

@@ -78,6 +78,14 @@ Proof.
  rewrite in_map_iff. intros (y & E & Y). apply Ij in E. now subst.
 Qed.
 
+Lemma Injective_map_NoDup_in A B (f:A->B) (l:list A) :
+  (forall x y, In x l -> In y l -> f x = f y -> x = y) -> NoDup l -> NoDup (map f l).
+Proof.
+ pose proof @in_cons. pose proof @in_eq.
+ intros Ij N; revert Ij; induction N; cbn [map]; constructor; auto.
+ rewrite in_map_iff. intros (y & E & Y). apply Ij in E; auto; congruence.
+Qed.
+
 Lemma Injective_list_carac A B (d:decidable_eq A)(f:A->B) :
   Injective f <-> (forall l, NoDup l -> NoDup (map f l)).
 Proof.

theories/Logic/HLevels.v

@@ -8,39 +8,12 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** The first three levels of homotopy type theory: homotopy propositions,
-    homotopy sets and homotopy one types. For more information,
-    https://github.com/HoTT/HoTT
-    and
-    https://homotopytypetheory.org/book
+Require Export Coq.Logic.HLevelsDef.
 
-    Univalence is not assumed here, and equality is Coq's usual inductive
-    type eq in sort Prop. This is a little different from HoTT, where
-    sort Prop does not exist and equality is directly in sort Type. *)
-
-
-(* It is almost impossible to prove that a type is a homotopy proposition
+(* It is rarely possible to prove that a type is a homotopy proposition
    without funext, so we assume it here. *)
 Require Import Coq.Logic.FunctionalExtensionality.
 
-(* A homotopy proposition is a type that has at most one element.
-   Its unique inhabitant, when it exists, is to be interpreted as the
-   proof of the homotopy proposition.
-   Homotopy propositions are therefore an alternative to the sort Prop,
-   to select which types represent mathematical propositions. *)
-Definition IsHProp (P : Type) : Prop
-  := forall p q : P, p = q.
-
-(* A homotopy set is a type such as each equality type x = y is a
-   homotopy proposition. For example, any type which equality is
-   decidable in sort Prop is a homotopy set, as shown in file
-   Coq.Logic.Eqdep_dec.v. *)
-Definition IsHSet (X : Type) : Prop
-  := forall (x y : X) (p q : x = y), p = q.
-
-Definition IsHOneType (X : Type) : Prop
-  := forall (x y : X) (p q : x = y) (r s : p = q), r = s.
-
 Lemma forall_hprop : forall (A : Type) (P : A -> Prop),
     (forall x:A, IsHProp (P x))
     -> IsHProp (forall x:A, P x).
@@ -49,83 +22,20 @@ Proof.
   intro x. apply H.
 Qed.
 
-(* Homotopy propositions are stable by conjunction, but not by disjunction,
-   which can have a proof by the left and another proof by the right. *)
-Lemma and_hprop : forall P Q : Prop,
-    IsHProp P -> IsHProp Q -> IsHProp (P /\ Q).
-Proof.
-  intros. intros p q. destruct p,q.
-  replace p0 with p.
-  - replace q0 with q.
-    + reflexivity.
-    + apply H0.
-  - apply H.
-Qed.
-
 Lemma impl_hprop : forall P Q : Prop,
     IsHProp Q -> IsHProp (P -> Q).
 Proof.
   intros P Q H p q. apply functional_extensionality.
   intros. apply H.
 Qed.
 
-Lemma false_hprop : IsHProp False.
-Proof.
-  intros p q. contradiction.
-Qed.
-
-Lemma true_hprop : IsHProp True.
-Proof.
-  intros p q. destruct p,q. reflexivity.
-Qed.
-
 (* All negations are homotopy propositions. *)
 Lemma not_hprop : forall P : Type, IsHProp (P -> False).
 Proof.
   intros P p q. apply functional_extensionality.
   intros. contradiction.
 Qed.
 
-(* Homotopy propositions are included in homotopy sets.
-   They are the first 2 levels of a cumulative hierarchy of types
-   indexed by the natural numbers. In homotopy type theory,
-   homotopy propositions are call (-1)-types and homotopy
-   sets 0-types. *)
-Lemma hset_hprop : forall X : Type,
-    IsHProp X -> IsHSet X.
-Proof.
-  intros X H.
-  assert (forall (x y z:X) (p : y = z), eq_trans (H x y) p = H x z).
-  { intros. unfold eq_trans, eq_ind. destruct p. reflexivity. }
-  assert (forall (x y z:X) (p : y = z),
-             p = eq_trans (eq_sym (H x y)) (H x z)).
-  { intros. rewrite <- (H0 x y z p). unfold eq_trans, eq_sym, eq_ind.
-    destruct p, (H x y). reflexivity. }
-  intros x y p q.
-  rewrite (H1 x x y p), (H1 x x y q). reflexivity.
-Qed.
-
-Lemma eq_trans_cancel : forall {X : Type} {x y z : X} (p : x = y) (q r : y = z),
-  (eq_trans p q = eq_trans p r) -> q = r.
-Proof.
-  intros. destruct p. simpl in H. destruct r.
-  simpl in H. rewrite eq_trans_refl_l in H. exact H.
-Qed.
-
-Lemma hset_hOneType : forall X : Type,
-    IsHSet X -> IsHOneType X.
-Proof.
-  intros X f x y p q.
-  pose (fun a => f x y p a) as g.
-  assert (forall a (r : q = a), eq_trans (g q) r = g a).
-  { intros. destruct a. subst q. reflexivity. }
-  intros r s. pose proof (H p (eq_sym r)).
-  pose proof (H p (eq_sym s)).
-  rewrite <- H1 in H0. apply eq_trans_cancel in H0.
-  rewrite <- eq_sym_involutive. rewrite <- (eq_sym_involutive r).
-  rewrite H0. reflexivity.
-Qed.
-
 (* "IsHProp X" sounds like a proposition, because it asserts
    a property of the type X. And indeed: *)
 Lemma hprop_hprop : forall X : Type,

theories/Logic/HLevelsDef.v

@@ -0,0 +1,100 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** The first three levels of homotopy type theory: homotopy propositions,
+    homotopy sets and homotopy one types. For more information,
+    https://github.com/HoTT/HoTT
+    and
+    https://homotopytypetheory.org/book
+
+    Univalence is not assumed here, and equality is Coq's usual inductive
+    type eq in sort Prop. This is a little different from HoTT, where
+    sort Prop does not exist and equality is directly in sort Type. *)
+
+(* A homotopy proposition is a type that has at most one element.
+   Its unique inhabitant, when it exists, is to be interpreted as the
+   proof of the homotopy proposition.
+   Homotopy propositions are therefore an alternative to the sort Prop,
+   to select which types represent mathematical propositions. *)
+Definition IsHProp (P : Type) : Prop
+  := forall p q : P, p = q.
+
+(* A homotopy set is a type such as each equality type x = y is a
+   homotopy proposition. For example, any type which equality is
+   decidable in sort Prop is a homotopy set, as shown in file
+   Coq.Logic.Eqdep_dec.v. *)
+Definition IsHSet (X : Type) : Prop
+  := forall (x y : X) (p q : x = y), p = q.
+
+Definition IsHOneType (X : Type) : Prop
+  := forall (x y : X) (p q : x = y) (r s : p = q), r = s.
+
+Lemma false_hprop : IsHProp False.
+Proof.
+  intros p q. contradiction.
+Qed.
+
+Lemma true_hprop : IsHProp True.
+Proof.
+  intros p q. destruct p,q. reflexivity.
+Qed.
+
+(* Homotopy propositions are stable by conjunction, but not by disjunction,
+   which can have a proof by the left and another proof by the right. *)
+Lemma and_hprop : forall P Q : Prop,
+    IsHProp P -> IsHProp Q -> IsHProp (P /\ Q).
+Proof.
+  intros. intros p q. destruct p,q.
+  replace p0 with p.
+  - replace q0 with q.
+    + reflexivity.
+    + apply H0.
+  - apply H.
+Qed.
+
+(* Homotopy propositions are included in homotopy sets.
+   They are the first 2 levels of a cumulative hierarchy of types
+   indexed by the natural numbers. In homotopy type theory,
+   homotopy propositions are call (-1)-types and homotopy
+   sets 0-types. *)
+Lemma hset_hprop : forall X : Type,
+    IsHProp X -> IsHSet X.
+Proof.
+  intros X H.
+  assert (forall (x y z:X) (p : y = z), eq_trans (H x y) p = H x z).
+  { intros. unfold eq_trans, eq_ind. destruct p. reflexivity. }
+  assert (forall (x y z:X) (p : y = z),
+             p = eq_trans (eq_sym (H x y)) (H x z)).
+  { intros. rewrite <- (H0 x y z p). unfold eq_trans, eq_sym, eq_ind.
+    destruct p, (H x y). reflexivity. }
+  intros x y p q.
+  rewrite (H1 x x y p), (H1 x x y q). reflexivity.
+Qed.
+
+Lemma eq_trans_cancel : forall {X : Type} {x y z : X} (p : x = y) (q r : y = z),
+  (eq_trans p q = eq_trans p r) -> q = r.
+Proof.
+  intros. destruct p. simpl in H. destruct r.
+  simpl in H. rewrite eq_trans_refl_l in H. exact H.
+Qed.
+
+Lemma hset_hOneType : forall X : Type,
+    IsHSet X -> IsHOneType X.
+Proof.
+  intros X f x y p q.
+  pose (fun a => f x y p a) as g.
+  assert (forall a (r : q = a), eq_trans (g q) r = g a).
+  { intros. destruct a. subst q. reflexivity. }
+  intros r s. pose proof (H p (eq_sym r)).
+  pose proof (H p (eq_sym s)).
+  rewrite <- H1 in H0. apply eq_trans_cancel in H0.
+  rewrite <- eq_sym_involutive. rewrite <- (eq_sym_involutive r).
+  rewrite H0. reflexivity.
+Qed.

theories/NArith/BinNat.v

@@ -1039,6 +1039,30 @@ Proof.
  intros; apply iter_ind; trivial.
 Qed.
 
+(** Properties of [iter_op] *)
+
+Lemma iter_op_0_r {A} op zero x : @N.iter_op A op zero x N0 = zero. Proof. trivial. Qed.
+
+Lemma iter_op_1_r {A} op zero x : @N.iter_op A op zero x (N.pos xH) = x. Proof. trivial. Qed.
+
+Lemma iter_op_succ_r {A} op zero x n
+  (opp_zero_r : x = op x zero)
+  (op_assoc  : forall x y z : A, op x (op y z) = op (op x y) z)
+  : @N.iter_op A op zero x (N.succ n) = op x (N.iter_op op zero x n).
+Proof. case n; cbn; auto using Pos.iter_op_succ. Qed.
+
+Lemma iter_op_add_r {A} op zero x n
+  (opp_zero_r : x = op x zero)
+  (op_assoc  : forall x y z : A, op x (op y z) = op (op x y) z)
+  : @N.iter_op A op zero x (N.succ n) = op x (N.iter_op op zero x n).
+Proof. induction n using N.peano_ind; cbn; rewrite ?iter_op_succ_r; auto. Qed.
+
+Lemma iter_op_correct {A} op zero x n
+  (opp_zero_r : x = op x zero)
+  (op_assoc  : forall x y z : A, op x (op y z) = op (op x y) z)
+  : @N.iter_op A op zero x n = N.iter n (op x) zero.
+Proof. case n; cbn; auto using Pos.iter_op_correct. Qed.
+
 End N.
 
 Bind Scope N_scope with N.t N.