From e56b8fea84d60fe434632b9d3b829ee685fb0c8f Mon Sep 17 00:00:00 2001
From: Aaron Anderson <awainverse@gmail.com>
Date: Fri, 29 Apr 2022 20:31:25 +0000
Subject: [PATCH] feat(model_theory/graph): First-order language and theory of
 graphs (#13720)

Defines `first_order.language.graph`, the language of graphs
Defines `first_order.Theory.simple_graph`, the theory of simple graphs
Produces models of the theory of simple graphs from simple graphs and vice versa.
---
 src/model_theory/graph.lean | 113 ++++++++++++++++++++++++++++++++++++
 src/model_theory/order.lean |   6 +-
 2 files changed, 118 insertions(+), 1 deletion(-)
 create mode 100644 src/model_theory/graph.lean

diff --git a/src/model_theory/graph.lean b/src/model_theory/graph.lean
new file mode 100644
index 0000000000000..e5d2763808457
--- /dev/null
+++ b/src/model_theory/graph.lean
@@ -0,0 +1,113 @@
+/-
+Copyright (c) 2022 Aaron Anderson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Aaron Anderson
+-/
+import model_theory.satisfiability
+import combinatorics.simple_graph.basic
+
+/-!
+# First-Ordered Structures in Graph Theory
+This file defines first-order languages, structures, and theories in graph theory.
+
+## Main Definitions
+* `first_order.language.graph` is the language consisting of a single relation representing
+adjacency.
+* `simple_graph.Structure` is the first-order structure corresponding to a given simple graph.
+* `first_order.language.Theory.simple_graph` is the theory of simple graphs.
+* `first_order.language.simple_graph_of_structure` gives the simple graph corresponding to a model
+of the theory of simple graphs.
+
+-/
+
+universes u v w w'
+
+namespace first_order
+namespace language
+open_locale first_order
+open Structure
+
+variables {L : language.{u v}} {α : Type w} {V : Type w'} {n : ℕ}
+
+/-! ### Simple Graphs -/
+
+/-- The language consisting of a single relation representing adjacency. -/
+protected def graph : language :=
+language.mk₂ empty empty empty empty unit
+
+/-- The symbol representing the adjacency relation. -/
+def adj : language.graph.relations 2 := unit.star
+
+/-- Any simple graph can be thought of as a structure in the language of graphs. -/
+def _root_.simple_graph.Structure (G : simple_graph V) :
+  language.graph.Structure V :=
+Structure.mk₂ empty.elim empty.elim empty.elim empty.elim (λ _, G.adj)
+
+namespace graph
+
+instance : is_relational (language.graph) := language.is_relational_mk₂
+
+instance : subsingleton (language.graph.relations n) :=
+language.subsingleton_mk₂_relations
+
+end graph
+
+/-- The theory of simple graphs. -/
+protected def Theory.simple_graph : language.graph.Theory :=
+{adj.irreflexive, adj.symmetric}
+
+@[simp] lemma Theory.simple_graph_model_iff [language.graph.Structure V] :
+  V ⊨ Theory.simple_graph ↔
+    irreflexive (λ x y : V, rel_map adj ![x,y]) ∧ symmetric (λ x y : V, rel_map adj ![x,y]) :=
+by simp [Theory.simple_graph]
+
+instance simple_graph_model (G : simple_graph V) :
+  @Theory.model _ V G.Structure Theory.simple_graph :=
+begin
+  simp only [Theory.simple_graph_model_iff, rel_map_apply₂],
+  exact ⟨G.loopless, G.symm⟩,
+end
+
+variables (V)
+
+/-- Any model of the theory of simple graphs represents a simple graph. -/
+@[simps] def simple_graph_of_structure [language.graph.Structure V] [V ⊨ Theory.simple_graph] :
+  simple_graph V :=
+{ adj := λ x y, rel_map adj ![x,y],
+  symm := relations.realize_symmetric.1 (Theory.realize_sentence_of_mem Theory.simple_graph
+      (set.mem_insert_of_mem _ (set.mem_singleton _))),
+  loopless := relations.realize_irreflexive.1 (Theory.realize_sentence_of_mem Theory.simple_graph
+      (set.mem_insert _ _)) }
+
+variables {V}
+
+@[simp] lemma _root_.simple_graph.simple_graph_of_structure (G : simple_graph V) :
+  @simple_graph_of_structure V G.Structure _ = G :=
+by { ext, refl }
+
+@[simp] lemma Structure_simple_graph_of_structure
+  [S : language.graph.Structure V] [V ⊨ Theory.simple_graph] :
+  (simple_graph_of_structure V).Structure = S :=
+begin
+  ext n f xs,
+  { exact (is_relational.empty_functions n).elim f },
+  { ext n r xs,
+    rw iff_eq_eq,
+    cases n,
+    { exact r.elim },
+    { cases n,
+      { exact r.elim },
+      { cases n,
+        { cases r,
+          change rel_map adj ![xs 0, xs 1] = _,
+          refine congr rfl (funext _),
+          simp [fin.forall_fin_two], },
+        { exact r.elim } } } }
+end
+
+theorem Theory.simple_graph_is_satisfiable :
+  Theory.is_satisfiable Theory.simple_graph :=
+⟨@Theory.Model.of _ _ unit (simple_graph.Structure ⊥) _ _⟩
+
+end language
+end first_order
diff --git a/src/model_theory/order.lean b/src/model_theory/order.lean
index 0eeff59b2aad4..f483e7782e196 100644
--- a/src/model_theory/order.lean
+++ b/src/model_theory/order.lean
@@ -40,7 +40,9 @@ variables {L : language.{u v}} {α : Type w} {M : Type w'} {n : ℕ}
 protected def order : language :=
 language.mk₂ empty empty empty empty unit
 
-instance order.Structure [has_le M] : language.order.Structure M :=
+namespace order
+
+instance Structure [has_le M] : language.order.Structure M :=
 Structure.mk₂ empty.elim empty.elim empty.elim empty.elim (λ _, (≤))
 
 instance : is_relational (language.order) := language.is_relational_mk₂
@@ -48,6 +50,8 @@ instance : is_relational (language.order) := language.is_relational_mk₂
 instance : subsingleton (language.order.relations n) :=
 language.subsingleton_mk₂_relations
 
+end order
+
 /-- A language is ordered if it has a symbol representing `≤`. -/
 class is_ordered (L : language.{u v}) := (le_symb : L.relations 2)