提交 #9

import Mathlib.Data.Int.Bitwise

axiom Z.bit0_odd : forall (a : ℤ), Int.testBit a 0 = Int.bodd a

axiom Z_div_mod_eq_full
     : forall a b : ℤ, a = b * (a / b) + a % b
axiom Zodd_mod
     : forall a : ℤ, Int.bodd a = ((a % 2) == 1)

axiom Z.bit0_mod
     : forall a : ℤ, Bool.toInt (Int.testBit a 0) = a % 2

axiom Z.testbit_succ_r
     : forall (a : ℤ) (b : Bool) (n : Nat),
0 <= n -> Int.testBit (2 * a + Bool.toInt b) (n.succ) = Int.testBit a n

axiom Z.odd_sub
     : forall n m : ℤ, Int.bodd (n - m) = xor (Int.bodd n) (Int.bodd m)

lemma Zodd_b2z : ∀ (b : Bool), Int.bodd (Bool.toInt b) = b := by
  intro b
  cases b <;> rfl


lemma decomp : ∀ (x : ℤ), x = 2 * (x / 2) + Bool.toInt (Int.bodd x) :=
by
  intro x
  rw [<- Z.bit0_odd]
  rw [Z.bit0_mod]
  apply Z_div_mod_eq_full

lemma b2z_div2 : ∀ (b : Bool), (Bool.toInt b / 2 : ℤ) = 0 := by
  intro b
  cases b <;> rfl

lemma b2z_exists : ∀ (x y : ℤ) (c0 : Bool),
  ∃ (cr : Bool),
    Bool.toInt ((not (Int.bodd x)) && Int.bodd y) +
    Bool.toInt ((not (xor (Int.bodd x) (Int.bodd y))) && c0) = Bool.toInt cr := by
  intro x y c0
  have hx := Int.bodd x
  have hy := Int.bodd y
  cases hx <;> cases hy <;> cases c0 <;> simp
  · cases x.bodd <;> cases y.bodd <;> simp
  · cases x.bodd <;> cases y.bodd <;> simp
  · cases x.bodd <;> cases y.bodd <;> simp
  · cases x.bodd <;> cases y.bodd <;> simp

def sub_borrow_bit (x y : ℤ) (c : Bool) : ℕ → Bool
  | 0 => c
  | n + 1 =>
    let pc := sub_borrow_bit x y c n
    ((not (x.testBit n)) && y.testBit n) ||
    (pc && (not (xor (x.testBit n) (y.testBit n))))

lemma borrow_bit_rew : ∀ (x y : ℤ) (c : Bool) (n : ℕ),
    sub_borrow_bit x y c n =
    match n with
    | 0 => c
    | n + 1 =>
      let pc := sub_borrow_bit x y c n
      ((not (x.testBit n)) && y.testBit n) ||
      (pc && (not (xor (x.testBit n) (y.testBit n))))
 := by
  intro x y c n
  cases n <;> rfl

lemma sub_shift : ∀ a b : ℤ,
    ((a - b) / 2) = (a / 2 - b / 2 - Bool.toInt ((not (Int.bodd a)) && Int.bodd b)) := by
  intro a b
  rw [Zodd_mod]
  rw [Zodd_mod]
  have LB: (!a % 2 == 1 && b % 2 == 1) = true ∨
  (!a % 2 == 1 && b % 2 == 1) = false := by
    simp
    intro HF
    omega

  rcases LB with (LB | LB)
  · rw [LB]
    simp
    rw [Bool.and_eq_true] at LB
    rcases LB with ⟨LB1, LB2⟩
    rw [Bool.not_eq_true'] at LB1
    simp at LB1 LB2
    omega

  · have LB1: (!a % 2 == 1)  ∨ (a % 2 == 1) := by
      simp
      omega

    rcases LB1 with (LB1 | LB1)
    · rw [LB1]
      simp at *
      specialize LB LB1
      have t: (b % 2 == 1)=false := by
        simp
        assumption
      rw [t]
      simp
      omega
    · rw [LB1]
      simp at *
      omega

lemma sub_borrow_bit_eq : ∀ (n : ℕ) (x y : ℤ) (cr c0 : Bool)
  (_ :
    Bool.toInt ((not (Int.bodd x)) && Int.bodd y) +
    Bool.toInt ((not (xor (Int.bodd x) (Int.bodd y))) && c0) =
      Bool.toInt cr),
    sub_borrow_bit (x / 2) (y / 2) cr n =
    (((not (x.testBit n)) && y.testBit n) ||
    (sub_borrow_bit x y c0 n && (not (xor (x.testBit n) (y.testBit n))))) := by
  intro n
  induction n with
  | zero =>
    intros x y cr c0 CR
    have hx : x.bodd ∨ ! x.bodd := by simp
    have hy : y.bodd ∨ ! y.bodd := by simp
    rcases hx with (hx | hx) <;> rcases hy with (hy | hy) <;> cases c0 <;> cases cr <;>
    simp [sub_borrow_bit, Z.bit0_odd] at * <;> rw [hx, hy] at * <;> simp at *

  | succ n IHn =>
    intro x y cr c0 CR
    rw [borrow_bit_rew]
    simp
    apply IHn at CR
    rw [CR]
    simp [sub_borrow_bit]

    rw [show (x.testBit (n + 1)) = ((x / 2).testBit n) from ?_]
    · rw [show (y.testBit (n + 1)) = ((y / 2).testBit n) from ?_]
      rw (config := { occs := .pos [1]}) [(decomp y)]
      rw [Z.testbit_succ_r]
      omega
    · rw (config := { occs := .pos [1]}) [(decomp x)]
      rw [Z.testbit_succ_r]
      omega

lemma xtestbit_sub_sound : ∀ (n : ℕ) (x y : ℤ) (c0 : Bool),
    ((x - y - Bool.toInt c0).testBit n) =
    xor (xor (x.testBit n) (y.testBit n)) (sub_borrow_bit x y c0 n) :=
by
  intro n
  induction n with
  | zero =>
    intros x y c0
    simp [sub_borrow_bit] at *
    rw [Z.bit0_odd]
    rw [Z.bit0_odd]
    rw [Z.bit0_odd]
    rw [Z.odd_sub]
    rw [Z.odd_sub]
    rw [Zodd_b2z]
    cases x.bodd <;> cases y.bodd <;> cases c0 <;> simp

  | succ n IHn =>
    intro x y c0
    rw [decomp (x - y - Bool.toInt c0), Z.testbit_succ_r] <;> try omega
    simp [sub_borrow_bit]
    rw (config := { occs := .pos [2]}) [(decomp x)]
    rw (config := { occs := .pos [2]}) [(decomp y)]
    rw [Z.testbit_succ_r] <;> try omega
    rw [sub_shift, sub_shift, b2z_div2, Z.odd_sub, Zodd_b2z]

    have CR := b2z_exists x y c0
    rcases CR with ⟨cr, CR⟩

    have Heq:
      (x / 2 - y / 2 - (!x.bodd && y.bodd).toInt - 0 - (!(x.bodd ^^ y.bodd) && c0).toInt) =
      x / 2 - y / 2 - Bool.toInt cr := by
      simp
      have hx : x.bodd ∨ ! x.bodd := by simp
      have hy : y.bodd ∨ ! y.bodd := by simp
      have Heq1: - (!x.bodd && y.bodd).toInt - (!(x.bodd ^^ y.bodd) && c0).toInt = - cr.toInt := by
        rcases c0 <;> rcases cr <;> rcases hx <;> rcases hy <;>
        simp at * <;> omega
      omega
    rw [Heq]; clear Heq
    rw [IHn]
    simp
    clear IHn
    have Heq:= sub_borrow_bit_eq n x y cr c0 CR
    rw [Heq]
    simp
    simp [Z.testbit_succ_r]


lemma testbit_sub_sound : ∀ (n : ℕ) (x y : ℤ),
    ((x - y).testBit n) = xor (xor (x.testBit n) (y.testBit n)) (sub_borrow_bit x y false n) := by
  intro n x y
  rw [show (x - y) = (x - y - Bool.toInt false) by simp [Bool.toInt]]
  exact xtestbit_sub_sound n x y false