phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_divu s w n b1 b2 z1 z2 :
  BvUnfold n false false b1 z1 →
  BvUnfold n false false b2 z2 →
  BvUnfold n s w (bv_divu b1 b2) (if w then z1 `div` z2 else if s then bv_swrap n (z1 `div` z2) else z1 `div` z2).
Proof.
  intros [Hz1] [Hz2]. constructor.
  destruct w, s; rewrite ?bv_divu_signed, ?bv_divu_unsigned, ?Hz1, ?Hz2; try bv_wrap_simplify_solve.
  - pose proof (bv_unsigned_in_range _ (bv_divu b1 b2)) as Hr. rewrite bv_divu_unsigned in Hr. subst.
    by rewrite bv_wrap_small.
  - done.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_modu s w n b1 b2 z1 z2 :
  BvUnfold n false false b1 z1 →
  BvUnfold n false false b2 z2 →
  BvUnfold n s w (bv_modu b1 b2) (if w then z1 `mod` z2 else if s then bv_swrap n (z1 `mod` z2) else z1 `mod` z2).
Proof.
  intros [Hz1] [Hz2]. constructor.
  destruct w, s; rewrite ?bv_modu_signed, ?bv_modu_unsigned, ?Hz1, ?Hz2; try bv_wrap_simplify_solve.
  - pose proof (bv_unsigned_in_range _ (bv_modu b1 b2)) as Hr. rewrite bv_modu_unsigned in Hr. subst.
    by rewrite bv_wrap_small.
  - done.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_divs s w n b1 b2 z1 z2 :
  BvUnfold n true false b1 z1 →
  BvUnfold n true false b2 z2 →
  BvUnfold n s w (bv_divs b1 b2) (if w then z1 `div` z2 else bv_suwrap s n (z1 `div` z2)).
Proof.
  intros [Hz1] [Hz2]. constructor.
  destruct w, s; rewrite ?bv_divs_signed, ?bv_divs_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_quots s w n b1 b2 z1 z2 :
  BvUnfold n true false b1 z1 →
  BvUnfold n true false b2 z2 →
  BvUnfold n s w (bv_quots b1 b2) (if w then z1 `quot` z2 else bv_suwrap s n (z1 `quot` z2)).
Proof.
  intros [Hz1] [Hz2]. constructor.
  destruct w, s; rewrite ?bv_quots_signed, ?bv_quots_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_mods s w n b1 b2 z1 z2 :
  BvUnfold n true false b1 z1 →
  BvUnfold n true false b2 z2 →
  BvUnfold n s w (bv_mods b1 b2) (if w then z1 `mod` z2 else bv_suwrap s n (z1 `mod` z2)).
Proof.
  intros [Hz1] [Hz2]. constructor.
  destruct w, s; rewrite ?bv_mods_signed, ?bv_mods_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_rems s w n b1 b2 z1 z2 :
  BvUnfold n true false b1 z1 →
  BvUnfold n true false b2 z2 →
  BvUnfold n s w (bv_rems b1 b2) (if w then z1 `rem` z2 else bv_suwrap s n (z1 `rem` z2)).
Proof.
  intros [Hz1] [Hz2]. constructor.
  destruct w, s; rewrite ?bv_rems_signed, ?bv_rems_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_shiftl s w n b1 b2 z1 z2 :
  BvUnfold n false false b1 z1 →
  BvUnfold n false false b2 z2 →
  BvUnfold n s w (bv_shiftl b1 b2) (if w then z1 ≪ z2 else bv_suwrap s n (z1 ≪ z2)).
Proof.
  intros [Hz1] [Hz2]. constructor.
  destruct w, s; rewrite ?bv_shiftl_signed, ?bv_shiftl_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_shiftr s w n b1 b2 z1 z2 :
  BvUnfold n false false b1 z1 →
  BvUnfold n false false b2 z2 →
  BvUnfold n s w (bv_shiftr b1 b2) (if w then z1 ≫ z2 else if s then bv_swrap n (z1 ≫ z2) else (z1 ≫ z2)).
Proof.
  intros [Hz1] [Hz2]. constructor.
  destruct w, s; rewrite ?bv_shiftr_signed, ?bv_shiftr_unsigned, ?Hz1, ?Hz2; try bv_wrap_simplify_solve.
  - pose proof (bv_unsigned_in_range _ (bv_shiftr b1 b2)) as Hr. rewrite bv_shiftr_unsigned in Hr. subst.
    by rewrite bv_wrap_small.
  - done.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_ashiftr s w n b1 b2 z1 z2 :
  BvUnfold n true false b1 z1 →
  BvUnfold n false false b2 z2 →
  BvUnfold n s w (bv_ashiftr b1 b2) (if w then z1 ≫ z2 else bv_suwrap s n (z1 ≫ z2)).
Proof.
  intros [Hz1] [Hz2]. constructor.
  destruct w, s; rewrite ?bv_ashiftr_signed, ?bv_ashiftr_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_or s w n b1 b2 z1 z2 :
  BvUnfold n false false b1 z1 →
  BvUnfold n false false b2 z2 →
  BvUnfold n s w (bv_or b1 b2) (if w then Z.lor z1 z2 else if s then bv_swrap n (Z.lor z1 z2) else Z.lor z1 z2).
Proof.
  intros [Hz1] [Hz2]. constructor.
  destruct w, s; rewrite ?bv_or_signed, ?bv_or_unsigned, ?Hz1, ?Hz2; try bv_wrap_simplify_solve.
  - pose proof (bv_unsigned_in_range _ (bv_or b1 b2)) as Hr. rewrite bv_or_unsigned in Hr. subst.
    by rewrite bv_wrap_small.
  - done.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_and s w n b1 b2 z1 z2 :
  BvUnfold n false false b1 z1 →
  BvUnfold n false false b2 z2 →
  BvUnfold n s w (bv_and b1 b2) (if w then Z.land z1 z2 else if s then bv_swrap n (Z.land z1 z2) else Z.land z1 z2).
Proof.
  intros [Hz1] [Hz2]. constructor.
  destruct w, s; rewrite ?bv_and_signed, ?bv_and_unsigned, ?Hz1, ?Hz2; try bv_wrap_simplify_solve.
  - pose proof (bv_unsigned_in_range _ (bv_and b1 b2)) as Hr. rewrite bv_and_unsigned in Hr. subst.
    by rewrite bv_wrap_small.
  - done.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_xor s w n b1 b2 z1 z2 :
  BvUnfold n false false b1 z1 →
  BvUnfold n false false b2 z2 →
  BvUnfold n s w (bv_xor b1 b2) (if w then Z.lxor z1 z2 else if s then bv_swrap n (Z.lxor z1 z2) else Z.lxor z1 z2).
Proof.
  intros [Hz1] [Hz2]. constructor.
  destruct w, s; rewrite ?bv_xor_signed, ?bv_xor_unsigned, ?Hz1, ?Hz2; try bv_wrap_simplify_solve.
  - pose proof (bv_unsigned_in_range _ (bv_xor b1 b2)) as Hr. rewrite bv_xor_unsigned in Hr. subst.
    by rewrite bv_wrap_small.
  - done.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_not s w n b z :
  BvUnfold n false false b z →
  BvUnfold n s w (bv_not b) (if w then Z.lnot z else bv_suwrap s n (Z.lnot z)).
Proof.
  intros [Hz]. constructor.
  destruct w, s; rewrite ?bv_not_signed, ?bv_not_unsigned, ?Hz; bv_wrap_simplify_solve.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_zero_extend s w n n' b z `{!TCFastDone ((n' <=? n) = true)%N} :
  BvUnfold n' false false b z →
  BvUnfold n s w (bv_zero_extend n b) (if w then z else if s then bv_swrap n z else z).
Proof.
  intros [Hz]. constructor. unfold TCFastDone in *. rewrite ->?N.leb_le in *.
  destruct w, s; rewrite ?bv_zero_extend_signed, ?bv_zero_extend_unsigned, ?Hz by done;
    try bv_wrap_simplify_solve.
  - rewrite <-Hz, bv_wrap_small; [done|]. bv_saturate. pose proof (bv_modulus_le_mono n' n). lia.
  - done.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_sign_extend s w n n' b z `{!TCFastDone ((n' <=? n) = true)%N} :
  BvUnfold n' true false b z →
  BvUnfold n s w (bv_sign_extend n b) (if w then z else if s then z else bv_wrap n z).
Proof.
  intros [Hz]. constructor. unfold TCFastDone in *. rewrite ->?N.leb_le in *.
  destruct w, s; rewrite ?bv_sign_extend_signed, ?bv_sign_extend_unsigned, ?Hz by done;
    try bv_wrap_simplify_solve.
  - subst. rewrite <-(bv_sign_extend_signed n) at 2 by done. by rewrite bv_swrap_bv_signed, bv_sign_extend_signed.
  - done.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_extract s w n n' n1 b z :
  BvUnfold n' false false b z →
  BvUnfold n s w (bv_extract n1 n b) (if w then z ≫ Z.of_N n1 else bv_suwrap s n (z ≫ Z.of_N n1)).
Proof.
  intros [Hz]. constructor.
  destruct w, s; rewrite ?bv_extract_signed, ?bv_extract_unsigned, ?Hz; bv_wrap_simplify_solve.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_concat s w n n1 n2 b1 b2 z1 z2 `{!TCFastDone (n = n1 + n2)%N} :
  BvUnfold n1 false false b1 z1 →
  BvUnfold n2 false false b2 z2 →
  BvUnfold n s w (bv_concat n b1 b2) (if w then Z.lor (z1 ≪ Z.of_N n2) z2 else if s then  bv_swrap n (Z.lor (z1 ≪ Z.of_N n2) z2) else Z.lor (z1 ≪ Z.of_N n2) z2).
Proof.
  intros [Hz1] [Hz2]. constructor. unfold TCFastDone in *.
  destruct w, s; rewrite ?bv_concat_signed, ?bv_concat_unsigned, ?Hz1, ?Hz2 by done;
    try bv_wrap_simplify_solve.
  - subst. rewrite <-(bv_concat_unsigned (n1 + n2)) at 2 by done.
    by rewrite bv_wrap_bv_unsigned, bv_concat_unsigned.
  - done.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_add_Z s w n b1 z1 z2 :
  BvUnfold n s true b1 z1 →
  BvUnfold n s w (bv_add_Z b1 z2) (if w then z1 + z2 else bv_suwrap s n (z1 + z2)).
Proof.
  intros [Hz1]. constructor.
  destruct w, s; rewrite ?bv_add_Z_signed, ?bv_add_Z_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_sub_Z s w n b1 z1 z2 :
  BvUnfold n s true b1 z1 →
  BvUnfold n s w (bv_sub_Z b1 z2) (if w then z1 - z2 else bv_suwrap s n (z1 - z2)).
Proof.
  intros [Hz1]. constructor.
  destruct w, s; rewrite ?bv_sub_Z_signed, ?bv_sub_Z_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_mul_Z s w n b1 z1 z2 :
  BvUnfold n s true b1 z1 →
  BvUnfold n s w (bv_mul_Z b1 z2) (if w then z1 * z2 else bv_suwrap s n (z1 * z2)).
Proof.
  intros [Hz1]. constructor.
  destruct w, s; rewrite ?bv_mul_Z_signed, ?bv_mul_Z_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
Qed.
(* stdpp_bitvector/tactics.v *)
Ltac bv_unfold_eq
:=
  lazymatch goal with
  | |- @bv_unsigned ?n ?b = ?z =>
      simple notypeclasses refine (@bv_unfold_proof n false false b z _)
  | |- @bv_signed ?n ?b = ?z =>
      simple notypeclasses refine (@bv_unfold_proof n true false b z _)
  end;
  typeclasses eauto with bv_unfold_db.
(* stdpp_bitvector/tactics.v *)
Ltac bv_unfold
:=
  repeat (match goal with
            (* TODO: Detect if there is a bv_wrap around the
            bv_unsigned (like after applying bv_eq_wrapped) *)
          | |- context [@bv_unsigned ?n ?b] =>
              pattern (@bv_unsigned n b);
              simple refine (eq_rec_r _ _ _); [shelve| |bv_unfold_eq]; cbn beta
          | |- context [@bv_signed ?n ?b] =>
              pattern (@bv_signed n b);
              simple refine (eq_rec_r _ _ _); [shelve| |bv_unfold_eq]; cbn beta
          end); unfold BV_UNFOLD_BLOCK.
(* stdpp_bitvector/tactics.v *)
(* * Reduction of closed terms *)
Ltac reduce_closed_N_tac
:= idtac.
(* stdpp_bitvector/tactics.v *)
Ltac reduce_closed_N
:=
  idtac;
  reduce_closed_N_tac;
  repeat match goal with
  | |- context [N.add ?a ?b] => progress reduce_closed (N.add a b)
  | H : context [N.add ?a ?b] |- _ => progress reduce_closed (N.add a b)
  end.
(* stdpp_bitvector/tactics.v *)
Ltac reduce_closed_bv_simplify_tac
:= idtac.
(* stdpp_bitvector/tactics.v *)
Ltac reduce_closed_bv_simplify
:=
  idtac;
  reduce_closed_bv_simplify_tac;
  (* reduce closed logical operators that lia does not understand *)
  repeat match goal with
  | |- context [Z.lor ?a ?b] => progress reduce_closed (Z.lor a b)
  | H : context [Z.lor ?a ?b] |- _ => progress reduce_closed (Z.lor a b)
  | |- context [Z.land ?a ?b] => progress reduce_closed (Z.land a b)
  | H : context [Z.land ?a ?b] |- _ => progress reduce_closed (Z.land a b)
  | |- context [Z.lxor ?a ?b] => progress reduce_closed (Z.lxor a b)
  | H : context [Z.lxor ?a ?b] |- _ => progress reduce_closed (Z.lxor a b)
  end.
(* stdpp_bitvector/tactics.v *)
(* * [bv_solve] tactic *)
Ltac bv_solve_unfold_tac
:= idtac.
(* stdpp_bitvector/tactics.v *)
Ltac bv_solve
:=
  bv_simplify_arith;
  (* we unfold signed so we just need to saturate unsigned *)
  bv_saturate_unsigned;
  bv_solve_unfold_tac;
  unfold bv_signed, bv_swrap, bv_wrap, bv_half_modulus, bv_modulus, bv_unsigned in *;
  simpl;
  lia.
(* stdpp_bitvector/tactics.v *)
Class BvSolve (P : Prop) : Prop
:= bv_solve_proof : P.
(* stdpp_unstable/bitblast.v *)
(* * Helper lemmas to upstream *)
Lemma Nat_eqb_eq n1 n2 :
  (n1 =? n2)%nat = bool_decide (n1 = n2).
Proof. case_bool_decide; [by apply Nat.eqb_eq | by apply Nat.eqb_neq]. Qed.
(* stdpp_unstable/bitblast.v *)
Lemma Z_eqb_eq n1 n2 :
  (n1 =? n2)%Z = bool_decide (n1 = n2).
Proof. case_bool_decide; [by apply Z.eqb_eq | by apply Z.eqb_neq]. Qed.
(* stdpp_unstable/bitblast.v *)
Lemma Z_testbit_pos_testbit p n :
  (0 ≤ n)%Z →
  Z.testbit (Z.pos p) n = Pos.testbit p (Z.to_N n).
Proof. by destruct n, p. Qed.
(* stdpp_unstable/bitblast.v *)
Lemma negb_forallb {A} (ls : list A) f :
   negb (forallb f ls) = existsb (negb ∘ f) ls.
Proof. induction ls; [done|]; simpl. rewrite negb_andb. congruence. Qed.
(* stdpp_unstable/bitblast.v *)
Lemma Z_bits_inj'' a b :
  a = b → (∀ n : Z, 0 ≤ n → Z.testbit a n = Z.testbit b n).
Proof. apply Z.bits_inj_iff'. Qed.
(* stdpp_unstable/bitblast.v *)
Lemma tac_tactic_in_hyp (P1 P2 : Prop) :
  P1 → (P1 → P2) → P2.
Proof. eauto. Qed.
(* stdpp_unstable/bitblast.v *)
(* ** bitranges *)
Fixpoint pos_to_bit_ranges_aux (p : positive) : (nat * nat) * list (nat * nat)
:=
  match p with
  | xH => ((0, 1)%nat, [])
  | xO p' =>
      let x := pos_to_bit_ranges_aux p' in
      ((S x.1.1, x.1.2), prod_map S id <$> x.2)
  | xI p' =>
      let x := pos_to_bit_ranges_aux p' in
      if (x.1.1 =? 0)%nat then
        ((0%nat, S x.1.2), prod_map S id <$> x.2)
      else
        ((0%nat, 1%nat), prod_map S id <$> (x.1 :: x.2))
  end.
(* stdpp_unstable/bitblast.v *)
(* Compute (pos_to_bit_ranges 21%positive). (** 0b10101  [(0, 1); (2, 1); (4, 1)] *) *)
Definition pos_to_bit_ranges (p : positive) : list (nat * nat)
:=
  let x := pos_to_bit_ranges_aux p in x.1::x.2.
(* stdpp_unstable/bitblast.v *)
Lemma pos_to_bit_ranges_spec p rs :
  pos_to_bit_ranges p = rs →
  (∀ n, Pos.testbit p n ↔ ∃ r, r ∈ rs ∧ (N.of_nat r.1 ≤ n ∧ n < N.of_nat r.1 + N.of_nat r.2)%N).
Proof.
  unfold pos_to_bit_ranges => <-.
  elim: p => //; csimpl.
  - move => p IH n. rewrite Nat_eqb_eq. case_match; subst.
    + split; [|done] => _. case_match.
      all: eexists _; split; [by apply list_elem_of_here|] => /=; lia.
    + rewrite {}IH. split; move => [r[/elem_of_cons[Heq|Hin] ?]]; simplify_eq/=.
      * (* r = (pos_to_bit_ranges_aux p).1 *)
        case_bool_decide as Heq; simplify_eq/=.
        -- eexists _. split; [by apply list_elem_of_here|] => /=. lia.
        -- eexists _. split. { apply list_elem_of_further. apply list_elem_of_here. }
          simplify_eq/=. lia.
      * (* r ∈ (pos_to_bit_ranges_aux p).2 *)
        case_bool_decide as Heq; simplify_eq/=.
        -- eexists _. split. { apply list_elem_of_further. apply list_elem_of_fmap. by eexists _. }
           simplify_eq/=. lia.
        -- eexists _. split. { do 2 apply list_elem_of_further. apply list_elem_of_fmap. by eexists _. }
           simplify_eq/=. lia.
      * eexists _. split; [by apply list_elem_of_here|]. case_bool_decide as Heq; simplify_eq/=; lia.
      * case_bool_decide as Heq; simplify_eq/=.
        -- move: Hin => /= /list_elem_of_fmap[?[??]]; subst. eexists _. split; [by apply list_elem_of_further |].
           simplify_eq/=. lia.
        -- rewrite -fmap_cons in Hin. move: Hin => /list_elem_of_fmap[?[??]]; subst. naive_solver lia.
  - move => p IH n. case_match; subst.
    + split; [done|] => -[[l h][/elem_of_cons[?|/(list_elem_of_fmap _ _ _)[[??][??]]]?]]; simplify_eq/=; lia.
    + rewrite IH. split; move => [r[/elem_of_cons[Heq|Hin] ?]]; simplify_eq/=.
      * eexists _. split; [by apply list_elem_of_here|] => /=; lia.
      * eexists _. split. { apply list_elem_of_further. apply list_elem_of_fmap. by eexists _. }
        destruct r; simplify_eq/=. lia.
      * eexists _. split; [by apply list_elem_of_here|] => /=; lia.
      * move: Hin => /list_elem_of_fmap[r'[??]]; subst. eexists _. split; [by apply list_elem_of_further|].
         destruct r'; simplify_eq/=. lia.
  - move => n. setoid_rewrite list_elem_of_singleton. case_match; split => //; subst; naive_solver lia.
Qed.
(* stdpp_unstable/bitblast.v *)
Definition Z_to_bit_ranges (z : Z) : list (nat * nat)
:=
  match z with
  | Z0 => []
  | Z.pos p => pos_to_bit_ranges p
  | Z.neg p => []
  end.
(* stdpp_unstable/bitblast.v *)
Lemma Z_to_bit_ranges_spec z n rs :
  (0 ≤ n)%Z →
  (0 ≤ z)%Z →
  Z_to_bit_ranges z = rs →
  Z.testbit z n ↔ Exists (λ r, Z.of_nat r.1 ≤ n ∧ n < Z.of_nat r.1 + Z.of_nat r.2) rs.
Proof.
  move => /= ??.
  destruct z => //=.
  + move => <-. rewrite Z.bits_0 Exists_nil. done.
  + move => /pos_to_bit_ranges_spec Hbit. rewrite Z_testbit_pos_testbit // Hbit Exists_exists. naive_solver lia.
Qed.
(* stdpp_unstable/bitblast.v *)
(* * [simpl_bool] *)
Ltac simpl_bool_cbn
:= cbn [andb orb negb].
(* stdpp_unstable/bitblast.v *)
Ltac simpl_bool
:=
  repeat match goal with
         | |- context C [true && ?b] => simpl_bool_cbn
         | |- context C [false && ?b] => simpl_bool_cbn
         | |- context C [true || ?b] => simpl_bool_cbn
         | |- context C [false || ?b] => simpl_bool_cbn
         | |- context C [negb true] => simpl_bool_cbn
         | |- context C [negb false] => simpl_bool_cbn
         | |- context C [?b && true] => rewrite (Bool.andb_true_r b)
         | |- context C [?b && false] => rewrite (Bool.andb_false_r b)
         | |- context C [?b || true] => rewrite (Bool.orb_true_r b)
         | |- context C [?b || false] => rewrite (Bool.orb_false_r b)
         | |- context C [xorb ?b true] => rewrite (Bool.xorb_true_r b)
         | |- context C [xorb ?b false] => rewrite (Bool.xorb_false_r b)
         | |- context C [xorb true ?b] => rewrite (Bool.orb_true_l b)
         | |- context C [xorb false ?b] => rewrite (Bool.orb_false_l b)
         end.
(* stdpp_unstable/bitblast.v *)
Ltac simplify_bitblast_index
:= autorewrite with simplify_bitblast_index_db.
(* stdpp_unstable/bitblast.v *)
(* ** [IsPowerOfTwo] *)
Class IsPowerOfTwo (z n : Z)
:= {
  is_power_of_two_proof : z = 2 ^ n;
}.
(* stdpp_unstable/bitblast.v *)
Lemma is_power_of_two_pow2 n :
  IsPowerOfTwo (2 ^ n) n.
Proof. constructor. done. Qed.
(* stdpp_unstable/bitblast.v *)
Lemma is_power_of_two_const n p :
  (∀ x, [(n, 1%nat)] = x → prod_map Z.of_nat id <$> Z_to_bit_ranges (Z.pos p) = x) →
  IsPowerOfTwo (Z.pos p) n.
Proof.
  move => Hn. constructor. have {}Hn := Hn _ ltac:(done).
  apply Z.bits_inj_iff' => i ?.
  apply eq_bool_prop_intro. rewrite Z_to_bit_ranges_spec; [|done|lia|done].
  move: Hn => /(fmap_cons_inv _ _ _)[[n' ?][?/=[[??][/(@eq_sym _ _ _)/fmap_nil_inv->->]]]]. subst.
  rewrite Exists_cons Exists_nil /=.
  rewrite Z.pow2_bits_eqb ?Z_eqb_eq ?bool_decide_spec; lia.
Qed.
(* stdpp_unstable/bitblast.v *)
(* ** [BitblastBounded] *)
Class BitblastBounded (z n : Z)
:= {
  bitblast_bounded_proof : 0 ≤ z < 2 ^ n;
}.
(* stdpp_unstable/bitblast.v *)
(* ** [Bitblast] *)
Class Bitblast (z n : Z) (b : bool)
:= {
  bitblast_proof : Z.testbit z n = b;
}.
(* stdpp_unstable/bitblast.v *)
Definition BITBLAST_TESTBIT
:= Z.testbit.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_id z n :
  Bitblast z n (bool_decide (0 ≤ n) && BITBLAST_TESTBIT z n).
Proof. constructor. case_bool_decide => //=. rewrite Z.testbit_neg_r //; lia. Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_id_bounded z z' n :
  BitblastBounded z z' →
  Bitblast z n (bool_decide (0 ≤ n < z') && BITBLAST_TESTBIT z n).
Proof.
  move => [Hb]. constructor.
  move: (Hb) => /Z.bounded_iff_bits_nonneg' Hn.
  case_bool_decide => //=.
  destruct (decide (0 ≤ n)); [|rewrite Z.testbit_neg_r //; lia].
  apply Hn; try lia.
  destruct (decide (0 ≤ z')) => //.
  rewrite Z.pow_neg_r in Hb; lia.
Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_0 n :
  Bitblast 0 n false.
Proof. constructor. by rewrite Z.bits_0. Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_pos p n rs b :
  (∀ x, rs = x → (λ p, (Z.of_nat p.1, Z.of_nat p.1 + Z.of_nat p.2)) <$> Z_to_bit_ranges (Z.pos p) = x) →
  existsb (λ '(r1, r2), bool_decide (r1 ≤ n ∧ n < r2)) rs = b →
  Bitblast (Z.pos p) n b.
Proof.
  move => Hr <-. constructor. rewrite -(Hr rs) //.
  destruct (decide (0 ≤ n)). 2: {
    rewrite Z.testbit_neg_r; [|lia]. elim: (Z_to_bit_ranges (Z.pos p)) => // [??]; csimpl => <-.
    case_bool_decide => //; lia.
  }
  apply eq_bool_prop_intro. rewrite Z_to_bit_ranges_spec; [|done..]. rewrite existb_True Exists_fmap.
  f_equiv => -[??] /=. by rewrite bool_decide_spec.
Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_neg p n rs b :
  (∀ x, rs = x → (λ p, (Z.of_nat p.1, Z.of_nat p.1 + Z.of_nat p.2)) <$> Z_to_bit_ranges (Z.pred (Z.pos p)) = x) →
  forallb (λ '(r1, r2), bool_decide (n < r1 ∨ r2 ≤ n)) rs = b →
  Bitblast (Z.neg p) n (bool_decide (0 ≤ n) && b).
Proof.
  move => Hr <-. constructor. rewrite -(Hr rs) //.
  case_bool_decide => /=; [|rewrite Z.testbit_neg_r; [done|lia]].
  have -> : Z.neg p = Z.lnot (Z.pred (Z.pos p)).
  { rewrite -Pos2Z.opp_pos. have := Z.add_lnot_diag (Z.pred (Z.pos p)). lia. }
  rewrite Z.lnot_spec //. symmetry. apply negb_sym.
  apply eq_bool_prop_intro. rewrite Z_to_bit_ranges_spec; [|done|lia|done].
  rewrite negb_forallb existb_True Exists_fmap.
  f_equiv => -[??] /=. rewrite negb_True bool_decide_spec. lia.
Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_land z1 z2 n b1 b2 :
  Bitblast z1 n b1 →
  Bitblast z2 n b2 →
  Bitblast (Z.land z1 z2) n (b1 && b2).
Proof. move => [<-] [<-]. constructor. by rewrite Z.land_spec. Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_lor z1 z2 n b1 b2 :
  Bitblast z1 n b1 →
  Bitblast z2 n b2 →
  Bitblast (Z.lor z1 z2) n (b1 || b2).
Proof. move => [<-] [<-]. constructor. by rewrite Z.lor_spec. Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_lxor z1 z2 n b1 b2 :
  Bitblast z1 n b1 →
  Bitblast z2 n b2 →
  Bitblast (Z.lxor z1 z2) n (xorb b1 b2).
Proof. move => [<-] [<-]. constructor. by rewrite Z.lxor_spec. Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_shiftr z1 z2 n b1 :
  Bitblast z1 (n + z2) b1 →
  Bitblast (z1 ≫ z2) n (bool_decide (0 ≤ n) && b1).
Proof.
  move => [<-]. constructor.
  case_bool_decide => /=; [by rewrite Z.shiftr_spec| rewrite Z.testbit_neg_r //; lia].
Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_shiftl z1 z2 n b1 :
  Bitblast z1 (n - z2) b1 →
  Bitblast (z1 ≪ z2) n (bool_decide (0 ≤ n) && b1).
Proof.
  move => [<-]. constructor.
  case_bool_decide => /=; [by rewrite Z.shiftl_spec| rewrite Z.testbit_neg_r //; lia].
Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_lnot z1 n b1 :
  Bitblast z1 n b1 →
  Bitblast (Z.lnot z1) n (bool_decide (0 ≤ n) && negb b1).
Proof.
  move => [<-]. constructor.
  case_bool_decide => /=; [by rewrite Z.lnot_spec| rewrite Z.testbit_neg_r //; lia].
Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_ldiff z1 z2 n b1 b2 :
  Bitblast z1 n b1 →
  Bitblast z2 n b2 →
  Bitblast (Z.ldiff z1 z2) n (b1 && negb b2).
Proof. move => [<-] [<-]. constructor. by rewrite Z.ldiff_spec. Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_ones z1 n :
  Bitblast (Z.ones z1) n (bool_decide (0 ≤ n < z1) || bool_decide (z1 < 0 ∧ 0 ≤ n)).
Proof.
  constructor. case_bool_decide; [by apply Z.ones_spec_low|] => /=.
  case_bool_decide.
  - rewrite Z.ones_equiv Z.pow_neg_r; [|lia]. apply Z.bits_m1. lia.
  - destruct (decide (0 ≤ n)); [|rewrite Z.testbit_neg_r //; lia].
    apply Z.ones_spec_high; lia.
Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_pow2 n n' :
  Bitblast (2 ^ n') n (bool_decide (n = n' ∧ 0 ≤ n)).
Proof.
  constructor. case_bool_decide; destruct_and?; subst; [by apply Z.pow2_bits_true|].
  destruct (decide (0 ≤ n)); [|rewrite Z.testbit_neg_r //; lia].
  apply Z.pow2_bits_false. lia.
Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_setbit z1 n b1 n' :
  Bitblast (Z.lor z1 (2 ^ n')) n b1 →
  Bitblast (Z.setbit z1 n') n b1.
Proof. by rewrite Z.setbit_spec'. Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_mod z1 z2 z2' n b1 :
  IsPowerOfTwo z2 z2' →
  Bitblast z1 n b1 →
  Bitblast (z1 `mod` z2) n ((bool_decide (z2' < 0 ∧ 0 ≤ n) || bool_decide (n < z2')) && b1).
Proof.
  move => [->] [<-]. constructor.
  case_bool_decide => /=. { rewrite Z.pow_neg_r ?Zmod_0_r; [done|lia]. }
  destruct (decide (0 ≤ n)). 2: { rewrite !Z.testbit_neg_r ?andb_false_r //; lia. }
  rewrite -Z.land_ones; [|lia]. rewrite Z.land_spec Z.ones_spec; [|lia..].
  by rewrite andb_comm.
Qed.
(* stdpp_unstable/bitblast.v *)
(* TODO: What are good instances for +? Maybe something based on Z_add_nocarry_lor? *)
Lemma bitblast_add_0 z1 z2 b1 b2 :
  Bitblast z1 0 b1 →
  Bitblast z2 0 b2 →
  Bitblast (z1 + z2) 0 (xorb b1 b2).
Proof. move => [<-] [<-]. constructor. apply Z.add_bit0. Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_add_1 z1 z2 b10 b11 b20 b21 :
  Bitblast z1 0 b10 →
  Bitblast z2 0 b20 →
  Bitblast z1 1 b11 →
  Bitblast z2 1 b21 →
  Bitblast (z1 + z2) 1 (xorb (xorb b11 b21) (b10 && b20)).
Proof. move => [<-] [<-] [<-] [<-]. constructor. apply Z.add_bit1. Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_clearbit z n b m :
  Bitblast z n b →
  Bitblast (Z.clearbit z m) n (bool_decide (n ≠ m) && b).
Proof.
  move => [<-]. constructor.
  case_bool_decide; subst => /=.
  - by apply Z.clearbit_neq.
  - by apply Z.clearbit_eq.
Qed.