From a64a7c8837a6d0e800faba38d3410fa64faea023 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 9 Aug 2022 20:39:11 +0200
Subject: [PATCH] Modules for `Pos` and `Nat`.

---
 stdpp/list.v         |  26 +--
 stdpp/list_numbers.v |   2 +-
 stdpp/numbers.v      | 463 ++++++++++++++++++++++---------------------
 stdpp/pmap.v         |  42 ++--
 stdpp/relations.v    |   2 +-
 5 files changed, 274 insertions(+), 261 deletions(-)

diff --git a/stdpp/list.v b/stdpp/list.v
index 2320e73e..9a084b61 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -406,7 +406,7 @@ for example used for the countable instance of lists and in namespaces.
 Fixpoint positives_flatten_go (xs : list positive) (acc : positive) : positive :=
   match xs with
   | [] => acc
-  | x :: xs => positives_flatten_go xs (acc~1~0 ++ Preverse (Pdup x))
+  | x :: xs => positives_flatten_go xs (acc~1~0 ++ Pos.reverse (Pos.dup x))
   end.
 
 (** Flatten a list of positives into a single positive by duplicating the bits
@@ -3355,7 +3355,7 @@ Section Forall2.
     { rewrite <-(resize_resize l m n) by done. by apply Forall2_resize. }
     intros. assert (n = length k); subst.
     { by rewrite <-(Forall2_length (resize n x l) k), resize_length. }
-    rewrite (nat_le_add_sub (length k) m), !resize_add,
+    rewrite (Nat.le_add_sub (length k) m), !resize_add,
       resize_all, drop_all, resize_nil by lia.
     auto using Forall2_app, Forall2_replicate_r,
       Forall_resize, Forall_drop, resize_length.
@@ -3368,7 +3368,7 @@ Section Forall2.
     { rewrite <-(resize_resize k m n) by done. by apply Forall2_resize. }
     assert (n = length l); subst.
     { by rewrite (Forall2_length l (resize n y k)), resize_length. }
-    rewrite (nat_le_add_sub (length l) m), !resize_add,
+    rewrite (Nat.le_add_sub (length l) m), !resize_add,
       resize_all, drop_all, resize_nil by lia.
     auto using Forall2_app, Forall2_replicate_l,
       Forall_resize, Forall_drop, resize_length.
@@ -3802,7 +3802,7 @@ Section find.
           naive_solver eauto using lookup_app_l_Some with lia. }
         apply list_find_Some. split_and!; [done..|].
         intros j z ??. eapply (Hleast (length l1 + j)); [|lia].
-        by rewrite lookup_app_r, nat_sub_add by lia.
+        by rewrite lookup_app_r, Nat.sub_add' by lia.
     - intros [(?&?&Hleast)%list_find_Some|(?&Hl1&(?&?&Hleast)%list_find_Some)].
       + apply list_find_Some. split_and!; [by auto using lookup_app_l_Some..|].
         assert (i < length l1) by eauto using lookup_lt_Some.
@@ -4844,7 +4844,8 @@ Global Instance TCForall_app {A} (P : A → Prop) xs ys :
   TCForall P xs → TCForall P ys → TCForall P (xs ++ ys).
 Proof. rewrite !TCForall_Forall. apply Forall_app_2. Qed.
 
-Lemma TCForall2_Forall2 {A B} (P : A → B → Prop) xs ys : TCForall2 P xs ys ↔ Forall2 P xs ys.
+Lemma TCForall2_Forall2 {A B} (P : A → B → Prop) xs ys :
+  TCForall2 P xs ys ↔ Forall2 P xs ys.
 Proof. split; induction 1; constructor; auto. Qed.
 
 Lemma TCExists_Exists {A} (P : A → Prop) l : TCExists P l ↔ Exists P l.
@@ -4866,16 +4867,16 @@ Section positives_flatten_unflatten.
   Qed.
 
   Lemma positives_unflatten_go_app p suffix xs acc :
-    positives_unflatten_go (suffix ++ Preverse (Pdup p)) xs acc =
+    positives_unflatten_go (suffix ++ Pos.reverse (Pos.dup p)) xs acc =
     positives_unflatten_go suffix xs (acc ++ p).
   Proof.
     revert suffix acc.
     induction p as [p IH|p IH|]; intros acc suffix; simpl.
-    - rewrite 2!Preverse_xI.
+    - rewrite 2!Pos.reverse_xI.
       rewrite 2!(assoc_L (++)).
       rewrite IH.
       reflexivity.
-    - rewrite 2!Preverse_xO.
+    - rewrite 2!Pos.reverse_xO.
       rewrite 2!(assoc_L (++)).
       rewrite IH.
       reflexivity.
@@ -4927,7 +4928,8 @@ Section positives_flatten_unflatten.
   Qed.
 
   Lemma positives_flatten_cons x xs :
-    positives_flatten (x :: xs) = 1~1~0 ++ Preverse (Pdup x) ++ positives_flatten xs.
+    positives_flatten (x :: xs)
+    = 1~1~0 ++ Pos.reverse (Pos.dup x) ++ positives_flatten xs.
   Proof.
     change (x :: xs) with ([x] ++ xs)%list.
     rewrite positives_flatten_app.
@@ -4953,9 +4955,9 @@ Section positives_flatten_unflatten.
     rewrite !positives_flatten_cons, !(assoc _); intros Hl.
     assert (xs = ys) as <- by eauto; clear IH; f_equal.
     apply (inj (.++ positives_flatten xs)) in Hl.
-    rewrite 2!Preverse_Pdup in Hl.
-    apply (Pdup_suffix_eq _ _ p1 p2) in Hl.
-    by apply (inj Preverse).
+    rewrite 2!Pos.reverse_dup in Hl.
+    apply (Pos.dup_suffix_eq _ _ p1 p2) in Hl.
+    by apply (inj Pos.reverse).
   Qed.
 End positives_flatten_unflatten.
 
diff --git a/stdpp/list_numbers.v b/stdpp/list_numbers.v
index b85189c7..90aae69f 100644
--- a/stdpp/list_numbers.v
+++ b/stdpp/list_numbers.v
@@ -264,7 +264,7 @@ Section mjoin.
     split; [|naive_solver].
     destruct 1 as (j'&l'&i'&?&?&Hj); decompose_Forall.
     assert (i' < length l') by eauto using lookup_lt_Some.
-    apply Nat_mul_split_l in Hj; naive_solver.
+    apply Nat.mul_split_l in Hj; naive_solver.
   Qed.
 End mjoin.
 
diff --git a/stdpp/numbers.v b/stdpp/numbers.v
index 91cec423..24a1cff5 100644
--- a/stdpp/numbers.v
+++ b/stdpp/numbers.v
@@ -14,7 +14,7 @@ Proof. solve_decision. Defined.
 Global Arguments Nat.sub !_ !_ / : assert.
 Global Arguments Nat.max : simpl nomatch.
 
-Typeclasses Opaque lt.
+Typeclasses Opaque Nat.lt.
 
 Reserved Notation "x ≤ y ≤ z" (at level 70, y at next level).
 Reserved Notation "x ≤ y < z" (at level 70, y at next level).
@@ -36,87 +36,92 @@ Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
 Infix "`max`" := Nat.max (at level 35) : nat_scope.
 Infix "`min`" := Nat.min (at level 35) : nat_scope.
 
-Global Instance nat_eq_dec: EqDecision nat := eq_nat_dec.
-Global Instance nat_le_dec: RelDecision le := le_dec.
-Global Instance nat_lt_dec: RelDecision lt := lt_dec.
-Global Instance nat_inhabited: Inhabited nat := populate 0%nat.
-Global Instance S_inj: Inj (=) (=) S.
-Proof. by injection 1. Qed.
-Global Instance nat_le_po: PartialOrder (≤).
-Proof. repeat split; repeat intro; auto with lia. Qed.
-Global Instance nat_le_total: Total (≤).
-Proof. repeat intro; lia. Qed.
-
-Global Instance nat_le_pi: ∀ x y : nat, ProofIrrel (x ≤ y).
-Proof.
-  assert (∀ x y (p : x ≤ y) y' (q : x ≤ y'),
-    y = y' → eq_dep nat (le x) y p y' q) as aux.
-  { fix FIX 3. intros x ? [|y p] ? [|y' q].
-    - done.
-    - clear FIX. intros; exfalso; auto with lia.
-    - clear FIX. intros; exfalso; auto with lia.
-    - injection 1. intros Hy. by case (FIX x y p y' q Hy). }
-  intros x y p q.
-  by apply (Eqdep_dec.eq_dep_eq_dec (λ x y, decide (x = y))), aux.
-Qed.
-Global Instance nat_lt_pi: ∀ x y : nat, ProofIrrel (x < y).
-Proof. unfold lt. apply _. Qed.
-
-Lemma nat_le_sum (x y : nat) : x ≤ y ↔ ∃ z, y = x + z.
-Proof. split; [exists (y - x); lia | intros [z ->]; lia]. Qed.
-
-(** [Arith.Minus.minus_plus] is deprecated starting in 8.16 *)
-Lemma nat_sub_add n m : n + m - n = m.
-Proof. lia. Qed.
-(** [Arith.Minus.le_plus_minus] is deprecated starting in 8.16 *)
-Lemma nat_le_add_sub n m : n ≤ m → m = n + (m - n).
-Proof. lia. Qed.
-
-Lemma Nat_lt_succ_succ n : n < S (S n).
-Proof. auto with arith. Qed.
-Lemma Nat_mul_split_l n x1 x2 y1 y2 :
-  x2 < n → y2 < n → x1 * n + x2 = y1 * n + y2 → x1 = y1 ∧ x2 = y2.
-Proof.
-  intros Hx2 Hy2 E. cut (x1 = y1); [intros; subst;lia |].
-  revert y1 E. induction x1; simpl; intros [|?]; simpl; auto with lia.
-Qed.
-Lemma Nat_mul_split_r n x1 x2 y1 y2 :
-  x1 < n → y1 < n → x1 + x2 * n = y1 + y2 * n → x1 = y1 ∧ x2 = y2.
-Proof. intros. destruct (Nat_mul_split_l n x2 x1 y2 y1); auto with lia. Qed.
-
 Notation lcm := Nat.lcm.
 Notation divide := Nat.divide.
 Notation "( x | y )" := (divide x y) : nat_scope.
-Global Instance Nat_divide_dec : RelDecision Nat.divide.
-Proof.
-  refine (λ x y, cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
-Defined.
-Global Instance: PartialOrder divide.
-Proof.
-  repeat split; try apply _. intros ??. apply Nat.divide_antisym_nonneg; lia.
-Qed.
-Global Hint Extern 0 (_ | _) => reflexivity : core.
-Lemma Nat_divide_ne_0 x y : (x | y) → y ≠ 0 → x ≠ 0.
-Proof. intros Hxy Hy ->. by apply Hy, Nat.divide_0_l. Qed.
-
-Lemma Nat_iter_S {A} n (f: A → A) x : Nat.iter (S n) f x = f (Nat.iter n f x).
-Proof. done. Qed.
-Lemma Nat_iter_S_r {A} n (f: A → A) x : Nat.iter (S n) f x = Nat.iter n f (f x).
-Proof. induction n; by f_equal/=. Qed.
-Lemma Nat_iter_add {A} n1 n2 (f : A → A) x :
-  Nat.iter (n1 + n2) f x = Nat.iter n1 f (Nat.iter n2 f x).
-Proof. induction n1; by f_equal/=. Qed.
-Lemma Nat_iter_mul {A} n1 n2 (f : A → A) x :
-  Nat.iter (n1 * n2) f x = Nat.iter n1 (Nat.iter n2 f) x.
-Proof.
-  intros. induction n1 as [|n1 IHn1]; [done|].
-  simpl. by rewrite Nat_iter_add, IHn1.
-Qed.
-
-Lemma Nat_iter_ind {A} (P : A → Prop) f x k :
-  P x → (∀ y, P y → P (f y)) → P (Nat.iter k f x).
-Proof. induction k; simpl; auto. Qed.
 
+Module Nat.
+  Global Instance eq_dec: EqDecision nat := eq_nat_dec.
+  Global Instance le_dec: RelDecision le := le_dec.
+  Global Instance lt_dec: RelDecision lt := lt_dec.
+  Global Instance inhabited: Inhabited nat := populate 0.
+
+  Global Instance succ_inj: Inj (=) (=) Nat.succ.
+  Proof. by injection 1. Qed.
+
+  Global Instance le_po: PartialOrder (≤).
+  Proof. repeat split; repeat intro; auto with lia. Qed.
+  Global Instance le_total: Total (≤).
+  Proof. repeat intro; lia. Qed.
+
+  Global Instance le_pi: ∀ x y : nat, ProofIrrel (x ≤ y).
+  Proof.
+    assert (∀ x y (p : x ≤ y) y' (q : x ≤ y'),
+      y = y' → eq_dep nat (le x) y p y' q) as aux.
+    { fix FIX 3. intros x ? [|y p] ? [|y' q].
+      - done.
+      - clear FIX. intros; exfalso; auto with lia.
+      - clear FIX. intros; exfalso; auto with lia.
+      - injection 1. intros Hy. by case (FIX x y p y' q Hy). }
+    intros x y p q.
+    by apply (Eqdep_dec.eq_dep_eq_dec (λ x y, decide (x = y))), aux.
+  Qed.
+  Global Instance lt_pi: ∀ x y : nat, ProofIrrel (x < y).
+  Proof. unfold lt. apply _. Qed.
+
+  Lemma le_sum (x y : nat) : x ≤ y ↔ ∃ z, y = x + z.
+  Proof. split; [exists (y - x); lia | intros [z ->]; lia]. Qed.
+
+  (** [Arith.Minus.minus_plus] is deprecated starting in 8.16 *)
+  Lemma sub_add' n m : n + m - n = m.
+  Proof. lia. Qed.
+  (** [Arith.Minus.le_plus_minus] is deprecated starting in 8.16 *)
+  Lemma le_add_sub n m : n ≤ m → m = n + (m - n).
+  Proof. lia. Qed.
+
+  Lemma lt_succ_succ n : n < S (S n).
+  Proof. auto with arith. Qed.
+  Lemma mul_split_l n x1 x2 y1 y2 :
+    x2 < n → y2 < n → x1 * n + x2 = y1 * n + y2 → x1 = y1 ∧ x2 = y2.
+  Proof.
+    intros Hx2 Hy2 E. cut (x1 = y1); [intros; subst;lia |].
+    revert y1 E. induction x1; simpl; intros [|?]; simpl; auto with lia.
+  Qed.
+  Lemma mul_split_r n x1 x2 y1 y2 :
+    x1 < n → y1 < n → x1 + x2 * n = y1 + y2 * n → x1 = y1 ∧ x2 = y2.
+  Proof. intros. destruct (mul_split_l n x2 x1 y2 y1); auto with lia. Qed.
+
+  Global Instance divide_dec : RelDecision Nat.divide.
+  Proof.
+    refine (λ x y, cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
+  Defined.
+  Global Instance divide_po : PartialOrder divide.
+  Proof.
+    repeat split; try apply _. intros ??. apply Nat.divide_antisym_nonneg; lia.
+  Qed.
+  Global Hint Extern 0 (_ | _) => reflexivity : core.
+
+  Lemma divide_ne_0 x y : (x | y) → y ≠ 0 → x ≠ 0.
+  Proof. intros Hxy Hy ->. by apply Hy, Nat.divide_0_l. Qed.
+
+  Lemma iter_succ {A} n (f: A → A) x : Nat.iter (S n) f x = f (Nat.iter n f x).
+  Proof. done. Qed.
+  Lemma iter_succ_r {A} n (f: A → A) x : Nat.iter (S n) f x = Nat.iter n f (f x).
+  Proof. induction n; by f_equal/=. Qed.
+  Lemma iter_add {A} n1 n2 (f : A → A) x :
+    Nat.iter (n1 + n2) f x = Nat.iter n1 f (Nat.iter n2 f x).
+  Proof. induction n1; by f_equal/=. Qed.
+  Lemma iter_mul {A} n1 n2 (f : A → A) x :
+    Nat.iter (n1 * n2) f x = Nat.iter n1 (Nat.iter n2 f) x.
+  Proof.
+    intros. induction n1 as [|n1 IHn1]; [done|].
+    simpl. by rewrite iter_add, IHn1.
+  Qed.
+
+  Lemma iter_ind {A} (P : A → Prop) f x k :
+    P x → (∀ y, P y → P (f y)) → P (Nat.iter k f x).
+  Proof. induction k; simpl; auto. Qed.
+End Nat.
 
 (** * Notations and properties of [positive] *)
 Local Open Scope positive_scope.
@@ -135,154 +140,160 @@ Notation "(~0)" := xO (only parsing) : positive_scope.
 Notation "(~1)" := xI (only parsing) : positive_scope.
 
 Global Arguments Pos.of_nat : simpl never.
-Global Arguments Pmult : simpl never.
-
-Global Instance positive_eq_dec: EqDecision positive := Pos.eq_dec.
-Global Instance positive_le_dec: RelDecision Pos.le.
-Proof. refine (λ x y, decide ((x ?= y) ≠ Gt)). Defined.
-Global Instance positive_lt_dec: RelDecision Pos.lt.
-Proof. refine (λ x y, decide ((x ?= y) = Lt)). Defined.
-Global Instance positive_le_total: Total Pos.le.
-Proof. repeat intro; lia. Qed.
-
-Global Instance positive_inhabited: Inhabited positive := populate 1.
-
-Global Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end.
-Global Instance maybe_xI : Maybe xI := λ p, match p with p~1 => Some p | _ => None end.
-Global Instance xO_inj : Inj (=) (=) (~0).
-Proof. by injection 1. Qed.
-Global Instance xI_inj : Inj (=) (=) (~1).
-Proof. by injection 1. Qed.
-
-(** Since [positive] represents lists of bits, we define list operations
-on it. These operations are in reverse, as positives are treated as snoc
-lists instead of cons lists. *)
-Fixpoint Papp (p1 p2 : positive) : positive :=
-  match p2 with
-  | 1 => p1
-  | p2~0 => (Papp p1 p2)~0
-  | p2~1 => (Papp p1 p2)~1
-  end.
-Infix "++" := Papp : positive_scope.
-Notation "(++)" := Papp (only parsing) : positive_scope.
-Notation "( p ++.)" := (Papp p) (only parsing) : positive_scope.
-Notation "(.++ q )" := (λ p, Papp p q) (only parsing) : positive_scope.
-
-Fixpoint Preverse_go (p1 p2 : positive) : positive :=
-  match p2 with
-  | 1 => p1
-  | p2~0 => Preverse_go (p1~0) p2
-  | p2~1 => Preverse_go (p1~1) p2
-  end.
-Definition Preverse : positive → positive := Preverse_go 1.
-
-Global Instance Papp_1_l : LeftId (=) 1 (++).
-Proof. intros p. by induction p; intros; f_equal/=. Qed.
-Global Instance Papp_1_r : RightId (=) 1 (++).
-Proof. done. Qed.
-Global Instance Papp_assoc : Assoc (=) (++).
-Proof. intros ?? p. by induction p; intros; f_equal/=. Qed.
-Global Instance Papp_inj p : Inj (=) (=) (.++ p).
-Proof. intros ???. induction p; simplify_eq; auto. Qed.
-
-Lemma Preverse_go_app p1 p2 p3 :
-  Preverse_go p1 (p2 ++ p3) = Preverse_go p1 p3 ++ Preverse_go 1 p2.
-Proof.
-  revert p3 p1 p2.
-  cut (∀ p1 p2 p3, Preverse_go (p2 ++ p3) p1 = p2 ++ Preverse_go p3 p1).
-  { by intros go p3; induction p3; intros p1 p2; simpl; auto; rewrite <-?go. }
-  intros p1; induction p1 as [p1 IH|p1 IH|]; intros p2 p3; simpl; auto.
-  - apply (IH _ (_~1)).
-  - apply (IH _ (_~0)).
-Qed.
-Lemma Preverse_app p1 p2 : Preverse (p1 ++ p2) = Preverse p2 ++ Preverse p1.
-Proof. unfold Preverse. by rewrite Preverse_go_app. Qed.
-Lemma Preverse_xO p : Preverse (p~0) = (1~0) ++ Preverse p.
-Proof Preverse_app p (1~0).
-Lemma Preverse_xI p : Preverse (p~1) = (1~1) ++ Preverse p.
-Proof Preverse_app p (1~1).
-
-Lemma Preverse_involutive p :
-  Preverse (Preverse p) = p.
-Proof.
-  induction p as [p IH|p IH|]; simpl.
-  - by rewrite Preverse_xI, Preverse_app, IH.
-  - by rewrite Preverse_xO, Preverse_app, IH.
-  - reflexivity.
-Qed.
-
-Global Instance Preverse_inj : Inj (=) (=) Preverse.
-Proof.
-  intros p q eq.
-  rewrite <- (Preverse_involutive p).
-  rewrite <- (Preverse_involutive q).
-  by rewrite eq.
-Qed.
-
-Fixpoint Plength (p : positive) : nat :=
-  match p with 1 => 0%nat | p~0 | p~1 => S (Plength p) end.
-Lemma Papp_length p1 p2 : Plength (p1 ++ p2) = (Plength p2 + Plength p1)%nat.
-Proof. by induction p2; f_equal/=. Qed.
-
-Lemma Plt_sum (x y : positive) : x < y ↔ ∃ z, y = x + z.
-Proof.
-  split.
-  - exists (y - x)%positive. symmetry. apply Pplus_minus. lia.
-  - intros [z ->]. lia.
-Qed.
-
-(** Duplicate the bits of a positive, i.e. 1~0~1 -> 1~0~0~1~1 and
-    1~1~0~0 -> 1~1~1~0~0~0~0 *)
-Fixpoint Pdup (p : positive) : positive :=
-  match p with
-  | 1 => 1
-  | p'~0 => (Pdup p')~0~0
-  | p'~1 => (Pdup p')~1~1
-  end.
-
-Lemma Pdup_app p q :
-  Pdup (p ++ q) = Pdup p ++ Pdup q.
-Proof.
-  revert p.
-  induction q as [p IH|p IH|]; intros q; simpl.
-  - by rewrite IH.
-  - by rewrite IH.
-  - reflexivity.
-Qed.
-
-Lemma Pdup_suffix_eq p q s1 s2 :
-  s1~1~0 ++ Pdup p = s2~1~0 ++ Pdup q → p = q.
-Proof.
-  revert q.
-  induction p as [p IH|p IH|]; intros [q|q|] eq; simplify_eq/=.
-  - by rewrite (IH q).
-  - by rewrite (IH q).
-  - reflexivity.
-Qed.
-
-Global Instance Pdup_inj : Inj (=) (=) Pdup.
-Proof.
-  intros p q eq.
-  apply (Pdup_suffix_eq _ _ 1 1).
-  by rewrite eq.
-Qed.
-
-Lemma Preverse_Pdup p :
-  Preverse (Pdup p) = Pdup (Preverse p).
-Proof.
-  induction p as [p IH|p IH|]; simpl.
-  - rewrite 3!Preverse_xI.
-    rewrite (assoc_L (++)).
-    rewrite IH.
-    rewrite Pdup_app.
-    reflexivity.
-  - rewrite 3!Preverse_xO.
-    rewrite (assoc_L (++)).
-    rewrite IH.
-    rewrite Pdup_app.
-    reflexivity.
-  - reflexivity.
-Qed.
+Global Arguments Pos.mul : simpl never.
+
+Module Pos.
+  Global Instance eq_dec: EqDecision positive := Pos.eq_dec.
+  Global Instance le_dec: RelDecision Pos.le.
+  Proof. refine (λ x y, decide ((x ?= y) ≠ Gt)). Defined.
+  Global Instance lt_dec: RelDecision Pos.lt.
+  Proof. refine (λ x y, decide ((x ?= y) = Lt)). Defined.
+  Global Instance le_total: Total Pos.le.
+  Proof. repeat intro; lia. Qed.
+
+  Global Instance inhabited: Inhabited positive := populate 1.
+
+  Global Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end.
+  Global Instance maybe_xI : Maybe xI := λ p, match p with p~1 => Some p | _ => None end.
+  Global Instance xO_inj : Inj (=) (=) (~0).
+  Proof. by injection 1. Qed.
+  Global Instance xI_inj : Inj (=) (=) (~1).
+  Proof. by injection 1. Qed.
+
+  (** Since [positive] represents lists of bits, we define list operations
+  on it. These operations are in reverse, as positives are treated as snoc
+  lists instead of cons lists. *)
+  Fixpoint app (p1 p2 : positive) : positive :=
+    match p2 with
+    | 1 => p1
+    | p2~0 => (app p1 p2)~0
+    | p2~1 => (app p1 p2)~1
+    end.
+
+  Module Import app_notations.
+    Infix "++" := app : positive_scope.
+    Notation "(++)" := app (only parsing) : positive_scope.
+    Notation "( p ++.)" := (app p) (only parsing) : positive_scope.
+    Notation "(.++ q )" := (λ p, app p q) (only parsing) : positive_scope.
+  End app_notations.
+
+  Fixpoint reverse_go (p1 p2 : positive) : positive :=
+    match p2 with
+    | 1 => p1
+    | p2~0 => reverse_go (p1~0) p2
+    | p2~1 => reverse_go (p1~1) p2
+    end.
+  Definition reverse : positive → positive := reverse_go 1.
+
+  Global Instance app_1_l : LeftId (=) 1 (++).
+  Proof. intros p. by induction p; intros; f_equal/=. Qed.
+  Global Instance app_1_r : RightId (=) 1 (++).
+  Proof. done. Qed.
+  Global Instance app_assoc : Assoc (=) (++).
+  Proof. intros ?? p. by induction p; intros; f_equal/=. Qed.
+  Global Instance app_inj p : Inj (=) (=) (.++ p).
+  Proof. intros ???. induction p; simplify_eq; auto. Qed.
+
+  Lemma reverse_go_app p1 p2 p3 :
+    reverse_go p1 (p2 ++ p3) = reverse_go p1 p3 ++ reverse_go 1 p2.
+  Proof.
+    revert p3 p1 p2.
+    cut (∀ p1 p2 p3, reverse_go (p2 ++ p3) p1 = p2 ++ reverse_go p3 p1).
+    { by intros go p3; induction p3; intros p1 p2; simpl; auto; rewrite <-?go. }
+    intros p1; induction p1 as [p1 IH|p1 IH|]; intros p2 p3; simpl; auto.
+    - apply (IH _ (_~1)).
+    - apply (IH _ (_~0)).
+  Qed.
+  Lemma reverse_app p1 p2 : reverse (p1 ++ p2) = reverse p2 ++ reverse p1.
+  Proof. unfold reverse. by rewrite reverse_go_app. Qed.
+  Lemma reverse_xO p : reverse (p~0) = (1~0) ++ reverse p.
+  Proof reverse_app p (1~0).
+  Lemma reverse_xI p : reverse (p~1) = (1~1) ++ reverse p.
+  Proof reverse_app p (1~1).
+
+  Lemma reverse_involutive p : reverse (reverse p) = p.
+  Proof.
+    induction p as [p IH|p IH|]; simpl.
+    - by rewrite reverse_xI, reverse_app, IH.
+    - by rewrite reverse_xO, reverse_app, IH.
+    - reflexivity.
+  Qed.
+
+  Global Instance reverse_inj : Inj (=) (=) reverse.
+  Proof.
+    intros p q eq.
+    rewrite <-(reverse_involutive p).
+    rewrite <-(reverse_involutive q).
+    by rewrite eq.
+  Qed.
+
+  Fixpoint length (p : positive) : nat :=
+    match p with 1 => 0%nat | p~0 | p~1 => S (length p) end.
+  Lemma app_length p1 p2 : length (p1 ++ p2) = (length p2 + length p1)%nat.
+  Proof. by induction p2; f_equal/=. Qed.
+
+  Lemma lt_sum (x y : positive) : x < y ↔ ∃ z, y = x + z.
+  Proof.
+    split.
+    - exists (y - x)%positive. symmetry. apply Pplus_minus. lia.
+    - intros [z ->]. lia.
+  Qed.
+
+  (** Duplicate the bits of a positive, i.e. 1~0~1 -> 1~0~0~1~1 and
+      1~1~0~0 -> 1~1~1~0~0~0~0 *)
+  Fixpoint dup (p : positive) : positive :=
+    match p with
+    | 1 => 1
+    | p'~0 => (dup p')~0~0
+    | p'~1 => (dup p')~1~1
+    end.
+
+  Lemma dup_app p q :
+    dup (p ++ q) = dup p ++ dup q.
+  Proof.
+    revert p.
+    induction q as [p IH|p IH|]; intros q; simpl.
+    - by rewrite IH.
+    - by rewrite IH.
+    - reflexivity.
+  Qed.
+
+  Lemma dup_suffix_eq p q s1 s2 :
+    s1~1~0 ++ dup p = s2~1~0 ++ dup q → p = q.
+  Proof.
+    revert q.
+    induction p as [p IH|p IH|]; intros [q|q|] eq; simplify_eq/=.
+    - by rewrite (IH q).
+    - by rewrite (IH q).
+    - reflexivity.
+  Qed.
+
+  Global Instance dup_inj : Inj (=) (=) dup.
+  Proof.
+    intros p q eq.
+    apply (dup_suffix_eq _ _ 1 1).
+    by rewrite eq.
+  Qed.
+
+  Lemma reverse_dup p :
+    reverse (dup p) = dup (reverse p).
+  Proof.
+    induction p as [p IH|p IH|]; simpl.
+    - rewrite 3!reverse_xI.
+      rewrite (assoc_L (++)).
+      rewrite IH.
+      rewrite dup_app.
+      reflexivity.
+    - rewrite 3!reverse_xO.
+      rewrite (assoc_L (++)).
+      rewrite IH.
+      rewrite dup_app.
+      reflexivity.
+    - reflexivity.
+  Qed.
+End Pos.
+
+Export Pos.app_notations.
 
 Local Close Scope positive_scope.
 
diff --git a/stdpp/pmap.v b/stdpp/pmap.v
index f269f482..28acdc29 100644
--- a/stdpp/pmap.v
+++ b/stdpp/pmap.v
@@ -85,7 +85,7 @@ Fixpoint Pto_list_raw {A} (j : positive) (t : Pmap_raw A)
     (acc : list (positive * A)) : list (positive * A) :=
   match t with
   | PLeaf => acc
-  | PNode o l r => from_option (λ x, [(Preverse j, x)]) [] o ++
+  | PNode o l r => from_option (λ x, [(Pos.reverse j, x)]) [] o ++
      Pto_list_raw (j~0) l (Pto_list_raw (j~1) r acc)
   end%list.
 Fixpoint Pomap_raw {A B} (f : A → option B) (t : Pmap_raw A) : Pmap_raw B :=
@@ -170,7 +170,7 @@ Lemma Plookup_fmap {A B} (f : A → B) t i : (Pfmap_raw f t) !! i = f <$> t !! i
 Proof. revert i. by induction t; intros [?|?|]; simpl. Qed.
 Lemma Pelem_of_to_list {A} (t : Pmap_raw A) j i acc x :
   (i,x) ∈ Pto_list_raw j t acc ↔
-    (∃ i', i = i' ++ Preverse j ∧ t !! i' = Some x) ∨ (i,x) ∈ acc.
+    (∃ i', i = i' ++ Pos.reverse j ∧ t !! i' = Some x) ∨ (i,x) ∈ acc.
 Proof.
   split.
   { revert j acc. induction t as [|[y|] l IHl r IHr]; intros j acc; simpl.
@@ -178,14 +178,14 @@ Proof.
     - rewrite elem_of_cons. intros [?|?]; simplify_eq.
       { left; exists 1. by rewrite (left_id_L 1 (++))%positive. }
       destruct (IHl (j~0) (Pto_list_raw j~1 r acc)) as [(i'&->&?)|?]; auto.
-      { left; exists (i' ~ 0). by rewrite Preverse_xO, (assoc_L _). }
+      { left; exists (i' ~ 0). by rewrite Pos.reverse_xO, (assoc_L _). }
       destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
-      left; exists (i' ~ 1). by rewrite Preverse_xI, (assoc_L _).
+      left; exists (i' ~ 1). by rewrite Pos.reverse_xI, (assoc_L _).
     - intros.
       destruct (IHl (j~0) (Pto_list_raw j~1 r acc)) as [(i'&->&?)|?]; auto.
-      { left; exists (i' ~ 0). by rewrite Preverse_xO, (assoc_L _). }
+      { left; exists (i' ~ 0). by rewrite Pos.reverse_xO, (assoc_L _). }
       destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
-      left; exists (i' ~ 1). by rewrite Preverse_xI, (assoc_L _). }
+      left; exists (i' ~ 1). by rewrite Pos.reverse_xI, (assoc_L _). }
   revert t j i acc. assert (∀ t j i acc,
     (i, x) ∈ acc → (i, x) ∈ Pto_list_raw j t acc) as help.
   { intros t; induction t as [|[y|] l IHl r IHr]; intros j i acc;
@@ -195,45 +195,45 @@ Proof.
   - done.
   - rewrite elem_of_cons. destruct i as [i|i|]; simplify_eq/=.
     + right. apply help. specialize (IHr (j~1) i).
-      rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
+      rewrite Pos.reverse_xI, (assoc_L _) in IHr. by apply IHr.
     + right. specialize (IHl (j~0) i).
-      rewrite Preverse_xO, (assoc_L _) in IHl. by apply IHl.
+      rewrite Pos.reverse_xO, (assoc_L _) in IHl. by apply IHl.
     + left. by rewrite (left_id_L 1 (++))%positive.
   - destruct i as [i|i|]; simplify_eq/=.
     + apply help. specialize (IHr (j~1) i).
-      rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
+      rewrite Pos.reverse_xI, (assoc_L _) in IHr. by apply IHr.
     + specialize (IHl (j~0) i).
-      rewrite Preverse_xO, (assoc_L _) in IHl. by apply IHl.
+      rewrite Pos.reverse_xO, (assoc_L _) in IHl. by apply IHl.
 Qed.
 Lemma Pto_list_nodup {A} j (t : Pmap_raw A) acc :
-  (∀ i x, (i ++ Preverse j, x) ∈ acc → t !! i = None) →
+  (∀ i x, (i ++ Pos.reverse j, x) ∈ acc → t !! i = None) →
   NoDup acc → NoDup (Pto_list_raw j t acc).
 Proof.
   revert j acc. induction t as [|[y|] l IHl r IHr]; simpl; intros j acc Hin ?.
   - done.
   - repeat constructor.
     { rewrite Pelem_of_to_list. intros [(i&Hi&?)|Hj].
-      { apply (f_equal Plength) in Hi.
-        rewrite Preverse_xO, !Papp_length in Hi; simpl in *; lia. }
+      { apply (f_equal Pos.length) in Hi.
+        rewrite Pos.reverse_xO, !Pos.app_length in Hi; simpl in *; lia. }
       rewrite Pelem_of_to_list in Hj. destruct Hj as [(i&Hi&?)|Hj].
-      { apply (f_equal Plength) in Hi.
-        rewrite Preverse_xI, !Papp_length in Hi; simpl in *; lia. }
+      { apply (f_equal Pos.length) in Hi.
+        rewrite Pos.reverse_xI, !Pos.app_length in Hi; simpl in *; lia. }
       specialize (Hin 1 y). rewrite (left_id_L 1 (++))%positive in Hin.
       discriminate (Hin Hj). }
     apply IHl.
     { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
-      + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
+      + rewrite Pos.reverse_xO, Pos.reverse_xI, !(assoc_L _) in Hi.
         by apply (inj (.++ _)) in Hi.
-      + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
+      + apply (Hin (i~0) x). by rewrite Pos.reverse_xO, (assoc_L _) in Hi. }
     apply IHr; auto. intros i x Hi.
-    apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
+    apply (Hin (i~1) x). by rewrite Pos.reverse_xI, (assoc_L _) in Hi.
   - apply IHl.
     { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
-      + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
+      + rewrite Pos.reverse_xO, Pos.reverse_xI, !(assoc_L _) in Hi.
         by apply (inj (.++ _)) in Hi.
-      + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
+      + apply (Hin (i~0) x). by rewrite Pos.reverse_xO, (assoc_L _) in Hi. }
     apply IHr; auto. intros i x Hi.
-    apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
+    apply (Hin (i~1) x). by rewrite Pos.reverse_xI, (assoc_L _) in Hi.
 Qed.
 Lemma Pomap_lookup {A B} (f : A → option B) t i :
   Pomap_raw f t !! i = t !! i ≫= f.
diff --git a/stdpp/relations.v b/stdpp/relations.v
index badc1c07..5e78f264 100644
--- a/stdpp/relations.v
+++ b/stdpp/relations.v
@@ -177,7 +177,7 @@ Section general.
   Lemma bsteps_weaken n m x y :
     n ≤ m → bsteps R n x y → bsteps R m x y.
   Proof.
-    intros. rewrite (nat_le_add_sub n m); auto using bsteps_add_r.
+    intros. rewrite (Nat.le_add_sub n m); auto using bsteps_add_r.
   Qed.
   Lemma bsteps_add_l n m x y :
     bsteps R n x y → bsteps R (m + n) x y.
-- 
GitLab