castNum_eq_bitwise — Mathlib

English

There exists a general framework showing that, under suitable hypotheses, bitwise operations on Num correspond to the same bitwise operations on their α-casts, i.e. f(m,n) corresponds to Nat.bitwise g (cast m) (cast n).

Русский

Существует общая конструкция, по которой битовые операции над Num соответствуют тем же битовым операциям над их образами в α, т.е. f(m,n) соответствует Nat.bitwise g (cast m) (cast n).

LaTeX

$$$\forall m,n\,\exists f,g\;\text{such that } f(m,n) = \;\text{Nat.bitwise } g (\operatorname{cast}(m)) (\operatorname{cast}(n))$$$

Lean4

theorem castNum_eq_bitwise {f : Num → Num → Num} {g : Bool → Bool → Bool} (p : PosNum → PosNum → Num)
    (gff : g false false = false) (f00 : f 0 0 = 0) (f0n : ∀ n, f 0 (pos n) = cond (g false true) (pos n) 0)
    (fn0 : ∀ n, f (pos n) 0 = cond (g true false) (pos n) 0) (fnn : ∀ m n, f (pos m) (pos n) = p m n)
    (p11 : p 1 1 = cond (g true true) 1 0)
    (p1b : ∀ b n, p 1 (PosNum.bit b n) = bit (g true b) (cond (g false true) (pos n) 0))
    (pb1 : ∀ a m, p (PosNum.bit a m) 1 = bit (g a true) (cond (g true false) (pos m) 0))
    (pbb : ∀ a b m n, p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)) :
    ∀ m n : Num, (f m n : ℕ) = Nat.bitwise g m n := by
  intro m n
  obtain - | m := m <;> obtain - | n := n <;> try simp only [show zero = 0 from rfl, show ((0 : Num) : ℕ) = 0 from rfl]
  · rw [f00, Nat.bitwise_zero]; rfl
  · rw [f0n, Nat.bitwise_zero_left]
    cases g false true <;> rfl
  · rw [fn0, Nat.bitwise_zero_right]
    cases g true false <;> rfl
  · rw [fnn]
    have this b (n : PosNum) : (cond b (↑n) 0 : ℕ) = ↑(cond b (pos n) 0 : Num) := by cases b <;> rfl
    have this' b (n : PosNum) : ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n := by cases b <;> simp
    induction m generalizing n with
      | one => ?_
      | bit1 m IH => ?_
      | bit0 m IH => ?_ <;>
      obtain - | n | n := n
    any_goals
      simp only [show one = 1 from rfl, show pos 1 = 1 from rfl, show PosNum.bit0 = PosNum.bit false from rfl,
        show PosNum.bit1 = PosNum.bit true from rfl, show ((1 : Num) : ℕ) = Nat.bit true 0 from rfl]
    all_goals
      repeat rw [this']
      rw [Nat.bitwise_bit gff]
    any_goals rw [Nat.bitwise_zero, p11]; cases g true true <;> rfl
    any_goals rw [Nat.bitwise_zero_left, ← Bool.cond_eq_ite, this, ← bit_to_nat, p1b]
    any_goals rw [Nat.bitwise_zero_right, ← Bool.cond_eq_ite, 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]

Похожие утверждения