English
In the inductive definition, inserting a new element c at the front yields the IH-expressed value with a recursive call on the tail.
Русский
В условии рекурсии добавление нового элемента c в начало списка даёт значение, выраженное IH, с рекурсивным вызовом на хвосте.
LaTeX
$$$ \text{@insertRec } \ H0 \ IH (l.insert c.1 c.2) = IH c.1 c.2 l h ( @insertRec \ α β _ C H0 IH l ) $$$
Lean4
theorem insertRec_insert {C : AList β → Sort*} (H0 : C ∅)
(IH : ∀ (a : α) (b : β a) (l : AList β), a ∉ l → C l → C (l.insert a b)) {c : Sigma β} {l : AList β} (h : c.1 ∉ l) :
@insertRec α β _ C H0 IH (l.insert c.1 c.2) = IH c.1 c.2 l h (@insertRec α β _ C H0 IH l) :=
by
obtain ⟨l, hl⟩ := l
suffices
@insertRec α β _ C H0 IH ⟨c :: l, nodupKeys_cons.2 ⟨h, hl⟩⟩ ≍
IH c.1 c.2 ⟨l, hl⟩ h (@insertRec α β _ C H0 IH ⟨l, hl⟩)
by
cases c
apply eq_of_heq
convert this <;> rw [insert_of_notMem h]
rw [insertRec]
apply cast_heq
