feat(ModelTheory/Complexity): define literals

Mathlib/ModelTheory/Complexity.lean

@@ -1,19 +1,22 @@
 /-
 Copyright (c) 2021 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Aaron Anderson
+Authors: Aaron Anderson, Metin Ersin Arıcan
 -/
 import Mathlib.ModelTheory.Equivalence
 
 /-!
 # Quantifier Complexity
 
-This file defines quantifier complexity of first-order formulas, and constructs prenex normal forms.
+This file defines quantifier complexity of first-order formulas, defines literals, and constructs
+prenex normal forms.
 
 ## Main Definitions
 
 - `FirstOrder.Language.BoundedFormula.IsAtomic` defines atomic formulas - those which are
   constructed only from terms and relations.
+- `FirstOrder.Language.BoundedFormula.IsLiteral` defines literals - those which are `⊥`, `⊤`,
+  atomic formulas or negation of atomic formulas.
 - `FirstOrder.Language.BoundedFormula.IsQF` defines quantifier-free formulas - those which are
   constructed only from atomic formulas and boolean operations.
 - `FirstOrder.Language.BoundedFormula.IsPrenex` defines when a formula is in prenex normal form -
@@ -26,6 +29,28 @@ This file defines quantifier complexity of first-order formulas, and constructs
 - `FirstOrder.Language.BoundedFormula.realize_toPrenex` shows that the prenex normal form of a
   formula has the same realization as the original formula.
 
+## TODO
+
+- `FirstOrder.Language.BoundedFormula.toDNF` constructs a disjunctive normal form of a given
+  quantifier-free formula.
+- `FirstOrder.Language.BoundedFormula.toCNF` constructs a conjunctive normal form of a given
+  quantifier-free formula.
+- `FirstOrder.Language.BoundedFormula.IsConjunctive` defines conjunctive formulas - those which are
+  constructed only from literals and conjunctions.
+- `FirstOrder.Language.BoundedFormula.IsDisjunctive` defines disjunctive formulas - those which are
+  constructed only from literals and disjunctions.
+- `FirstOrder.Language.BoundedFormula.IsDNF` defines formulas in disjunctive normal form - those
+  which are disjunctions of conjunctive formulas.
+- `FirstOrder.Language.BoundedFormula.IsCNF` defines formulas in conjunctive normal form - those
+  which are conjunctions of disjunctive formulas.
+- `FirstOrder.Language.BoundedFormula.toDNF_semanticallyEquivalent` shows that the disjunctive
+  normal form of a formula is semantically equivalent to the original formula.
+- `FirstOrder.Language.BoundedFormula.toCNF_semanticallyEquivalent` shows that the conjunctive
+  normal form of a formula is semantically equivalent to the original formula.
+- `FirstOrder.Language.BoundedFormula.IsDNF.components` which gives the literals of a DNF as
+  a list of lists.
+- `FirstOrder.Language.BoundedFormula.IsCNF.components` which gives the literals of a CNF as
+  a list of lists.
 -/
 
 universe u v w u' v'
@@ -44,6 +69,53 @@ open FirstOrder Structure Fin
 
 namespace BoundedFormula
 
+/-- An auxilary operation which is semantically equivalent to
+  `FirstOrder.Language.BoundedFormula.not`. It takes a bounded formula `φ`, assuming any negation
+  symbol inside `φ` occurs in front of an atomic formula or `⊥`, it applies negation to `φ`, pushes
+  the negation inwards through `⊓`, `⊔`, `∀'`, `∃'`, and eliminates double negations. -/
+def simpleNot : {n : ℕ} → L.BoundedFormula α n → L.BoundedFormula α n
+  | _, falsum => ⊤
+  | _, equal t₁ t₂ => ∼(t₁.bdEqual t₂)
+  | _, rel R ts => ∼(rel R ts)
+  | _, ⊤ => ⊥
+  | _, ∼(equal t₁ t₂) => t₁.bdEqual t₂
+  | _, ∼(rel R ts) => rel R ts
+  | _, ∀' φ => ∃' φ.simpleNot
+  | _, ∃' φ => ∀' φ.simpleNot
+  | _, BoundedFormula.inf φ ψ => φ.simpleNot ⊔ ψ.simpleNot
+  | _, BoundedFormula.sup φ ψ => φ.simpleNot ⊓ ψ.simpleNot
+  | _, φ => ∼φ
+
+@[simp]
+theorem realize_simpleNot {n : ℕ} (φ : L.BoundedFormula α n) {v : α → M} {xs : Fin n → M} :
+    φ.simpleNot.Realize v xs ↔ φ.not.Realize v xs := by
+  unfold simpleNot
+  split
+  · rfl
+  · rfl
+  · rfl
+  · simp
+  · simp only [realize_not, realize_imp, realize_falsum, imp_false, not_not]
+    rfl
+  · simp only [realize_not, realize_imp, realize_falsum, imp_false, not_not]
+  · rename_i φ
+    simp only [realize_ex, realize_simpleNot φ, realize_not, realize_all, not_forall]
+  · rename_i φ
+    simp only [realize_all, realize_simpleNot φ, realize_not, realize_imp, realize_falsum,
+      imp_false, not_not]
+  · rename_i φ ψ
+    simp only [realize_sup, realize_simpleNot φ, realize_not, realize_simpleNot ψ, realize_imp,
+      realize_falsum, imp_false, imp_iff_not_or, not_not]
+  · rename_i φ ψ
+    simp only [realize_inf, realize_simpleNot φ, realize_not, realize_simpleNot ψ, realize_imp,
+      realize_falsum, imp_false, imp_iff_not_or, not_or, not_not]
+  · rfl
+
+theorem simpleNot_semanticallyEquivalent_not {T : L.Theory} {n : ℕ} (φ : L.BoundedFormula α n) :
+    (φ.simpleNot ⇔[T] φ.not) := by
+  simp only [Theory.Iff, Theory.ModelsBoundedFormula, realize_iff,
+    realize_simpleNot, realize_not, implies_true]
+
 /-- An atomic formula is either equality or a relation symbol applied to terms.
 Note that `⊥` and `⊤` are not considered atomic in this convention. -/
 inductive IsAtomic : L.BoundedFormula α n → Prop
@@ -66,6 +138,42 @@ theorem IsAtomic.liftAt {k m : ℕ} (h : IsAtomic φ) : (φ.liftAt k m).IsAtomic
 theorem IsAtomic.castLE {h : l ≤ n} (hφ : IsAtomic φ) : (φ.castLE h).IsAtomic :=
   IsAtomic.recOn hφ (fun _ _ => IsAtomic.equal _ _) fun _ _ => IsAtomic.rel _ _
 
+protected theorem IsAtomic.simpleNot_eq_not {φ : L.BoundedFormula α n} (hφ : φ.IsAtomic) :
+    φ.simpleNot = ∼φ := by
+  induction hφ with
+  | equal t₁ t₂ => rfl
+  | rel R ts => rfl
+
+protected theorem IsAtomic.simpleNot_of_not_eq {φ : L.BoundedFormula α n} (hφ : φ.IsAtomic) :
+    φ.not.simpleNot = φ := by
+  induction hφ with
+  | equal t₁ t₂ => rfl
+  | rel R ts => rfl
+
+/-- A literal is either `⊥`, `⊤`, an atomic formula or the negation of an atomic formula. -/
+inductive IsLiteral : L.BoundedFormula α n → Prop
+  | falsum : IsLiteral BoundedFormula.falsum
+  | of_isAtomic {φ : L.BoundedFormula α n} (h : φ.IsAtomic) : IsLiteral φ
+  | not_falsum : IsLiteral BoundedFormula.falsum.not
+  | of_not_of_isAtomic {φ : L.BoundedFormula α n} (h : φ.IsAtomic) : IsLiteral φ.not
+
+theorem IsAtomic.isLiteral {φ : L.BoundedFormula α n} (hφ : φ.IsAtomic) : IsLiteral φ :=
+  IsLiteral.of_isAtomic hφ
+
+protected theorem IsLiteral.simpleNot {φ : L.BoundedFormula α n} (hφ : φ.IsLiteral) :
+    φ.simpleNot.IsLiteral := by
+  induction hφ with
+  | falsum =>
+    exact IsLiteral.not_falsum
+  | of_isAtomic hφ =>
+    rw [hφ.simpleNot_eq_not]
+    exact IsLiteral.of_not_of_isAtomic hφ
+  | not_falsum =>
+    exact IsLiteral.falsum
+  | of_not_of_isAtomic hφ =>
+    rw [hφ.simpleNot_of_not_eq]
+    exact hφ.isLiteral
+
 /-- A quantifier-free formula is a formula defined without quantifiers. These are all equivalent
 to boolean combinations of atomic formulas. -/
 inductive IsQF : L.BoundedFormula α n → Prop

Mathlib/ModelTheory/Equivalence.lean

@@ -194,6 +194,20 @@ protected theorem imp {φ ψ φ' ψ' : L.BoundedFormula α n} (h : φ ⇔[T] ψ)
     BoundedFormula.realize_imp]
   exact fun M v xs => imp_congr h.realize_bd_iff h'.realize_bd_iff
 
+protected theorem sup {φ ψ φ' ψ' : L.BoundedFormula α n}
+    (h : φ ⇔[T] ψ) (h' : φ' ⇔[T] ψ') :
+    (φ ⊔ φ') ⇔[T] (ψ ⊔ ψ') := by
+  simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff,
+    BoundedFormula.realize_sup]
+  exact fun M v xs => or_congr h.realize_bd_iff h'.realize_bd_iff
+
+protected theorem inf {φ ψ φ' ψ' : L.BoundedFormula α n}
+    (h : φ ⇔[T] ψ) (h' : φ' ⇔[T] ψ') :
+    (φ ⊓ φ') ⇔[T] (ψ ⊓ ψ') := by
+  simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff,
+    BoundedFormula.realize_inf]
+  exact fun M v xs => and_congr h.realize_bd_iff h'.realize_bd_iff
+
 end Iff
 
 /-- Semantic equivalence forms an equivalence relation on formulas. -/
@@ -205,7 +219,7 @@ end Theory
 
 namespace BoundedFormula
 
-variable (φ ψ : L.BoundedFormula α n)
+variable (φ ψ χ : L.BoundedFormula α n)
 
 theorem iff_not_not : φ ⇔[T] φ.not.not := fun M v xs => by
   simp
@@ -216,15 +230,39 @@ theorem imp_iff_not_sup : (φ.imp ψ) ⇔[T] (φ.not ⊔ ψ) :=
 theorem sup_iff_not_inf_not : (φ ⊔ ψ) ⇔[T] (φ.not ⊓ ψ.not).not :=
   fun M v xs => by simp [imp_iff_not_or]
 
+theorem not_sup_semanticallyEquivalent_inf_not : (φ ⊔ ψ).not ⇔[T] (φ.not ⊓ ψ.not) :=
+  fun M v xs => by simp [imp_iff_not_or]
+
 theorem inf_iff_not_sup_not : (φ ⊓ ψ) ⇔[T] (φ.not ⊔ ψ.not).not :=
   fun M v xs => by simp
 
+theorem not_inf_semanticallyEquivalent_sup_not : (φ ⊓ ψ).not ⇔[T] (φ.not ⊔ ψ.not) :=
+  fun M v xs => by simp [imp_iff_not_or]
+
+theorem inf_sup_left_semanticallyEquivalent : χ ⊓ (φ ⊔ ψ) ⇔[T] (χ ⊓ φ) ⊔ (χ ⊓ ψ) :=
+  fun M v xs => by simp [and_or_left]
+
+theorem sup_inf_right_semanticallyEquivalent : (φ ⊔ ψ) ⊓ χ ⇔[T] (φ ⊓ χ) ⊔ (ψ ⊓ χ) :=
+  fun M v xs => by simp [or_and_right]
+
+theorem inf_sup_right_semanticallyEquivalent : (φ ⊓ ψ) ⊔ χ ⇔[T] (φ ⊔ χ) ⊓ (ψ ⊔ χ) :=
+  fun M v xs => by simp [and_or_right]
+
+theorem sup_inf_left_semanticallyEquivalent : χ ⊔ (φ ⊓ ψ) ⇔[T] (χ ⊔ φ) ⊓ (χ ⊔ ψ) :=
+  fun M v xs => by simp [or_and_left]
+
 theorem all_iff_not_ex_not (φ : L.BoundedFormula α (n + 1)) :
     φ.all ⇔[T] φ.not.ex.not := fun M v xs => by simp
 
+theorem not_all_semanticallyEquivalent_ex_not (φ : L.BoundedFormula α (n + 1)) :
+    φ.all.not ⇔[T] φ.not.ex := fun M v xs => by simp
+
 theorem ex_iff_not_all_not (φ : L.BoundedFormula α (n + 1)) :
     φ.ex ⇔[T] φ.not.all.not := fun M v xs => by simp
 
+theorem not_ex_semanticallyEquivalent_all_not (φ : L.BoundedFormula α (n + 1)) :
+    φ.ex.not ⇔[T] φ.not.all := fun M v xs => by simp
+
 theorem iff_all_liftAt : φ ⇔[T] (φ.liftAt 1 n).all :=
   fun M v xs => by
   rw [realize_iff, realize_all_liftAt_one_self]

Mathlib/ModelTheory/Semantics.lean

@@ -235,6 +235,10 @@ variable {v : α → M} {xs : Fin l → M}
 theorem realize_bot : (⊥ : L.BoundedFormula α l).Realize v xs ↔ False :=
   Iff.rfl
 
+@[simp]
+theorem realize_falsum : (falsum : L.BoundedFormula α l).Realize v xs ↔ False :=
+  Iff.rfl
+
 @[simp]
 theorem realize_not : φ.not.Realize v xs ↔ ¬φ.Realize v xs :=
   Iff.rfl

Mathlib/ModelTheory/Syntax.lean

@@ -366,11 +366,21 @@ protected def ex (φ : L.BoundedFormula α (n + 1)) : L.BoundedFormula α n :=
 instance : Top (L.BoundedFormula α n) :=
   ⟨BoundedFormula.not ⊥⟩
 
+/-- The conjunction of two bounded formulas is also a bounded formula. -/
+@[match_pattern]
+protected def inf (φ ψ : L.BoundedFormula α n) : L.BoundedFormula α n :=
+  (φ.imp ψ.not).not
+
 instance : Inf (L.BoundedFormula α n) :=
-  ⟨fun f g => (f.imp g.not).not⟩
+  ⟨fun f g => f.inf g⟩
+
+/-- The disjunction of two bounded formulas is also a bounded formula. -/
+@[match_pattern]
+protected def sup (φ ψ : L.BoundedFormula α n) : L.BoundedFormula α n :=
+  φ.not.imp ψ
 
 instance : Sup (L.BoundedFormula α n) :=
-  ⟨fun f g => f.not.imp g⟩
+  ⟨fun f g => f.sup g⟩
 
 /-- The biimplication between two bounded formulas. -/
 protected def iff (φ ψ : L.BoundedFormula α n) :=