extendPeriodic8_eq_mod

formal source

  47@[simp] lemma extendPeriodic8_zero (w : Pattern 8) : extendPeriodic8 w 0 = w ⟨0, by decide⟩ := by
  48  simp [extendPeriodic8]
  49
  50@[simp] lemma extendPeriodic8_eq_mod (w : Pattern 8) (t : Nat) :
  51  extendPeriodic8 w t = w ⟨t % 8, Nat.mod_lt _ (by decide)⟩ := by
  52  rfl
  53
  54lemma extendPeriodic8_period (w : Pattern 8) (t : Nat) :
  55  extendPeriodic8 w (t + 8) = extendPeriodic8 w t := by
  56  dsimp [extendPeriodic8]
  57  have hmod : (t + 8) % 8 = t % 8 := by
  58    rw [Nat.add_mod]
  59    simp
  60  have h8 : 0 < 8 := by decide
  61  have hfin : (⟨(t + 8) % 8, Nat.mod_lt _ h8⟩ : Fin 8)
  62            = ⟨t % 8, Nat.mod_lt _ h8⟩ := by
  63    apply Fin.mk_eq_mk.mpr
  64    exact hmod
  65  rw [hfin]
  66
  67/-- Sum of the first `m` bits of a stream. -/
  68def sumFirst (m : Nat) (s : Stream) : Nat :=
  69  ∑ i : Fin m, (if s i.val then 1 else 0)
  70
  71/-- Base case: the sum of the first 0 bits is 0. -/
  72@[simp] lemma sumFirst_zero (s : Stream) : sumFirst 0 s = 0 := by
  73  simp [sumFirst]
  74
  75/-- If a stream agrees with a window on its first `n` bits, then the first‑`n` sum equals `Z`. -/
  76lemma sumFirst_eq_Z_on_cylinder {n : Nat} (w : Pattern n)
  77  {s : Stream} (hs : s ∈ Cylinder w) :
  78  sumFirst n s = Z_of_window w := by
  79  unfold sumFirst Z_of_window Cylinder at *
  80  have : (fun i : Fin n => (if s i.val then 1 else 0)) =