Categoricity of dlo

FormalTextbookModelTheory.lean

@@ -1,4 +1,114 @@
--- This module serves as the root of the `FormalTextbookModelTheory` library.
--- Import modules here that should be built as part of the library.
-import FormalTextbookModelTheory.ForMathlib.DLO
-import FormalTextbookModelTheory.Basic
+import FormalTextbookModelTheory.ForMathlib2.Matrix
+import FormalTextbookModelTheory.ForMathlib2.Cardinal
+import FormalTextbookModelTheory.ForMathlib2.DLO
+
+---region automatically create leanblueprint
+
+import Lean.Elab.Print
+import Mathlib.Lean.Expr.Basic
+import Batteries.Tactic.PrintDependents
+
+set_option linter.hashCommand false
+
+open Lean Elab Command
+
+abbrev excludedRootNames : NameSet := NameSet.empty
+  |>.insert `Init
+  |>.insert `Lean
+  |>.insert `Qq
+  |>.insert `ImportGraph
+  |>.insert `ProofWidgets
+  |>.insert `Std
+  |>.insert `Aesop
+  |>.insert `Batteries
+  |>.insert `Mathlib
+
+def userDefinedModules : CommandElabM (Array Name) := do
+  let env ← getEnv
+  let allowedImports := env.allImportedModuleNames.filter (!excludedRootNames.contains ·.getRoot)
+  return allowedImports.qsort Name.lt
+
+def test_userDefinedModules : CommandElabM Unit := do
+  let modules ← userDefinedModules
+  logInfo modules.toList.toString
+
+def moduleNameToFileName (moduleName : Name) : System.FilePath :=
+  System.FilePath.addExtension (System.mkFilePath $ moduleName.toString.splitOn ".") "lean"
+
+def test_moduleNameToFileName : CommandElabM Unit := do
+  let modules ← userDefinedModules
+  let mut fnames := #[]
+  for module in modules do
+    fnames := fnames.push (moduleNameToFileName module)
+  logInfo fnames.toList.toString
+
+def userDefinedDecls : CommandElabM (Array Name) := do
+  let env ← getEnv
+  --
+  let mut modIdx : HashSet Nat := .empty
+  let mut modsSeen : NameSet := .empty
+  let allowedImports ← userDefinedModules
+  for imp in allowedImports do
+    if let some nm := env.getModuleIdx? imp then
+      modIdx := modIdx.insert nm
+      modsSeen := modsSeen.insert imp
+ --
+  let consts := env.constants
+  let newDeclNames := consts.fold (init := ({} : NameSet)) fun a b _c =>
+    match env.getModuleIdxFor? b with
+      | none => a
+      | some idx => if modIdx.contains idx then a.insert b else a
+  --
+  let mut newDeclNamesFiltered := #[]
+  for decl in newDeclNames do
+    if decl.isAnonymous then
+      continue
+    if decl.isNum then
+      continue
+    if decl.isAuxLemma then
+      continue
+    if decl.isInternal then
+      continue
+    if decl.isInternalDetail then
+      continue
+    if decl.isImplementationDetail then
+      continue
+    if decl.isInaccessibleUserName then
+      continue
+    newDeclNamesFiltered := newDeclNamesFiltered.push decl
+  return newDeclNamesFiltered.qsort Name.lt
+
+def test_userDefinedDecls : CommandElabM Unit := do
+  let decls ← userDefinedDecls
+  logInfo decls.size.repr
+  logInfo decls.toList.toString
+
+def getDocstring (decl : Name) : CoreM (Option String) := do
+  return ← findDocString? (← getEnv) decl
+
+def test_getDocstring : CoreM Unit := do
+  let doc ← getDocstring `FirstOrder.Language.Order.DLO.aleph0_categorical_of_dlo
+  IO.println doc
+
+
+/-- extracts the names of the declarations in `env` on which `decl` depends. -/
+-- source:
+-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Counting.20prerequisites.20of.20a.20theorem/near/425370265
+def getVisited (env : Environment) (decl : Name) :=
+  let (_, { visited, .. }) := Elab.Command.CollectAxioms.collect decl |>.run env |>.run {}
+  visited
+
+def getDependencies (decl : Name) : CommandElabM (Array Name) := do
+  let env ← getEnv
+  let visited := (getVisited env decl).toArray
+  let decls ← userDefinedDecls
+  let visited := visited.filter $ fun name => name ∈ decls ∧ name ≠ decl
+  return visited
+
+#eval test_userDefinedModules
+#eval test_moduleNameToFileName
+#eval test_userDefinedDecls
+#eval test_getDocstring
+#eval (getDependencies `FirstOrder.Language.Order.orderStructure_of_LE)
+
+--end

FormalTextbookModelTheory/ForMathlib/DLO.lean

@@ -3,19 +3,34 @@ import Mathlib.ModelTheory.Basic
 import Mathlib.ModelTheory.Syntax
 import Mathlib.ModelTheory.Semantics
 import Mathlib.ModelTheory.Satisfiability
+import Mathlib.ModelTheory.Bundled
 import Mathlib.ModelTheory.Order
+import Mathlib.Order.CountableDenseLinearOrder
+import FormalTextbookModelTheory.ForMathlib.Order
 
 open Cardinal
 open FirstOrder
+open Language
+open Order
 
-universe u v w
+namespace FirstOrder.Language.Order
 
-notation "L≤" => Language.order
+-- def to_Lle_homomorphism {M N : Type w} [L≤.Structure M] [L≤.Structure N] (f : M →o N) : M →[L≤] N :=
+--   by sorry
 
 theorem aleph0_categorical_of_dlo : aleph0.Categorical L≤.dlo := by
+  unfold Categorical
+  rintro ⟨M⟩ ⟨N⟩ hM hN
+  simp only at *
+  constructor
+
+  have instLinearOrderM : LinearOrder M := by exact inst_LinearOrder_of_dlo L≤
+  have instLinearOrderN : LinearOrder N := by exact inst_LinearOrder_of_dlo L≤
+  have instDensolyOrderedM : @DenselyOrdered M (inst_Preorder_of_dlo L≤).toLT := by
+    exact inst_DenselyOrdered_of_dlo L≤
+
   sorry
 
-#check aleph0_categorical_of_dlo
+#check iso_of_countable_dense
 
--- Here, we will put definitions and theorems about the theory
--- of dense linear orders without endpoints.
+end FirstOrder.Language.Order

FormalTextbookModelTheory/ForMathlib/Language.lean

@@ -0,0 +1,87 @@
+import Mathlib.SetTheory.Cardinal.Basic
+import Mathlib.ModelTheory.Basic
+import Mathlib.ModelTheory.Satisfiability
+import Mathlib.ModelTheory.Order
+
+universe u v w
+
+open Cardinal
+open FirstOrder Language Structure
+
+namespace FirstOrder.Language
+
+class IsRelational₂ (L : Language.{u, v}) extends IsRelational L : Prop where
+  only_rel₂ : ∀ {n}, n ≠ 2 → IsEmpty (L.Relations n)
+
+namespace Structure --region Structure
+
+variable {L : Language.{u, v}} {M : Type w}
+
+section Relational
+
+lemma funMap_eq_funMap_of_relational [IsRelational L] (𝓜₁ 𝓜₂ : L.Structure M)
+    : @funMap L M 𝓜₁ = @funMap L M 𝓜₂ := by
+  rw [Subsingleton.elim (@funMap L M 𝓜₁) (@funMap L M 𝓜₂)]
+
+lemma funMap_eq_funMap_of_relational' [IsRelational L] (𝓜₁ 𝓜₂ : L.Structure M)
+    {n} (nFun : L.Functions n) (x : Fin n → M)
+    : 𝓜₁.funMap nFun x = 𝓜₂.funMap nFun x := by
+  rw [Subsingleton.elim (𝓜₁.funMap) (𝓜₂.funMap)]
+
+@[ext]
+lemma structure_eq_structure_of_relational [IsRelational L]
+    {𝓜₁ 𝓜₂ : L.Structure M} (h : @RelMap L M 𝓜₁ = @RelMap L M 𝓜₂) : 𝓜₁ = 𝓜₂ := by
+  ext1
+  · apply funMap_eq_funMap_of_relational
+  · apply h
+
+lemma structure_eq_of_structure_of_relational_iff [IsRelational L]
+    {𝓜₁ 𝓜₂: L.Structure M} : 𝓜₁ = 𝓜₂ ↔ @RelMap L M 𝓜₁ = @RelMap L M 𝓜₂ := by
+  constructor <;> intro h
+  · simp only [h, implies_true]
+  · ext1; exact h
+
+lemma structure_eq_of_structure_of_relational_iff' [IsRelational L]
+    {𝓜₁ 𝓜₂: L.Structure M} : 𝓜₁ = 𝓜₂ ↔ ∀ {n} r x, @RelMap L M 𝓜₁ n r x = @RelMap L M 𝓜₂ n r x := by
+  constructor <;> intro h
+  · simp only [h, implies_true]
+  · ext1; funext n r x; exact h r x
+
+end Relational
+
+section Relational₂
+
+lemma RelMap_eq_RelMap_of_relational₂ [IsRelational₂ L] (𝓜₁ 𝓜₂ : L.Structure M)
+    {n} (hn : n ≠ 2) : @RelMap L M 𝓜₁ n = @RelMap L M 𝓜₂ n := by
+  have : IsEmpty (L.Relations n) := by exact IsRelational₂.only_rel₂ hn
+  rw [Subsingleton.elim (@RelMap L M 𝓜₁ n) (@RelMap L M 𝓜₂ n)]
+
+lemma RelMap_eq_RelMap_of_relational₂' [IsRelational₂ L] (𝓜₁ 𝓜₂ : L.Structure M)
+    {n} (hn : n ≠ 2) (nRel : L.Relations n) (x : Fin n → M) :
+    𝓜₁.RelMap nRel x ↔ 𝓜₂.RelMap nRel x := by
+  have : IsEmpty (L.Relations n) := by exact IsRelational₂.only_rel₂ hn
+  rw [Subsingleton.elim (𝓜₁.RelMap) (𝓜₂.RelMap)]
+
+@[ext]
+lemma structure_eq_structure_of_relational₂ [IsRelational₂ L]
+    {𝓜₁ 𝓜₂ : L.Structure M}
+    (h : @RelMap L M 𝓜₁ 2 = @RelMap L M 𝓜₂ 2) : 𝓜₁ = 𝓜₂ := by
+  ext1
+  funext n
+  by_cases h' : n = 2
+  · subst h'
+    exact h
+  · apply RelMap_eq_RelMap_of_relational₂
+    exact h'
+
+lemma structure_eq_of_structure_of_relational₂_iff [IsRelational₂ L]
+    {𝓜₁ 𝓜₂ : L.Structure M} : 𝓜₁ = 𝓜₂ ↔ @RelMap L M 𝓜₁ 2 = @RelMap L M 𝓜₂ 2 := by
+  constructor <;> intro h
+  · simp only [h, implies_true]
+  · ext1; exact h
+
+end Relational₂
+
+end Structure --end
+
+end FirstOrder.Language

FormalTextbookModelTheory/ForMathlib/Matrix.lean

@@ -0,0 +1,27 @@
+import Mathlib.Data.Fin.VecNotation
+import Mathlib.Logic.Equiv.Fin
+
+namespace Matrix
+
+variable {α : Type*}
+
+lemma Vector_eq_VecNotation₂ (v : Fin 2 → α) : v = ![v 0, v 1] := by
+  simp only [vecCons]
+  induction (‹_› : Fin _ → α) using Fin.consCases
+  simp only [Fin.cons_eq_cons]
+  induction (‹_› : Fin _ → α) using Fin.consCases
+  simp only [Fin.cons_eq_cons]
+  simp only [Fin.cons_zero, Fin.cons_one, true_and]
+  apply (by infer_instance : Subsingleton (Fin 0 → α)).allEq
+
+end Matrix
+
+/-
+lemma Vector_eq_VecNotation (v : Fin 2 → α) : v = ![v 0, v 1] := by
+  simp only [vecCons]
+
+  repeat induction (‹_› : Fin _ → α) using Fin.consCases; simp only [Fin.cons_eq_cons]
+
+  simp [Fin.cons_zero, Fin.cons_one]
+  apply (by infer_instance : Subsingleton (Fin 0 → α)).allEq
+-/