From cb25928e6e9797964b0466ddf27f5762c36e633b Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Wed, 24 Nov 2021 12:09:13 +0100
Subject: [PATCH] Upstreaming a small collection of lemmas

---
 CHANGELOG.md       | 12 ++++++++++++
 theories/base.v    | 14 ++++++++++++--
 theories/numbers.v |  7 +++++++
 theories/option.v  |  8 ++++++--
 4 files changed, 37 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ad19d616..5290cabd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,6 +3,18 @@ API-breaking change is listed.
 
 ## std++ master
 
+- 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
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+s/\bIs_true_false\b/Is_true_false_2/g
+s/\beq_None_ne_Some\b/eq_None_ne_Some_1/g
+EOF
+```
+
 ## std++ 1.6.0 (2021-11-05)
 
 Coq 8.14 is newly supported by this release, and Coq 8.10 to 8.13 remain
diff --git a/theories/base.v b/theories/base.v
index aa64494f..029b7fa4 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -642,8 +642,18 @@ Lemma orb_True b1 b2 : b1 || b2 ↔ b1 ∨ b2.
 Proof. destruct b1, b2; simpl; tauto. Qed.
 Lemma negb_True b : negb b ↔ ¬b.
 Proof. destruct b; simpl; tauto. Qed.
-Lemma Is_true_false (b : bool) : b = false → ¬b.
-Proof. now intros -> ?. Qed.
+Lemma Is_true_true (b : bool) : b ↔ b = true.
+Proof. now destruct b. Qed.
+Lemma Is_true_true_1 (b : bool) : b → b = true.
+Proof. apply Is_true_true. Qed.
+Lemma Is_true_true_2 (b : bool) : b = true → b.
+Proof. apply Is_true_true. Qed.
+Lemma Is_true_false (b : bool) : ¬ b ↔ b = false.
+Proof. now destruct b; simpl. Qed.
+Lemma Is_true_false_1 (b : bool) : ¬b → b = false.
+Proof. apply Is_true_false. Qed.
+Lemma Is_true_false_2 (b : bool) : b = false → ¬b.
+Proof. apply Is_true_false. Qed.
 
 (** ** Unit *)
 Global Instance unit_equiv : Equiv unit := λ _ _, True.
diff --git a/theories/numbers.v b/theories/numbers.v
index 9600f0fc..d3e77341 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -535,6 +535,13 @@ Proof.
   - etrans; [|apply Z.pow_pos_nonneg]; lia.
 Qed.
 
+Lemma Z_add_nocarry_lor a b :
+  Z.land a b = 0 →
+  a + b = Z.lor a b.
+Proof. intros ?. rewrite <-Z.lxor_lor by done. by rewrite Z.add_nocarry_lxor. Qed.
+
+Lemma Z_opp_lnot a : -a - 1 = Z.lnot a.
+Proof. pose proof (Z.add_lnot_diag a). lia. Qed.
 
 Local Close Scope Z_scope.
 
diff --git a/theories/option.v b/theories/option.v
index 37b52505..0189d77e 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -13,8 +13,12 @@ Lemma None_ne_Some {A} (x : A) : None ≠ Some x.
 Proof. congruence. Qed.
 Lemma Some_ne_None {A} (x : A) : Some x ≠ None.
 Proof. congruence. Qed.
-Lemma eq_None_ne_Some {A} (mx : option A) x : mx = None → mx ≠ Some x.
-Proof. congruence. Qed.
+Lemma eq_None_ne_Some {A} (mx : option A) : (∀ x, mx ≠ Some x) ↔ mx = None.
+Proof. destruct mx; split; congruence. Qed.
+Lemma eq_None_ne_Some_1 {A} (mx : option A) x : mx = None → mx ≠ Some x.
+Proof. intros ?. by apply eq_None_ne_Some. Qed.
+Lemma eq_None_ne_Some_2 {A} (mx : option A) : (∀ x, mx ≠ Some x) → mx = None.
+Proof. intros ?. by apply eq_None_ne_Some. Qed.
 Global Instance Some_inj {A} : Inj (=) (=) (@Some A).
 Proof. congruence. Qed.
 
-- 
GitLab