METATHEOREM derivation preserves size (teorth#233)

Theorem: if `L ==> L'` then either `L'` is trivial (`w = w`) or `L'` is at least as large as `L`. We give a proof theoretic proof, a model theoretic might be nice as well, but this is still kind of cute. Re-created to replace teorth#152 --------- Co-authored-by: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
b-mehta · Oct 3, 2024 · aa110cf · aa110cf
1 parent c0fc978
commit aa110cf
Show file tree

Hide file tree

Showing 2 changed files with 52 additions and 0 deletions.
diff --git a/equational_theories.lean b/equational_theories.lean
@@ -8,5 +8,6 @@ import equational_theories.AllEquations
 import equational_theories.InfModel
 import equational_theories.Generated
 import equational_theories.Counting
+import equational_theories.OrderMetatheorem
 import equational_theories.SmallMagmas
 import equational_theories.Homomorphisms
diff --git a/equational_theories/OrderMetatheorem.lean b/equational_theories/OrderMetatheorem.lean
@@ -0,0 +1,51 @@
+import equational_theories.Completeness
+import equational_theories.Counting
+
+theorem FreeMagma.orderLtSubst {α} (t : FreeMagma α) (σ : α → FreeMagma α) :
+  FreeMagma.order t ≤ FreeMagma.order (t ⬝ σ) :=
+by
+  cases t <;> simp [order]
+  case Fork t u =>
+    have h₁ := FreeMagma.orderLtSubst t σ
+    have h₂ := FreeMagma.orderLtSubst u σ
+    omega
+
+open Law
+-- We use min here, as we want terms of *at least* size n.
+@[simp]
+def MagmaLaw.order {α} (E : MagmaLaw α) : Nat := min (FreeMagma.order E.lhs) (FreeMagma.order E.rhs)
+
+@[inline, simp]
+def Ctx.IsOfOrder {α} (Γ : Ctx α) (n : Nat) := ∀ E ∈ Γ, n ≤ MagmaLaw.order E
+
+theorem derive.PreservesOrder {α} (Γ : Ctx α) (n : Nat) (sizeBound : Ctx.IsOfOrder Γ n)
+    (E : MagmaLaw α) (h : Γ ⊢ E) :
+    E.lhs = E.rhs ∨ n ≤ MagmaLaw.order E := by
+  rw [or_iff_not_imp_left, ← ne_eq]
+  intro h2
+  induction h with
+  | Ax E h => exact sizeBound E h
+  | Ref t => simp at h2
+  | Sym t u _ ih => simpa [MagmaLaw.order, min_comm] using ih h2.symm
+  | Trans t u v _ _ ih₁ ih₂ =>
+    simp at ih₁ ih₂ h2 ⊢
+    by_cases h : t = u
+    · subst h
+      exact ih₂ h2
+    by_cases h3 : u = v
+    · subst h3
+      exact ih₁ h2
+    exact ⟨ih₁ h |>.1, ih₂ h3 |>.2⟩
+  | Subst t u σ _ ih =>
+    simp at ih h2 ⊢
+    specialize ih (by rintro rfl; contradiction)
+    exact ⟨ih.1.trans <| t.orderLtSubst σ, ih.2.trans <| u.orderLtSubst σ⟩
+  | Cong t₁ t₂ u₁ u₂ _ _ ih₁ ih₂ => 
+    simp at ih₁ ih₂ h2 ⊢
+    by_cases h : t₁ = t₂ <;> [specialize ih₂ (h2 h); specialize ih₁ h] <;> omega
+
+theorem models.PreservesOrder {α} (Γ : Ctx α) (n : Nat)(sizeBound : Ctx.IsOfOrder Γ n) (E : MagmaLaw α)(h : Γ ⊧ E) :
+  E.lhs = E.rhs ∨ n ≤ MagmaLaw.order E :=
+by
+  have ⟨ h ⟩ := Completeness _ _ h
+  apply derive.PreservesOrder <;> trivial