phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_bool_to_Z b n:
  Bitblast (bool_to_Z b) n (bool_decide (n = 0) && b).
Proof.
  constructor. destruct b; simpl_bool; repeat case_bool_decide;
    subst; try done; rewrite ?Z.bits_0; by destruct n.
Qed.
(* stdpp_unstable/bitblast.v *)
(* Instances for [bv] *)
Lemma bitblast_bv_wrap z1 n n1 b1:
  Bitblast z1 n b1 →
  Bitblast (bv_wrap n1 z1) n (bool_decide (n < Z.of_N n1) && b1).
Proof.
  intros [<-]. constructor.
  destruct (decide (0 ≤ n)); [by rewrite bv_wrap_spec| rewrite !Z.testbit_neg_r; [|lia..]; btauto].
Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_bounded_bv_unsigned n (b : bv n):
  BitblastBounded (bv_unsigned b) (Z.of_N n).
Proof. constructor. apply bv_unsigned_in_range. Qed.
(* stdpp_unstable/bitblast.v *)
Lemma bitblast_bv_swrap z1 n n1 b1 b2 :
  Bitblast z1 n b1 →
  Bitblast z1 (Z.of_N n1-1) b2 →
  Bitblast (bv_swrap n1 z1) n (if bool_decide (n < Z.of_N n1-1) then b1 else b2).
Proof.
  intros [<-] [<-]. constructor.
  destruct (decide (0 ≤ n)).
  - by rewrite bv_swrap_spec.
  - case_bool_decide.
    + rewrite !Z.testbit_neg_r; [done|lia..].
    + rewrite !Z.testbit_neg_r; [done|lia..].
Qed.
(* stdpp_unstable/bitblast.v *)
(* ** Helper definitions and lemmas for the tactics *)
Definition BITBLAST_BOOL_DECIDE
:= @bool_decide.
(* stdpp_unstable/bitblast.v *)
Lemma tac_bitblast_bool_decide_true G (P : Prop) `{!Decision P} :
  P →
  G true →
  G (bool_decide P).
Proof. move => ??. by rewrite bool_decide_eq_true_2. Qed.
(* stdpp_unstable/bitblast.v *)
Lemma tac_bitblast_bool_decide_false G (P : Prop) `{!Decision P} :
  ¬ P →
  G false →
  G (bool_decide P).
Proof. move => ??. by rewrite bool_decide_eq_false_2. Qed.
(* stdpp_unstable/bitblast.v *)
Lemma tac_bitblast_bool_decide_split G (P : Prop) `{!Decision P} :
  (P → G true) →
  (¬ P → G false) →
  G (bool_decide P).
Proof. move => ??. case_bool_decide; eauto. Qed.
(* stdpp_unstable/bitblast.v *)
(* ** Core tactics *)
Ltac bitblast_done
:=
  solve [ first [ done | lia | btauto ] ].
(* stdpp_unstable/bitblast.v *)
(* [bitblast_blast_eq] applies to goals of the form [Z.testbit _ _ = ?x] and bitblasts the
  Z.testbit using the [Bitblast] typeclass. *)
Ltac bitblast_blast_eq
:=
  lazymatch goal with |- Z.testbit _ _ = _ => idtac end;
  etrans; [ notypeclasses refine (bitblast_proof _ _ _); typeclasses eauto with bitblast | ];
  simplify_bitblast_index;
  exact eq_refl.
(* stdpp_unstable/bitblast.v *)
(* [bitblast_bool_decide_simplify] get rids of unnecessary bool_decide in the goal. *)
Ltac bitblast_bool_decide_simplify
:=
  repeat lazymatch goal with
         | |- context [@bool_decide ?P ?Dec] =>
             pattern (@bool_decide P Dec);
             lazymatch goal with
             | |- ?G _ =>
                 first [
                     refine (@tac_bitblast_bool_decide_true G P Dec _ _); [lia|];
                     simpl_bool_cbn
                   |
                     refine (@tac_bitblast_bool_decide_false G P Dec _ _); [lia|];
                     simpl_bool_cbn
                   |
                     change_no_check (G (@BITBLAST_BOOL_DECIDE P Dec))
               ]
             end;
             cbv beta
         end;
  (** simpl_bool contains rewriting so it can be quite slow and thus we only do it at the end. *)
  simpl_bool;
  lazymatch goal with
  | |- ?G => let x := eval unfold BITBLAST_BOOL_DECIDE in G in change_no_check x
  end.
(* stdpp_unstable/bitblast.v *)
(* [bitblast_bool_decide_split] performs a case distinction on a bool_decide in the goal. *)
Ltac bitblast_bool_decide_split
:=
  lazymatch goal with
  | |- context [@bool_decide ?P ?Dec] =>
      pattern (@bool_decide P Dec);
      lazymatch goal with
      | |- ?G _ =>
          refine (@tac_bitblast_bool_decide_split G P Dec _ _) => ?; cbv beta; simpl_bool
      end
  end.
(* stdpp_unstable/bitblast.v *)
(* [bitblast_unfold] bitblasts all [Z.testbit] in the goal. *)
Ltac bitblast_unfold
:=
  repeat lazymatch goal with
  | |- context [Z.testbit ?z ?n] =>
      pattern (Z.testbit z n);
      simple refine (eq_rec_r _ _ _); [shelve| |bitblast_blast_eq]; cbv beta
  end;
  lazymatch goal with
  | |- ?G => let x := eval unfold BITBLAST_TESTBIT in G in change_no_check x
  end.
(* stdpp_unstable/bitblast.v *)
(* [bitblast_raw] bitblasts all [Z.testbit] in the goal and simplifies the result. *)
Ltac bitblast_raw
:=
  bitblast_unfold;
  bitblast_bool_decide_simplify;
  try bitblast_done;
  repeat (bitblast_bool_decide_split; bitblast_bool_decide_simplify; try bitblast_done).