From 091726034110408555f0bca58cfebbf39b524147 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 18 Mar 2026 07:22:06 +0000 Subject: [PATCH] feat: add simp lemmas for kernel-friendly functions (#12950) This PR adds simp lemmas equating kernel-friendly function names with their operator notation equivalents: `Nat.land_eq`, `Nat.lor_eq`, `Nat.xor_eq`, `Nat.shiftLeft_eq'`, `Nat.shiftRight_eq'`, and `Bool.rec_eq`. These are useful when proofs involve reflection and need to simplify kernel-reduced terms back to operator notation. Closes #12716 Co-authored-by: Claude --- src/Init/Data/Bool.lean | 3 +++ src/Init/Data/Nat/Bitwise/Basic.lean | 6 ++++++ 2 files changed, 9 insertions(+) diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean index e6eb98c13b..edc24c29b6 100644 --- a/src/Init/Data/Bool.lean +++ b/src/Init/Data/Bool.lean @@ -664,3 +664,6 @@ but may be used locally. @[simp] theorem Bool.not'_eq_not (a : Bool) : a.not' = a.not := by cases a <;> simp [Bool.not'] + +theorem Bool.rec_eq {α : Sort _} (b : Bool) {x y : α} : Bool.rec y x b = if b then x else y := by + cases b <;> simp diff --git a/src/Init/Data/Nat/Bitwise/Basic.lean b/src/Init/Data/Nat/Bitwise/Basic.lean index d5a19263f0..ad920d6cfe 100644 --- a/src/Init/Data/Nat/Bitwise/Basic.lean +++ b/src/Init/Data/Nat/Bitwise/Basic.lean @@ -102,6 +102,12 @@ instance : XorOp Nat := ⟨Nat.xor⟩ instance : ShiftLeft Nat := ⟨Nat.shiftLeft⟩ instance : ShiftRight Nat := ⟨Nat.shiftRight⟩ +@[simp] theorem land_eq {m n : Nat} : m.land n = m &&& n := rfl +@[simp] theorem lor_eq {m n : Nat} : m.lor n = m ||| n := rfl +@[simp] theorem xor_eq {m n : Nat} : m.xor n = m ^^^ n := rfl +@[simp] theorem shiftLeft_eq' {m n : Nat} : m.shiftLeft n = m <<< n := rfl +@[simp] theorem shiftRight_eq' {m n : Nat} : m.shiftRight n = m >>> n := rfl + theorem shiftLeft_eq (a b : Nat) : a <<< b = a * 2 ^ b := match b with | 0 => (Nat.mul_one _).symm