Codyroux/compactness (teorth#123)

* [DO NOT MERGE] Define a proof theory for the equational logic of magmas. For now just soundness. * Start adding theorems to the blueprint, clean up notation in Lean. * Fix some rebase snafus, improve notation. * Add a brief overview of the completness theorem. * Nix bluprint \lean pragmas for now, to fix build. * [FEAT] Prove compactness theorem for formal magmas. * Remove blueprint pragmas, for now. * Minor cleanup. * Minor cleanup * Fix broken proof. * Update equational_theories.lean * partial update of intro --------- Co-authored-by: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
b-mehta · Sep 30, 2024 · 25d8c48 · 25d8c48
1 parent 4908465
commit 25d8c48
Show file tree

Hide file tree

Showing 6 changed files with 334 additions and 1 deletion.
diff --git a/Unidecode-1.3.8-py3-none-any.whl b/Unidecode-1.3.8-py3-none-any.whl
diff --git a/blueprint/src/chapter/intro.tex b/blueprint/src/chapter/intro.tex
@@ -49,7 +49,14 @@ \chapter{Basic theory of magmas}
 $$ \pi_*(1 \circ (0 \circ 1)) = 2 \circ (1 \circ 2)$$
 and so forth.
 
-\begin{definition}[Law]\label{law-def}\uses{induced-def}  Let $X$ be a set. A \emph{law} with alphabet $X$ is a formal expression of the form $w \formaleq w'$, where $w, w' \in M_X$ are words with alphabet $X$ (thus one can identify laws with alphabet $X$ with elements of $M_X \times M_X$).  A magma $G$ \emph{satisfies} the law $w \formaleq w'$ if we have $\varphi_f( w ) = \varphi_f ( w' )$ for all $f: X \to G$, in which case we write $G \models w \formaleq w'$.
+\begin{definition}[Law]\label{law-def}
+  \lean{MagmaLaw}\leanok
+  \uses{induced-def}
+  Let $X$ be a set. A \emph{law} with alphabet $X$ is a formal expression of the form $w \formaleq w'$,
+  where $w, w' \in M_X$ are words with alphabet $X$ (thus one can identify laws with alphabet $X$
+  with elements of $M_X \times M_X$).  A magma $G$ \emph{satisfies} the law $w \formaleq w'$ if
+  we have $\varphi_f( w ) = \varphi_f ( w' )$ for all $f: X \to G$, in which case we write
+  $G \models w \formaleq w'$.
 \end{definition}
 
 Thus, for instance, the commutative law
@@ -62,6 +69,41 @@ \chapter{Basic theory of magmas}
 \end{equation}
 for all $x, y \in G$.  We refer to \eqref{comm-law-2} as the \emph{equation} associated to the law \eqref{comm-law}.  One can think of equations as the ``semantic'' intrepretation of a ``syntactic'' law.  However, we shall often abuse notation and a law with its associated equation thus we shall (somewhat carelessly) also refer to \eqref{comm-law-2} as ``the commutative law'' (rather than ``the commutative equation'').
 
+\begin{definition}[Models]\label{models-def}
+  \lean{models}\leanok
+  \uses{law-def}
+  Given an arbitrary set $\Gamma$ of laws, a magma $G$ is a \emph{model} of $\Gamma$ with the
+  (overloaded) notation $G\models\Gamma$ if $G\models w\formaleq w'$ for every $w\formaleq w'$ in $\Gamma$.
+\end{definition}
+
+\begin{definition}[Derivation]\label{derivation-def}
+  \lean{derive}\leanok
+  \uses{law-def}
+  Given a set $\Gamma$ of laws and a law $w\formaleq w'$ over a fixed alphabet $X$, we say that
+  $\Gamma$ \emph{derives} $w\formaleq w'$, and write $\Gamma\vdash w\formaleq w'$, if the law can
+  be obtained using a finite number of applications of the following rules:
+  \begin{enumerate}
+    \item if $w\formaleq w' \in \Gamma$, then $\Gamma\vdash w\formaleq w'$
+    \item $\Gamma\vdash w\formaleq w$ for any word $w$
+    \item if $\Gamma\vdash w\formaleq w'$ then $\Gamma\vdash w'\formaleq w$
+    \item if $\Gamma\vdash w\formaleq w'$ and $\Gamma\vdash w'\formaleq w''$ then $\Gamma\vdash w\formaleq w''$
+    \item if $\Gamma\vdash w\formaleq w'$ then $\Gamma\vdash w\sigma\formaleq w'\sigma$, where $\sigma$ is an arbitrary map from $X$ to words in $M_X$ and $w\sigma$ replaces each occurence of an element of $X$ with it's image by $\sigma$ in $w$.
+    \item if $\Gamma\vdash w_1\formaleq w_2$ and $\Gamma\vdash w_3\formaleq w_4$ then $\Gamma\vdash w_1 \circ w_3\formaleq w2\circ w_4$
+  \end{enumerate}
+\end{definition}
+
+This definition is useful because of the following theorem:
+
+\begin{theorem}[Completeness]\label{sound-complete} (Birkhoff's completeness theorem)
+  \lean{Completeness}\leanok
+  For any set of laws $\Gamma$ and words $w, w'$ over a fixed alphabet
+  $$ \Gamma\vdash w\formaleq w'\ \mathrm{iff}\ \Gamma\models w\formaleq w' $$
+\end{theorem}
+\begin{proof}
+  \leanok
+  TODO.
+\end{proof}
+
 \begin{lemma}[Pushforward]\label{push}\uses{law-def}  Let $w \formaleq w'$ be a law with some alphabet $X$, $G$ be a magma, and $\pi: X \to Y$ be a function.  If $G \models w \formaleq w'$, then $G \models \pi_*(w) \formaleq \pi_*(w')$.  In particular, if $\pi$ is a bijection, the statements If $G \models w \formaleq w'$, then $G \models \pi_*(w) \formaleq \pi_*(w')$ are equivalent.
 \end{lemma}
 

diff --git a/equational_theories.lean b/equational_theories.lean
@@ -1,3 +1,5 @@
+import equational_theories.Completeness
+import equational_theories.Compactness
 import equational_theories.FreeMagma
 import equational_theories.Subgraph
 import equational_theories.AllEquations

diff --git a/equational_theories/Compactness.lean b/equational_theories/Compactness.lean
@@ -0,0 +1,74 @@
+import equational_theories.Completeness
+import Mathlib.Data.Finset.Basic
+
+def derive.getAxioms {α} [DecidableEq α] {Γ : Ctx α} {E : MagmaLaw α}(h : Γ ⊢ E) : Finset (MagmaLaw α) :=
+match h with
+| .Ax _ E _ => {E}
+| .Ref _ _ => {}
+| .Sym _ _ _ h => derive.getAxioms h
+| .Trans _ _ _ _ h₁ h₂ => derive.getAxioms h₁ ∪ derive.getAxioms h₂
+| .Subst _ _ _ _ h => derive.getAxioms h
+| .Cong _ _ _ _ _ h₁ h₂ => derive.getAxioms h₁ ∪ derive.getAxioms h₂
+
+def ToCtx {α} (S : Set (MagmaLaw α)) : Ctx α := S
+
+instance Ctx.hasSubset {α} : HasSubset (Ctx α) := Set.instHasSubset
+
+theorem foo (S T : Set Nat) : S ⊆ S ∪ T :=
+by exact Set.subset_union_left
+
+def derive.Weak {α} {Γ Δ : Ctx α}{E : MagmaLaw α}(inc : Γ ⊆ Δ) (h : Γ ⊢ E) :
+  Δ ⊢ E :=
+by
+  cases h
+  case Ax => apply derive.Ax; apply inc; trivial
+  case Ref => apply derive.Ref
+  case Sym => apply derive.Sym; apply derive.Weak <;> trivial
+  case Trans => apply derive.Trans <;> try apply derive.Weak <;> trivial
+  case Subst => apply derive.Subst ; apply derive.Weak <;> trivial
+  case Cong => apply derive.Cong <;> apply derive.Weak <;> trivial
+
+def derive.getAxiomsEnough {α} [DecidableEq α] {Γ : Ctx α} {E : MagmaLaw α}(h : Γ ⊢ E) :
+  ToCtx (derive.getAxioms h) ⊢ E :=
+by
+  cases h <;> simp [ToCtx, getAxioms]
+  case Ax =>
+    constructor; simp
+  case Ref =>
+    apply derive.Ref
+  case Sym _ _ h =>
+    apply derive.Sym
+    apply derive.getAxiomsEnough
+  case Trans _ _ _ h₁ h₂ =>
+    apply derive.Trans
+    . have j := derive.getAxiomsEnough h₁
+      apply derive.Weak
+      . apply Set.subset_union_left
+      . exact j
+    . have j := derive.getAxiomsEnough h₂
+      apply derive.Weak
+      . apply Set.subset_union_right
+      . exact j
+  case Subst =>
+    apply derive.Subst
+    apply derive.getAxiomsEnough
+  case Cong _ _ _ h₁ h₂ =>
+    apply derive.Cong
+    . have j := derive.getAxiomsEnough h₁
+      apply derive.Weak
+      . apply Set.subset_union_left
+      . exact j
+    . have j := derive.getAxiomsEnough h₂
+      apply derive.Weak
+      . apply Set.subset_union_right
+      . exact j
+
+def Compactness {α} [DecidableEq α] {Γ : Ctx α} {E : MagmaLaw α}(h : Γ ⊧ E) :
+  ∃ (Δ : Finset (MagmaLaw α)), Nonempty <| ToCtx Δ ⊧ E :=
+by
+  have h' := Completeness _ _ h
+  have ⟨ h'' ⟩ := h'
+  exists (derive.getAxioms h'')
+  constructor
+  apply Soundness
+  apply derive.getAxiomsEnough
diff --git a/equational_theories/Completeness.lean b/equational_theories/Completeness.lean
@@ -0,0 +1,213 @@
+-- Statement and proof of the completeness theorem for magmas,
+-- we roughly follow Baader & Nipkow's "Term Rewriting and All That",
+-- and
+import equational_theories.FreeMagma
+import Mathlib.Data.Set.Defs
+
+structure MagmaLaw (α : Type) where
+  lhs : FreeMagma α
+  rhs : FreeMagma α
+deriving DecidableEq
+
+local infix:60 " ≃ " => MagmaLaw.mk
+
+def substFreeMagma {α β} (t : FreeMagma α) (σ : α → FreeMagma β) : FreeMagma β :=
+match t with
+| .Leaf a => σ a
+| t₁ ⋆ t₂ => substFreeMagma t₁ σ ⋆ substFreeMagma t₂ σ
+
+infix:66 " ⬝ " => substFreeMagma
+
+@[inline, simp]
+def Ctx α := Set (MagmaLaw α)
+
+-- FIXME: figure out how to remove this.
+instance Ctx.Membership α : Membership (MagmaLaw α) (Ctx α) := ⟨ Set.instMembership.mem ⟩
+
+section DeriveDef
+
+set_option hygiene false
+
+local infix:50 " ⊢ " =>  derive
+
+-- We keep this in type, because we're going to want to gather
+-- the (finite!) set of required axioms later.
+inductive derive {α} : Ctx α → MagmaLaw α → Type :=
+| Ax Γ E (h : E ∈ Γ) : Γ ⊢ E
+| Ref Γ t : Γ ⊢ (t ≃ t)
+| Sym Γ t u : Γ ⊢ (t ≃ u) → Γ ⊢ (u ≃ t)
+| Trans Γ t u v : Γ ⊢ (t ≃ u) → Γ ⊢ (u ≃ v) → Γ ⊢ (t ≃ v)
+-- This is not as polymorphic as it could be, shouldn't be an issue at the moment
+| Subst Γ t u σ : Γ ⊢ (t ≃ u) → Γ ⊢ (t ⬝ σ ≃ u ⬝ σ)
+| Cong Γ t₁ t₂ u₁ u₂ : Γ ⊢ (t₁ ≃ t₂) → Γ ⊢ (u₁ ≃ u₂) → Γ ⊢ (t₁ ⋆ u₁ ≃ t₂ ⋆ u₂)
+
+end DeriveDef
+
+def satisfiesPhi {α G : Type} [Magma G] (φ : α → G) (E : MagmaLaw α) : Prop :=
+  evalInMagma φ E.lhs = evalInMagma φ E.rhs
+
+def satisfies {α : Type} (G : Type) [Magma G] (E : MagmaLaw α) := ∀ (φ : α → G), satisfiesPhi φ E
+
+def satisfiesSet {α : Type} (G : Type) [Magma G] (Γ : Set (MagmaLaw α)) : Prop :=
+  ∀ E ∈ Γ, satisfies G E
+
+
+def models {α} (Γ : Ctx α) (E : MagmaLaw α) : Prop :=
+  ∀ (G : Type)[Magma G], satisfiesSet G Γ → satisfies G E
+
+infix:50 " ⊧ " => (satisfies)
+
+infix:50 " ⊧ " => (satisfiesSet)
+
+infix:50 " ⊧ " => (models)
+
+infix:50 " ⊢ " => (derive)
+
+theorem SubstEval {α} G [Magma G] (t : FreeMagma α) (σ : α → FreeMagma α) (φ : α → G) :
+  evalInMagma φ (t ⬝ σ) = evalInMagma (evalInMagma φ ∘ σ) t :=
+by
+  cases t
+  case Leaf => simp [evalInMagma, substFreeMagma]
+  case Fork t₁ t₂ =>
+  simp [evalInMagma, substFreeMagma]
+  repeat rw [SubstEval]
+
+theorem Soundness {α} (Γ : Ctx α) E (h : Γ ⊢ E) : Γ ⊧ E :=
+by
+  intros G _
+  cases h
+  case Ax mem => intros mset; apply mset; trivial
+  case Ref => intros; intro; simp[satisfiesPhi]
+  -- FIXME: try aesop here, might be a 1-liner
+  case Sym t u prf =>
+    intros φ mset
+    have h := Soundness _ _ prf
+    simp [models, satisfiesPhi] at *
+    symm; apply h; trivial
+  case Trans _ _ _ prf₁ prf₂ =>
+    intros φ mset
+    have h₁ := Soundness _ _ prf₁
+    have h₂ := Soundness _ _ prf₂
+    simp [models, satisfiesPhi] at *
+    rw [h₁, h₂] <;> trivial
+  case Subst t u σ prf =>
+    intros φ mset
+    have h := Soundness _ _ prf
+    simp [models, satisfiesPhi, evalInMagma] at *
+    repeat rw [SubstEval]
+    rw [h]; trivial
+  case Cong _ _ _ prf₁ prf₂ =>
+    intros _ _
+    have h₁ := Soundness _ _ prf₁
+    have h₂ := Soundness _ _ prf₂
+    simp [models, satisfiesPhi, evalInMagma] at *
+    rw [h₁, h₂] <;> trivial
+
+-- A little trickery here: since we'd rather have the derivations in Type
+-- (we want to extract the "used" axioms, e.g.) we smush the derivation
+-- down to prop using Nonempty for creating a setoid.
+def RelOfLaws {α} (Γ : Ctx α) : FreeMagma α → FreeMagma α → Prop :=
+  λ t u ↦ Nonempty (Γ ⊢ t ≃ u)
+
+-- eazy peezy since we basically have exactly the axioms.
+theorem RelOfLaws.isEquivalence {α} (Γ : Ctx α) : Equivalence (RelOfLaws Γ) :=
+by
+  constructor <;> simp [RelOfLaws]
+  case refl =>
+    intros x; constructor; apply derive.Ref
+  case symm => intros x y h; cases h; constructor; apply derive.Sym; trivial
+  case trans =>
+    intros x y z h₁ h₂; cases h₁; cases h₂; constructor; apply derive.Trans <;> trivial
+
+instance SetoidOfLaws {α} (Γ : Ctx α): Setoid (FreeMagma α) :=
+  ⟨ RelOfLaws Γ, RelOfLaws.isEquivalence Γ ⟩
+
+
+-- This is the quotient type we care about: it will be a model of Γ.
+def FreeMagmaWithLaws {α} (Γ : Ctx α) : Type := Quotient (SetoidOfLaws Γ)
+
+@[simp]
+def embed {α} (Γ : Ctx α) (x : FreeMagma α) : FreeMagmaWithLaws Γ := Quotient.mk _ x
+
+def ForkWithLaws {α} (Γ : Ctx α) : FreeMagmaWithLaws Γ → FreeMagmaWithLaws Γ → FreeMagmaWithLaws Γ :=
+Quotient.lift₂ (λ x y ↦ embed Γ (x ⋆ y))
+(
+  by
+    simp [HasEquiv.Equiv, Setoid.r, RelOfLaws]
+    intros x z y w d₁ d₂; cases d₁; cases d₂
+    apply Quotient.sound; simp [HasEquiv.Equiv, Setoid.r, RelOfLaws]; constructor
+    apply derive.Cong <;> trivial
+)
+
+instance FreeMagmaWithLaws.Magma {α} (Γ : Ctx α) : Magma (FreeMagmaWithLaws Γ) := { op := ForkWithLaws Γ }
+
+theorem FreeMagmaWithLaws.evalInMagmaIsQuot {α} (Γ : Ctx α) (t : FreeMagma α) (σ : α → FreeMagma α):
+  evalInMagma (embed Γ ∘ σ) t = embed Γ (t ⬝ σ) :=
+by
+  cases t <;> simp [evalInMagma]
+  case Leaf => trivial
+  case Fork =>
+  simp [Magma.op, ForkWithLaws]
+  repeat rw [FreeMagmaWithLaws.evalInMagmaIsQuot]
+  simp [Quotient.lift₂, Quotient.mk, Quotient.lift]
+  apply Quot.sound; simp [Setoid.r, RelOfLaws, substFreeMagma]
+  constructor; apply derive.Ref
+
+theorem substLFId {α} (t : FreeMagma α) : t ⬝ Lf = t :=
+by
+  cases t <;> simp [substFreeMagma]
+  constructor <;> apply substLFId
+
+
+@[simp]
+def LfEmbed {α} (Γ : Ctx α) : α → FreeMagmaWithLaws Γ := embed Γ ∘ Lf
+
+-- Mostly forward reasoning here, so we delay the intros.
+theorem FreeMagmaWithLaws.isDerives {α} (Γ : Ctx α) (E : MagmaLaw α) :
+  FreeMagmaWithLaws Γ ⊧ E → Nonempty (Γ ⊢ E) :=
+by
+  simp [satisfies, satisfiesPhi, evalInMagma]
+  intros eq; have h := (eq (LfEmbed Γ))
+  simp at h
+  repeat rw [FreeMagmaWithLaws.evalInMagmaIsQuot] at h
+  have h' := Quotient.exact h
+  simp [HasEquiv.Equiv, Setoid.r, RelOfLaws] at h'
+  repeat rw [substLFId] at h'
+  apply h'
+
+-- Sadly, we falter here and use choice. Somewhat confident it's not needed.
+theorem PhiAsSubst_aux {α} (Γ : Ctx α) (φ : α → FreeMagmaWithLaws Γ) :
+  ∃ (σ : α → FreeMagma α), ∀ x, φ x = (embed Γ) (σ x) :=
+by
+  apply Classical.axiomOfChoice (r := λ x y ↦ φ x = (embed Γ) y)
+  intros x
+  have ⟨a, h⟩ := (Quotient.exists_rep (φ x))
+  exists a
+  symm; trivial
+
+theorem PhiAsSubst {α} (Γ : Ctx α) (φ : α → FreeMagmaWithLaws Γ) :
+  ∃ (σ : α → FreeMagma α), φ = (embed Γ) ∘ σ :=
+by
+  have ⟨ σ, h ⟩ := PhiAsSubst_aux Γ φ
+  exists σ
+  apply funext
+  trivial
+
+theorem FreeMagmaWithLaws.isModel {α} (Γ : Ctx α) : FreeMagmaWithLaws Γ ⊧ Γ :=
+by
+  simp [satisfiesSet]
+  intros E mem φ
+  simp [satisfiesPhi]
+  have ⟨σ, eq_sig⟩ := (PhiAsSubst _ φ)
+  rw [eq_sig]
+  repeat rw [FreeMagmaWithLaws.evalInMagmaIsQuot]
+  apply Quotient.sound; simp [HasEquiv.Equiv, Setoid.r, RelOfLaws]
+  constructor
+  apply derive.Subst; apply derive.Ax; trivial
+
+-- Birkhoff's completeness theorem
+theorem Completeness {α} (Γ : Ctx α) (E : MagmaLaw α) (h : Γ ⊧ E) : Nonempty (Γ ⊢ E) :=
+by
+  apply FreeMagmaWithLaws.isDerives
+  apply h
+  apply FreeMagmaWithLaws.isModel
diff --git a/equational_theories/FreeMagma.lean b/equational_theories/FreeMagma.lean
@@ -19,6 +19,8 @@ theorem FreeMagma_op_eq_fork (α : Type u) (a b : FreeMagma α) : a ∘ b = a
 
 notation "Lf" => FreeMagma.Leaf
 
+instance FreeMagma.Magma {α} : Magma (FreeMagma α) := ⟨ Fork ⟩
+
 def fmapFreeMagma {α : Type u} {β : Type v} (f : α → β) : FreeMagma α → FreeMagma β
   | Lf a => FreeMagma.Leaf (f a)
   | lchild ⋆ rchild => FreeMagma.Fork (fmapFreeMagma f lchild) (fmapFreeMagma f rchild)