提交 #24

import Mathlib.Data.Int.Bitwise
import Mathlib.Data.Nat.Notation
import Mathlib.Tactic.ApplyFun
import Mathlib.Tactic.Lemma
import Mathlib.Tactic.NormNum

def sub_borrow_bit (x y : Int) (c : Bool) : Nat → Bool
  | 0 => c
  | n + 1 =>
    let xₙ := x.testBit n
    let yₙ := y.testBit n
    let cₙ := sub_borrow_bit x y c n
    !xₙ && yₙ || cₙ && !(xₙ ^^ yₙ)

lemma Nat.odd_mod (a : ℕ) : a.bodd = (a % 2 == 1) := by
  apply_fun Bool.toNat
  rw [← Nat.mod_two_of_bodd]
  rcases a.mod_two_eq_zero_or_one with (h | h) <;> simp [h]
  simp

lemma Nat.bit₀_odd (a : ℕ) : a.testBit 0 = a.bodd := by
  simp [a.odd_mod]
  rfl

lemma Int.odd_mod (a : ℤ) : a.bodd = (a % 2 == 1) := by
  cases a with
  | ofNat n =>
    change n.bodd = _
    rw [n.odd_mod]
    simp
    omega
  | negSucc n =>
    change (!n.bodd) = _
    rw [n.odd_mod, Int.negSucc_emod _ two_pos]
    change _ = (2 - 1 - n % ((2 : ℕ) : ℤ) == ((1 : ℕ) : ℤ))
    rw [← Int.natCast_mod]
    rcases n.mod_two_eq_zero_or_one with (h | h) <;> simp [h]

lemma Int.bit₀_odd (a : ℤ) : a.testBit 0 = a.bodd := by
  cases a with
  | ofNat n => exact n.bit₀_odd
  | negSucc n =>
    change (!_) = (!_)
    rw [n.bit₀_odd]

lemma Int.bit₀_mod (a : ℤ) : (a.testBit 0).toInt = a % 2 := by
  rw [a.bit₀_odd]
  have h₁ := a.bodd_add_div2
  rw [a.div2_val] at h₁
  have h₂ := a.ediv_add_emod 2
  have h₃ := h₁.trans h₂.symm
  rw [Int.add_comm _ (a % 2)] at h₃
  simp at h₃
  rw [← h₃]
  grind

lemma Int.testbit_succ (a : ℤ) (n : Nat) : a.testBit n.succ = (a / 2).testBit n := by
  conv => lhs; rw [← a.bit_decomp, a.div2_val]
  exact (a / 2).testBit_bit_succ n _

lemma decomp (x : ℤ) : x = 2 * (x / 2) + x.bodd.toInt := by
  rw [← x.bit₀_odd, x.bit₀_mod]
  exact (x.ediv_add_emod 2).symm

lemma sub_shift₀ (a b : ℤ) : ((a - b) / 2) = (a / 2 - b / 2 - (!a.bodd && b.bodd).toInt) := by
  conv => lhs; rw [decomp a, decomp b]
  rw [add_sub_add_comm, ← Int.mul_sub, Int.mul_add_ediv_left _ _ (by simp)]
  congr 1
  generalize a.bodd = a₀
  generalize b.bodd = b₀
  revert a₀ b₀
  decide

lemma sub_shift₁ (a b : ℤ) : ((a - b - 1) / 2) = (a / 2 - b / 2 - (!a.bodd || b.bodd).toInt) := by
  conv => lhs; rw [decomp a, decomp b]
  rw [add_sub_add_comm, ← Int.mul_sub, Int.add_sub_assoc, Int.mul_add_ediv_left _ _ (by simp)]
  congr 1
  generalize a.bodd = a₀
  generalize b.bodd = b₀
  revert a₀ b₀
  decide

lemma sub_borrow_bit_succ (x y : ℤ) (c : Bool) (n : ℕ) :
  sub_borrow_bit x y c n.succ = sub_borrow_bit (x / 2) (y / 2) (!x.bodd && y.bodd || c && !(x.bodd ^^ y.bodd)) n := by
  induction n with
  | zero =>
    change sub_borrow_bit x y c 1 = (!x.bodd && y.bodd || c && !(x.bodd ^^ y.bodd))
    unfold sub_borrow_bit
    simp only
    repeat rw [Int.bit₀_odd]
    rfl
  | succ n h =>
    change (_ || _) = (_ || _)
    rw [h]
    repeat rw [Int.testbit_succ]

theorem xtestbit_sub_sound (n : ℕ) (x y : ℤ) (c₀ : Bool) :
  ((x - y - c₀.toInt).testBit n) = (x.testBit n ^^ y.testBit n ^^ sub_borrow_bit x y c₀ n) := by
  induction n generalizing x y c₀ with
  | zero =>
    unfold sub_borrow_bit
    repeat rw [Int.bit₀_odd]
    change (x + (-y) + (-c₀.toInt)).bodd = _
    simp
    cases c₀ <;> simp
  | succ n h =>
    cases c₀ with
    | false =>
      simp only [Bool.toInt_false, sub_zero]
      repeat rw [Int.testbit_succ]
      rw [sub_shift₀ x y]
      let c₁ := !x.bodd && y.bodd
      change (x / 2 - y / 2 - c₁.toInt).testBit n = _
      convert h (x / 2) (y / 2) c₁ using 2
      rw [sub_borrow_bit_succ x y false n]
      congr
      simp [c₁]
    | true =>
      simp only [Bool.toInt_true]
      repeat rw [Int.testbit_succ]
      rw [sub_shift₁ x y]
      let c₁ := !x.bodd || y.bodd
      change (x / 2 - y / 2 - c₁.toInt).testBit n = _
      convert h (x / 2) (y / 2) c₁ using 2
      rw [sub_borrow_bit_succ x y true n]
      congr 1
      simp [c₁]
      generalize x.bodd = x₀
      generalize y.bodd = y₀
      revert x₀ y₀
      decide

#print axioms xtestbit_sub_sound