feat(model_theory/syntax, semantics): Lemmas about relabeling variabl…

…es (#14225)

Proves lemmas about relabeling variables in terms and formulas
Defines `first_order.language.bounded_formula.to_formula`, which turns turns all of the extra variables of a `bounded_formula` into free variables.

src/logic/equiv/fin.lean

@@ -247,6 +247,10 @@ fin_sum_fin_equiv.symm_apply_apply (sum.inl x)
   fin_sum_fin_equiv.symm (fin.nat_add m x) = sum.inr x :=
 fin_sum_fin_equiv.symm_apply_apply (sum.inr x)
 
+@[simp] lemma fin_sum_fin_equiv_symm_last :
+  fin_sum_fin_equiv.symm (fin.last n) = sum.inr 0 :=
+fin_sum_fin_equiv_symm_apply_nat_add 0
+
 /-- The equivalence between `fin (m + n)` and `fin (n + m)` which rotates by `n`. -/
 def fin_add_flip : fin (m + n) ≃ fin (n + m) :=
 (fin_sum_fin_equiv.symm.trans (equiv.sum_comm _ _)).trans fin_sum_fin_equiv

src/model_theory/semantics.lean

@@ -74,7 +74,7 @@ begin
 end
 
 @[simp] lemma realize_lift_at {n n' m : ℕ} {t : L.term (α ⊕ fin n)}
-  {v : (α ⊕ fin (n + n')) → M} :
+  {v : α ⊕ fin (n + n') → M} :
   (t.lift_at n' m).realize v = t.realize (v ∘
     (sum.map id (λ i, if ↑i < m then fin.cast_add n' i else fin.add_nat n' i))) :=
 realize_relabel
@@ -287,9 +287,9 @@ begin
 end
 
 lemma realize_relabel {m n : ℕ}
-  {φ : L.bounded_formula α n} {g : α → (β ⊕ fin m)} {v : β → M} {xs : fin (m + n) → M} :
+  {φ : L.bounded_formula α n} {g : α → β ⊕ fin m} {v : β → M} {xs : fin (m + n) → M} :
   (φ.relabel g).realize v xs ↔
-    φ.realize (sum.elim v (xs ∘ (fin.cast_add n)) ∘ g) (xs ∘ (fin.nat_add m)) :=
+    φ.realize (sum.elim v (xs ∘ fin.cast_add n) ∘ g) (xs ∘ fin.nat_add m) :=
 begin
   induction φ with _ _ _ _ _ _ _ _ _ _ _ ih1 ih2 n' _ ih3,
   { refl },
@@ -697,6 +697,33 @@ begin
       exact ⟨_, _, h⟩ } }
 end
 
+@[simp] lemma realize_to_formula (φ : L.bounded_formula α n) (v : α ⊕ fin n → M) :
+  φ.to_formula.realize v ↔ φ.realize (v ∘ sum.inl) (v ∘ sum.inr) :=
+begin
+  induction φ with _ _ _ _ _ _ _ _ _ _ _ ih1 ih2 _ _ ih3 a8 a9 a0,
+  { refl },
+  { simp [bounded_formula.realize] },
+  { simp [bounded_formula.realize] },
+  { rw [to_formula, formula.realize, realize_imp, ← formula.realize, ih1, ← formula.realize, ih2,
+      realize_imp], },
+  { rw [to_formula, formula.realize, realize_all, realize_all],
+    refine forall_congr (λ 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],
+    rcongr,
+    { cases x,
+      { simp },
+      { refine fin.last_cases _ (λ i, _) x,
+        { rw [sum.elim_inr, snoc_last, function.comp_app, sum.elim_inr, function.comp_app,
+            fin_sum_fin_equiv_symm_last, sum.map_inr, sum.elim_inr, function.comp_app],
+          exact (congr rfl (subsingleton.elim _ _)).trans (snoc_last _ _) },
+        { simp only [cast_succ, function.comp_app, sum.elim_inr,
+            fin_sum_fin_equiv_symm_apply_cast_add, sum.map_inl, sum.elim_inl],
+          rw [← cast_succ, snoc_cast_succ] } } },
+    { exact subsingleton.elim _ _ } }
+end
+
 end bounded_formula
 
 namespace equiv

src/model_theory/syntax.lean

@@ -53,7 +53,7 @@ namespace language
 
 variables (L : language.{u v}) {L' : language}
 variables {M : Type w} {N P : Type*} [L.Structure M] [L.Structure N] [L.Structure P]
-variables {α : Type u'} {β : Type v'}
+variables {α : Type u'} {β : Type v'} {γ : Type*}
 open_locale first_order
 open Structure fin
 
@@ -86,19 +86,35 @@ open finset
 | (var i) := var (g i)
 | (func f ts) := func f (λ i, (ts i).relabel)
 
+@[simp] lemma relabel_id (t : L.term α) :
+  t.relabel id = t :=
+begin
+  induction t with _ _ _ _ ih,
+  { refl, },
+  { simp [ih] },
+end
+
+@[simp] lemma relabel_relabel (f : α → β) (g : β → γ) (t : L.term α) :
+  (t.relabel f).relabel g = t.relabel (g ∘ f) :=
+begin
+  induction t with _ _ _ _ ih,
+  { refl, },
+  { simp [ih] },
+end
+
 /-- 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⟩)
 | (func F ts) f := func F (λ i, (ts i).restrict_var
-  (f ∘ (set.inclusion (subset_bUnion_of_mem _ (mem_univ i)))))
+  (f ∘ set.inclusion (subset_bUnion_of_mem _ (mem_univ i))))
 
 /-- Restricts a term to use only a set of the given variables on the left side of a sum. -/
 def restrict_var_left [decidable_eq α] {γ : Type*} :
   Π (t : L.term (α ⊕ γ)) (f : t.var_finset_left → β), L.term (β ⊕ γ)
 | (var (sum.inl a)) f := var (sum.inl (f ⟨a, mem_singleton_self a⟩))
 | (var (sum.inr a)) f := var (sum.inr a)
 | (func F ts) f := func F (λ i, (ts i).restrict_var_left
-  (f ∘ (set.inclusion (subset_bUnion_of_mem _ (mem_univ i)))))
+  (f ∘ set.inclusion (subset_bUnion_of_mem _ (mem_univ i))))
 
 end term
 
@@ -263,18 +279,18 @@ open finset
 | n (all f) := f.free_var_finset
 
 /-- Casts `L.bounded_formula α m` as `L.bounded_formula α n`, where `m ≤ n`. -/
-def cast_le : ∀ {m n : ℕ} (h : m ≤ n), L.bounded_formula α m → L.bounded_formula α n
+@[simp] def cast_le : ∀ {m n : ℕ} (h : m ≤ n), L.bounded_formula α m → L.bounded_formula α n
 | m n h falsum := falsum
-| m n h (equal t₁ t₂) := (t₁.relabel (sum.map id (fin.cast_le h))).bd_equal
+| m n h (equal t₁ t₂) := equal (t₁.relabel (sum.map id (fin.cast_le h)))
     (t₂.relabel (sum.map id (fin.cast_le h)))
-| m n h (rel R ts) := R.bounded_formula (term.relabel (sum.map id (fin.cast_le h)) ∘ ts)
+| m n h (rel R ts) := rel R (term.relabel (sum.map id (fin.cast_le h)) ∘ ts)
 | m n h (imp f₁ f₂) := (f₁.cast_le h).imp (f₂.cast_le h)
 | m n h (all f) := (f.cast_le (add_le_add_right h 1)).all
 
 /-- A function to help relabel the variables in bounded formulas. -/
-def relabel_aux (g : α → (β ⊕ fin n)) (k : ℕ) :
+def relabel_aux (g : α → β ⊕ fin n) (k : ℕ) :
   α ⊕ fin k → β ⊕ fin (n + k) :=
-(sum.map id fin_sum_fin_equiv) ∘ (equiv.sum_assoc _ _ _) ∘ (sum.map g id)
+sum.map id fin_sum_fin_equiv ∘ equiv.sum_assoc _ _ _ ∘ sum.map g id
 
 @[simp] lemma sum_elim_comp_relabel_aux {m : ℕ} {g : α → (β ⊕ fin n)}
   {v : β → M} {xs : fin (n + m) → M} :
@@ -289,27 +305,49 @@ begin
   { simp [bounded_formula.relabel_aux] }
 end
 
+@[simp] lemma relabel_aux_sum_inl (k : ℕ) :
+  relabel_aux (sum.inl : α → α ⊕ fin n) k =
+  sum.map id (nat_add n) :=
+begin
+  ext x,
+  cases x;
+  { simp [relabel_aux] },
+end
+
 /-- Relabels a bounded formula's variables along a particular function. -/
-def relabel (g : α → (β ⊕ fin n)) :
+@[simp] def relabel (g : α → (β ⊕ fin n)) :
   ∀ {k : ℕ}, L.bounded_formula α k → L.bounded_formula β (n + k)
 | k falsum := falsum
-| k (equal t₁ t₂) := (t₁.relabel (relabel_aux g k)).bd_equal (t₂.relabel (relabel_aux g k))
-| k (rel R ts) := R.bounded_formula (term.relabel (relabel_aux g k) ∘ ts)
+| k (equal t₁ t₂) := equal (t₁.relabel (relabel_aux g k)) (t₂.relabel (relabel_aux g k))
+| k (rel R ts) := rel R (term.relabel (relabel_aux g k) ∘ ts)
 | k (imp f₁ f₂) := f₁.relabel.imp f₂.relabel
 | k (all f) := f.relabel.all
 
+@[simp] lemma relabel_sum_inl (φ : L.bounded_formula α n) :
+  (φ.relabel sum.inl : L.bounded_formula α (0 + n)) =
+  φ.cast_le (ge_of_eq (zero_add n)) :=
+begin
+  induction φ with _ _ _ _ _ _ _ _ _ _ _ ih1 ih2 _ _ ih3,
+  { refl },
+  { simp [fin.nat_add_zero, cast_le_of_eq] },
+  { simp [fin.nat_add_zero, cast_le_of_eq] },
+  { simp [ih1, ih2] },
+  { simp only [ih3, relabel, cast_le],
+    refl, },
+end
+
 /-- Restricts a bounded formula to only use a particular set of free variables. -/
 def restrict_free_var [decidable_eq α] : Π {n : ℕ} (φ : L.bounded_formula α n)
   (f : φ.free_var_finset → β), L.bounded_formula β n
 | n falsum f := falsum
 | n (equal t₁ t₂) f := equal
-  (t₁.restrict_var_left (f ∘ (set.inclusion (subset_union_left _ _))))
-  (t₂.restrict_var_left (f ∘ (set.inclusion (subset_union_right _ _))))
+  (t₁.restrict_var_left (f ∘ set.inclusion (subset_union_left _ _)))
+  (t₂.restrict_var_left (f ∘ set.inclusion (subset_union_right _ _)))
 | n (rel R ts) f := rel R (λ i, (ts i).restrict_var_left
   (f ∘ set.inclusion (subset_bUnion_of_mem _ (mem_univ i))))
 | n (imp φ₁ φ₂) f :=
-  (φ₁.restrict_free_var (f ∘ (set.inclusion (subset_union_left _ _)))).imp
-  (φ₂.restrict_free_var (f ∘ (set.inclusion (subset_union_right _ _))))
+  (φ₁.restrict_free_var (f ∘ set.inclusion (subset_union_left _ _))).imp
+  (φ₂.restrict_free_var (f ∘ set.inclusion (subset_union_right _ _)))
 | n (all φ) f := (φ.restrict_free_var f).all
 
 /-- Places universal quantifiers on all extra variables of a bounded formula. -/
@@ -340,6 +378,15 @@ def lift_at : ∀ {n : ℕ} (n' m : ℕ), L.bounded_formula α n → L.bounded_f
 | n (imp φ₁ φ₂) tf := (φ₁.subst tf).imp (φ₂.subst tf)
 | n (all φ) tf := (φ.subst tf).all
 
+/-- 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
+| n (equal t₁ t₂) := t₁.equal t₂
+| n (rel R ts) := R.formula ts
+| n (imp φ₁ φ₂) := φ₁.to_formula.imp φ₂.to_formula
+| n (all φ) := (φ.to_formula.relabel
+  (sum.elim (sum.inl ∘ sum.inl) (sum.map sum.inr id ∘ fin_sum_fin_equiv.symm))).all
+
 variables {l : ℕ} {φ ψ : L.bounded_formula α l} {θ : L.bounded_formula α l.succ}
 variables {v : α → M} {xs : fin l → M}