Add bool_to_Z

CHANGELOG.md

@@ -3,7 +3,8 @@ API-breaking change is listed.
 
 ## std++ master
 
-- Add lemmas for lookup on `mjoin` for lists (by Michael Sammler).
+- Add `bool_to_Z` that converts true to 1 and false to 0. (by Michael Sammler)
+- Add lemmas for lookup on `mjoin` for lists. (by Michael Sammler)
 - Rename `Is_true_false` → `Is_true_false_2` and `eq_None_ne_Some` → `eq_None_ne_Some_1`.
 
 The following `sed` script should perform most of the renaming

theories/numbers.v

@@ -543,6 +543,21 @@ Proof. intros ?. rewrite <-Z.lxor_lor by done. by rewrite Z.add_nocarry_lxor. Qe
 Lemma Z_opp_lnot a : -a - 1 = Z.lnot a.
 Proof. pose proof (Z.add_lnot_diag a). lia. Qed.
 
+(** ** [bool_to_Z] *)
+Definition bool_to_Z (b : bool) : Z :=
+  if b then 1 else 0.
+
+Lemma bool_to_Z_bound b : 0 ≤ bool_to_Z b < 2.
+Proof. destruct b; simpl; lia. Qed.
+Lemma bool_to_Z_eq_0 b : bool_to_Z b = 0 ↔ b = false.
+Proof. destruct b; naive_solver. Qed.
+Lemma bool_to_Z_neq_0 b : bool_to_Z b ≠ 0 ↔ b = true.
+Proof. destruct b; naive_solver. Qed.
+Lemma bool_to_Z_spec b n:
+  Z.testbit (bool_to_Z b) n = bool_decide (n = 0) && b.
+Proof. by destruct b, n. Qed.
+
+
 Local Close Scope Z_scope.
 
 (** * Injectivity of casts *)