IndisputableMonolith.Verification.Necessity.FibSubst

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Verification
   5namespace Necessity
   6namespace FibSubst
   7
   8/-! 2-letter substitution system yielding Fibonacci recurrences on counts. -/
   9
  10abbrev Word := List Bool
  11
  12/-- The Fibonacci sequence: F(0)=0, F(1)=1, F(n+2)=F(n+1)+F(n) -/
  13def fib : ℕ → ℕ
  14  | 0 => 0
  15  | 1 => 1
  16  | n + 2 => fib (n + 1) + fib n
  17
  18/-- Fibonacci substitution on a single symbol. -/
  19def fibSub : Bool → Word
  20  | false => [false, true]
  21  | true  => [false]
  22
  23/-- Extend substitution to words by concatenation. -/
  24def fibSubWord (w : Word) : Word := w.flatMap fibSub
  25
  26/-- Count of `false` symbols in a word. -/
  27def countFalse : Word → Nat
  28  | []        => 0
  29  | b :: bs   => (if b = false then 1 else 0) + countFalse bs
  30
  31/-- Count of `true` symbols in a word. -/
  32def countTrue : Word → Nat
  33  | []        => 0
  34  | b :: bs   => (if b = true then 1 else 0) + countTrue bs
  35
  36@[simp] lemma countFalse_nil : countFalse ([] : Word) = 0 := rfl
  37@[simp] lemma countTrue_nil : countTrue ([] : Word) = 0 := rfl
  38
  39@[simp] lemma countFalse_cons_false (w : Word) :
  40  countFalse (false :: w) = countFalse w + 1 := by
  41  simp [countFalse, Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
  42
  43@[simp] lemma countFalse_cons_true (w : Word) :
  44  countFalse (true :: w) = countFalse w := by
  45  simp [countFalse]
  46
  47@[simp] lemma countTrue_cons_false (w : Word) :
  48  countTrue (false :: w) = countTrue w := by
  49  simp [countTrue]
  50
  51@[simp] lemma countTrue_cons_true (w : Word) :
  52  countTrue (true :: w) = countTrue w + 1 := by
  53  simp [countTrue, Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
  54
  55lemma countFalse_append (w₁ w₂ : Word) :
  56  countFalse (w₁ ++ w₂) = countFalse w₁ + countFalse w₂ := by
  57  induction w₁ with
  58  | nil => simp
  59  | cons b bs ih =>
  60      cases b
  61      · simp [ih, Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
  62      · simp [ih]
  63
  64lemma countTrue_append (w₁ w₂ : Word) :
  65  countTrue (w₁ ++ w₂) = countTrue w₁ + countTrue w₂ := by
  66  induction w₁ with
  67  | nil => simp
  68  | cons b bs ih =>
  69      cases b
  70      · simp [ih]
  71      · simp [ih, Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
  72
  73/-- Counts for substituted single symbols. -/
  74lemma counts_sub_false :
  75  countFalse (fibSub false) = 1 ∧ countTrue (fibSub false) = 1 := by
  76  simp [fibSub]
  77
  78lemma counts_sub_true :
  79  countFalse (fibSub true) = 1 ∧ countTrue (fibSub true) = 0 := by
  80  simp [fibSub]
  81
  82/-- Counts for substituted words decompose additively. -/
  83lemma counts_sub_word (w : Word) :
  84  countFalse (fibSubWord w) = countFalse w + countTrue w ∧
  85  countTrue (fibSubWord w) = countFalse w := by
  86  induction w with
  87  | nil => simp [fibSubWord]
  88  | cons b bs ih =>
  89      cases ih with
  90      | _ ihF ihT =>
  91        cases b
  92        · -- b = false
  93          have : fibSubWord (false :: bs) = fibSub false ++ fibSubWord bs := by
  94            simp [fibSubWord, List.flatMap]
  95          have hF : countFalse (fibSub false) = 1 := (counts_sub_false).1
  96          have hT : countTrue (fibSub false) = 1 := (counts_sub_false).2
  97          simp [this, countFalse_append, countTrue_append, ihF, ihT, hF, hT, countFalse_cons_false, countTrue_cons_false, Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
  98        · -- b = true
  99          have : fibSubWord (true :: bs) = fibSub true ++ fibSubWord bs := by
 100            simp [fibSubWord, List.flatMap]
 101          have hF : countFalse (fibSub true) = 1 := (counts_sub_true).1
 102          have hT : countTrue (fibSub true) = 0 := (counts_sub_true).2
 103          simp [this, countFalse_append, countTrue_append, ihF, ihT, hF, hT, countFalse_cons_true, countTrue_cons_true, Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
 104
 105/-- Iterate substitution starting from the seed word `[false]`. -/
 106def iter (n : Nat) : Word := (fibSubWord^[n]) [false]
 107
 108@[simp] lemma counts_iter_succ (n : Nat) :
 109  countFalse (iter (n+1)) = countFalse (iter n) + countTrue (iter n) ∧
 110  countTrue (iter (n+1)) = countFalse (iter n) := by
 111  have h_unfold : iter (n+1) = fibSubWord (iter n) := by
 112    simp [iter, Function.iterate_succ_apply']
 113  rw [h_unfold]
 114  exact counts_sub_word (iter n)
 115
 116/-- Fibonacci recursion on counts: starting from `[false]` we have
 117    counts (false) = (1,0) and recurrence
 118    F_{n+1} = F_n + T_n;  T_{n+1} = F_n. -/
 119lemma counts_iter_fib (n : Nat) :
 120  (countFalse (iter n), countTrue (iter n)) = (fib (n+1), fib n) := by
 121  induction n with
 122  | zero => simp [iter, fib]
 123  | succ n ih =>
 124      rcases counts_iter_succ n with ⟨hF, hT⟩
 125      have ihF : countFalse (iter n) = fib (n + 1) := (congrArg Prod.fst ih)
 126      have ihT : countTrue (iter n) = fib n := (congrArg Prod.snd ih)
 127      ext <;> simp [hF, hT, ihF, ihT, fib]
 128
 129end FibSubst
 130end Necessity
 131end Verification
 132end IndisputableMonolith
 133