max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add simp lemmas for kernel-friendly functions (#12950)

Browse source 
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 <noreply@anthropic.com>
This commit is contained in:
Bhavik Mehta 2026-03-18 07:22:06 +00:00 • committed by GitHub
parent 61a3443a95
commit 0917260341
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Data/Bool.lean
View file

@ -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

6
src/Init/Data/Nat/Bitwise/Basic.lean
View file

@ -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