English
For any φ, the Realize of φ.toFormula corresponds to Realize of φ after appropriate relabeling and decomposition.
Русский
Для любой φ реализация φ.toFormula соответствует реализации φ после соответствующего переназначения и разложения.
LaTeX
$$$\text{realize_toFormula}(\varphi, v) \iff \text{Realize}_{toFormula}(v, \varphi)$$$
Lean4
@[simp]
theorem realize_toFormula (φ : L.BoundedFormula α n) (v : α ⊕ (Fin n) → M) :
φ.toFormula.Realize v ↔ φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) := by
induction φ with
| falsum => rfl
| equal => simp [BoundedFormula.Realize]
| rel => simp [BoundedFormula.Realize]
| imp _ _ ih1 ih2 =>
rw [toFormula, Formula.Realize, realize_imp, ← Formula.Realize, ih1, ← Formula.Realize, ih2, realize_imp]
| all _ ih3 =>
rw [toFormula, Formula.Realize, realize_all, realize_all]
refine forall_congr' fun a => ?_
have h := ih3 (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a))
simp only [Sum.elim_comp_inl, Sum.elim_comp_inr] at h
rw [← h, realize_relabel, Formula.Realize, iff_iff_eq]
simp only [Function.comp_def]
congr with x
· rcases x with _ | x
· simp
· refine Fin.lastCases ?_ ?_ x
· simp [Fin.snoc]
· simp only [castSucc, Sum.elim_inr, finSumFinEquiv_symm_apply_castAdd, Sum.map_inl, Sum.elim_inl]
rw [← castSucc]
simp
· exact Fin.elim0 x
