English
Decode(listEncode(l)) recovers l after encoding.
Русский
Декодирование после кодирования восстанавливает исходный список.
LaTeX
$$$\text{listDecode}(\text{List.flatMap }\text{listEncode } l) = l$$$
Lean4
theorem listDecode_encode_list (l : List (L.Term α)) : listDecode (l.flatMap listEncode) = l :=
by
suffices h :
∀ (t : L.Term α) (l : List (α ⊕ (Σ i, L.Functions i))), listDecode (t.listEncode ++ l) = t :: listDecode l by
induction l with
| nil => rfl
| cons t l lih => rw [flatMap_cons, h t (l.flatMap listEncode), lih]
intro t l
induction t generalizing l with
| var => rw [listEncode, singleton_append, listDecode]
| @func n f ts ih =>
rw [listEncode, cons_append, listDecode]
have h :
listDecode (((finRange n).flatMap fun i : Fin n => (ts i).listEncode) ++ l) =
(finRange n).map ts ++ listDecode l :=
by
induction finRange n with
| nil => rfl
| cons i l' l'ih => rw [flatMap_cons, List.append_assoc, ih, map_cons, l'ih, cons_append]
simp only [h, length_append, length_map, length_finRange, le_add_iff_nonneg_right, _root_.zero_le, ↓reduceDIte,
getElem_fin, cons.injEq, func.injEq, heq_eq_eq, true_and]
refine ⟨funext (fun i => ?_), ?_⟩
·
simp only [length_map, length_finRange, is_lt, getElem_append_left, getElem_map, getElem_finRange, cast_mk,
Fin.eta]
· simp only [length_map, length_finRange, drop_left']
