feat(model_theory/syntax, semantics): Substitution of variables in te…

…rms and formulas (#13632)

Defines `first_order.language.term.subst` and `first_order.language.bounded_formula.subst`, which substitute free variables in terms and formulas with terms.

src/model_theory/semantics.lean

@@ -27,8 +27,8 @@ sentence of `T` is realized in `M`. Also denoted `T ⊨ φ`.
 * `first_order.language.bounded_formula.realize_to_prenex` shows that the prenex normal form of a
 formula has the same realization as the original formula.
 * Several results in this file show that syntactic constructions such as `relabel`, `cast_le`,
-`lift_at`, and the actions of language maps commute with realization of terms, formulas, sentences,
-and theories.
+`lift_at`, `subst`, and the actions of language maps commute with realization of terms, formulas,
+sentences, and theories.
 
 ## Implementation Notes
 * Formulas use a modified version of de Bruijn variables. Specifically, a `L.bounded_formula α n`
@@ -103,6 +103,14 @@ end
 lemma realize_con {A : set M} {a : A} {v : α → M} :
   (L.con a).term.realize v = a := rfl
 
+@[simp] lemma realize_subst {t : L.term α} {tf : α → L.term β} {v : β → M} :
+  (t.subst tf).realize v = t.realize (λ a, (tf a).realize v) :=
+begin
+  induction t with _ _ _ _ ih,
+  { refl },
+  { simp [ih] }
+end
+
 end term
 
 namespace Lhom
@@ -323,7 +331,26 @@ begin
   rw [if_pos i.is_lt],
 end
 
-lemma realize_all_lift_at_one_self [nonempty M] {n : ℕ} {φ : L.bounded_formula α n}
+@[simp] lemma realize_subst_aux {tf : α → L.term β} {v : β → M} {xs : fin n → M} :
+  (λ x, term.realize (sum.elim v xs) (sum.elim (term.relabel sum.inl ∘ tf) (var ∘ sum.inr) x)) =
+    sum.elim (λ (a : α), term.realize v (tf a)) xs :=
+funext (λ x, sum.cases_on x (λ x,
+  by simp only [sum.elim_inl, term.realize_relabel, sum.elim_comp_inl]) (λ x, rfl))
+
+lemma realize_subst {φ : L.bounded_formula α n} {tf : α → L.term β} {v : β → M} {xs : fin n → M} :
+  (φ.subst tf).realize v xs ↔ φ.realize (λ a, (tf a).realize v) xs :=
+begin
+  induction φ with _ _ _ _ _ _ _ _ _ _ _ ih1 ih2 _ _ ih,
+  { refl },
+  { simp only [subst, bounded_formula.realize, realize_subst, realize_subst_aux] },
+  { simp only [subst, bounded_formula.realize, realize_subst, realize_subst_aux] },
+  { simp only [subst, realize_imp, ih1, ih2] },
+  { simp only [ih, subst, realize_all] }
+end
+
+variables [nonempty M]
+
+lemma realize_all_lift_at_one_self {n : ℕ} {φ : L.bounded_formula α n}
   {v : α → M} {xs : fin n → M} :
   (φ.lift_at 1 n).all.realize v xs ↔ φ.realize v xs :=
 begin
@@ -336,8 +363,6 @@ begin
     simp }
 end
 
-variables [nonempty M]
-
 lemma realize_to_prenex_imp_right {φ ψ : L.bounded_formula α n}
   (hφ : is_qf φ) (hψ : is_prenex ψ) {v : α → M} {xs : fin n → M} :
   (φ.to_prenex_imp_right ψ).realize v xs ↔ (φ.imp ψ).realize v xs :=

src/model_theory/syntax.lean

@@ -24,6 +24,8 @@ This file defines first-order terms, formulas, sentences, and theories in a styl
 * `first_order.language.bounded_formula.cast_le` adds more `fin`-indexed variables.
 * `first_order.language.bounded_formula.lift_at` raises the indexes of the `fin`-indexed variables
 above a particular index.
+* `first_order.language.term.subst` and `first_order.language.bounded_formula.subst` substitute
+variables with given terms.
 * Language maps can act on syntactic objects with functions such as
 `first_order.language.Lhom.on_formula`.
 
@@ -96,6 +98,11 @@ instance inhabited_of_constant [inhabited L.constants] : inhabited (L.term α) :
 def lift_at {n : ℕ} (n' m : ℕ) : L.term (α ⊕ fin n) → L.term (α ⊕ fin (n + n')) :=
 relabel (sum.map id (λ i, if ↑i < m then fin.cast_add n' i else fin.add_nat n' i))
 
+/-- Substitutes the variables in a given term with terms. -/
+@[simp] def subst : L.term α → (α → L.term β) → L.term β
+| (var a) tf := tf a
+| (func f ts) tf := (func f (λ i, (ts i).subst tf))
+
 end term
 
 localized "prefix `&`:max := first_order.language.term.var ∘ sum.inr" in first_order
@@ -272,6 +279,16 @@ def lift_at : ∀ {n : ℕ} (n' m : ℕ), L.bounded_formula α n → L.bounded_f
 | n n' m (imp f₁ f₂) := (f₁.lift_at n' m).imp (f₂.lift_at n' m)
 | n n' m (all f) := ((f.lift_at n' m).cast_le (by rw [add_assoc, add_comm 1, ← add_assoc])).all
 
+/-- Substitutes the variables in a given formula with terms. -/
+@[simp] def subst : ∀ {n : ℕ}, L.bounded_formula α n → (α → L.term β) → L.bounded_formula β n
+| n falsum tf := falsum
+| n (equal t₁ t₂) tf := equal (t₁.subst (sum.elim (term.relabel sum.inl ∘ tf) (var ∘ sum.inr)))
+  (t₂.subst (sum.elim (term.relabel sum.inl ∘ tf) (var ∘ sum.inr)))
+| n (rel R ts) tf := rel R
+  (λ i, (ts i).subst (sum.elim (term.relabel sum.inl ∘ tf) (var ∘ sum.inr)))
+| n (imp φ₁ φ₂) tf := (φ₁.subst tf).imp (φ₂.subst tf)
+| n (all φ) tf := (φ.subst tf).all
+
 variables {l : ℕ} {φ ψ : L.bounded_formula α l} {θ : L.bounded_formula α l.succ}
 variables {v : α → M} {xs : fin l → M}