snocBit

formal source

  31
  32/-- Append a fresh *last* coordinate `b` to a pattern `p : Pattern d`, yielding a pattern in
  33dimension `d+1`. -/
  34def snocBit {d : Nat} (p : Pattern d) (b : Bool) : Pattern (d + 1) :=
  35  fun j => Fin.lastCases b (fun k => p k) j
  36
  37@[simp] lemma snocBit_castSucc {d : Nat} (p : Pattern d) (b : Bool) (k : Fin d) :
  38    snocBit p b k.castSucc = p k := by
  39  simp [snocBit]
  40
  41@[simp] lemma snocBit_last {d : Nat} (p : Pattern d) (b : Bool) :
  42    snocBit p b (Fin.last d) = b := by
  43  simp [snocBit]
  44
  45/-! ## The recursive BRGC path -/
  46
  47private lemma twoPow_succ_eq_add (d : Nat) : 2 ^ (d + 1) = 2 ^ d + 2 ^ d := by
  48  -- `2^(d+1) = 2^d * 2 = 2 * 2^d = 2^d + 2^d`
  49  simpa [pow_succ, Nat.mul_comm, Nat.two_mul]
  50
  51/-- The recursive BRGC path as a `Fin (2^d) → Pattern d`. -/
  52def brgcPath : (d : Nat) → Fin (2 ^ d) → Pattern d
  53  | 0, _ =>
  54      -- unique 0-bit pattern
  55      fun _ => False
  56  | (d + 1), i =>
  57      let T : Nat := 2 ^ d
  58      let hTT : 2 ^ (d + 1) = T + T := by
  59        simpa [T, twoPow_succ_eq_add d]
  60      let i' : Fin (T + T) := i.cast hTT
  61      let left : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d k) false
  62      let right : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d (Fin.rev k)) true
  63      Fin.append left right i'
  64