feat: add non-branching boolean operations

Author: fgdorais

src/Init/Data/Bool.lean

@@ -12,6 +12,42 @@ public section
 
 namespace Bool
 
+/--
+Boolean “logical or”. `lor x y`.
+
+`land x y` is `true` when both of `x` or `y` are `true`. It is functionally the same as
+`x && y` but it does not have short-circuiting behavior: any call to `land` will evaluate both
+arguments.
+
+Examples:
+ * `land false false = false`
+ * `land true false = false`
+ * `land false true = false`
+ * `land true true = true`
+-/
+@[expose, extern "lean_bool_land"]
+def land (x y : Bool) : Bool := x && y
+
+@[simp] theorem land_eq_and (x y : Bool) : land x y = (x && y) := rfl
+
+/--
+Boolean “logical or”. `lor x y`.
+
+`lor x y` is `true` when at least one of `x` or `y` is `true`. It is functionally the same as
+`x || y` but it does not have short-circuiting behavior: any call to `lor` will evaluate both
+arguments.
+
+Examples:
+ * `lor false false = false`
+ * `lor true false = true`
+ * `lor false true = true`
+ * `lor true true = true`
+-/
+@[expose, extern "lean_bool_lor"]
+def lor (x y : Bool) : Bool := x || y
+
+@[simp] theorem lor_eq_or (x y : Bool) : lor x y = (x || y) := rfl
+
 /--
 Boolean “exclusive or”. `xor x y` can be written `x ^^ y`.
 
@@ -25,11 +61,14 @@ Examples:
  * `false ^^ true = true`
  * `true ^^ true = false`
 -/
-abbrev xor : Bool → Bool → Bool := bne
+@[expose, reducible, extern "lean_bool_xor"]
+def xor : Bool → Bool → Bool := bne
+
+@[inherit_doc] infixl:33 " ^^ " => Bool.xor
 
-@[inherit_doc] infixl:33 " ^^ " => xor
+recommended_spelling "xor" for "^^" in [Bool.xor, «term_^^_»]
 
-recommended_spelling "xor" for "^^" in [xor, «term_^^_»]
+theorem xor_eq_bne (x y : Bool) : (x ^^ y) = (x != y) := rfl
 
 instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∀ x, p x) :=
   match inst true, inst false with
@@ -48,11 +87,13 @@ instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∃ x, p x) :
 instance : LE Bool := ⟨(. → .)⟩
 instance : LT Bool := ⟨(!. && .)⟩
 
+@[extern "lean_bool_dec_le"]
 instance (x y : Bool) : Decidable (x ≤ y) := inferInstanceAs (Decidable (x → y))
+@[extern "lean_bool_dec_lt"]
 instance (x y : Bool) : Decidable (x < y) := inferInstanceAs (Decidable (!x && y))
 
-instance : Max Bool := ⟨or⟩
-instance : Min Bool := ⟨and⟩
+instance : Max Bool := ⟨lor⟩
+instance : Min Bool := ⟨land⟩
 
 theorem false_ne_true : false ≠ true := Bool.noConfusion
 
@@ -385,7 +426,8 @@ theorem and_or_inj_left_iff :
 /--
 Converts `true` to `1` and `false` to `0`.
 -/
-@[expose] def toNat (b : Bool) : Nat := cond b 1 0
+@[expose, extern "lean_bool_to_nat"]
+def toNat (b : Bool) : Nat := cond b 1 0
 
 @[simp, bitvec_to_nat, grind =] theorem toNat_false : false.toNat = 0 := rfl
 

src/Init/Prelude.lean

@@ -1006,7 +1006,8 @@ Decides whether two Booleans are equal.
 This function should normally be called via the `DecidableEq Bool` instance that it exists to
 support.
 -/
-@[inline] def Bool.decEq (a b : Bool) : Decidable (Eq a b) :=
+@[extern "lean_bool_dec_eq"]
+def Bool.decEq (a b : Bool) : Decidable (Eq a b) :=
    match a, b with
    | false, false => isTrue rfl
    | false, true  => isFalse (fun h => Bool.noConfusion h)
@@ -1177,7 +1178,8 @@ Boolean negation, also known as Boolean complement. `not x` can be written `!x`.
 This is a function that maps the value `true` to `false` and the value `false` to `true`. The
 propositional connective is `Not : Prop → Prop`.
 -/
-@[inline] def Bool.not : Bool → Bool
+@[extern "lean_bool_complement"]
+def Bool.not : Bool → Bool
   | true  => false
   | false => true
 

src/include/lean/lean.h

@@ -1780,6 +1780,7 @@ static inline uint8_t lean_int_dec_nonneg(b_lean_obj_arg a) {
 
 /* Bool */
 
+static inline lean_obj_res lean_bool_to_nat(uint8_t a) { return lean_usize_to_nat((size_t)a); }
 static inline uint8_t lean_bool_to_uint8(uint8_t a) { return a; }
 static inline uint16_t lean_bool_to_uint16(uint8_t a) { return (uint16_t)a; }
 static inline uint32_t lean_bool_to_uint32(uint8_t a) { return (uint32_t)a; }
@@ -1790,7 +1791,13 @@ static inline uint16_t lean_bool_to_int16(uint8_t a) { return (uint16_t)(int16_t
 static inline uint32_t lean_bool_to_int32(uint8_t a) { return (uint32_t)(int32_t)a; }
 static inline uint64_t lean_bool_to_int64(uint8_t a) { return (uint64_t)(int64_t)a; }
 static inline size_t lean_bool_to_isize(uint8_t a) { return (size_t)(ptrdiff_t)a; }
-
+static inline uint8_t lean_bool_land(uint8_t a, uint8_t b) { return a & b; }
+static inline uint8_t lean_bool_lor(uint8_t a, uint8_t b) { return a | b; }
+static inline uint8_t lean_bool_xor(uint8_t a, uint8_t b) { return a ^ b; }
+static inline uint8_t lean_bool_complement(uint8_t a) { return a == 0; }
+static inline uint8_t lean_bool_dec_eq(uint8_t a, uint8_t b) { return a == b; }
+static inline uint8_t lean_bool_dec_lt(uint8_t a, uint8_t b) { return a < b; }
+static inline uint8_t lean_bool_dec_le(uint8_t a, uint8_t b) { return a <= b; }
 
 /* UInt8 */