English
An induction principle for the reduction process on Δ m: to prove C(A) for all A, it suffices to prove it for the base via reduce_mem_reps and closure under S and T moves.
Русский
Принцип индукции по процессе редукции на Δ m: чтобы доказать C(A) для всех A, достаточно показать для базового случая через reduce_mem_reps и замкнутость по переходам под S и T.
LaTeX
$$$\text{induction_on} : \text{(Corresp)}$$$
Lean4
@[elab_as_elim]
theorem induction_on {C : Δ m → Prop} {A : Δ m} (hm : m ≠ 0)
(h0 : ∀ A : Δ m, A.1 1 0 = 0 → 0 < A.1 0 0 → 0 ≤ A.1 0 1 → |(A.1 0 1)| < |(A.1 1 1)| → C A)
(hS : ∀ B, C B → C (S • B)) (hT : ∀ B, C B → C (T • B)) : C A :=
by
have h_reduce : C (reduce A) := by
rcases reduce_mem_reps hm A with ⟨H1, H2, H3, H4⟩
exact h0 _ H1 H2 H3 H4
suffices ∀ A : Δ m, C (reduce A) → C A from this _ h_reduce
apply reduce_rec
· intro A h
by_cases h1 : 0 < A.1 0 0
· simp only [reduce_of_pos h h1, prop_red_T_pow hS hT, imp_self]
· simp only [reduce_of_not_pos h h1, prop_red_T_pow hS hT, prop_red_S hS, imp_self]
intro A hc ih hA
rw [← reduce_reduceStep hc] at hA
simpa only [reduceStep, prop_red_S hS, prop_red_T_pow hS hT] using ih hA
