From 08fecbf6de2986d267e52f19724c609c4a2775a4 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Tue, 30 Nov 2021 16:17:01 +0100
Subject: [PATCH] Add bool_to_Z

---
 CHANGELOG.md       |  3 ++-
 theories/numbers.v | 15 +++++++++++++++
 2 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 68862da2..b728eee9 100644
--- a/CHANGELOG.md
+++ b/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
diff --git a/theories/numbers.v b/theories/numbers.v
index d3e77341..f8f237cf 100644
--- a/theories/numbers.v
+++ b/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 *)
-- 
GitLab