Lean4
@[simp]
theorem listDecode_encode_list (l : List (Σ n, L.BoundedFormula α n)) :
listDecode (l.flatMap (fun φ => φ.2.listEncode)) = l :=
by
suffices h :
∀ (φ : Σ n, L.BoundedFormula α n) (l' : List ((Σ k, L.Term (α ⊕ Fin k)) ⊕ ((Σ n, L.Relations n) ⊕ ℕ))),
(listDecode (listEncode φ.2 ++ l')) = φ :: (listDecode l')
by
induction l with
| nil => simp [listDecode]
| cons φ l ih => rw [flatMap_cons, h φ _, ih]
rintro ⟨n, φ⟩
induction φ with
| falsum => intro l; rw [listEncode, singleton_append, listDecode]
| equal =>
intro l
rw [listEncode, cons_append, cons_append, listDecode, dif_pos]
· simp only [eq_mp_eq_cast, cast_eq, nil_append]
· simp only
| @rel φ_n φ_l φ_R ts =>
intro l
rw [listEncode, cons_append, cons_append, singleton_append, cons_append, listDecode]
have h :
∀ i : Fin φ_l,
((List.map Sum.getLeft?
(List.map
(fun i : Fin φ_l =>
Sum.inl (⟨(⟨φ_n, rel φ_R ts⟩ : Σ n, L.BoundedFormula α n).fst, ts i⟩ : Σ n, L.Term (α ⊕ (Fin n))))
(finRange φ_l) ++
l))[↑i]?).join =
some ⟨_, ts i⟩ :=
by
intro i
simp only [Option.join, map_append, map_map, getElem?_fin, id, Option.bind_eq_some_iff, getElem?_eq_some_iff,
length_append, length_map, length_finRange, exists_eq_right]
refine ⟨lt_of_lt_of_le i.2 le_self_add, ?_⟩
rw [getElem_append_left, getElem_map]
· simp only [getElem_finRange, cast_mk, Fin.eta, Function.comp_apply, Sum.getLeft?_inl]
· simp only [length_map, length_finRange, is_lt]
rw [dif_pos]
swap
· exact fun i => Option.isSome_iff_exists.2 ⟨⟨_, ts i⟩, h i⟩
rw [dif_pos]
swap
· intro i
obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i)
rw [h2]
simp only [Option.join, eq_mp_eq_cast, cons.injEq, Sigma.mk.inj_iff, heq_eq_eq, rel.injEq, true_and]
refine ⟨funext fun i => ?_, ?_⟩
· obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i)
rw [cast_eq_iff_heq]
exact (Sigma.ext_iff.1 ((Sigma.eta (Option.get _ h1)).trans h2)).2
rw [List.drop_append, length_map, length_finRange, Nat.sub_self, drop, drop_eq_nil_of_le, nil_append]
rw [length_map, length_finRange]
| imp _ _ ih1 ih2 =>
intro l
simp only [] at *
rw [listEncode, List.append_assoc, cons_append, listDecode]
simp only [ih1, ih2, length_cons, le_add_iff_nonneg_left, _root_.zero_le, ↓reduceDIte, getElem_cons_zero,
getElem_cons_succ, sigmaImp_apply, drop_succ_cons, drop_zero]
| all _ ih =>
intro l
simp only [] at *
rw [listEncode, cons_append, listDecode]
simp only [ih, length_cons, le_add_iff_nonneg_left, _root_.zero_le, ↓reduceDIte, getElem_cons_zero, sigmaAll_apply,
drop_succ_cons, drop_zero]
