English
Transform a bounded formula by turning all in-scope bound variables into free variables, producing a formula with free variables α ⊕ Fin n. The recursion handles falsum, equality, relation, implication, and universal quantification accordingly.
Русский
Преобразование ограниченной формулы: все связанные переменные становятся свободными, формула имеет свободные переменные α ⊕ Fin n; разбор по случаям: falsum, равенство, отношение, импликация, все.
LaTeX
$$$\\text{toFormula}(\\lambda n. \\phi) = \\begin{cases} \\text{falsum}, & \\phi = \\text{falsum} \\\\ \\phi_1.\\text{equal} \\; t_1 t_2, & \\phi = \\text{equal } t_1 t_2 \\\\ \\phi.\\text{rel } R ts, & \\phi = \\text{rel } R ts \\\\ \\text{...} \end{cases}$$$
Lean4
/-- Turns all the in-scope bound variables into free variables. -/
@[simp]
def toFormula : ∀ {n : ℕ}, L.BoundedFormula α n → L.Formula (α ⊕ (Fin n))
| _n, falsum => falsum
| _n, equal t₁ t₂ => t₁.equal t₂
| _n, rel R ts => R.formula ts
| _n, imp φ₁ φ₂ => φ₁.toFormula.imp φ₂.toFormula
| _n, all φ => (φ.toFormula.relabel (Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ finSumFinEquiv.symm))).all
