refactor(model_theory/terms_and_formulas): Improvements to basics of first-order formulas (#12091)

Improves the simp set of lemmas related to `realize_bounded_formula` and `realize_formula`, so that they simplify higher-level definitions directly, and keep bounded formulas and formulas separate.
Generalizes relabelling of bounded formulas.
Defines `close_with_exists` and `close_with_forall` to quantify bounded formulas into closed formulas.
Defines `bd_iff` and `iff`.

Author: awainverse

src/model_theory/basic.lean

@@ -128,10 +128,10 @@ localized "notation A ` ≃[`:25 L `] ` B := L.equiv A B" in first_order
 variables {L M N} {P : Type*} [L.Structure P] {Q : Type*} [L.Structure Q]
 
 instance : has_coe_t L.const M :=
-⟨λ c, fun_map c fin.elim0⟩
+⟨λ c, fun_map c default⟩
 
 lemma fun_map_eq_coe_const {c : L.const} {x : fin 0 → M} :
-  fun_map c x = c := congr rfl (funext fin.elim0)
+  fun_map c x = c := congr rfl (subsingleton.elim _ _)
 
 /-- Given a language with a nonempty type of constants, any structure will be nonempty. This cannot
   be a global instance, because `L` becomes a metavariable. -/
@@ -158,7 +158,7 @@ lemma ext_iff {f g : M →[L] N} : f = g ↔ ∀ x, f x = g x :=
   φ (fun_map f x) = fun_map f (φ ∘ x) := φ.map_fun' f x
 
 @[simp] lemma map_const (φ : M →[L] N) (c : L.const) : φ c = c :=
-(φ.map_fun c fin.elim0).trans (congr rfl (funext fin.elim0))
+(φ.map_fun c default).trans fun_map_eq_coe_const
 
 @[simp] lemma map_rel (φ : M →[L] N) {n : ℕ} (r : L.relations n) (x : fin n → M) :
   rel_map r x → rel_map r (φ ∘ x) := φ.map_rel' r x
@@ -197,7 +197,7 @@ instance has_coe_to_fun : has_coe_to_fun (M ↪[L] N) (λ _, M → N) := ⟨λ f
   φ (fun_map f x) = fun_map f (φ ∘ x) := φ.map_fun' f x
 
 @[simp] lemma map_const (φ : M ↪[L] N) (c : L.const) : φ c = c :=
-(φ.map_fun c fin.elim0).trans (congr rfl (funext fin.elim0))
+(φ.map_fun c default).trans fun_map_eq_coe_const
 
 @[simp] lemma map_rel (φ : M ↪[L] N) {n : ℕ} (r : L.relations n) (x : fin n → M) :
   rel_map r (φ ∘ x) ↔ rel_map r x := φ.map_rel' r x
@@ -300,7 +300,7 @@ lemma symm_apply_apply (f : M ≃[L] N) (a : M) : f.symm (f a) = a := f.to_equiv
   φ (fun_map f x) = fun_map f (φ ∘ x) := φ.map_fun' f x
 
 @[simp] lemma map_const (φ : M ≃[L] N) (c : L.const) : φ c = c :=
-(φ.map_fun c fin.elim0).trans (congr rfl (funext fin.elim0))
+(φ.map_fun c default).trans fun_map_eq_coe_const
 
 @[simp] lemma map_rel (φ : M ≃[L] N) {n : ℕ} (r : L.relations n) (x : fin n → M) :
   rel_map r (φ ∘ x) ↔ rel_map r x := φ.map_rel' r x

src/model_theory/definability.lean

@@ -36,7 +36,7 @@ variables (L) {α : Type} [fintype α]
 /-- A subset of a finite Cartesian product of a structure is definable when membership in
   the set is given by a first-order formula. -/
 structure is_definable (s : set (α → M)) : Prop :=
-(exists_formula : ∃ (φ : L.formula α), s = set_of (realize_formula M φ))
+(exists_formula : ∃ (φ : L.formula α), s = set_of φ.realize)
 
 variables {L}
 
@@ -67,17 +67,16 @@ lemma is_definable.union {f g : set (α → M)} (hf : L.is_definable f) (hg : L.
   rcases hg.exists_formula with ⟨θ, hθ⟩,
   refine ⟨φ ⊔ θ, _⟩,
   ext,
-  simp only [hφ, hθ, set.sup_eq_union, realize_not, realize_bounded_formula,
-    bounded_formula.has_sup_sup, set.mem_union_eq, set.mem_set_of_eq],
-  tauto,
+  rw [hφ, hθ, set.mem_set_of_eq, formula.realize_sup, set.mem_union_eq, set.mem_set_of_eq,
+    set.mem_set_of_eq],
 end⟩
 
 @[simp]
 lemma is_definable.compl {s : set (α → M)} (hf : L.is_definable s) :
   L.is_definable sᶜ :=
 ⟨begin
   rcases hf.exists_formula with ⟨φ, hφ⟩,
-  refine ⟨bd_not φ, _⟩,
+  refine ⟨φ.not, _⟩,
   rw hφ,
   refl,
 end⟩

src/model_theory/direct_limit.lean

@@ -16,7 +16,6 @@ This file constructs the direct limit of a directed system of first-order embedd
   first-order embeddings between the structures indexed by `G`.
 -/
 
-
 universes v w u₁ u₂
 
 open_locale first_order

src/model_theory/elementary_maps.lean

@@ -31,7 +31,7 @@ variables [L.Structure M] [L.Structure N] [L.Structure P] [L.Structure Q]
 structure elementary_embedding :=
 (to_fun : M → N)
 (map_formula' : ∀{n} (φ : L.formula (fin n)) (x : fin n → M),
-  realize_formula N φ (to_fun ∘ x) ↔ realize_formula M φ x . obviously)
+  φ.realize (to_fun ∘ x) ↔ φ.realize x . obviously)
 
 localized "notation A ` ↪ₑ[`:25 L `] ` B := L.elementary_embedding A B" in first_order
 
@@ -42,14 +42,13 @@ namespace elementary_embedding
 instance has_coe_to_fun : has_coe_to_fun (M ↪ₑ[L] N) (λ _, M → N) :=
 ⟨λ f, f.to_fun⟩
 
-@[simp] lemma map_formula (f : M ↪ₑ[L] N) {α : Type} [fintype α] (φ : L.formula α)
-  (x : α → M) :
-  realize_formula N φ (f ∘ x) ↔ realize_formula M φ x :=
+@[simp] lemma map_formula (f : M ↪ₑ[L] N) {α : Type} [fintype α] (φ : L.formula α) (x : α → M) :
+  φ.realize (f ∘ x) ↔ φ.realize x :=
 begin
   have g := fintype.equiv_fin α,
   have h := f.map_formula' (φ.relabel g) (x ∘ g.symm),
-  rw [realize_formula_relabel, realize_formula_relabel,
-    function.comp.assoc x g.symm g, g.symm_comp_self, function.comp.right_id] at h,
+  rw [formula.realize_relabel, formula.realize_relabel, function.comp.assoc x g.symm g,
+    g.symm_comp_self, function.comp.right_id] at h,
   rw [← h, iff_eq_eq],
   congr,
   ext y,
@@ -59,29 +58,28 @@ end
 @[simp] lemma map_fun (φ : M ↪ₑ[L] N) {n : ℕ} (f : L.functions n) (x : fin n → M) :
   φ (fun_map f x) = fun_map f (φ ∘ x) :=
 begin
-  have h := φ.map_formula (formula.graph f) (fin.snoc x (fun_map f x)),
-  rw [realize_graph, fin.comp_snoc, realize_graph] at h,
+  have h := φ.map_formula (formula.graph f) (fin.cons (fun_map f x) x),
+  rw [formula.realize_graph, fin.comp_cons, formula.realize_graph] at h,
   rw [eq_comm, h]
 end
 
 @[simp] lemma map_const (φ : M ↪ₑ[L] N) (c : L.const) : φ c = c :=
-(φ.map_fun c fin.elim0).trans (congr rfl (funext fin.elim0))
+(φ.map_fun c default).trans fun_map_eq_coe_const
 
 @[simp] lemma map_rel (φ : M ↪ₑ[L] N) {n : ℕ} (r : L.relations n) (x : fin n → M) :
   rel_map r (φ ∘ x) ↔ rel_map r x :=
 begin
-  have h := φ.map_formula (bd_rel r (var ∘ sum.inl)) x,
+  have h := φ.map_formula (r.formula var) x,
   exact h
 end
 
 @[simp] lemma injective (φ : M ↪ₑ[L] N) :
   function.injective φ :=
 begin
   intros x y,
-  have h := φ.map_formula (formula.equal (var 0) (var 1) : L.formula (fin 2))
-    (λ i, if i = 0 then x else y),
-  rw [realize_equal, realize_equal] at h,
-  simp only [nat.one_ne_zero, realize_term, fin.one_eq_zero_iff, if_true, eq_self_iff_true,
+  have h := φ.map_formula ((var 0).equal (var 1) : L.formula (fin 2)) (λ i, if i = 0 then x else y),
+  rw [formula.realize_equal, formula.realize_equal] at h,
+  simp only [nat.one_ne_zero, term.realize, fin.one_eq_zero_iff, if_true, eq_self_iff_true,
     function.comp_app, if_false] at h,
   exact h.1,
 end
@@ -158,26 +156,32 @@ def to_elementary_embedding (f : M ≃[L] N) : M ↪ₑ[L] N :=
 
 end equiv
 
-@[simp] lemma realize_term_substructure {α : Type} {S : L.substructure M} (v : α → S)
+@[simp] lemma realize_term_substructure {α : Type*} {S : L.substructure M} (v : α → S)
   (t : L.term α) :
-  realize_term (coe ∘ v) t = (↑(realize_term v t) : M) :=
-S.subtype.realize_term v t
+  t.realize (coe ∘ v) = (↑(t.realize v) : M) :=
+S.subtype.realize_term t
 
-@[simp] lemma realize_bounded_formula_top {α : Type} {n : ℕ} (v : α → (⊤ : L.substructure M))
-  (xs : fin n → (⊤ : L.substructure M)) (φ : L.bounded_formula α n) :
-  realize_bounded_formula (⊤ : L.substructure M) φ v xs ↔
-  realize_bounded_formula M φ (coe ∘ v) (coe ∘ xs) :=
+namespace substructure
+
+@[simp] lemma realize_bounded_formula_top {α : Type*} {n : ℕ} {φ : L.bounded_formula α n}
+  {v : α → (⊤ : L.substructure M)} {xs : fin n → (⊤ : L.substructure M)} :
+  φ.realize v xs ↔ φ.realize ((coe : _ → M) ∘ v) (coe ∘ xs) :=
 begin
-  rw ← substructure.top_equiv.realize_bounded_formula v xs φ,
+  rw ← substructure.top_equiv.realize_bounded_formula φ,
   simp,
 end
 
-namespace substructure
+@[simp] lemma realize_formula_top {α : Type*} {φ : L.formula α} {v : α → (⊤ : L.substructure M)} :
+  φ.realize v ↔ φ.realize ((coe : (⊤ : L.substructure M) → M) ∘ v) :=
+begin
+  rw ← substructure.top_equiv.realize_formula φ,
+  simp,
+end
 
 /-- A substructure is elementary when every formula applied to a tuple in the subtructure
   agrees with its value in the overall structure. -/
 def is_elementary (S : L.substructure M) : Prop :=
-∀{n} (φ : L.formula (fin n)) (x : fin n → S), realize_formula M φ (coe ∘ x) ↔ realize_formula S φ x
+∀{n} (φ : L.formula (fin n)) (x : fin n → S), φ.realize ((coe : _ → M) ∘ x) ↔ φ.realize x
 
 end substructure
 
@@ -213,11 +217,7 @@ def subtype (S : L.elementary_substructure M) : S ↪ₑ[L] M :=
 
 /-- The substructure `M` of the structure `M` is elementary. -/
 instance : has_top (L.elementary_substructure M) :=
-⟨⟨⊤, λ n φ x, begin
-  rw formula at φ,
-  rw [realize_formula, realize_formula, realize_bounded_formula_top, iff_eq_eq],
-  exact congr rfl (funext fin_zero_elim),
-end⟩⟩
+⟨⟨⊤, λ n φ x, substructure.realize_formula_top.symm⟩⟩
 
 instance : inhabited (L.elementary_substructure M) := ⟨⊤⟩
 

src/model_theory/quotients.lean

@@ -62,12 +62,12 @@ begin
   rw [quotient.fin_choice_eq, quotient.lift_mk],
 end
 
-lemma realize_term_quotient_mk {β : Type*} (x : β → M) (t : L.term β) :
-  realize_term (λ i, ⟦x i⟧) t = ⟦@realize_term _ _ ps.to_structure _ x t⟧ :=
+lemma term.realize_quotient_mk {β : Type*} (t : L.term β) (x : β → M)  :
+  t.realize (λ i, ⟦x i⟧) = ⟦@term.realize _ _ ps.to_structure _ x t⟧ :=
 begin
-  induction t with a1 a2 a3 a4 ih a6 a7 a8 a9 a0,
+  induction t with _ _ _ _ ih,
   { refl },
-  simp only [ih, fun_map_quotient_mk, realize_term],
+  { simp only [ih, fun_map_quotient_mk, term.realize] },
 end
 
 end language