English
Lifting the index of a bounded formula (liftAt n' m) yields Realize equivalent to the Realize of φ with xs modified by a specified piecewise function that depends on m and n'.
Русский
Поднятие индекса ограниченной формулы (liftAt n' m) даёт эквивалентность Реализации к Реализации φ с xs, модифицированным по заданной кусочной функции.
LaTeX
$$$ (\phi.liftAt n' m).Realize v xs \iff \phi.Realize v \big( xs \circ \big( \lambda i. \text{if } i < m \text{ then } \text{Fin.castAdd } n' i \; \text{else } i.addNat n'\big) \big) $$$
Lean4
theorem realize_liftAt {n n' m : ℕ} {φ : L.BoundedFormula α n} {v : α → M} {xs : Fin (n + n') → M}
(hmn : m + n' ≤ n + 1) :
(φ.liftAt n' m).Realize v xs ↔ φ.Realize v (xs ∘ fun i => if ↑i < m then Fin.castAdd n' i else Fin.addNat i n') :=
by
rw [liftAt]
induction φ with
| falsum => simp [mapTermRel, Realize]
| equal => simp [mapTermRel, Realize, Sum.elim_comp_map]
| rel => simp [mapTermRel, Realize, Sum.elim_comp_map]
| imp _ _ ih1 ih2 => simp only [mapTermRel, Realize, ih1 hmn, ih2 hmn]
| @all k _ ih3 =>
have h : k + 1 + n' = k + n' + 1 := by rw [add_assoc, add_comm 1 n', ← add_assoc]
simp only [mapTermRel, Realize, realize_castLE_of_eq h, ih3 (hmn.trans k.succ.le_succ)]
refine forall_congr' fun x => iff_eq_eq.mpr (congr rfl (funext (Fin.lastCases ?_ fun i => ?_)))
· simp only [Function.comp_apply, val_last, snoc_last]
refine (congr rfl (Fin.ext ?_)).trans (snoc_last _ _)
split_ifs <;> dsimp; cutsat
· simp only [Function.comp_apply, Fin.snoc_castSucc]
refine (congr rfl (Fin.ext ?_)).trans (snoc_castSucc _ _ _)
simp only [coe_castSucc, coe_cast]
split_ifs <;> simp
