phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/natmap.v *)
Lemma lookup_natset_to_bools sz X i β :
  i < sz → natset_to_bools sz X !! i = Some β ↔ (i ∈ X ↔ β = true).
Proof.
  unfold natset_to_bools, elem_of, mapset_elem_of, lookup at 2, natmap_lookup; simpl.
  intros. destruct (mapset_car X) as [l ?]; simpl.
  destruct (l !! i) as [mu|] eqn:Hmu; simpl.
  { rewrite lookup_resize, list_lookup_fmap, Hmu
      by (rewrite ?length_fmap; eauto using lookup_lt_Some).
    destruct mu as [[]|], β; simpl; intuition congruence. }
  rewrite lookup_resize_new by (rewrite ?length_fmap;
    eauto using lookup_ge_None_1); destruct β; intuition congruence.
Qed.
(* stdpp/natmap.v *)
Lemma lookup_natset_to_bools_true sz X i :
  i < sz → natset_to_bools sz X !! i = Some true ↔ i ∈ X.
Proof. intros. rewrite lookup_natset_to_bools by done. intuition. Qed.
(* stdpp/natmap.v *)
Lemma lookup_natset_to_bools_false sz X i :
  i < sz → natset_to_bools sz X !! i = Some false ↔ i ∉ X.
Proof. intros. rewrite lookup_natset_to_bools by done. naive_solver. Qed.
(* stdpp/natmap.v *)
Lemma natset_to_bools_union sz X1 X2 :
  natset_to_bools sz (X1 ∪ X2) = natset_to_bools sz X1 ||* natset_to_bools sz X2.
Proof.
  apply list_eq; intros i; rewrite lookup_zip_with.
  destruct (decide (i < sz)); [|by rewrite !lookup_natset_to_bools_ge by lia].
  apply option_eq; intros β.
  rewrite lookup_natset_to_bools, elem_of_union by done; intros.
  destruct (decide (i ∈ X1)), (decide (i ∈ X2)); repeat first
    [ rewrite (λ X H, proj2 (lookup_natset_to_bools_true sz X i H)) by done
    | rewrite (λ X H, proj2 (lookup_natset_to_bools_false sz X i H)) by done];
    destruct β; naive_solver.
Qed.
(* stdpp/natmap.v *)
Lemma natset_to_bools_to_natset βs sz :
  natset_to_bools sz (bools_to_natset βs) = resize sz false βs.
Proof.
  apply list_eq; intros i. destruct (decide (i < sz));
    [|by rewrite lookup_natset_to_bools_ge, lookup_resize_old by lia].
  apply option_eq; intros β.
  rewrite lookup_natset_to_bools, elem_of_bools_to_natset by done.
  destruct (decide (i < length βs)).
  { rewrite lookup_resize by done.
    destruct (lookup_lt_is_Some_2 βs i) as [[]]; destruct β; naive_solver. }
  rewrite lookup_resize_new, lookup_ge_None_2 by lia. destruct β; naive_solver.
Qed.
(* stdpp/natmap.v *)
(* A [natmap A] forms a stack with elements of type [A] and possible holes *)
Definition natmap_push {A} (o : option A) (m : natmap A) : natmap A
:=
  let (l,Hl) := m in NatMap _ (natmap_cons_canon_wf o l Hl).
(* stdpp/natmap.v *)
Definition natmap_pop_raw {A} (l : natmap_raw A) : natmap_raw A
:= tail l.
(* stdpp/natmap.v *)
Lemma natmap_pop_wf {A} (l : natmap_raw A) :
  natmap_wf l → natmap_wf (natmap_pop_raw l).
Proof. destruct l; simpl; eauto using natmap_wf_inv. Qed.
(* stdpp/natmap.v *)
Definition natmap_pop {A} (m : natmap A) : natmap A
:=
  let (l,Hl) := m in NatMap _ (natmap_pop_wf _ Hl).
(* stdpp/natmap.v *)
Lemma lookup_natmap_push_O {A} o (m : natmap A) : natmap_push o m !! 0 = o.
Proof. by destruct o, m as [[|??]]. Qed.
(* stdpp/natmap.v *)
Lemma lookup_natmap_push_S {A} o (m : natmap A) i :
  natmap_push o m !! S i = m !! i.
Proof. by destruct o, m as [[|??]]. Qed.
(* stdpp/natmap.v *)
Lemma lookup_natmap_pop {A} (m : natmap A) i : natmap_pop m !! i = m !! S i.
Proof. by destruct m as [[|??]]. Qed.
(* stdpp/natmap.v *)
Lemma natmap_push_pop {A} (m : natmap A) :
  natmap_push (m !! 0) (natmap_pop m) = m.
Proof.
  apply map_eq. intros i. destruct i.
  - by rewrite lookup_natmap_push_O.
  - by rewrite lookup_natmap_push_S, lookup_natmap_pop.
Qed.
(* stdpp/natmap.v *)
Lemma natmap_pop_push {A} o (m : natmap A) : natmap_pop (natmap_push o m) = m.
Proof. apply natmap_eq. by destruct o, m as [[|??]]. Qed.
(* stdpp/nat_cancel.v *)
(* The class [NatCancel m n m' n'] is a simple canceler for natural numbers
implemented using type classes.

Input: [m], [n]; output: [m'], [n'].

It turns an equality [n = m] into an equality [n' = m'] by canceling out terms
that appear on both sides of the equality. We provide instances to handle the
following connectives over natural numbers:

  n := 0 | t | n + m | S m

Here, [t] represents arbitrary terms that do not fit the grammar. The instances
the class perform a depth-first traversal (from left to right) through [n] and
try to cancel each leaf in [m]. This implies that the shape of the original
expressions [n] and [m] are preserved as much as possible. For example,
canceling:

  S (S m2) + (k1 + (S k2 + k3)) + n1 = 2 + S ((n1 + S n2) + S (S m1 + m2))

Results in:

  k1 + (k2 + k3) = S (n2 + S (S m1))

The instances are setup up so that canceling is performed in two stages.

- In the first stage, using the class [NatCancelL], it traverses [m] w.r.t. [S]
  and [+].
- In the second stage, for each leaf (i.e. a constant or arbitrary term)
  obtained by the traversal in stage 1, it uses the class [NatCancelR] to
  cancel the leaf in [n].

Be warned: Since the canceler is implemented using type classes it should only
be used it either of the inputs is relatively small. For bigger inputs, an
approach based on reflection would be better, but for small inputs, the overhead
of reification will probably not be worth it. *)
Class NatCancel (m n m' n' : nat)
:= nat_cancel : m' + n = m + n'.
(* stdpp/nat_cancel.v *)
Class NatCancelL (m n m' n' : nat)
:= nat_cancel_l : m' + n = m + n'.
(* stdpp/nat_cancel.v *)
Class NatCancelR (m n m' n' : nat)
:= nat_cancel_r : NatCancelL m n m' n'.
(* stdpp/nat_cancel.v *)
(* The implementation of the canceler is highly non-deterministic, but since
  it will always succeed, no backtracking will ever be performed. In order to
  avoid issues like:

    https://gitlab.mpi-sws.org/FP/iris-coq/issues/153

  we wrap the entire canceler in the [NoBackTrack] class. *)
Instance nat_cancel_start m n m' n' :
    TCNoBackTrack (NatCancelL m n m' n') → NatCancel m n m' n'.
Proof. by intros [?]. Qed.
(* stdpp/nat_cancel.v *)
Class MakeNatS (n1 n2 m : nat)
:= make_nat_S : m = n1 + n2.
(* stdpp/nat_cancel.v *)
Instance make_nat_S_0_l n : MakeNatS 0 n n.
Proof. done. Qed.
(* stdpp/nat_cancel.v *)
Instance make_nat_S_1 n : MakeNatS 1 n (S n).
Proof. done. Qed.
(* stdpp/nat_cancel.v *)
Class MakeNatAdd (n1 n2 m : nat)
:= make_nat_add : m = n1 + n2.
(* stdpp/nat_cancel.v *)
Instance make_nat_add_0_l n : MakeNatAdd 0 n n.
Proof. done. Qed.
(* stdpp/nat_cancel.v *)
Instance make_nat_add_0_r n : MakeNatAdd n 0 n.
Proof. unfold MakeNatAdd. by rewrite Nat.add_0_r. Qed.
(* stdpp/nat_cancel.v *)
Instance make_nat_add_default n1 n2 : MakeNatAdd n1 n2 (n1 + n2) | 100.
Proof. done. Qed.
(* stdpp/nat_cancel.v *)
Instance nat_cancel_leaf_here m : NatCancelR m m 0 0 | 0.
Proof. by unfold NatCancelR, NatCancelL. Qed.
(* stdpp/nat_cancel.v *)
Instance nat_cancel_leaf_else m n : NatCancelR m n m n | 100.
Proof. by unfold NatCancelR. Qed.
(* stdpp/nat_cancel.v *)
Instance nat_cancel_leaf_add m m' m'' n1 n2 n1' n2' n1'n2' :
    NatCancelR m n1 m' n1' → NatCancelR m' n2 m'' n2' →
    MakeNatAdd n1' n2' n1'n2' → NatCancelR m (n1 + n2) m'' n1'n2' | 2.
Proof. unfold NatCancelR, NatCancelL, MakeNatAdd. lia. Qed.
(* stdpp/nat_cancel.v *)
Instance nat_cancel_leaf_S_here m n m' n' :
    NatCancelR m n m' n' → NatCancelR (S m) (S n) m' n' | 3.
Proof. unfold NatCancelR, NatCancelL. lia. Qed.
(* stdpp/nat_cancel.v *)
Instance nat_cancel_leaf_S_else m n m' n' :
    NatCancelR m n m' n' → NatCancelR m (S n) m' (S n') | 4.
Proof. unfold NatCancelR, NatCancelL. lia. Qed.
(* stdpp/nat_cancel.v *)
(* The instance [nat_cancel_S_both] is redundant, but may reduce proof search
  quite a bit, e.g. when canceling constants in constants. *)
Instance nat_cancel_S_both m n m' n' :
    NatCancelL m n m' n' → NatCancelL (S m) (S n) m' n' | 1.
Proof. unfold NatCancelL. lia. Qed.
(* stdpp/nat_cancel.v *)
Instance nat_cancel_add m1 m2 m1' m2' m1'm2' n n' n'' :
    NatCancelL m1 n m1' n' → NatCancelL m2 n' m2' n'' →
    MakeNatAdd m1' m2' m1'm2' → NatCancelL (m1 + m2) n m1'm2' n'' | 2.
Proof. unfold NatCancelL, MakeNatAdd. lia. Qed.
(* stdpp/nat_cancel.v *)
Instance nat_cancel_S m m' m'' Sm' n n' n'' :
    NatCancelL m n m' n' → NatCancelR 1 n' m'' n'' →
    MakeNatS m'' m' Sm' → NatCancelL (S m) n Sm' n'' | 3.
Proof. unfold NatCancelR, NatCancelL, MakeNatS. lia. Qed.
(* stdpp/nmap.v *)
Record Nmap (A : Type) : Type
:= NMap { Nmap_0 : option A; Nmap_pos : Pmap A }.
(* stdpp/nmap.v *)
Instance Nmap_eq_dec `{EqDecision A} : EqDecision (Nmap A).
Proof.
 refine (λ t1 t2,
  match t1, t2 with
  | NMap x t1, NMap y t2 => cast_if_and (decide (x = y)) (decide (t1 = t2))
  end); abstract congruence.
Defined.
(* stdpp/nmap.v *)
Instance Nmap_empty {A} : Empty (Nmap A)
:= NMap None ∅.
(* stdpp/nmap.v *)
Instance Nmap_lookup {A} : Lookup N A (Nmap A)
:= λ i t,
  match i with
  | 0 => Nmap_0 t
  | N.pos p => Nmap_pos t !! p
  end.
(* stdpp/nmap.v *)
Instance Nmap_partial_alter {A} : PartialAlter N A (Nmap A)
:= λ f i t,
  match i, t with
  | 0, NMap o t => NMap (f o) t
  | N.pos p, NMap o t => NMap o (partial_alter f p t)
  end.
(* stdpp/nmap.v *)
Instance Nmap_fmap: FMap Nmap
:= λ A B f t,
  match t with NMap o t => NMap (f <$> o) (f <$> t) end.
(* stdpp/nmap.v *)
Instance Nmap_omap: OMap Nmap
:= λ A B f t,
  match t with NMap o t => NMap (o ≫= f) (omap f t) end.
(* stdpp/nmap.v *)
Instance Nmap_merge: Merge Nmap
:= λ A B C f t1 t2,
  match t1, t2 with
  | NMap o1 t1, NMap o2 t2 => NMap (diag_None f o1 o2) (merge f t1 t2)
  end.
(* stdpp/nmap.v *)
Instance Nmap_fold {A} : MapFold N A (Nmap A)
:= λ B f d t,
  match t with
  | NMap mx t =>
     map_fold (f ∘ N.pos) match mx with Some x => f 0 x d | None => d end t
  end.
(* stdpp/nmap.v *)
Instance Nmap_map: FinMap N Nmap.
Proof.
  split.
  - intros ? [??] [??] H. f_equal; [apply (H 0)|].
    apply map_eq. intros i. apply (H (N.pos i)).
  - by intros ? [|?].
  - intros ? f [? t] [|i]; simpl; [done |]. apply lookup_partial_alter_eq.
  - intros ? f [? t] [|i] [|j]; simpl; try intuition congruence.
    intros. apply lookup_partial_alter_ne. congruence.
  - intros ??? [??] []; simpl; [done|]. apply lookup_fmap.
  - intros ?? f [??] [|?]; simpl; [done|]; apply (lookup_omap f).
  - intros ??? f [??] [??] [|?]; simpl; [done|]; apply (lookup_merge f).
  - done.
  - intros A P Hemp Hins [mx t].
    induction t as [|i x t ? Hfold IH] using map_fold_fmap_ind.
    { destruct mx as [x|]; [|done].
      replace (NMap (Some x) ∅) with (<[0:=x]> ∅ : Nmap _) by done.
      by apply Hins. }
    apply (Hins (N.pos i) x (NMap mx t)); [done| |done].
    intros A' B f g b. apply Hfold.
Qed.
(* stdpp/nmap.v *)
(* We construct sets of [N]s satisfying extensional equality. *)
Notation Nset
:= (mapset Nmap).
(* stdpp/nmap.v *)
Instance Nmap_dom {A} : Dom (Nmap A) Nset
:= mapset_dom.
(* stdpp/nmap.v *)
Instance : FinMapDom N Nmap Nset
:= mapset_dom_spec.
(* stdpp/numbers.v *)
Instance comparison_eq_dec : EqDecision comparison.
Proof. solve_decision. Defined.
(* stdpp/numbers.v *)
(* We do *not* add notation for [≥] mapping to [ge], and we do also not use the
[>] notation from the Coq standard library. Using such notations leads to
annoying problems: if you have [x < y] in the context and need [y > x] for some
lemma, [assumption] won't work because [x < y] and [y > x] are not
definitionally equal. It is just generally frustrating to deal with this
mismatch, and much preferable to state logically equivalent things in syntactically
equal ways.

As an alternative, we could define [>] and [≥] as [parsing only] notation that
maps to [<] and [≤], respectively (similar to math-comp). This would change the
notation for [<] from the Coq standard library to something that is not
definitionally equal, so we avoid that as well.

This concern applies to all number types: [nat], [N], [Z], [positive], [Qc] and
[Qp]. *)
Notation "x ≤ y ≤ z"
:= (x ≤ y ∧ y ≤ z)%nat : nat_scope.
(* stdpp/numbers.v *)
Notation "x ≤ y < z"
:= (x ≤ y ∧ y < z)%nat : nat_scope.
(* stdpp/numbers.v *)
Notation "x < y ≤ z"
:= (x < y ∧ y ≤ z)%nat : nat_scope.
(* stdpp/numbers.v *)
Notation "x ≤ y ≤ z ≤ z'"
:= (x ≤ y ∧ y ≤ z ∧ z ≤ z')%nat : nat_scope.
(* stdpp/numbers.v *)
Notation "(≤)"
:= le (only parsing) : nat_scope.
(* stdpp/numbers.v *)
Notation "(<)"
:= lt (only parsing) : nat_scope.
(* stdpp/numbers.v *)
(* TODO: Consider removing these notations to avoid populting the global
scope? *)
Notation lcm
:= Nat.lcm.
(* stdpp/numbers.v *)
Notation divide
:= Nat.divide.
(* stdpp/numbers.v *)
Notation "( x | y )"
:= (divide x y) : nat_scope.
(* stdpp/numbers.v *)
Instance add_assoc' : Assoc (=) Nat.add
:= Nat.add_assoc.
(* stdpp/numbers.v *)
Instance add_comm' : Comm (=) Nat.add
:= Nat.add_comm.
(* stdpp/numbers.v *)
Instance add_left_id : LeftId (=) 0 Nat.add
:= Nat.add_0_l.
(* stdpp/numbers.v *)
Instance add_right_id : RightId (=) 0 Nat.add
:= Nat.add_0_r.
(* stdpp/numbers.v *)
Instance sub_right_id : RightId (=) 0 Nat.sub
:= Nat.sub_0_r.
(* stdpp/numbers.v *)
Instance mul_assoc' : Assoc (=) Nat.mul
:= Nat.mul_assoc.
(* stdpp/numbers.v *)
Instance mul_comm' : Comm (=) Nat.mul
:= Nat.mul_comm.
(* stdpp/numbers.v *)
Instance mul_left_id : LeftId (=) 1 Nat.mul
:= Nat.mul_1_l.
(* stdpp/numbers.v *)
Instance mul_right_id : RightId (=) 1 Nat.mul
:= Nat.mul_1_r.
(* stdpp/numbers.v *)
Instance mul_left_absorb : LeftAbsorb (=) 0 Nat.mul
:= Nat.mul_0_l.
(* stdpp/numbers.v *)
Instance mul_right_absorb : RightAbsorb (=) 0 Nat.mul
:= Nat.mul_0_r.
(* stdpp/numbers.v *)
Instance div_right_id : RightId (=) 1 Nat.div
:= Nat.div_1_r.
(* stdpp/numbers.v *)
Instance eq_dec: EqDecision nat
:= eq_nat_dec.
(* stdpp/numbers.v *)
Instance le_dec: RelDecision le
:= le_dec.
(* stdpp/numbers.v *)
Instance lt_dec: RelDecision lt
:= lt_dec.
(* stdpp/numbers.v *)
Instance inhabited: Inhabited nat
:= populate 0.
(* stdpp/numbers.v *)
Instance succ_inj: Inj (=) (=) Nat.succ.
Proof. by injection 1. Qed.
(* stdpp/numbers.v *)
Instance le_po: PartialOrder (≤).
Proof. repeat split; repeat intro; auto with lia. Qed.
(* stdpp/numbers.v *)
Instance le_total: Total (≤).
Proof. repeat intro; lia. Qed.
(* stdpp/numbers.v *)
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.
(* stdpp/numbers.v *)
Instance lt_pi: ∀ x y : nat, ProofIrrel (x < y).
Proof. unfold Peano.lt. apply _. Qed.
(* stdpp/numbers.v *)
(* Given a measure/size [f : B → nat], you can do induction on the size of
  [b : B] using [induction (lt_wf_0_projected f b)]. *)
Lemma lt_wf_0_projected {B} (f : B → nat) : well_founded (λ x y, f x < f y).
Proof. by apply (wf_projected (<) f), lt_wf_0. Qed.
(* stdpp/numbers.v *)
Lemma le_sum (x y : nat) : x ≤ y ↔ ∃ z, y = x + z.
Proof. split; [exists (y - x); lia | intros [z ->]; lia]. Qed.
(* stdpp/numbers.v *)
(* This is similar to but slightly different than Coq's
      [add_sub : ∀ n m : nat, n + m - m = n]. *)
Lemma add_sub' n m : n + m - n = m.
Proof. lia. Qed.
(* stdpp/numbers.v *)
Lemma le_add_sub n m : n ≤ m → m = n + (m - n).
Proof. lia. Qed.
(* stdpp/numbers.v *)
(* Cancellation for multiplication. Coq's stdlib has these lemmas for [Z],
  but those for [nat] are missing. We use the naming scheme of Coq's stdlib. *)
Lemma mul_reg_l n m p : p ≠ 0 → p * n = p * m → n = m.
Proof.
    pose proof (Z.mul_reg_l (Z.of_nat n) (Z.of_nat m) (Z.of_nat p)). lia.
  Qed.
(* stdpp/numbers.v *)
Lemma mul_reg_r n m p : p ≠ 0 → n * p = m * p → n = m.
Proof. rewrite <-!(Nat.mul_comm p). apply mul_reg_l. Qed.
(* stdpp/numbers.v *)
Lemma lt_succ_succ n : n < S (S n).
Proof. auto with arith. Qed.
(* stdpp/numbers.v *)
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.
(* stdpp/numbers.v *)
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.
(* stdpp/numbers.v *)
Instance divide_dec : RelDecision Nat.divide.
Proof.
    refine (λ x y, cast_if (decide (lcm x y = y)));
      abstract (by rewrite Nat.divide_lcm_iff).
  Defined.
(* stdpp/numbers.v *)
Instance divide_po : PartialOrder divide.
Proof.
    repeat split; try apply _. intros ??. apply Nat.divide_antisym; lia.
  Qed.
(* stdpp/numbers.v *)
Lemma divide_ne_0 x y : (x | y) → y ≠ 0 → x ≠ 0.
Proof. intros Hxy Hy ->. by apply Hy, Nat.divide_0_l. Qed.
(* stdpp/numbers.v *)
Lemma iter_succ {A} n (f: A → A) x : Nat.iter (S n) f x = f (Nat.iter n f x).
Proof. done. Qed.
(* stdpp/numbers.v *)
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.
(* stdpp/numbers.v *)
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.
(* stdpp/numbers.v *)
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.
(* stdpp/numbers.v *)
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.
(* stdpp/numbers.v *)
Notation "x ≤ y ≤ z"
:= (x ≤ y ∧ y ≤ z) : positive_scope.
(* stdpp/numbers.v *)
Notation "x ≤ y < z"
:= (x ≤ y ∧ y < z) : positive_scope.
(* stdpp/numbers.v *)
Notation "x < y ≤ z"
:= (x < y ∧ y ≤ z) : positive_scope.
(* stdpp/numbers.v *)
Notation "x ≤ y ≤ z ≤ z'"
:= (x ≤ y ∧ y ≤ z ∧ z ≤ z') : positive_scope.
(* stdpp/numbers.v *)
Notation "(≤)"
:= Pos.le (only parsing) : positive_scope.
(* stdpp/numbers.v *)
Notation "(<)"
:= Pos.lt (only parsing) : positive_scope.
(* stdpp/numbers.v *)
Notation "(~0)"
:= xO (only parsing) : positive_scope.
(* stdpp/numbers.v *)
Notation "(~1)"
:= xI (only parsing) : positive_scope.
(* stdpp/numbers.v *)
Instance add_assoc' : Assoc (=) Pos.add
:= Pos.add_assoc.
(* stdpp/numbers.v *)
Instance add_comm' : Comm (=) Pos.add
:= Pos.add_comm.
(* stdpp/numbers.v *)
Instance mul_assoc' : Assoc (=) Pos.mul
:= Pos.mul_assoc.
(* stdpp/numbers.v *)
Instance mul_comm' : Comm (=) Pos.mul
:= Pos.mul_comm.
(* stdpp/numbers.v *)
Instance mul_left_id : LeftId (=) 1 Pos.mul
:= Pos.mul_1_l.
(* stdpp/numbers.v *)
Instance mul_right_id : RightId (=) 1 Pos.mul
:= Pos.mul_1_r.
(* stdpp/numbers.v *)
Instance eq_dec: EqDecision positive
:= Pos.eq_dec.
(* stdpp/numbers.v *)
Instance le_dec: RelDecision Pos.le.
Proof. refine (λ x y, decide ((x ?= y) ≠ Gt)). Defined.
(* stdpp/numbers.v *)
Instance lt_dec: RelDecision Pos.lt.
Proof. refine (λ x y, decide ((x ?= y) = Lt)). Defined.
(* stdpp/numbers.v *)
Instance le_total: Total Pos.le.
Proof. repeat intro; lia. Qed.
(* stdpp/numbers.v *)
Instance inhabited: Inhabited positive
:= populate 1.
(* stdpp/numbers.v *)
Instance maybe_xO : Maybe xO
:= λ p, match p with p~0 => Some p | _ => None end.
(* stdpp/numbers.v *)
Instance maybe_xI : Maybe xI
:= λ p, match p with p~1 => Some p | _ => None end.
(* stdpp/numbers.v *)
Instance xO_inj : Inj (=) (=) (~0).
Proof. by injection 1. Qed.
(* stdpp/numbers.v *)
Instance xI_inj : Inj (=) (=) (~1).
Proof. by injection 1. Qed.
(* stdpp/numbers.v *)
(* 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.
(* stdpp/numbers.v *)
Notation "(++)"
:= app (only parsing) : positive_scope.
(* stdpp/numbers.v *)
Notation "( p ++.)"
:= (app p) (only parsing) : positive_scope.
(* stdpp/numbers.v *)
Notation "(.++ q )"
:= (λ p, app p q) (only parsing) : positive_scope.
(* stdpp/numbers.v *)
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.
(* stdpp/numbers.v *)
Definition reverse : positive → positive
:= reverse_go 1.
(* stdpp/numbers.v *)
Instance app_1_l : LeftId (=) 1 (++).
Proof. intros p. by induction p; intros; f_equal/=. Qed.
(* stdpp/numbers.v *)
Instance app_1_r : RightId (=) 1 (++).
Proof. done. Qed.
(* stdpp/numbers.v *)
Instance app_assoc : Assoc (=) (++).
Proof. intros ?? p. by induction p; intros; f_equal/=. Qed.
(* stdpp/numbers.v *)
Instance app_inj p : Inj (=) (=) (.++ p).
Proof. intros ???. induction p; simplify_eq; auto. Qed.
(* stdpp/numbers.v *)
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.
(* stdpp/numbers.v *)
Lemma reverse_app p1 p2 : reverse (p1 ++ p2) = reverse p2 ++ reverse p1.
Proof. unfold reverse. by rewrite reverse_go_app. Qed.
(* stdpp/numbers.v *)
Lemma reverse_xO p : reverse (p~0) = (1~0) ++ reverse p.
Proof. apply (reverse_app p (1~0)). Qed.
(* stdpp/numbers.v *)
Lemma reverse_xI p : reverse (p~1) = (1~1) ++ reverse p.
Proof. apply (reverse_app p (1~1)). Qed.
(* stdpp/numbers.v *)
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.
(* stdpp/numbers.v *)
Instance reverse_inj : Inj (=) (=) reverse.
Proof.
    intros p q eq.
    rewrite <-(reverse_involutive p).
    rewrite <-(reverse_involutive q).
    by rewrite eq.
  Qed.
(* stdpp/numbers.v *)
Fixpoint length (p : positive) : nat
:=
    match p with 1 => 0%nat | p~0 | p~1 => S (length p) end.
(* stdpp/numbers.v *)
Lemma length_app p1 p2 : length (p1 ++ p2) = (length p2 + length p1)%nat.
Proof. by induction p2; f_equal/=. Qed.
(* stdpp/numbers.v *)
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.
(* stdpp/numbers.v *)
(* 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.
(* stdpp/numbers.v *)
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.
(* stdpp/numbers.v *)
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.
(* stdpp/numbers.v *)
Instance dup_inj : Inj (=) (=) dup.
Proof.
    intros p q eq.
    apply (dup_suffix_eq _ _ 1 1).
    by rewrite eq.
  Qed.
(* stdpp/numbers.v *)
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.
(* stdpp/numbers.v *)
Notation "x ≤ y ≤ z"
:= (x ≤ y ∧ y ≤ z)%N : N_scope.
(* stdpp/numbers.v *)
Notation "x ≤ y < z"
:= (x ≤ y ∧ y < z)%N : N_scope.
(* stdpp/numbers.v *)
Notation "x < y ≤ z"
:= (x < y ∧ y ≤ z)%N : N_scope.
(* stdpp/numbers.v *)
Notation "x ≤ y ≤ z ≤ z'"
:= (x ≤ y ∧ y ≤ z ∧ z ≤ z')%N : N_scope.
(* stdpp/numbers.v *)
Notation "(≤)"
:= N.le (only parsing) : N_scope.
(* stdpp/numbers.v *)
Notation "(<)"
:= N.lt (only parsing) : N_scope.
(* stdpp/numbers.v *)
Instance add_assoc' : Assoc (=) N.add
:= N.add_assoc.
(* stdpp/numbers.v *)
Instance add_comm' : Comm (=) N.add
:= N.add_comm.