Imports

/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module

public import Mathlib.Logic.Function.Basic
public import Aesop
public import Mathlib.Data.Int.Notation
public import Mathlib.Data.Nat.Notation
public import Mathlib.Logic.IsEmpty.Defs
public import Mathlib.Tactic.Attr.Core
public import Mathlib.Tactic.Push
public import Mathlib.Tactic.SplitIfs

set_option doc.verso true

Maintaining the number of unequal binary digits

Counting unequal positions below a fixed width detects equality when both bit streams agree beyond that width. Flipping one digit changes this count by one, positively for an initially equal pair and negatively for an initially unequal pair.

Main definitions

mismatchCount counts unequal positions below a width.
flipAt changes one position of a bit stream.

Main statements

mismatchCount_le bounds the count by the width.
mismatchCount_flip_left gives the displacement caused by one bit change.

Tags

binary counter, Hamming distance, bit stream

@[expose] public sectionnamespace Geb.BitTree.BinaryMachine

The number of unequal positions below the given width.

def mismatchCount (width : ℕ) (a b : ℕ → Bool) : ℕ :=
  (List.range width).countP fun i ↦ a i != b i

Flip one bit of a stream.

def flipAt (a : ℕ → Bool) (i : ℕ) : ℕ → Bool := Function.update a i (!a i)

Extending the width adds the contribution from the new position.

theorem mismatchCount_succ (width : ℕ) (a b : ℕ → Bool) :
    mismatchCount (width + 1) a b =
      mismatchCount width a b + if a width = b width then 0 else 1 := bywidth:ℕa:ℕ → Boolb:ℕ → Bool⊢ mismatchCount (width + 1) a b = mismatchCount width a b + if a width = b width then 0 else 1
  simp [mismatchCount, List.range_succ]All goals completed! 🐙

There cannot be more unequal positions than positions.

theorem mismatchCount_le (width : ℕ) (a b : ℕ → Bool) :
    mismatchCount width a b ≤ width := bywidth:ℕa:ℕ → Boolb:ℕ → Bool⊢ mismatchCount width a b ≤ width
  simpa [mismatchCount] using
    (List.countP_le_length (l := List.range width) (p := fun i ↦ a i != b i))All goals completed! 🐙

The count depends only on the bits below the given width.

theorem mismatchCount_congr (width : ℕ) (a a' b b' : ℕ → Bool)
    (ha : ∀ i < width, a i = a' i) (hb : ∀ i < width, b i = b' i) :
    mismatchCount width a b = mismatchCount width a' b' := bywidth:ℕa:ℕ → Boola':ℕ → Boolb:ℕ → Boolb':ℕ → Boolha:∀ (i : ℕ), i < width → a i = a' ihb:∀ (i : ℕ), i < width → b i = b' i⊢ mismatchCount width a b = mismatchCount width a' b'
  apply List.countP_congrwidth:ℕa:ℕ → Boola':ℕ → Boolb:ℕ → Boolb':ℕ → Boolha:∀ (i : ℕ), i < width → a i = a' ihb:∀ (i : ℕ), i < width → b i = b' i⊢ ∀ (x : ℕ), x ∈ List.range width → ((a x != b x) = true ↔ (a' x != b' x) = true)
  intro i hiwidth:ℕa:ℕ → Boola':ℕ → Boolb:ℕ → Boolb':ℕ → Boolha:∀ (i : ℕ), i < width → a i = a' ihb:∀ (i : ℕ), i < width → b i = b' ii:ℕhi:i ∈ List.range width⊢ (a i != b i) = true ↔ (a' i != b' i) = true
  rw [ha i (List.mem_range.mp hi),width:ℕa:ℕ → Boola':ℕ → Boolb:ℕ → Boolb':ℕ → Boolha:∀ (i : ℕ), i < width → a i = a' ihb:∀ (i : ℕ), i < width → b i = b' ii:ℕhi:i ∈ List.range width⊢ (a' i != b i) = true ↔ (a' i != b' i) = true hb i (List.mem_range.mp hi)width:ℕa:ℕ → Boola':ℕ → Boolb:ℕ → Boolb':ℕ → Boolha:∀ (i : ℕ), i < width → a i = a' ihb:∀ (i : ℕ), i < width → b i = b' ii:ℕhi:i ∈ List.range width⊢ (a' i != b' i) = true ↔ (a' i != b' i) = true]All goals completed! 🐙

Interchanging the streams preserves the mismatch count.

theorem mismatchCount_comm (width : ℕ) (a b : ℕ → Bool) :
    mismatchCount width a b = mismatchCount width b a := bywidth:ℕa:ℕ → Boolb:ℕ → Bool⊢ mismatchCount width a b = mismatchCount width b a
  apply List.countP_congrwidth:ℕa:ℕ → Boolb:ℕ → Bool⊢ ∀ (x : ℕ), x ∈ List.range width → ((a x != b x) = true ↔ (b x != a x) = true)
  intro i _width:ℕa:ℕ → Boolb:ℕ → Booli:ℕa✝:i ∈ List.range width⊢ (a i != b i) = true ↔ (b i != a i) = true
  simp [ne_comm]All goals completed! 🐙

A flip beyond the counted positions leaves the count unchanged.

theorem mismatchCount_flip_left_of_le (width i : ℕ) (a b : ℕ → Bool) (h : width ≤ i) :
    mismatchCount width (flipAt a i) b = mismatchCount width a b := bywidth:ℕi:ℕa:ℕ → Boolb:ℕ → Boolh:width ≤ i⊢ mismatchCount width (flipAt a i) b = mismatchCount width a b
  apply mismatchCount_congrhawidth:ℕi:ℕa:ℕ → Boolb:ℕ → Boolh:width ≤ i⊢ ∀ (i_1 : ℕ), i_1 < width → flipAt a i i_1 = a i_1hbwidth:ℕi:ℕa:ℕ → Boolb:ℕ → Boolh:width ≤ i⊢ ∀ (i : ℕ), i < width → b i = b i
  ·hawidth:ℕi:ℕa:ℕ → Boolb:ℕ → Boolh:width ≤ i⊢ ∀ (i_1 : ℕ), i_1 < width → flipAt a i i_1 = a i_1 intro j hjhawidth:ℕi:ℕa:ℕ → Boolb:ℕ → Boolh:width ≤ ij:ℕhj:j < width⊢ flipAt a i j = a j
    exact Function.update_of_ne (bywidth:ℕi:ℕa:ℕ → Boolb:ℕ → Boolh:width ≤ ij:ℕhj:j < width⊢ j ≠ i omegaAll goals completed! 🐙) _ _
  ·hbwidth:ℕi:ℕa:ℕ → Boolb:ℕ → Boolh:width ≤ i⊢ ∀ (i : ℕ), i < width → b i = b i intro j _hbwidth:ℕi:ℕa:ℕ → Boolb:ℕ → Boolh:width ≤ ij:ℕa✝:j < width⊢ b j = b j
    rflAll goals completed! 🐙

Flipping a position changes its contribution from zero to one or from one to zero.

theorem mismatchCount_flip_left (width i : ℕ) (a b : ℕ → Bool) (h : i < width) :
    (mismatchCount width (flipAt a i) b : ℤ) =
      (mismatchCount width a b : ℤ) + if a i = b i then 1 else -1 := bywidth:ℕi:ℕa:ℕ → Boolb:ℕ → Boolh:i < width⊢ ↑(mismatchCount width (flipAt a i) b) = ↑(mismatchCount width a b) + if a i = b i then 1 else -1
  revert iwidth:ℕa:ℕ → Boolb:ℕ → Bool⊢ ∀ (i : ℕ), i < width → ↑(mismatchCount width (flipAt a i) b) = ↑(mismatchCount width a b) + if a i = b i then 1 else -1
  apply Nat.rec (motive := fun width ↦ ∀ i, i < width →
    (mismatchCount width (flipAt a i) b : ℤ) =
      (mismatchCount width a b : ℤ) + if a i = b i then 1 else -1) ?_ ?_ widthwidth:ℕa:ℕ → Boolb:ℕ → Bool⊢ ∀ (i : ℕ),
  i < Nat.zero → ↑(mismatchCount Nat.zero (flipAt a i) b) = ↑(mismatchCount Nat.zero a b) + if a i = b i then 1 else -1width:ℕa:ℕ → Boolb:ℕ → Bool⊢ ∀ (n : ℕ),
  (∀ (i : ℕ), i < n → ↑(mismatchCount n (flipAt a i) b) = ↑(mismatchCount n a b) + if a i = b i then 1 else -1) →
    ∀ (i : ℕ),
      i < n.succ → ↑(mismatchCount n.succ (flipAt a i) b) = ↑(mismatchCount n.succ a b) + if a i = b i then 1 else -1
  ·width:ℕa:ℕ → Boolb:ℕ → Bool⊢ ∀ (i : ℕ),
  i < Nat.zero → ↑(mismatchCount Nat.zero (flipAt a i) b) = ↑(mismatchCount Nat.zero a b) + if a i = b i then 1 else -1 intro i hiwidth:ℕa:ℕ → Boolb:ℕ → Booli:ℕhi:i < Nat.zero⊢ ↑(mismatchCount Nat.zero (flipAt a i) b) = ↑(mismatchCount Nat.zero a b) + if a i = b i then 1 else -1
    exact (Nat.not_lt_zero i hi).elimAll goals completed! 🐙
  ·width:ℕa:ℕ → Boolb:ℕ → Bool⊢ ∀ (n : ℕ),
  (∀ (i : ℕ), i < n → ↑(mismatchCount n (flipAt a i) b) = ↑(mismatchCount n a b) + if a i = b i then 1 else -1) →
    ∀ (i : ℕ),
      i < n.succ → ↑(mismatchCount n.succ (flipAt a i) b) = ↑(mismatchCount n.succ a b) + if a i = b i then 1 else -1 intro k ih i hiwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succ⊢ ↑(mismatchCount k.succ (flipAt a i) b) = ↑(mismatchCount k.succ a b) + if a i = b i then 1 else -1
    rw [mismatchCount_succ,width:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succ⊢ ↑(mismatchCount k (flipAt a i) b + if flipAt a i k = b k then 0 else 1) =
  ↑(mismatchCount k.succ a b) + if a i = b i then 1 else -1 mismatchCount_succwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succ⊢ ↑(mismatchCount k (flipAt a i) b + if flipAt a i k = b k then 0 else 1) =
  ↑(mismatchCount k a b + if a k = b k then 0 else 1) + if a i = b i then 1 else -1]width:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succ⊢ ↑(mismatchCount k (flipAt a i) b + if flipAt a i k = b k then 0 else 1) =
  ↑(mismatchCount k a b + if a k = b k then 0 else 1) + if a i = b i then 1 else -1
    by_cases hik : i = kposwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succhik:i = k⊢ ↑(mismatchCount k (flipAt a i) b + if flipAt a i k = b k then 0 else 1) =
  ↑(mismatchCount k a b + if a k = b k then 0 else 1) + if a i = b i then 1 else -1negwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succhik:¬i = k⊢ ↑(mismatchCount k (flipAt a i) b + if flipAt a i k = b k then 0 else 1) =
  ↑(mismatchCount k a b + if a k = b k then 0 else 1) + if a i = b i then 1 else -1
    ·poswidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succhik:i = k⊢ ↑(mismatchCount k (flipAt a i) b + if flipAt a i k = b k then 0 else 1) =
  ↑(mismatchCount k a b + if a k = b k then 0 else 1) + if a i = b i then 1 else -1 subst iposwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1hi:k < k.succ⊢ ↑(mismatchCount k (flipAt a k) b + if flipAt a k k = b k then 0 else 1) =
  ↑(mismatchCount k a b + if a k = b k then 0 else 1) + if a k = b k then 1 else -1
      rw [mismatchCount_flip_left_of_le k k a b (Nat.le_refl _)poswidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1hi:k < k.succ⊢ ↑(mismatchCount k a b + if flipAt a k k = b k then 0 else 1) =
  ↑(mismatchCount k a b + if a k = b k then 0 else 1) + if a k = b k then 1 else -1]poswidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1hi:k < k.succ⊢ ↑(mismatchCount k a b + if flipAt a k k = b k then 0 else 1) =
  ↑(mismatchCount k a b + if a k = b k then 0 else 1) + if a k = b k then 1 else -1
      simp only [flipAt, Function.update_self]poswidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1hi:k < k.succ⊢ ↑(mismatchCount k a b + if (!a k) = b k then 0 else 1) =
  ↑(mismatchCount k a b + if a k = b k then 0 else 1) + if a k = b k then 1 else -1
      cases a kpos.falsewidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1hi:k < k.succ⊢ ↑(mismatchCount k a b + if (!false) = b k then 0 else 1) =
  ↑(mismatchCount k a b + if false = b k then 0 else 1) + if false = b k then 1 else -1pos.truewidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1hi:k < k.succ⊢ ↑(mismatchCount k a b + if (!true) = b k then 0 else 1) =
  ↑(mismatchCount k a b + if true = b k then 0 else 1) + if true = b k then 1 else -1 <;>pos.falsewidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1hi:k < k.succ⊢ ↑(mismatchCount k a b + if (!false) = b k then 0 else 1) =
  ↑(mismatchCount k a b + if false = b k then 0 else 1) + if false = b k then 1 else -1pos.truewidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1hi:k < k.succ⊢ ↑(mismatchCount k a b + if (!true) = b k then 0 else 1) =
  ↑(mismatchCount k a b + if true = b k then 0 else 1) + if true = b k then 1 else -1 cases b kpos.true.falsewidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1hi:k < k.succ⊢ ↑(mismatchCount k a b + if (!true) = false then 0 else 1) =
  ↑(mismatchCount k a b + if true = false then 0 else 1) + if true = false then 1 else -1pos.true.truewidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1hi:k < k.succ⊢ ↑(mismatchCount k a b + if (!true) = true then 0 else 1) =
  ↑(mismatchCount k a b + if true = true then 0 else 1) + if true = true then 1 else -1 <;>pos.false.falsewidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1hi:k < k.succ⊢ ↑(mismatchCount k a b + if (!false) = false then 0 else 1) =
  ↑(mismatchCount k a b + if false = false then 0 else 1) + if false = false then 1 else -1pos.false.truewidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1hi:k < k.succ⊢ ↑(mismatchCount k a b + if (!false) = true then 0 else 1) =
  ↑(mismatchCount k a b + if false = true then 0 else 1) + if false = true then 1 else -1pos.true.falsewidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1hi:k < k.succ⊢ ↑(mismatchCount k a b + if (!true) = false then 0 else 1) =
  ↑(mismatchCount k a b + if true = false then 0 else 1) + if true = false then 1 else -1pos.true.truewidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1hi:k < k.succ⊢ ↑(mismatchCount k a b + if (!true) = true then 0 else 1) =
  ↑(mismatchCount k a b + if true = true then 0 else 1) + if true = true then 1 else -1 simpAll goals completed! 🐙 <;>pos.false.truewidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1hi:k < k.succ⊢ ↑(mismatchCount k a b) = ↑(mismatchCount k a b) + 1 + -1pos.true.falsewidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1hi:k < k.succ⊢ ↑(mismatchCount k a b) = ↑(mismatchCount k a b) + 1 + -1 omegaAll goals completed! 🐙
    ·negwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succhik:¬i = k⊢ ↑(mismatchCount k (flipAt a i) b + if flipAt a i k = b k then 0 else 1) =
  ↑(mismatchCount k a b + if a k = b k then 0 else 1) + if a i = b i then 1 else -1 have hki : k ≠ i := Ne.symm hiknegwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succhik:¬i = khki:k ≠ i⊢ ↑(mismatchCount k (flipAt a i) b + if flipAt a i k = b k then 0 else 1) =
  ↑(mismatchCount k a b + if a k = b k then 0 else 1) + if a i = b i then 1 else -1
      have hrec := ih i (bywidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succhik:¬i = khki:k ≠ i⊢ i < k omegaAll goals completed! 🐙)negwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succhik:¬i = khki:k ≠ ihrec:↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1⊢ ↑(mismatchCount k (flipAt a i) b + if flipAt a i k = b k then 0 else 1) =
  ↑(mismatchCount k a b + if a k = b k then 0 else 1) + if a i = b i then 1 else -1
      simp only [flipAt, Function.update_of_ne hki] at hrec ⊢negwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succhik:¬i = khki:k ≠ ihrec:↑(mismatchCount k (Function.update a i !a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1⊢ ↑(mismatchCount k (Function.update a i !a i) b + if a k = b k then 0 else 1) =
  ↑(mismatchCount k a b + if a k = b k then 0 else 1) + if a i = b i then 1 else -1
      split_ifs at hrec ⊢poswidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succhik:¬i = khki:k ≠ ih✝¹:a k = b kh✝:a i = b ihrec:↑(mismatchCount k (Function.update a i !a i) b) = ↑(mismatchCount k a b) + 1⊢ ↑(mismatchCount k (Function.update a i !a i) b + 0) = ↑(mismatchCount k a b + 0) + 1negwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succhik:¬i = khki:k ≠ ih✝¹:a k = b kh✝:¬a i = b ihrec:↑(mismatchCount k (Function.update a i !a i) b) = ↑(mismatchCount k a b) + -1⊢ ↑(mismatchCount k (Function.update a i !a i) b + 0) = ↑(mismatchCount k a b + 0) + -1poswidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succhik:¬i = khki:k ≠ ih✝¹:¬a k = b kh✝:a i = b ihrec:↑(mismatchCount k (Function.update a i !a i) b) = ↑(mismatchCount k a b) + 1⊢ ↑(mismatchCount k (Function.update a i !a i) b + 1) = ↑(mismatchCount k a b + 1) + 1negwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succhik:¬i = khki:k ≠ ih✝¹:¬a k = b kh✝:¬a i = b ihrec:↑(mismatchCount k (Function.update a i !a i) b) = ↑(mismatchCount k a b) + -1⊢ ↑(mismatchCount k (Function.update a i !a i) b + 1) = ↑(mismatchCount k a b + 1) + -1 <;>poswidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succhik:¬i = khki:k ≠ ih✝¹:a k = b kh✝:a i = b ihrec:↑(mismatchCount k (Function.update a i !a i) b) = ↑(mismatchCount k a b) + 1⊢ ↑(mismatchCount k (Function.update a i !a i) b + 0) = ↑(mismatchCount k a b + 0) + 1negwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succhik:¬i = khki:k ≠ ih✝¹:a k = b kh✝:¬a i = b ihrec:↑(mismatchCount k (Function.update a i !a i) b) = ↑(mismatchCount k a b) + -1⊢ ↑(mismatchCount k (Function.update a i !a i) b + 0) = ↑(mismatchCount k a b + 0) + -1poswidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succhik:¬i = khki:k ≠ ih✝¹:¬a k = b kh✝:a i = b ihrec:↑(mismatchCount k (Function.update a i !a i) b) = ↑(mismatchCount k a b) + 1⊢ ↑(mismatchCount k (Function.update a i !a i) b + 1) = ↑(mismatchCount k a b + 1) + 1negwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:∀ (i : ℕ), i < k → ↑(mismatchCount k (flipAt a i) b) = ↑(mismatchCount k a b) + if a i = b i then 1 else -1i:ℕhi:i < k.succhik:¬i = khki:k ≠ ih✝¹:¬a k = b kh✝:¬a i = b ihrec:↑(mismatchCount k (Function.update a i !a i) b) = ↑(mismatchCount k a b) + -1⊢ ↑(mismatchCount k (Function.update a i !a i) b + 1) = ↑(mismatchCount k a b + 1) + -1 omegaAll goals completed! 🐙

A flip of the other stream has the same displacement rule.

theorem mismatchCount_flip_right (width i : ℕ) (a b : ℕ → Bool) (h : i < width) :
    (mismatchCount width a (flipAt b i) : ℤ) =
      (mismatchCount width a b : ℤ) + if a i = b i then 1 else -1 := bywidth:ℕi:ℕa:ℕ → Boolb:ℕ → Boolh:i < width⊢ ↑(mismatchCount width a (flipAt b i)) = ↑(mismatchCount width a b) + if a i = b i then 1 else -1
  rw [mismatchCount_comm width a (flipAt b i),width:ℕi:ℕa:ℕ → Boolb:ℕ → Boolh:i < width⊢ ↑(mismatchCount width (flipAt b i) a) = ↑(mismatchCount width a b) + if a i = b i then 1 else -1 mismatchCount_flip_left width i b a h,width:ℕi:ℕa:ℕ → Boolb:ℕ → Boolh:i < width⊢ (↑(mismatchCount width b a) + if b i = a i then 1 else -1) = ↑(mismatchCount width a b) + if a i = b i then 1 else -1
    mismatchCount_comm width b awidth:ℕi:ℕa:ℕ → Boolb:ℕ → Boolh:i < width⊢ (↑(mismatchCount width a b) + if b i = a i then 1 else -1) = ↑(mismatchCount width a b) + if a i = b i then 1 else -1]width:ℕi:ℕa:ℕ → Boolb:ℕ → Boolh:i < width⊢ (↑(mismatchCount width a b) + if b i = a i then 1 else -1) = ↑(mismatchCount width a b) + if a i = b i then 1 else -1
  simp only [eq_comm]All goals completed! 🐙

Equality of bit streams below the width is equivalent to a zero count.

theorem mismatchCount_eq_zero (width : ℕ) (a b : ℕ → Bool) :
    mismatchCount width a b = 0 ↔ ∀ i < width, a i = b i := bywidth:ℕa:ℕ → Boolb:ℕ → Bool⊢ mismatchCount width a b = 0 ↔ ∀ (i : ℕ), i < width → a i = b i
  apply Nat.rec (motive := fun width ↦
    mismatchCount width a b = 0 ↔ ∀ i < width, a i = b i) ?_ ?_ widthwidth:ℕa:ℕ → Boolb:ℕ → Bool⊢ mismatchCount Nat.zero a b = 0 ↔ ∀ (i : ℕ), i < Nat.zero → a i = b iwidth:ℕa:ℕ → Boolb:ℕ → Bool⊢ ∀ (n : ℕ),
  (mismatchCount n a b = 0 ↔ ∀ (i : ℕ), i < n → a i = b i) →
    (mismatchCount n.succ a b = 0 ↔ ∀ (i : ℕ), i < n.succ → a i = b i)
  ·width:ℕa:ℕ → Boolb:ℕ → Bool⊢ mismatchCount Nat.zero a b = 0 ↔ ∀ (i : ℕ), i < Nat.zero → a i = b i simp [mismatchCount]All goals completed! 🐙
  ·width:ℕa:ℕ → Boolb:ℕ → Bool⊢ ∀ (n : ℕ),
  (mismatchCount n a b = 0 ↔ ∀ (i : ℕ), i < n → a i = b i) →
    (mismatchCount n.succ a b = 0 ↔ ∀ (i : ℕ), i < n.succ → a i = b i) intro k ihwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b i⊢ mismatchCount k.succ a b = 0 ↔ ∀ (i : ℕ), i < k.succ → a i = b i
    rw [mismatchCount_succwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b i⊢ (mismatchCount k a b + if a k = b k then 0 else 1) = 0 ↔ ∀ (i : ℕ), i < k.succ → a i = b i]width:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b i⊢ (mismatchCount k a b + if a k = b k then 0 else 1) = 0 ↔ ∀ (i : ℕ), i < k.succ → a i = b i
    constructormpwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b i⊢ (mismatchCount k a b + if a k = b k then 0 else 1) = 0 → ∀ (i : ℕ), i < k.succ → a i = b imprwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b i⊢ (∀ (i : ℕ), i < k.succ → a i = b i) → (mismatchCount k a b + if a k = b k then 0 else 1) = 0
    ·mpwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b i⊢ (mismatchCount k a b + if a k = b k then 0 else 1) = 0 → ∀ (i : ℕ), i < k.succ → a i = b i intro h i himpwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b ih:(mismatchCount k a b + if a k = b k then 0 else 1) = 0i:ℕhi:i < k.succ⊢ a i = b i
      have hk : a k = b k := bywidth:ℕa:ℕ → Boolb:ℕ → Bool⊢ mismatchCount width a b = 0 ↔ ∀ (i : ℕ), i < width → a i = b i
        split_ifs at hposwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b ii:ℕhi:i < k.succh✝:a k = b kh:mismatchCount k a b + 0 = 0⊢ a k = b k
        omegampwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b ih:(mismatchCount k a b + if a k = b k then 0 else 1) = 0i:ℕhi:i < k.succhk:a k = b k⊢ a i = b i
      have hprev : mismatchCount k a b = 0 := bywidth:ℕa:ℕ → Boolb:ℕ → Bool⊢ mismatchCount width a b = 0 ↔ ∀ (i : ℕ), i < width → a i = b i omegampwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b ih:(mismatchCount k a b + if a k = b k then 0 else 1) = 0i:ℕhi:i < k.succhk:a k = b khprev:mismatchCount k a b = 0⊢ a i = b i
      by_cases hik : i < kposwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b ih:(mismatchCount k a b + if a k = b k then 0 else 1) = 0i:ℕhi:i < k.succhk:a k = b khprev:mismatchCount k a b = 0hik:i < k⊢ a i = b inegwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b ih:(mismatchCount k a b + if a k = b k then 0 else 1) = 0i:ℕhi:i < k.succhk:a k = b khprev:mismatchCount k a b = 0hik:¬i < k⊢ a i = b i
      ·poswidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b ih:(mismatchCount k a b + if a k = b k then 0 else 1) = 0i:ℕhi:i < k.succhk:a k = b khprev:mismatchCount k a b = 0hik:i < k⊢ a i = b i exact ih.mp hprev i hikAll goals completed! 🐙
      ·negwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b ih:(mismatchCount k a b + if a k = b k then 0 else 1) = 0i:ℕhi:i < k.succhk:a k = b khprev:mismatchCount k a b = 0hik:¬i < k⊢ a i = b i have he : i = k := bywidth:ℕa:ℕ → Boolb:ℕ → Bool⊢ mismatchCount width a b = 0 ↔ ∀ (i : ℕ), i < width → a i = b i omeganegwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b ih:(mismatchCount k a b + if a k = b k then 0 else 1) = 0i:ℕhi:i < k.succhk:a k = b khprev:mismatchCount k a b = 0hik:¬i < khe:i = k⊢ a i = b i
        simpa [he] using hkAll goals completed! 🐙
    ·mprwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b i⊢ (∀ (i : ℕ), i < k.succ → a i = b i) → (mismatchCount k a b + if a k = b k then 0 else 1) = 0 intro hmprwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b ih:∀ (i : ℕ), i < k.succ → a i = b i⊢ (mismatchCount k a b + if a k = b k then 0 else 1) = 0
      have hk := h k (bywidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b ih:∀ (i : ℕ), i < k.succ → a i = b i⊢ k < k.succ omegaAll goals completed! 🐙)mprwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b ih:∀ (i : ℕ), i < k.succ → a i = b ihk:a k = b k⊢ (mismatchCount k a b + if a k = b k then 0 else 1) = 0
      have hprev := ih.mpr (fun i hi ↦ h i (bywidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b ih:∀ (i : ℕ), i < k.succ → a i = b ihk:a k = b ki:ℕhi:i < k⊢ i < k.succ omegaAll goals completed! 🐙))mprwidth:ℕa:ℕ → Boolb:ℕ → Boolk:ℕih:mismatchCount k a b = 0 ↔ ∀ (i : ℕ), i < k → a i = b ih:∀ (i : ℕ), i < k.succ → a i = b ihk:a k = b khprev:mismatchCount k a b = 0⊢ (mismatchCount k a b + if a k = b k then 0 else 1) = 0
      simp [hk, hprev]All goals completed! 🐙

If the streams agree beyond the width, their bounded count detects their equality.

theorem mismatchCount_eq_zero_iff_eq (width : ℕ) (a b : ℕ → Bool)
    (h : ∀ i, width ≤ i → a i = b i) : mismatchCount width a b = 0 ↔ a = b := bywidth:ℕa:ℕ → Boolb:ℕ → Boolh:∀ (i : ℕ), width ≤ i → a i = b i⊢ mismatchCount width a b = 0 ↔ a = b
  rw [mismatchCount_eq_zerowidth:ℕa:ℕ → Boolb:ℕ → Boolh:∀ (i : ℕ), width ≤ i → a i = b i⊢ (∀ (i : ℕ), i < width → a i = b i) ↔ a = b]width:ℕa:ℕ → Boolb:ℕ → Boolh:∀ (i : ℕ), width ≤ i → a i = b i⊢ (∀ (i : ℕ), i < width → a i = b i) ↔ a = b
  constructormpwidth:ℕa:ℕ → Boolb:ℕ → Boolh:∀ (i : ℕ), width ≤ i → a i = b i⊢ (∀ (i : ℕ), i < width → a i = b i) → a = bmprwidth:ℕa:ℕ → Boolb:ℕ → Boolh:∀ (i : ℕ), width ≤ i → a i = b i⊢ a = b → ∀ (i : ℕ), i < width → a i = b i
  ·mpwidth:ℕa:ℕ → Boolb:ℕ → Boolh:∀ (i : ℕ), width ≤ i → a i = b i⊢ (∀ (i : ℕ), i < width → a i = b i) → a = b intro hsmallmpwidth:ℕa:ℕ → Boolb:ℕ → Boolh:∀ (i : ℕ), width ≤ i → a i = b ihsmall:∀ (i : ℕ), i < width → a i = b i⊢ a = b
    funext impwidth:ℕa:ℕ → Boolb:ℕ → Boolh:∀ (i : ℕ), width ≤ i → a i = b ihsmall:∀ (i : ℕ), i < width → a i = b ii:ℕ⊢ a i = b i
    by_cases hi : i < widthposwidth:ℕa:ℕ → Boolb:ℕ → Boolh:∀ (i : ℕ), width ≤ i → a i = b ihsmall:∀ (i : ℕ), i < width → a i = b ii:ℕhi:i < width⊢ a i = b inegwidth:ℕa:ℕ → Boolb:ℕ → Boolh:∀ (i : ℕ), width ≤ i → a i = b ihsmall:∀ (i : ℕ), i < width → a i = b ii:ℕhi:¬i < width⊢ a i = b i
    ·poswidth:ℕa:ℕ → Boolb:ℕ → Boolh:∀ (i : ℕ), width ≤ i → a i = b ihsmall:∀ (i : ℕ), i < width → a i = b ii:ℕhi:i < width⊢ a i = b i exact hsmall i hiAll goals completed! 🐙
    ·negwidth:ℕa:ℕ → Boolb:ℕ → Boolh:∀ (i : ℕ), width ≤ i → a i = b ihsmall:∀ (i : ℕ), i < width → a i = b ii:ℕhi:¬i < width⊢ a i = b i exact h i (bywidth:ℕa:ℕ → Boolb:ℕ → Boolh:∀ (i : ℕ), width ≤ i → a i = b ihsmall:∀ (i : ℕ), i < width → a i = b ii:ℕhi:¬i < width⊢ width ≤ i omegaAll goals completed! 🐙)
  ·mprwidth:ℕa:ℕ → Boolb:ℕ → Boolh:∀ (i : ℕ), width ≤ i → a i = b i⊢ a = b → ∀ (i : ℕ), i < width → a i = b i intro he i _mprwidth:ℕa:ℕ → Boolb:ℕ → Boolh:∀ (i : ℕ), width ≤ i → a i = b ihe:a = bi:ℕa✝:i < width⊢ a i = b i
    exact congrFun he iAll goals completed! 🐙

end Geb.BitTree.BinaryMachine