feat(model_theory/syntax): Swapping between constants and variables (#14018)

`term.constants_vars_equiv` and `bounded_formula.constants_vars_equiv` send terms/formulas with constants to terms/formulas with extra variables and back. 



Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

Author: awainverse

src/model_theory/language_map.lean

@@ -27,7 +27,7 @@ the continuum hypothesis*][flypitch_itp]
 
 -/
 
-universes u v u' v' w
+universes u v u' v' w w'
 
 namespace first_order
 namespace language
@@ -179,7 +179,17 @@ class is_expansion_on (M : Type*) [L.Structure M] [L'.Structure M] : Prop :=
 (map_on_relation : ∀ {n} (R : L.relations n) (x : fin n → M),
   rel_map (ϕ.on_relation R) x = rel_map R x)
 
-attribute [simp] is_expansion_on.map_on_function is_expansion_on.map_on_relation
+@[simp] lemma map_on_function {M : Type*}
+  [L.Structure M] [L'.Structure M] [ϕ.is_expansion_on M]
+  {n} (f : L.functions n) (x : fin n → M) :
+  fun_map (ϕ.on_function f) x = fun_map f x :=
+is_expansion_on.map_on_function f x
+
+@[simp] lemma map_on_relation {M : Type*}
+  [L.Structure M] [L'.Structure M] [ϕ.is_expansion_on M]
+  {n} (R : L.relations n) (x : fin n → M) :
+  rel_map (ϕ.on_relation R) x = rel_map R x :=
+is_expansion_on.map_on_relation R x
 
 instance id_is_expansion_on (M : Type*) [L.Structure M] : is_expansion_on (Lhom.id L) M :=
 ⟨λ _ _ _, rfl, λ _ _ _, rfl⟩
@@ -211,6 +221,18 @@ instance sum_inr_is_expansion_on (M : Type*)
   (Lhom.sum_inr : L' →ᴸ L.sum L').is_expansion_on M :=
 ⟨λ _ f _, rfl, λ _ R _, rfl⟩
 
+@[simp] lemma fun_map_sum_inl [(L.sum L').Structure M]
+  [(Lhom.sum_inl : L →ᴸ L.sum L').is_expansion_on M]
+  {n} {f : L.functions n} {x : fin n → M} :
+  @fun_map (L.sum L') M _ n (sum.inl f) x = fun_map f x :=
+(Lhom.sum_inl : L →ᴸ L.sum L').map_on_function f x
+
+@[simp] lemma fun_map_sum_inr [(L'.sum L).Structure M]
+  [(Lhom.sum_inr : L →ᴸ L'.sum L).is_expansion_on M]
+  {n} {f : L.functions n} {x : fin n → M} :
+  @fun_map (L'.sum L) M _ n (sum.inr f) x = fun_map f x :=
+(Lhom.sum_inr : L →ᴸ L'.sum L).map_on_function f x
+
 @[priority 100] instance is_expansion_on_reduct (ϕ : L →ᴸ L') (M : Type*) [L'.Structure M] :
   @is_expansion_on L L' ϕ M (ϕ.reduct M) _ :=
 begin
@@ -307,15 +329,15 @@ section with_constants
 variable (L)
 
 section
-variables (α : Type w)
+variables (α : Type w')
 
 /-- Extends a language with a constant for each element of a parameter set in `M`. -/
-def with_constants : language.{(max u w) v} := L.sum (constants_on α)
+def with_constants : language.{(max u w') v} := L.sum (constants_on α)
 
 localized "notation L`[[`:95 α`]]`:90 := L.with_constants α" in first_order
 
 @[simp] lemma card_with_constants :
-  (L[[α]]).card = cardinal.lift.{w} L.card + cardinal.lift.{max u v} (# α) :=
+  (L[[α]]).card = cardinal.lift.{w'} L.card + cardinal.lift.{max u v} (# α) :=
 by rw [with_constants, card_sum, card_constants_on]
 
 /-- The language map adding constants.  -/
@@ -346,6 +368,18 @@ variables (L) (α)
 
 variables {α} {β : Type*}
 
+@[simp] lemma with_constants_fun_map_sum_inl [L[[α]].Structure M]
+  [(Lhom_with_constants L α).is_expansion_on M]
+  {n} {f : L.functions n} {x : fin n → M} :
+  @fun_map (L[[α]]) M _ n (sum.inl f) x = fun_map f x :=
+(Lhom_with_constants L α).map_on_function f x
+
+@[simp] lemma with_constants_rel_map_sum_inl [L[[α]].Structure M]
+  [(Lhom_with_constants L α).is_expansion_on M]
+  {n} {R : L.relations n} {x : fin n → M} :
+  @rel_map (L[[α]]) M _ n (sum.inl R) x = rel_map R x :=
+(Lhom_with_constants L α).map_on_relation R x
+
 /-- The language map extending the constant set.  -/
 def Lhom_with_constants_map (f : α → β) : L[[α]] →ᴸ L[[β]] :=
 Lhom.sum_map (Lhom.id L) (Lhom.constants_on_map f)
@@ -388,6 +422,13 @@ instance add_constants_expansion {L' : language} [L'.Structure M] (φ : L →ᴸ
   (φ.add_constants α).is_expansion_on M :=
 Lhom.sum_map_is_expansion_on _ _ M
 
+@[simp] lemma with_constants_fun_map_sum_inr {a : α} {x : fin 0 → M} :
+  @fun_map (L[[α]]) M _ 0 (sum.inr a : L[[α]].functions 0) x = L.con a :=
+begin
+  rw unique.eq_default x,
+  exact (Lhom.sum_inr : (constants_on α) →ᴸ L.sum _).map_on_function _ _,
+end
+
 variables {α} (A : set M)
 
 @[simp] lemma coe_con {a : A} : ((L.con a) : M) = a := rfl

src/model_theory/order.lean

@@ -169,7 +169,7 @@ variables [is_ordered L] [L.Structure M]
 @[simp] lemma rel_map_le_symb [has_le M] [L.is_ordered_structure M] {a b : M} :
   rel_map (le_symb : L.relations 2) ![a, b] ↔ a ≤ b :=
 begin
-  rw [← order_Lhom_le_symb, Lhom.is_expansion_on.map_on_relation],
+  rw [← order_Lhom_le_symb, Lhom.map_on_relation],
   refl,
 end
 

src/model_theory/semantics.lean

@@ -134,6 +134,48 @@ begin
     exact congr rfl (funext (λ i, ih i (h i (finset.mem_univ i)))) },
 end
 
+@[simp] lemma realize_constants_to_vars [L[[α]].Structure M]
+  [(Lhom_with_constants L α).is_expansion_on M]
+  {t : L[[α]].term β} {v : β → M} :
+  t.constants_to_vars.realize (sum.elim (λ a, ↑(L.con a)) v) = t.realize v :=
+begin
+  induction t with _ n f _ ih,
+  { simp },
+  { cases n,
+    { cases f,
+      { simp [ih], },
+      { simp only [realize, constants_to_vars, sum.elim_inl, fun_map_eq_coe_constants],
+        refl } },
+    { cases f,
+      { simp [ih] },
+      { exact is_empty_elim f } } }
+end
+
+@[simp] lemma realize_vars_to_constants [L[[α]].Structure M]
+  [(Lhom_with_constants L α).is_expansion_on M]
+  {t : L.term (α ⊕ β)} {v : β → M} :
+  t.vars_to_constants.realize v = t.realize (sum.elim (λ a, ↑(L.con a)) v) :=
+begin
+  induction t with ab n f ts ih,
+  { cases ab;
+    simp [language.con], },
+  { simp [ih], }
+end
+
+lemma realize_constants_vars_equiv_left [L[[α]].Structure M]
+  [(Lhom_with_constants L α).is_expansion_on M]
+  {n} {t : L[[α]].term (β ⊕ fin n)} {v : β → M} {xs : fin n → M} :
+  (constants_vars_equiv_left t).realize (sum.elim (sum.elim (λ a, ↑(L.con a)) v) xs) =
+    t.realize (sum.elim v xs) :=
+begin
+  simp only [constants_vars_equiv_left, realize_relabel, equiv.coe_trans, function.comp_app,
+    constants_vars_equiv_apply, relabel_equiv_symm_apply],
+  refine trans _ (realize_constants_to_vars),
+  rcongr,
+  rcases x with (a | (b | i));
+  simp,
+end
+
 end term
 
 namespace Lhom
@@ -144,7 +186,7 @@ namespace Lhom
 begin
   induction t with _ n f ts ih,
   { refl },
-  { simp only [term.realize, Lhom.on_term, Lhom.is_expansion_on.map_on_function, ih] }
+  { simp only [term.realize, Lhom.on_term, Lhom.map_on_function, ih] }
 end
 
 end Lhom
@@ -393,6 +435,20 @@ begin
   { simp [restrict_free_var, realize, ih3] },
 end
 
+lemma realize_constants_vars_equiv [L[[α]].Structure M]
+  [(Lhom_with_constants L α).is_expansion_on M]
+  {n} {φ : L[[α]].bounded_formula β n} {v : β → M} {xs : fin n → M} :
+  (constants_vars_equiv φ).realize (sum.elim (λ a, ↑(L.con a)) v) xs ↔ φ.realize v xs :=
+begin
+  refine realize_map_term_rel_id (λ n t xs, realize_constants_vars_equiv_left) (λ n R xs, _),
+  rw ← (Lhom_with_constants L α).map_on_relation (equiv.sum_empty (L.relations n)
+    ((constants_on α).relations n) R) xs,
+  rcongr,
+  cases R,
+  { simp, },
+  { exact is_empty_elim R }
+end
+
 variables [nonempty M]
 
 lemma realize_all_lift_at_one_self {n : ℕ} {φ : L.bounded_formula α n}
@@ -486,7 +542,7 @@ begin
   { refl },
   { simp only [on_bounded_formula, realize_bd_equal, realize_on_term],
     refl, },
-  { simp only [on_bounded_formula, realize_rel, realize_on_term, is_expansion_on.map_on_relation],
+  { simp only [on_bounded_formula, realize_rel, realize_on_term, Lhom.map_on_relation],
     refl, },
   { simp only [on_bounded_formula, ih1, ih2, realize_imp], },
   { simp only [on_bounded_formula, ih3, realize_all], },

src/model_theory/substructures.lean

@@ -577,7 +577,7 @@ def substructure_reduct : L'.substructure M ↪o L.substructure M :=
 { to_fun := λ S, { carrier := S,
     fun_mem := λ n f x hx, begin
       have h := S.fun_mem (φ.on_function f) x hx,
-      simp only [is_expansion_on.map_on_function, substructure.mem_carrier] at h,
+      simp only [Lhom.map_on_function, substructure.mem_carrier] at h,
       exact h,
     end },
   inj' := λ S T h, begin

src/model_theory/syntax.lean

@@ -31,6 +31,9 @@ above a particular index.
 variables with given terms.
 * Language maps can act on syntactic objects with functions such as
 `first_order.language.Lhom.on_formula`.
+* `first_order.language.term.constants_vars_equiv` and
+`first_order.language.bounded_formula.constants_vars_equiv` switch terms and formulas between having
+constants in the language and having extra variables indexed by the same type.
 
 ## Implementation Notes
 * Formulas use a modified version of de Bruijn variables. Specifically, a `L.bounded_formula α n`
@@ -112,6 +115,10 @@ end
   (term.relabel g ∘ term.relabel f : L.term α → L.term γ) = term.relabel (g ∘ f) :=
 funext (relabel_relabel f g)
 
+/-- Relabels a term's variables along a bijection. -/
+@[simps] def relabel_equiv (g : α ≃ β) : L.term α ≃ L.term β :=
+⟨relabel g, relabel g.symm, λ t, by simp, λ t, by simp⟩
+
 /-- Restricts a term to use only a set of the given variables. -/
 def restrict_var [decidable_eq α] : Π (t : L.term α) (f : t.var_finset → β), L.term β
 | (var a) f := var (f ⟨a, mem_singleton_self a⟩)
@@ -140,6 +147,54 @@ def functions.apply₂ (f : L.functions 2) (t₁ t₂ : L.term α) : L.term α :
 
 namespace term
 
+/-- Sends a term with constants to a term with extra variables. -/
+@[simp] def constants_to_vars : L[[γ]].term α → L.term (γ ⊕ α)
+| (var a) := var (sum.inr a)
+| (@func _ _ 0 f ts) := sum.cases_on f (λ f, func f (λ i, (ts i).constants_to_vars))
+    (λ c, var (sum.inl c))
+| (@func _ _ (n + 1) f ts) := sum.cases_on f (λ f, func f (λ i, (ts i).constants_to_vars))
+    (λ c, is_empty_elim c)
+
+/-- Sends a term with extra variables to a term with constants. -/
+@[simp] def vars_to_constants : L.term (γ ⊕ α) → L[[γ]].term α
+| (var (sum.inr a)) := var a
+| (var (sum.inl c)) := constants.term (sum.inr c)
+| (func f ts) := func (sum.inl f) (λ i, (ts i).vars_to_constants)
+
+/-- A bijection between terms with constants and terms with extra variables. -/
+@[simps] def constants_vars_equiv : L[[γ]].term α ≃ L.term (γ ⊕ α) :=
+⟨constants_to_vars, vars_to_constants, begin
+  intro t,
+  induction t with _ n f _ ih,
+  { refl },
+  { cases n,
+    { cases f,
+      { simp [constants_to_vars, vars_to_constants, ih] },
+      { simp [constants_to_vars, vars_to_constants, constants.term] } },
+    { cases f,
+      { simp [constants_to_vars, vars_to_constants, ih] },
+      { exact is_empty_elim f } } }
+end, begin
+  intro t,
+  induction t with x n f _ ih,
+  { cases x;
+    refl },
+  { cases n;
+    { simp [vars_to_constants, constants_to_vars, ih] } }
+end⟩
+
+/-- A bijection between terms with constants and terms with extra variables. -/
+def constants_vars_equiv_left : L[[γ]].term (α ⊕ β) ≃ L.term ((γ ⊕ α) ⊕ β) :=
+constants_vars_equiv.trans (relabel_equiv (equiv.sum_assoc _ _ _)).symm
+
+@[simp] lemma constants_vars_equiv_left_apply (t : L[[γ]].term (α ⊕ β)) :
+  constants_vars_equiv_left t = (constants_to_vars t).relabel (equiv.sum_assoc _ _ _).symm :=
+rfl
+
+@[simp] lemma constants_vars_equiv_left_symm_apply (t : L.term ((γ ⊕ α) ⊕ β)) :
+  constants_vars_equiv_left.symm t = vars_to_constants (t.relabel (equiv.sum_assoc _ _ _)) :=
+rfl
+
 instance inhabited_of_var [inhabited α] : inhabited (L.term α) :=
 ⟨var default⟩
 
@@ -485,6 +540,10 @@ end
 φ.map_term_rel (λ _ t, t.subst (sum.elim (term.relabel sum.inl ∘ f) (var ∘ sum.inr)))
   (λ _, id) (λ _, id)
 
+/-- A bijection sending formulas with constants to formulas with extra variables. -/
+def constants_vars_equiv : L[[γ]].bounded_formula α n ≃ L.bounded_formula (γ ⊕ α) n :=
+map_term_rel_equiv (λ _, term.constants_vars_equiv_left) (λ _, equiv.sum_empty _ _)
+
 /-- Turns the extra variables of a bounded formula into free variables. -/
 @[simp] def to_formula : ∀ {n : ℕ}, L.bounded_formula α n → L.formula (α ⊕ fin n)
 | n falsum := falsum