mem_Cylinder_zero

formal source

  30def Cylinder {n : Nat} (w : Pattern n) : Set Stream :=
  31  { s | ∀ i : Fin n, s i.val = w i }
  32
  33@[simp] lemma mem_Cylinder_zero (w : Pattern 0) (s : Stream) : s ∈ Cylinder w := by
  34  intro i; exact (Fin.elim0 i)
  35
  36@[simp] lemma Cylinder_zero (w : Pattern 0) : Cylinder w = Set.univ := by
  37  ext s; constructor
  38  · intro _; exact Set.mem_univ _
  39  · intro _; exact (mem_Cylinder_zero w s)
  40
  41/-- Periodic extension of an 8‑bit window. -/
  42def extendPeriodic8 (w : Pattern 8) : Stream := fun t =>
  43  let h8 : 0 < 8 := by decide
  44  let i : Fin 8 := ⟨t % 8, Nat.mod_lt _ h8⟩
  45  w i
  46
  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