From b7281bfec24725aa9ea262df01bd772e78dff6e0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 4 Apr 2020 15:12:15 +0200
Subject: Adding properties about implb.

This addresses a question on gitter (April 4).
---
 .../12018-master+implb-characterization.rst        | 19 ++++++
 theories/Bool/Bool.v                               | 79 ++++++++++++++++++++++
 2 files changed, 98 insertions(+)
 create mode 100644 doc/changelog/10-standard-library/12018-master+implb-characterization.rst

diff --git a/doc/changelog/10-standard-library/12018-master+implb-characterization.rst b/doc/changelog/10-standard-library/12018-master+implb-characterization.rst
new file mode 100644
index 0000000000..4b0abdfa3b
--- /dev/null
+++ b/doc/changelog/10-standard-library/12018-master+implb-characterization.rst
@@ -0,0 +1,19 @@
+- **Added:**
+  Added lemmas
+  :g:`orb_negb_l`,
+  :g:`andb_negb_l`,
+  :g:`implb_true_iff`,
+  :g:`implb_false_iff`,
+  :g:`implb_true_r`,
+  :g:`implb_false_r`,
+  :g:`implb_true_l`,
+  :g:`implb_false_l`,
+  :g:`implb_same`,
+  :g:`implb_contrapositive`,
+  :g:`implb_negb`,
+  :g:`implb_curry`,
+  :g:`implb_andb_distrib_r`,
+  :g:`implb_orb_distrib_r`,
+  :g:`implb_orb_distrib_l` in library :g:`Bool`
+  (`#12018 <https://github.com/coq/coq/pull/12018>`_,`
+  by Hugo Herbelin).`
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 1d5e3e54ff..756089907c 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -305,6 +305,11 @@ Proof.
 Qed.
 Hint Resolve orb_negb_r: bool.
 
+Lemma orb_negb_l : forall b:bool, negb b || b = true.
+Proof.
+  destr_bool.
+Qed.
+
 Notation orb_neg_b := orb_negb_r (only parsing).
 
 (** Commutativity *)
@@ -404,6 +409,11 @@ Proof.
 Qed.
 Hint Resolve andb_negb_r: bool.
 
+Lemma andb_negb_l : forall b:bool, negb b && b = false.
+Proof.
+  destr_bool.
+Qed.
+
 Notation andb_neg_b := andb_negb_r (only parsing).
 
 (** Commutativity *)
@@ -476,6 +486,75 @@ Notation absoption_andb := absorption_andb (only parsing).
 Notation absoption_orb := absorption_orb (only parsing).
 (* end hide *)
 
+(*********************************)
+(** * Properties of [implb]      *)
+(*********************************)
+
+Lemma implb_true_iff : forall b1 b2:bool, implb b1 b2 = true <-> (b1 = true -> b2 = true).
+Proof.
+  destr_bool; intuition.
+Qed.
+
+Lemma implb_false_iff : forall b1 b2:bool, implb b1 b2 = false <-> (b1 = true /\ b2 = false).
+Proof.
+  destr_bool; intuition.
+Qed.
+
+Lemma implb_true_r : forall b:bool, implb b true = true.
+Proof.
+  destr_bool.
+Qed.
+
+Lemma implb_false_r : forall b:bool, implb b false = negb b.
+Proof.
+  destr_bool.
+Qed.
+
+Lemma implb_true_l : forall b:bool, implb true b = b.
+Proof.
+  destr_bool.
+Qed.
+
+Lemma implb_false_l : forall b:bool, implb false b = true.
+Proof.
+  destr_bool.
+Qed.
+
+Lemma implb_same : forall b:bool, implb b b = true.
+Proof.
+  destr_bool.
+Qed.
+
+Lemma implb_contrapositive : forall b1 b2:bool, implb (negb b1) (negb b2) = implb b2 b1.
+Proof.
+  destr_bool.
+Qed.
+
+Lemma implb_negb : forall b1 b2:bool, implb (negb b1) b2 = implb (negb b2) b1.
+Proof.
+  destr_bool.
+Qed.
+
+Lemma implb_curry : forall b1 b2 b3:bool, implb (b1 && b2) b3 = implb b1 (implb b2 b3).
+Proof.
+  destr_bool.
+Qed.
+
+Lemma implb_andb_distrib_r : forall b1 b2 b3:bool, implb b1 (b2 && b3) = implb b1 b2 && implb b1 b3.
+Proof.
+  destr_bool.
+Qed.
+
+Lemma implb_orb_distrib_r : forall b1 b2 b3:bool, implb b1 (b2 || b3) = implb b1 b2 || implb b1 b3.
+Proof.
+  destr_bool.
+Qed.
+
+Lemma implb_orb_distrib_l : forall b1 b2 b3:bool, implb (b1 || b2) b3 = implb b1 b3 && implb b2 b3.
+Proof.
+  destr_bool.
+Qed.
+
 (*********************************)
 (** * Properties of [xorb]       *)
 (*********************************)
-- 
cgit v1.2.3