bitwise_eq_binaryRec — Mathlib

English

Let f be a binary Boolean operation on {true, false}. Then the two-argument function bitwise f on natural numbers is completely determined by a two-level recursion. Specifically, bitwise f is equal to the two-argument function defined by a nested binaryRec, with the first level controlled by the value of f(false, true) and the second level controlled by the value of f(true, false) in conjunction with the current bit of the first argument. In short, bitwise f is given by the recursion in which the base case depends on f(false,true) and the recursive step uses f(true,false) together with the previous bits and the combining operation f on the current bits.

Русский

Пусть f — булева бинарная операция на {истина, ложь}. Тогда побитовая операция bitwise f над натуральными числами полностью задаётся двойной рекурсией. Формула: bitwise f = binaryRec (λn. if f(false,true) then n else 0) (λa m Ia. binaryRec (λn. if f(true,false) then bit a m else 0) (λb n _. bit (f a b) (Ia n))). Проще говоря, битовая операция задаётся рекурсией по битам первых аргументов, при этом базовый случай и шаг рекурсии зависят от значения f на соответствующих битах.

LaTeX

$$$ bitwise f = binaryRec\left( \lambda n. \text{if } f(\text{false},\text{true}) \text{ then } n \text{ else } 0 \right) \left( \lambda a\, m\, Ia. \\ \quad binaryRec\left( \lambda n. \text{if } f(\text{true},\text{false}) \text{ then } \text{bit } a m \text{ else } 0 \right) \left( \lambda b\, n\, _ \Rightarrow \text{bit}(f a b) (Ia n) \right) \right) $$$

Lean4

theorem bitwise_eq_binaryRec (f : Bool → Bool → Bool) :
    bitwise f =
      binaryRec (fun n => cond (f false true) n 0) fun a m Ia =>
        binaryRec (cond (f true false) (bit a m) 0) fun b n _ => bit (f a b) (Ia n) :=
  by
  funext x y
  induction x using binaryRec' generalizing y with
  | zero => simp only [bitwise_zero_left, binaryRec_zero, Bool.cond_eq_ite]
  | bit xb x hxb ih =>
    rw [← bit_ne_zero_iff] at hxb
    simp_rw [binaryRec_of_ne_zero _ _ hxb, bodd_bit, div2_bit, eq_rec_constant]
    induction y using binaryRec' with
    | zero => simp only [bitwise_zero_right, binaryRec_zero, Bool.cond_eq_ite]
    | bit yb y hyb =>
      rw [← bit_ne_zero_iff] at hyb
      simp_rw [binaryRec_of_ne_zero _ _ hyb, bitwise_of_ne_zero hxb hyb, bodd_bit, ← div2_val, div2_bit,
        eq_rec_constant, ih]

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