zeroes_and_ones.lean

import logic.function.iterate
import tactic

def h : (ℕ → bool) → bool × (ℕ → bool) :=
λ s, (s 0, s ∘ nat.succ)

variables {X : Type} (f : X → bool × X)

def UMP (x : X) (n : ℕ) : bool :=
(f ((prod.snd ∘ f)^[n] x)).1

lemma commutes (x : X) : h (UMP f x) = ((f x).1, (UMP f (f x).2)) :=
begin
  ext,
  { simp [h, UMP] },
  { simp [h, UMP] }
end

lemma uniqueness (W : X → (ℕ → bool)) (hW : ∀ x, h (W x) = ((f x).1, (W (f x).2))) (x : X) : 
  W x = UMP f x :=
begin
  ext n,
  unfold UMP h at *,
  simp only [prod.ext_iff, function.funext_iff, function.comp_apply] at hW,
  induction n with n ih generalizing x,
  { simp [(hW x).1], },
  { simp [(hW x).2, ih] }
end