phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/vector.v *)
Lemma vec_to_list_drop_lookup {A n} (v : vec A n) (i : fin n) :
  drop i v = v !!! i :: drop (S i) v.
Proof. induction i as [|?? IHi]; inv_vec v; simpl; intros; [done | by rewrite IHi]. Qed.
(* stdpp/vector.v *)
Lemma vec_to_list_take_drop_lookup {A n} (v : vec A n) (i : fin n) :
  vec_to_list v = take i v ++ v !!! i :: drop (S i) v.
Proof. rewrite <-(take_drop i v) at 1. by rewrite vec_to_list_drop_lookup. Qed.
(* stdpp/vector.v *)
Lemma vlookup_lookup {A n} (v : vec A n) (i : fin n) x :
  v !!! i = x ↔ (v : list A) !! (i : nat) = Some x.
Proof.
  induction v as [|? ? v IH]; inv_fin i.
  - simpl; split; congruence.
  - done.
Qed.
(* stdpp/vector.v *)
Lemma vlookup_lookup' {A n} (v : vec A n) (i : nat) x :
  (∃ H : i < n, v !!! nat_to_fin H = x) ↔ (v : list A) !! i = Some x.
Proof.
  split.
  - intros [Hlt ?]. rewrite <-(fin_to_nat_to_fin i n Hlt). by apply vlookup_lookup.
  - intros Hvix. assert (Hlt:=lookup_lt_Some _ _ _ Hvix).
    rewrite length_vec_to_list in Hlt. exists Hlt.
    apply vlookup_lookup. by rewrite fin_to_nat_to_fin.
Qed.
(* stdpp/vector.v *)
Lemma elem_of_vlookup {A n} (v : vec A n) x :
  x ∈ vec_to_list v ↔ ∃ i, v !!! i = x.
Proof.
  rewrite list_elem_of_lookup. setoid_rewrite <-vlookup_lookup'.
  split; [by intros (?&?&?); eauto|]. intros [i Hx].
  exists i, (fin_to_nat_lt _). by rewrite nat_to_fin_to_nat.
Qed.
(* stdpp/vector.v *)
Lemma Forall_vlookup {A} (P : A → Prop) {n} (v : vec A n) :
  Forall P v ↔ ∀ i, P (v !!! i).
Proof. rewrite Forall_forall. setoid_rewrite elem_of_vlookup. naive_solver. Qed.
(* stdpp/vector.v *)
Lemma Forall_vlookup_1 {A} (P : A → Prop) {n} (v : vec A n) i :
  Forall P v → P (v !!! i).
Proof. by rewrite Forall_vlookup. Qed.
(* stdpp/vector.v *)
Lemma Forall_vlookup_2 {A} (P : A → Prop) {n} (v : vec A n) :
  (∀ i, P (v !!! i)) → Forall P v.
Proof. by rewrite Forall_vlookup. Qed.
(* stdpp/vector.v *)
Lemma Exists_vlookup {A} (P : A → Prop) {n} (v : vec A n) :
  Exists P v ↔ ∃ i, P (v !!! i).
Proof. rewrite Exists_exists. setoid_rewrite elem_of_vlookup. naive_solver. Qed.
(* stdpp/vector.v *)
Lemma Forall2_vlookup {A B} (P : A → B → Prop) {n}
    (v1 : vec A n) (v2 : vec B n) :
  Forall2 P v1 v2 ↔ ∀ i, P (v1 !!! i) (v2 !!! i).
Proof.
  split.
  - vec_double_ind v1 v2; [intros _ i; inv_fin i |].
    intros n v1 v2 IH a b; simpl. inv 1.
    intros i. inv_fin i; simpl; auto.
  - vec_double_ind v1 v2; [constructor|].
    intros ??? IH ?? H. constructor.
    + apply (H 0%fin).
    + apply IH, (λ i, H (FS i)).
Qed.
(* stdpp/vector.v *)
(* Given a function [fin n → A], we can construct a vector. *)
Fixpoint fun_to_vec {A n} {struct n} : (fin n → A) → vec A n
:=
  match n with
  | 0 => λ f, [#]
  | S n => λ f, f 0%fin ::: fun_to_vec (f ∘ FS)
  end.
(* stdpp/vector.v *)
Lemma lookup_fun_to_vec {A n} (f : fin n → A) i : fun_to_vec f !!! i = f i.
Proof.
  revert f. induction i as [|n i IH]; intros f; simpl; [done|]. by rewrite IH.
Qed.
(* stdpp/vector.v *)
(* The function [vmap f v] applies a function [f] element wise to [v]. *)
Notation vmap
:= Vector.map.
(* stdpp/vector.v *)
Lemma vlookup_map `(f : A → B) {n} (v : vec A n) i :
  vmap f v !!! i = f (v !!! i).
Proof. by induction v; inv_fin i; eauto. Qed.
(* stdpp/vector.v *)
Lemma vec_to_list_map `(f : A → B) {n} (v : vec A n) :
  vec_to_list (vmap f v) = f <$> vec_to_list v.
Proof. induction v as [|??? IHv]; simpl; [done|]. by rewrite IHv. Qed.
(* stdpp/vector.v *)
(* The function [vzip_with f v w] combines the vectors [v] and [w] element
wise using the function [f]. *)
Notation vzip_with
:= Vector.map2.
(* stdpp/vector.v *)
Lemma vlookup_zip_with `(f : A → B → C) {n} (v1 : vec A n) (v2 : vec B n) i :
  vzip_with f v1 v2 !!! i = f (v1 !!! i) (v2 !!! i).
Proof.
  vec_double_ind v1 v2.
  - intros i; inv_fin i.
  - intros n v1 v2 IH a b i.
    inv_fin i; eauto.
Qed.
(* stdpp/vector.v *)
Lemma vec_to_list_zip_with `(f : A → B → C) {n} (v1 : vec A n) (v2 : vec B n) :
  vec_to_list (vzip_with f v1 v2) =
    zip_with f (vec_to_list v1) (vec_to_list v2).
Proof.
  revert v2. induction v1 as [|??? IHv1]; intros v2; inv_vec v2; intros; simpl; [done|].
  by rewrite IHv1.
Qed.
(* stdpp/vector.v *)
Instance vec_insert A : ∀ m, Insert (fin m) A (vec A m)
:=
  fix go m i a {struct i} := let _ : ∀ m, Insert _ _ _ := @go in
  match i in fin m return vec A m → vec A m with
  | 0%fin => vec_S_inv _ (λ _ v, a ::: v)
  | FS j => vec_S_inv _ (λ x v, x ::: <[j:=a]> v)
  end.
(* stdpp/vector.v *)
(* Back-compat notation for [vinsert] *)
Notation vinsert
:= (@insert _ _ _ (@vec_insert _ _)) (only parsing).
(* stdpp/vector.v *)
Lemma vec_to_list_insert {A n} i x (v : vec A n) :
  vec_to_list (<[i:=x]> v) = <[fin_to_nat i:=x]> (vec_to_list v).
Proof. induction v as [|??? IHv]; inv_fin i; [done|]. simpl. intros. by rewrite IHv. Qed.
(* stdpp/vector.v *)
Lemma vlookup_insert_eq {A n} i x (v : vec A n) : <[i:=x]> v !!! i = x.
Proof. by induction i; inv_vec v. Qed.
(* stdpp/vector.v *)
Lemma vlookup_insert_ne {A n} i j x (v : vec A n) :
  i ≠ j → <[i:=x]> v !!! j = v !!! j.
Proof.
  induction i as [|?? IHi]; inv_fin j; inv_vec v; simpl; try done.
  intros. apply IHi. congruence.
Qed.
(* stdpp/vector.v *)
Lemma vlookup_insert {A n} i j x (v : vec A n) :
  <[i:=x]> v !!! j = if decide (i = j) then x else v !!! j.
Proof.
  case_decide; subst; eauto using vlookup_insert_eq, vlookup_insert_ne.
Qed.
(* stdpp/vector.v *)
Lemma vlookup_insert_id {A n} i (v : vec A n) : <[i:=v !!! i]> v = v.
Proof. by induction v; inv_fin i; intros; f_equal/=. Qed.
(* stdpp/vector.v *)
Lemma vinsert_insert_eq {A n} i x y (v : vec A n) : <[i:=x]> (<[i:=y]> v) = <[i:=x]> v.
Proof. by induction i; inv_vec v; intros; f_equal/=; auto. Qed.
(* stdpp/vector.v *)
Lemma vinsert_insert_ne {A n} i j x y (v : vec A n) :
  i ≠ j → <[i:=x]> (<[j:=y]> v) = <[j:=y]> (<[i:=x]> v).
Proof. by induction v; inv_fin i; inv_fin j; intros; f_equal/=; naive_solver. Qed.
(* stdpp/vector.v *)
Lemma vinsert_insert {A n} i j x y (v : vec A n) :
  <[i:=x]> (<[j:=y]> v) =
    if decide (i = j) then <[i:=x]> v else <[j:=y]> (<[i:=x]> v).
Proof.
  case_decide; subst; auto using vinsert_insert_eq, vinsert_insert_ne.
Qed.
(* stdpp/vector.v *)
Lemma vmap_insert {A B} (f : A → B) (n : nat) i x (v : vec A n) :
  vmap f (<[i:=x]> v) = <[i:=f x]> (vmap f v).
Proof. induction v; inv_fin i; intros; f_equal/=; auto. Qed.
(* stdpp/vector.v *)
Lemma Forall_vinsert {A} (P : A → Prop) {n} (v : vec A n) (i : fin n) (x : A) :
  Forall P v →
  P x →
  Forall P (vec_to_list (<[i:=x]> v)).
Proof. rewrite vec_to_list_insert. apply Forall_insert. Qed.
(* stdpp/vector.v *)
(* The functions [vtake i v] and [vdrop i v] take the first [i] elements of
a vector [v], respectively remove the first [i] elements of a vector [v]. *)
Fixpoint vtake {A n} (i : fin n) : vec A n → vec A i
:=
  match i in fin n return vec A n → vec A i with
  | 0%fin => λ _, [#]
  | FS i => vec_S_inv _ (λ x v, x ::: vtake i v)
  end.
(* stdpp/vector.v *)
Fixpoint vdrop {A n} (i : fin n) : vec A n → vec A (n - i)
:=
  match i in fin n return vec A n → vec A (n - i) with
  | 0%fin => id
  | FS i => vec_S_inv _ (λ _, vdrop i)
  end.
(* stdpp/vector.v *)
Lemma vec_to_list_take {A n} i (v : vec A n) :
  vec_to_list (vtake i v) = take (fin_to_nat i) (vec_to_list v).
Proof. induction i; inv_vec v; intros; f_equal/=; auto. Qed.
(* stdpp/vector.v *)
Lemma vec_to_list_drop {A n} i (v : vec A n) :
  vec_to_list (vdrop i v) = drop (fin_to_nat i) (vec_to_list v).
Proof. induction i; inv_vec v; intros; f_equal/=; auto. Qed.
(* stdpp/vector.v *)
(* The function [vreplicate n x] generates a vector with length [n] of elements
with value [x]. *)
Fixpoint vreplicate {A} (n : nat) (x : A) : vec A n
:=
  match n with 0 => [#] | S n => x ::: vreplicate n x end.
(* stdpp/vector.v *)
Lemma vec_to_list_replicate {A} n (x : A) :
  vec_to_list (vreplicate n x) = replicate n x.
Proof. induction n; by f_equal/=. Qed.
(* stdpp/vector.v *)
Lemma vlookup_replicate {A} n (x : A) i : vreplicate n x !!! i = x.
Proof. induction i; f_equal/=; auto. Qed.
(* stdpp/vector.v *)
Lemma vmap_replicate {A B} (f : A → B) n (x : A) :
  vmap f (vreplicate n x) = vreplicate n (f x).
Proof. induction n; f_equal/=; auto. Qed.
(* stdpp/vector.v *)
Lemma Forall_vreplicate {A} (P : A → Prop) n (x : A) :
  P x →
  Forall P (vreplicate n x).
Proof. rewrite vec_to_list_replicate. apply Forall_replicate. Qed.
(* stdpp/vector.v *)
(* Vectors are inhabited and countable *)
Instance vec_0_inhabited T : Inhabited (vec T 0)
:= populate [#].
(* stdpp/vector.v *)
Instance vec_inhabited `{Inhabited T} n : Inhabited (vec T n)
:=
  populate (vreplicate n inhabitant).
(* stdpp/vector.v *)
Instance vec_countable `{Countable A} n : Countable (vec A n).
Proof.
  apply (inj_countable vec_to_list (λ l,
    H ← guard (n = length l); Some (eq_rect _ _ (list_to_vec l) _ (eq_sym H)))).
  intros v. case_guard as Hn; simplify_eq/=.
  - rewrite list_to_vec_to_list.
    rewrite (proof_irrel (eq_sym _) Hn). by destruct Hn.
  - by rewrite length_vec_to_list in Hn.
Qed.
(* stdpp/well_founded.v *)
Lemma Acc_impl {A} (R1 R2 : relation A) x :
  Acc R1 x → (∀ y1 y2, R2 y1 y2 → R1 y1 y2) → Acc R2 x.
Proof. induction 1; constructor; auto. Qed.
(* stdpp/well_founded.v *)
(* The function [wf_guard n wfR] adds [2 ^ n - 1] times an [Acc_intro]
constructor ahead of the [wfR] proof. This definition can be used to make
opaque [well_founded] proofs "compute". For big enough [n], say [32], computation will
reach implementation limits before running into the opaque [well_founded] proof.

This trick is originally due to Georges Gonthier, see
https://sympa.inria.fr/sympa/arc/coq-club/2007-07/msg00013.html *)
Definition wf_guard `{R : relation A} (n : nat)
    (wfR : well_founded R) : well_founded R
:=
  Acc_intro_generator n wfR.
(* stdpp/well_founded.v *)
Lemma wf_projected `{R1 : relation A} `(R2 : relation B) (f : A → B) :
  (∀ x y, R1 x y → R2 (f x) (f y)) →
  well_founded R2 → well_founded R1.
Proof.
  intros Hf Hwf.
  cut (∀ y, Acc R2 y → ∀ x, y = f x → Acc R1 x).
  { intros aux x. apply (aux (f x)); auto. }
  induction 1 as [y _ IH]. intros x ?. subst.
  constructor. intros y ?. apply (IH (f y)); auto.
Qed.
(* stdpp/well_founded.v *)
Lemma Fix_F_proper `{R : relation A} (B : A → Type) (E : ∀ x, relation (B x))
    (F : ∀ x, (∀ y, R y x → B y) → B x)
    (HF : ∀ (x : A) (f g : ∀ y, R y x → B y),
      (∀ y Hy Hy', E _ (f y Hy) (g y Hy')) → E _ (F x f) (F x g))
    (x : A) (acc1 acc2 : Acc R x) :
  E _ (Fix_F B F acc1) (Fix_F B F acc2).
Proof. revert x acc1 acc2. fix FIX 2. intros x [acc1] [acc2]; simpl; auto. Qed.
(* stdpp/well_founded.v *)
Lemma Fix_unfold_rel `{R : relation A} (wfR : well_founded R)
    (B : A → Type) (E : ∀ x, relation (B x))
    (F: ∀ x, (∀ y, R y x → B y) → B x)
    (HF: ∀ (x: A) (f g: ∀ y, R y x → B y),
           (∀ y Hy Hy', E _ (f y Hy) (g y Hy')) → E _ (F x f) (F x g))
    (x: A) :
  E _ (Fix wfR B F x) (F x (λ y _, Fix wfR B F y)).
Proof.
  unfold Fix.
  destruct (wfR x); simpl.
  apply HF; intros.
  apply Fix_F_proper; auto.
Qed.
(* stdpp/well_founded.v *)
(* Generate an induction principle for [Acc] for reasoning about recursion on
[Acc], such as [countable.choose_proper].

We need an induction principle to prove predicates of [Acc] values, with
conclusion [∀ (x : A) (a : Acc R x), P x a]. Instead, [Acc_ind] has conclusion
[∀ x : A, Acc R x → P x], as if it were generated by
[Scheme Acc_rect := Minimality for Acc Sort Prop.] *)
Scheme Acc_dep_ind
:= Induction for Acc Sort Prop.
(* stdpp/zmap.v *)
Record Zmap (A : Type) : Type
:=
  ZMap { Zmap_0 : option A; Zmap_pos : Pmap A; Zmap_neg : Pmap A }.
(* stdpp/zmap.v *)
Instance Zmap_eq_dec `{EqDecision A} : EqDecision (Zmap A).
Proof.
 refine (λ t1 t2,
  match t1, t2 with
  | ZMap x t1 t1', ZMap y t2 t2' =>
     cast_if_and3 (decide (x = y)) (decide (t1 = t2)) (decide (t1' = t2'))
  end); abstract congruence.
Defined.
(* stdpp/zmap.v *)
Instance Zmap_empty {A} : Empty (Zmap A)
:= ZMap None ∅ ∅.
(* stdpp/zmap.v *)
Instance Zmap_lookup {A} : Lookup Z A (Zmap A)
:= λ i t,
  match i with
  | Z0 => Zmap_0 t | Zpos p => Zmap_pos t !! p | Zneg p => Zmap_neg t !! p
  end.
(* stdpp/zmap.v *)
Instance Zmap_partial_alter {A} : PartialAlter Z A (Zmap A)
:= λ f i t,
  match i, t with
  | Z0, ZMap o t t' => ZMap (f o) t t'
  | Z.pos p, ZMap o t t' => ZMap o (partial_alter f p t) t'
  | Z.neg p, ZMap o t t' => ZMap o t (partial_alter f p t')
  end.
(* stdpp/zmap.v *)
Instance Zmap_fmap: FMap Zmap
:= λ A B f t,
  match t with ZMap o t t' => ZMap (f <$> o) (f <$> t) (f <$> t') end.
(* stdpp/zmap.v *)
Instance Zmap_omap: OMap Zmap
:= λ A B f t,
  match t with ZMap o t t' => ZMap (o ≫= f) (omap f t) (omap f t') end.
(* stdpp/zmap.v *)
Instance Zmap_merge: Merge Zmap
:= λ A B C f t1 t2,
  match t1, t2 with
  | ZMap o1 t1 t1', ZMap o2 t2 t2' =>
     ZMap (diag_None f o1 o2) (merge f t1 t2) (merge f t1' t2')
  end.
(* stdpp/zmap.v *)
Instance Zmap_fold {A} : MapFold Z A (Zmap A)
:= λ B f d t,
  match t with
  | ZMap mx t t' => map_fold (f ∘ Z.pos) (map_fold (f ∘ Z.neg)
     match mx with Some x => f 0 x d | None => d end t') t
  end.
(* stdpp/zmap.v *)
Instance Zmap_map: FinMap Z Zmap.
Proof.
  split.
  - intros ? [??] [??] H. f_equal.
    + apply (H 0).
    + apply map_eq. intros i. apply (H (Z.pos i)).
    + apply map_eq. intros i. apply (H (Z.neg i)).
  - by intros ? [].
  - intros ? f [] [|?|?]; simpl; [done| |]; apply lookup_partial_alter_eq.
  - intros ? f [] [|?|?] [|?|?]; simpl; 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 t'].
    induction t as [|i x t ? Hfold IH] using map_fold_fmap_ind.
    { induction t' as [|i x t' ? Hfold IH] using map_fold_fmap_ind.
      { destruct mx as [x|]; [|done].
        replace (ZMap (Some x) ∅ ∅) with (<[0:=x]> ∅ : Zmap _) by done.
        by apply Hins. }
      apply (Hins (Z.neg i) x (ZMap mx ∅ t')); [done| |done].
      intros A' B f g b. apply Hfold. }
    apply (Hins (Z.pos i) x (ZMap mx t t')); [done| |done].
    intros A' B f g b. apply Hfold.
Qed.
(* stdpp/zmap.v *)
(* We construct sets of [Z]s satisfying extensional equality. *)
Notation Zset
:= (mapset Zmap).
(* stdpp/zmap.v *)
Instance Zmap_dom {A} : Dom (Zmap A) Zset
:= mapset_dom.
(* stdpp/zmap.v *)
Instance : FinMapDom Z Zmap Zset
:= mapset_dom_spec.
(* stdpp_bitvector/definitions.v *)
(* * Preliminary definitions *)
Definition bv_modulus (n : N) : Z
:= 2 ^ (Z.of_N n).
(* stdpp_bitvector/definitions.v *)
Definition bv_half_modulus (n : N) : Z
:= bv_modulus n `div` 2.
(* stdpp_bitvector/definitions.v *)
Definition bv_wrap (n : N) (z : Z) : Z
:= z `mod` bv_modulus n.
(* stdpp_bitvector/definitions.v *)
Definition bv_swrap (n : N) (z : Z) : Z
:= bv_wrap n (z + bv_half_modulus n) - bv_half_modulus n.
(* stdpp_bitvector/definitions.v *)
Lemma bv_modulus_pos n :
  0 < bv_modulus n.
Proof. apply Z.pow_pos_nonneg; lia. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_modulus_gt_1 n :
  n ≠ 0%N →
  1 < bv_modulus n.
Proof. intros ?. apply Z.pow_gt_1; lia. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_half_modulus_nonneg n :
  0 ≤ bv_half_modulus n.
Proof. apply Z.div_pos; [|done]. pose proof bv_modulus_pos n. lia. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_modulus_add n1 n2 :
  bv_modulus (n1 + n2) = bv_modulus n1 * bv_modulus n2.
Proof. unfold bv_modulus. rewrite N2Z.inj_add. eapply Z.pow_add_r; lia. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_half_modulus_twice n:
  n ≠ 0%N →
  bv_half_modulus n + bv_half_modulus n = bv_modulus n.
Proof.
  intros. unfold bv_half_modulus, bv_modulus.
  rewrite Z.add_diag. symmetry. apply Z_div_exact_2; [lia|].
  rewrite <-Z.pow_pred_r by lia. rewrite Z.mul_comm. by apply Z.mod_mul.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_half_modulus_lt_modulus n:
  bv_half_modulus n < bv_modulus n.
Proof.
  pose proof bv_modulus_pos n.
  apply Z_div_lt; [done| lia].
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_modulus_le_mono n m:
  (n ≤ m)%N →
  bv_modulus n ≤ bv_modulus m.
Proof. intros. apply Z.pow_le_mono; [done|lia]. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_half_modulus_le_mono n m:
  (n ≤ m)%N →
  bv_half_modulus n ≤ bv_half_modulus m.
Proof. intros. apply Z.div_le_mono; [done|]. by apply bv_modulus_le_mono. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_modulus_0:
  bv_modulus 0 = 1.
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_half_modulus_0:
  bv_half_modulus 0 = 0.
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_half_modulus_twice_mult n:
  bv_half_modulus n + bv_half_modulus n = (Z.of_N n `min` 1) * bv_modulus n.
Proof. destruct (decide (n = 0%N)); subst; [ rewrite bv_half_modulus_0 | rewrite bv_half_modulus_twice]; lia. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_in_range n z:
  0 ≤ bv_wrap n z < bv_modulus n.
Proof. apply Z.mod_pos_bound. apply bv_modulus_pos. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_swrap_in_range n z:
  n ≠ 0%N →
  - bv_half_modulus n ≤ bv_swrap n z < bv_half_modulus n.
Proof.
  intros ?. unfold bv_swrap.
  pose proof bv_half_modulus_twice n.
  pose proof bv_wrap_in_range n (z + bv_half_modulus n).
  lia.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_small n z :
  0 ≤ z < bv_modulus n → bv_wrap n z = z.
Proof. intros. by apply Z.mod_small. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_swrap_small n z :
  - bv_half_modulus n ≤ z < bv_half_modulus n →
  bv_swrap n z = z.
Proof.
  intros Hrange. unfold bv_swrap.
  destruct (decide (n = 0%N)); subst.
  { rewrite bv_half_modulus_0 in Hrange. lia. }
  pose proof bv_half_modulus_twice n.
  rewrite bv_wrap_small by lia. lia.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_0 n :
  bv_wrap n 0 = 0.
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_swrap_0 n :
  bv_swrap n 0 = 0.
Proof.
  pose proof bv_half_modulus_lt_modulus n.
  pose proof bv_half_modulus_nonneg n.
  unfold bv_swrap. rewrite bv_wrap_small; lia.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_idemp n b : bv_wrap n (bv_wrap n b) = bv_wrap n b.
Proof. unfold bv_wrap. by rewrite Zmod_mod. Qed.
(* stdpp_bitvector/definitions.v *)
Definition bv_wrap_factor (n : N) (x z : Z)
:=
  x = - z `div` bv_modulus n.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_factor_intro n z :
  ∃ x, bv_wrap_factor n x z ∧ bv_wrap n z = z + x * bv_modulus n.
Proof.
  eexists _. split; [done|].
  pose proof (bv_modulus_pos n). unfold bv_wrap. rewrite Z.mod_eq; lia.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_add_modulus c n z:
  bv_wrap n (z + c * bv_modulus n) = bv_wrap n z.
Proof. apply Z_mod_plus_full. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_add_modulus_1 n z:
  bv_wrap n (z + bv_modulus n) = bv_wrap n z.
Proof. rewrite <-(bv_wrap_add_modulus 1 n z). f_equal. lia. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_sub_modulus c n z:
  bv_wrap n (z - c * bv_modulus n) = bv_wrap n z.
Proof. rewrite <-(bv_wrap_add_modulus (-c) n z). f_equal. lia. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_sub_modulus_1 n z:
  bv_wrap n (z - bv_modulus n) = bv_wrap n z.
Proof. rewrite <-(bv_wrap_add_modulus (-1) n z). done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_add_idemp n x y :
  bv_wrap n (bv_wrap n x + bv_wrap n y) = bv_wrap n (x + y).
Proof. symmetry. apply Zplus_mod. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_add_idemp_l n x y :
  bv_wrap n (bv_wrap n x + y) = bv_wrap n (x + y).
Proof. apply Zplus_mod_idemp_l. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_add_idemp_r n x y :
  bv_wrap n (x + bv_wrap n y) = bv_wrap n (x + y).
Proof. apply Zplus_mod_idemp_r. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_opp_idemp n x :
  bv_wrap n (- bv_wrap n x) = bv_wrap n (- x).
Proof.
  unfold bv_wrap. pose proof (bv_modulus_pos n).
  destruct (decide (x `mod` bv_modulus n = 0)) as [Hx|Hx].
  - rewrite !Z.mod_opp_l_z; [done |lia|done|lia|by rewrite Hx].
  - rewrite !Z.mod_opp_l_nz, Z.mod_mod;
      [done|lia|lia|done|lia|by rewrite Z.mod_mod by lia].
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_mul_idemp n x y :
  bv_wrap n (bv_wrap n x * bv_wrap n y) = bv_wrap n (x * y).
Proof. etrans; [| apply Zmult_mod_idemp_r]. apply Zmult_mod_idemp_l. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_mul_idemp_l n x y :
  bv_wrap n (bv_wrap n x * y) = bv_wrap n (x * y).
Proof. apply Zmult_mod_idemp_l. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_mul_idemp_r n x y :
  bv_wrap n (x * bv_wrap n y) = bv_wrap n (x * y).
Proof. apply Zmult_mod_idemp_r. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_sub_idemp n x y :
  bv_wrap n (bv_wrap n x - bv_wrap n y) = bv_wrap n (x - y).
Proof.
  by rewrite <-!Z.add_opp_r, <-bv_wrap_add_idemp_r,
    bv_wrap_opp_idemp, bv_wrap_add_idemp.
 Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_sub_idemp_l n x y :
  bv_wrap n (bv_wrap n x - y) = bv_wrap n (x - y).
Proof. by rewrite <-!Z.add_opp_r, bv_wrap_add_idemp_l. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_sub_idemp_r n x y :
  bv_wrap n (x - bv_wrap n y) = bv_wrap n (x - y).
Proof.
  by rewrite <-!Z.add_opp_r, <-bv_wrap_add_idemp_r,
    bv_wrap_opp_idemp, bv_wrap_add_idemp_r.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_succ_idemp n x :
  bv_wrap n (Z.succ (bv_wrap n x)) = bv_wrap n (Z.succ x).
Proof. by rewrite <-!Z.add_1_r, bv_wrap_add_idemp_l. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_pred_idemp n x :
  bv_wrap n (Z.pred (bv_wrap n x)) = bv_wrap n (Z.pred x).
Proof. by rewrite <-!Z.sub_1_r, bv_wrap_sub_idemp_l. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_add_inj n x1 x2 y :
  bv_wrap n x1 = bv_wrap n x2 ↔ bv_wrap n (x1 + y) = bv_wrap n (x2 + y).
Proof.
  split; intros Heq.
  - by rewrite <-bv_wrap_add_idemp_l, Heq, bv_wrap_add_idemp_l.
  - pose proof (bv_wrap_factor_intro n (x1 + y)) as [f1[? Hx1]].
    pose proof (bv_wrap_factor_intro n (x2 + y)) as [f2[? Hx2]].
    assert (x1 = x2 + f2 * bv_modulus n - f1 * bv_modulus n) as -> by lia.
    by rewrite bv_wrap_sub_modulus, bv_wrap_add_modulus.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_swrap_wrap n z:
  bv_swrap n (bv_wrap n z) = bv_swrap n z.
Proof. unfold bv_swrap, bv_wrap. by rewrite Zplus_mod_idemp_l. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_bv_wrap n1 n2 bv :
  (n1 ≤ n2)%N →
  bv_wrap n1 (bv_wrap n2 bv) = bv_wrap n1 bv.
Proof.
  intros ?. unfold bv_wrap.
  rewrite <-Znumtheory.Zmod_div_mod; [done| apply bv_modulus_pos.. |].
  unfold bv_modulus. eexists (2 ^ (Z.of_N n2 - Z.of_N n1)).
  rewrite <-Z.pow_add_r by lia. f_equal. lia.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_land n z :
  bv_wrap n z = Z.land z (Z.ones (Z.of_N n)).
Proof. by rewrite Z.land_ones by lia. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_spec n z i:
  0 ≤ i →
  Z.testbit (bv_wrap n z) i = bool_decide (i < Z.of_N n) && Z.testbit z i.
Proof.
  intros ?. rewrite bv_wrap_land, Z.land_spec, Z.ones_spec by lia.
  case_bool_decide; simpl; by rewrite ?andb_true_r, ?andb_false_r.
Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_spec_low n z i:
  0 ≤ i < Z.of_N n →
  Z.testbit (bv_wrap n z) i = Z.testbit z i.
Proof. intros ?. rewrite bv_wrap_spec; [|lia]. case_bool_decide; [done|]. lia. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_wrap_spec_high n z i:
  Z.of_N n ≤ i →
  Z.testbit (bv_wrap n z) i = false.
Proof. intros ?. rewrite bv_wrap_spec; [|lia]. case_bool_decide; [|done]. lia. Qed.