English
A further variant of the induction framework for RelSeries, extending induction to more elaborate constructors.
Русский
Другая вариация индукции по RelSeries, расширяющая конструкторы.
LaTeX
$$InductionOn'' (motive) ...$$
Lean4
/-- Given two series of the form `a₀ -r→ ... -r→ X` and `X -r→ b ---> ...`,
then `a₀ -r→ ... -r→ X -r→ b ...` is another series obtained by combining the given two.
-/
@[simps length]
def smash (p q : RelSeries r) (connect : p.last = q.head) : RelSeries r
where
length := p.length + q.length
toFun := Fin.addCases (m := p.length) (n := q.length + 1) (p ∘ Fin.castSucc) q
step := by
apply Fin.addCases <;> intro i
· simp_rw [Fin.castSucc_castAdd, Fin.addCases_left, Fin.succ_castAdd]
convert p.step i
split_ifs with h
· rw [Fin.addCases_right, h, ← last, connect, head]
· apply Fin.addCases_left
simpa only [Fin.castSucc_natAdd, Fin.succ_natAdd, Fin.addCases_right] using q.step i
