feat: prove equality of Nat.bitwise and Nat.bitwise' (#7410)

This PR proves that `Nat.bitwise` (from core) and `Nat.bitwise'` (from mathlib) are equal



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: alexkeizer

Mathlib/Data/Int/Bitwise.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 -/
 import Mathlib.Data.Int.Basic
+import Mathlib.Data.Nat.Bitwise
 import Mathlib.Data.Nat.Pow
 import Mathlib.Data.Nat.Size
 import Mathlib.Init.Data.Int.Bitwise
@@ -205,9 +206,9 @@ theorem testBit_zero (b) : ∀ n, testBit (bit b n) 0 = b
 theorem testBit_succ (m b) : ∀ n, testBit (bit b n) (Nat.succ m) = testBit n m
   | (n : ℕ) => by rw [bit_coe_nat]; apply Nat.testBit_succ
   | -[n+1] => by
-    dsimp [testBit]
+    dsimp only [testBit]
     simp only [bit_negSucc]
-    cases b <;> simp [Nat.testBit_succ]
+    cases b <;> simp only [Bool.not_false, Bool.not_true, Nat.testBit_succ]
 #align int.test_bit_succ Int.testBit_succ
 
 -- Porting note: TODO

Mathlib/Data/Nat/Bitwise.lean

@@ -1,14 +1,15 @@
 /-
 Copyright (c) 2020 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
+Authors: Markus Himmel, Alex Keizer
 -/
 import Lean.Elab.Tactic
 import Mathlib.Data.List.Basic
 import Mathlib.Data.Nat.Bits
 import Mathlib.Data.Nat.Size
 import Mathlib.Data.Nat.Order.Lemmas
 import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Ring
 
 #align_import data.nat.bitwise from "leanprover-community/mathlib"@"6afc9b06856ad973f6a2619e3e8a0a8d537a58f2"
 
@@ -44,6 +45,104 @@ namespace Nat
 
 set_option linter.deprecated false
 
+section
+variable {f : Bool → Bool → Bool}
+
+lemma bitwise'_bit' {f : Bool → Bool → Bool} (a : Bool) (m : Nat) (b : Bool) (n : Nat)
+    (ham : m = 0 → a = true) (hbn : n = 0 → b = true) :
+    bitwise' f (bit a m) (bit b n) = bit (f a b) (bitwise' f m n) := by
+  rw [bitwise', binaryRec_eq', binaryRec_eq']
+  · apply Or.inr hbn
+  · apply Or.inr ham
+
+@[simp]
+lemma bitwise_zero_left (m : Nat) : bitwise f 0 m = if f false true then m else 0 :=
+  rfl
+
+@[simp]
+lemma bitwise_zero_right (n : Nat) : bitwise f n 0 = if f true false then n else 0 := by
+  unfold bitwise
+  simp only [ite_self, decide_False, Nat.zero_div, ite_true, ite_eq_right_iff]
+  rintro ⟨⟩
+  split_ifs <;> rfl
+
+@[simp]
+theorem bitwise'_zero_right (m : Nat) :
+    bitwise' f m 0 = bif f true false then m else 0 := by
+  unfold bitwise' binaryRec
+  simp only [Bool.cond_eq_ite, eq_mpr_eq_cast, cast_eq, dite_eq_ite]
+  split_ifs with hx <;> simp only [bit_decomp, binaryRec_zero, hx]
+
+lemma bitwise_zero : bitwise f 0 0 = 0 := by
+  simp only [bitwise_zero_right, ite_self]
+
+@[simp]
+lemma bitwise_of_ne_zero {n m : Nat} (hn : n ≠ 0) (hm : m ≠ 0) :
+    bitwise f n m = bit (f (bodd n) (bodd m)) (bitwise f (n / 2) (m / 2)) := by
+  conv_lhs => { unfold bitwise }
+  have mod_two_iff_bod x : (x % 2 = 1 : Bool) = bodd x := by
+    simp [mod_two_of_bodd, cond]; cases bodd x <;> rfl
+  simp only [hn, hm, mod_two_iff_bod, ite_false, bit, bit1, bit0, Bool.cond_eq_ite]
+  split_ifs <;> rfl
+
+@[simp]
+lemma bitwise'_of_ne_zero {n m : Nat} (hn : n ≠ 0) (hm : m ≠ 0) :
+    bitwise' f n m = bit (f (bodd n) (bodd m)) (bitwise' f (n / 2) (m / 2)) := by
+  conv_lhs => { rw [←bit_decomp n, ←bit_decomp m] }
+  rw [bitwise'_bit', bit, div2_val, div2_val]
+  case ham =>
+    obtain ⟨⟩ | n := n
+    · contradiction
+    · simp only [div2_succ, cond, bodd_succ, Bool.not_not]
+      cases bodd n <;> simp
+  case hbn =>
+    obtain ⟨⟩ | m := m
+    · contradiction
+    · simp only [div2_succ, cond, bodd_succ, Bool.not_not]
+      cases bodd m <;> simp
+
+lemma bitwise'_eq_bitwise (f) : bitwise' f = bitwise f := by
+  funext x y
+  induction' x using Nat.strongInductionOn with x ih generalizing y
+  cases' x with x <;> cases' y with y
+  · simp only [bitwise_zero, bitwise'_zero]
+  · simp only [bitwise_zero_left, bitwise'_zero_left, Bool.cond_eq_ite]
+  · simp only [bitwise_zero_right, bitwise'_zero_right, Bool.cond_eq_ite]
+  · specialize ih ((x+1) / 2) (div_lt_self' ..)
+    simp only [ne_eq, succ_ne_zero, not_false_eq_true, bitwise'_of_ne_zero, ih, bitwise_of_ne_zero]
+
+theorem lor'_eq_lor : lor' = lor :=
+  bitwise'_eq_bitwise _
+
+theorem land'_eq_land : land' = land :=
+  bitwise'_eq_bitwise _
+
+theorem xor'_eq_xor : lxor' = xor := by
+  unfold lxor' xor
+  have : _root_.xor = bne := by
+    funext x y; cases x <;> cases y <;> rfl
+  rw [this]
+  exact bitwise'_eq_bitwise _
+
+@[simp]
+lemma bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false := by rfl) (a m b n) :
+    bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n) := by
+  simp only [←bitwise'_eq_bitwise, bitwise'_bit h]
+
+@[simp]
+theorem lor_bit : ∀ a m b n, lor (bit a m) (bit b n) = bit (a || b) (lor m n) :=
+  bitwise_bit
+
+@[simp]
+theorem land_bit : ∀ a m b n, land (bit a m) (bit b n) = bit (a && b) (land m n) :=
+  bitwise_bit
+
+@[simp]
+theorem lxor_bit : ∀ a m b n, xor (bit a m) (bit b n) = bit (bne a b) (xor m n) :=
+  bitwise_bit
+
+end
+
 @[simp]
 theorem bit_false : bit false = bit0 :=
   rfl
@@ -161,6 +260,17 @@ theorem testBit_two_pow (n m : ℕ) : testBit (2 ^ n) m = (n = m) := by
     simp [h]
 #align nat.test_bit_two_pow Nat.testBit_two_pow
 
+theorem bitwise'_swap {f : Bool → Bool → Bool} (h : f false false = false) :
+    bitwise' (Function.swap f) = Function.swap (bitwise' f) := by
+  funext m n; revert n
+  dsimp [Function.swap]
+  apply binaryRec _ _ m <;> intro n
+  · rw [bitwise'_zero_left, bitwise'_zero_right, Bool.cond_eq_ite]
+  · intros a ih m'
+    apply bitCasesOn m'; intro b n'
+    rw [bitwise'_bit, bitwise'_bit, ih] <;> exact h
+#align nat.bitwise_swap Nat.bitwise'_swap
+
 /-- If `f` is a commutative operation on bools such that `f false false = false`, then `bitwise f`
     is also commutative. -/
 theorem bitwise'_comm {f : Bool → Bool → Bool} (hf : ∀ b b', f b b' = f b' b)

Mathlib/Data/Num/Lemmas.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Data.Num.Bitwise
 import Mathlib.Data.Int.CharZero
+import Mathlib.Data.Nat.Bitwise
 import Mathlib.Data.Nat.GCD.Basic
 import Mathlib.Data.Nat.PSub
 import Mathlib.Data.Nat.Size
@@ -922,7 +923,7 @@ theorem bitwise'_to_nat {f : Num → Num → Num} {g : Bool → Bool → Bool} (
     any_goals assumption
     any_goals rw [Nat.bitwise'_zero, p11]; cases g true true <;> rfl
     any_goals rw [Nat.bitwise'_zero_left, this, ← bit_to_nat, p1b]
-    any_goals rw [Nat.bitwise'_zero_right _ gff, this, ← bit_to_nat, pb1]
+    any_goals rw [Nat.bitwise'_zero_right, this, ← bit_to_nat, pb1]
     all_goals
       rw [← show ∀ n : PosNum, ↑(p m n) = Nat.bitwise' g ↑m ↑n from IH]
       rw [← bit_to_nat, pbb]

Mathlib/Init/Data/Nat/Bitwise.lean

@@ -409,14 +409,6 @@ theorem bitwise'_zero_left (f : Bool → Bool → Bool) (n) :
   unfold bitwise'; rw [binaryRec_zero]
 #align nat.bitwise_zero_left Nat.bitwise'_zero_left
 
-@[simp]
-theorem bitwise'_zero_right (f : Bool → Bool → Bool) (h : f false false = false) (m) :
-    bitwise' f m 0 = cond (f true false) m 0 := by
-  unfold bitwise'; apply bitCasesOn m; intros; rw [binaryRec_eq, binaryRec_zero]
-  exact bitwise'_bit_aux h
-#align nat.bitwise_zero_right Nat.bitwise'_zero_right
-
-@[simp]
 theorem bitwise'_zero (f : Bool → Bool → Bool) : bitwise' f 0 0 = 0 := by
   rw [bitwise'_zero_left]
   cases f false true <;> rfl
@@ -442,31 +434,6 @@ theorem bitwise'_bit {f : Bool → Bool → Bool} (h : f false false = false) (a
   · exact bitwise'_bit_aux h
 #align nat.bitwise_bit Nat.bitwise'_bit
 
-theorem bitwise'_swap {f : Bool → Bool → Bool} (h : f false false = false) :
-    bitwise' (Function.swap f) = Function.swap (bitwise' f) := by
-  funext m n; revert n
-  dsimp [Function.swap]
-  apply binaryRec _ _ m <;> intro n
-  · rw [bitwise'_zero_left, bitwise'_zero_right]
-    exact h
-  · intros a ih m'
-    apply bitCasesOn m'; intro b n'
-    rw [bitwise'_bit, bitwise'_bit, ih] <;> exact h
-#align nat.bitwise_swap Nat.bitwise'_swap
-
--- Porting note:
--- If someone wants to merge `bitwise` and `bitwise'`
--- (and similarly `lor` / `lor'` and `land` / `land'`)
--- they could start by proving the next theorem:
--- lemma bitwise_eq_bitwise' (f : Bool → Bool → Bool) :
---     bitwise f = bitwise' f := by
---   sorry
-
--- @[simp]
--- theorem bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false) (a m b n) :
---     bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n) := by
---   simp only [bitwise_eq_bitwise', bitwise'_bit h]
-
 @[simp]
 theorem lor'_bit : ∀ a m b n, lor' (bit a m) (bit b n) = bit (a || b) (lor' m n) :=
   bitwise'_bit rfl