diff --git a/AutoBlueprint/Latex/Basic.lean b/AutoBlueprint/Latex/Basic.lean deleted file mode 100644 index 3d5ad0a..0000000 --- a/AutoBlueprint/Latex/Basic.lean +++ /dev/null @@ -1,315 +0,0 @@ --- import Mathlib.ModelTheory.Basic -import Mathlib.Tactic.Linarith - -section - -def ite_lt [LT α] {x y : α} {flag : Prop} [Decidable flag] {z : α} (h₁ : x < z) (h₂ : y < z) - : (if flag then x else y) < z := by - by_cases hf : flag <;> {simp only [hf]; assumption} - -private def parse_line? (line : String) (field : String) : Option String := - let line := line.trim - if line.startsWith ("\\" ++ field ++ "{") && line.endsWith "}" then - let value := String.mk line.data.toArray[field.length + 2:line.length - 1].toArray.toList - if value.length > 0 then some value else none - else none - -private def parse_first_line? (line : String) : Option String := - parse_line? line "begin" - -private def parse_last_line? (line : String) : Option String := - parse_line? line "end" - -private def parse_label? (line : String) : Option String := - parse_line? line "label" - -private def parse_name? (line : String) : Option String := - parse_line? line "lean" - -private def parse_uses? (line : String) : Option (List String) := - let content := parse_line? line "uses" - match content with - | none => none - | some content => - let lst := List.map String.trim (content.splitOn ",") - some lst - -private def parse_content (lines : List String) : String := - String.intercalate "\n" (lines.filter (fun line => ¬ line.startsWith "\\")) - -private def split_environments? (s : String) : Option (String × String) := - let lines := List.map String.trim (s.splitOn "\n") - let begins := List.findIdxs (fun line => not (parse_first_line? line).isNone) lines - let ends := List.findIdxs (fun line => not (parse_last_line? line).isNone) lines - match hb : begins.length, he : ends.length with - | 2, 2 => - let begin₁ := begins[0] - let end₁ := ends[0] - let begin₂ := begins[1] - let end₂ := ends[1] - some ⟨String.intercalate "\n" (lines.toArray[begin₁:end₁ + 1].toArray.toList), - String.intercalate "\n" (lines.toArray[begin₂:end₂ + 1].toArray.toList)⟩ - | _, _ => none - - -end - -structure EnvironmentWithoutProof where - type : String - leanok : Bool - uses : List String - content : String - -namespace EnvironmentWithoutProof --region - -instance : ToString EnvironmentWithoutProof where - toString env := - "\\begin{" ++ env.type ++ "}\n" ++ - (if env.leanok then "\\leanok\n" else "") ++ - "\\uses{" ++ (String.intercalate ", " env.uses) ++ "}\n" ++ - env.content ++ "\n" ++ - "\\end{" ++ env.type ++ "}\n" - -def parse? (s : String) : Option EnvironmentWithoutProof := - let lines := List.map String.trim (s.splitOn "\n") - let len := lines.length - match h : len with - | 0 | 1 | 2 => none - | n + 3 => - let type_first? := parse_first_line? lines[0] - let type_last? := parse_last_line? lines[len - 1] - match type_first?, type_last? with - | _, none | none, _ => none - | some type, some type' => - if type ≠ type' then none else - let leanok := lines[1] == "\\leanok" - let uses_idx := if leanok then 2 else 1 - let uses? := parse_uses? (lines[uses_idx]'(by apply ite_lt <;> linarith)) - match uses? with - | none => none - | some uses => - let content := parse_content lines - some {type := type, leanok := leanok, uses := uses, content := content} - -end EnvironmentWithoutProof --end - -structure ProofEnvironment where - leanok : Bool - uses : List String - content : String - -def EnvironmentWithoutProof.toProofEnvironment {env : EnvironmentWithoutProof} (_ : env.type = "proof") - : ProofEnvironment := - {leanok := env.leanok, uses := env.uses, content := env.content} - -namespace ProofEnvironment --region - -def toEnvironmentWithoutProof (env : ProofEnvironment) : EnvironmentWithoutProof := - {env with type := "proof"} - -instance : Coe ProofEnvironment EnvironmentWithoutProof where - coe env := env.toEnvironmentWithoutProof - -instance : ToString ProofEnvironment where - toString env := toString (env : EnvironmentWithoutProof) - -def parse? (s : String) : Option ProofEnvironment := - let env? := EnvironmentWithoutProof.parse? s - match env? with - | none => none - | some env => - if h : env.type ≠ "proof" then none else - some $ env.toProofEnvironment (by push_neg at h; exact h) - -end ProofEnvironment --end - -structure EnvironmentWithProof where - type : String - label : String - name : String - leanok : Bool - uses : List String - content : String - proof : ProofEnvironment - -namespace EnvironmentWithProof --region - -instance : ToString EnvironmentWithProof where - toString env := - "\\begin{" ++ env.type ++ "}\n" ++ - "\\label{" ++ env.label ++ "}\n" ++ - "\\lean{" ++ env.name ++ "}\n" ++ - (if env.leanok then "\\leanok\n" else "") ++ - "\\uses{" ++ (String.intercalate ", " env.uses) ++ "}\n" ++ - env.content ++ "\n" ++ - "\\end{" ++ env.type ++ "}\n" ++ - toString env.proof - -def parse? (s : String) : Option EnvironmentWithProof := - let s? := split_environments? s - match s? with - | none => none - | some (s₁, s₂) => - let lines := List.map String.trim (s₁.splitOn "\n") - let len := lines.length - match h : len with - | 0 | 1 | 2 | 3 | 4 => none - | n + 5 => - let type_first? := parse_first_line? lines[0] - let type_last? := parse_last_line? lines[len - 1] - match type_first?, type_last? with - | _, none | none, _ => none - | some type, some type' => - if type ≠ type' then none else - let label? := parse_label? lines[1] - match label? with - | none => none - | some label => - let name? := parse_name? lines[2] - match name? with - | none => none - | some name => - let leanok := lines[3] == "\\leanok" - let uses_idx := if leanok then 4 else 3 - let uses? := parse_uses? (lines[uses_idx]'(by apply ite_lt <;> linarith)) - match uses? with - | none => none - | some uses => - let content := parse_content lines - let proof? := ProofEnvironment.parse? s₂ - match proof? with - | none => none - | some proof => - some {type := type, label := label, name := name, leanok := leanok, - uses := uses, content := content, proof := proof} - -end EnvironmentWithProof --end - -structure TheoremEnvironment where - label : String - name : String - leanok : Bool - uses : List String - content : String - proof : ProofEnvironment - -def EnvironmentWithProof.toTheoremEnvironment {env : EnvironmentWithProof} (_ : env.type = "theorem") - : TheoremEnvironment := - {label := env.label, name := env.name, leanok := env.leanok, - uses := env.uses, content := env.content, proof := env.proof} - -namespace TheoremEnvironment --region - -def toEnvironmentWithProof (env : TheoremEnvironment) : EnvironmentWithProof := - {env with type := "theorem"} - -instance : Coe TheoremEnvironment EnvironmentWithProof where - coe := toEnvironmentWithProof - -instance : ToString TheoremEnvironment where - toString env := toString (env : EnvironmentWithProof) - -def parse? (s : String) : Option TheoremEnvironment := - let env? := EnvironmentWithProof.parse? s - match env? with - | none => none - | some env => - if h : env.type ≠ "theorem" then none else - some $ env.toTheoremEnvironment (by push_neg at h; exact h) - -end TheoremEnvironment --end - -structure LemmaEnvironment where - label : String - name : String - leanok : Bool - uses : List String - content : String - proof : ProofEnvironment - -def EnvironmentWithProof.toLemmaEnvironment {env : EnvironmentWithProof} (_ : env.type = "lemma") - : LemmaEnvironment := - {label := env.label, name := env.name, leanok := env.leanok, - uses := env.uses, content := env.content, proof := env.proof} - -namespace LemmaEnvironment --region - -def toEnvironmentWithProof (env : LemmaEnvironment) : EnvironmentWithProof := - {env with type := "theorem"} - -instance : Coe LemmaEnvironment EnvironmentWithProof where - coe env := env.toEnvironmentWithProof - -instance : ToString LemmaEnvironment where - toString env := toString (env : EnvironmentWithProof) - -def parse? (s : String) : Option LemmaEnvironment := - let env? := EnvironmentWithProof.parse? s - match env? with - | none => none - | some env => - if h : env.type ≠ "lemma" then none else - some $ env.toLemmaEnvironment (by push_neg at h; exact h) - -end LemmaEnvironment --end - -namespace BlueprintLatex.Test --region - -def env₁ : ProofEnvironment where - leanok := false - uses := ["thm:merhaba"] - content := "This is a proof." - -def env₂ : TheoremEnvironment where - label := "thm:current_theorem" - name := "FirstOrder.Language.mytheorem" - leanok := true - uses := ["thm:old-theorem", "lem:old-lemma", "def:old-definition"] - content := "This is a very important theorem." - proof := env₁ - -#eval env₁ -#eval env₂ - -open EnvironmentWithoutProof - -def test_parse_line? : IO Unit := do - let line := "\\begin{merhaba}" - IO.println (parse_line? line "begin") - -def test_parse₁? : IO Unit := do - let stream ← IO.FS.Handle.mk "proof.tex" IO.FS.Mode.read - let s ← stream.readToEnd - let env? := parse? s - match env? with - | none => IO.println "No environment found" - | some env => - IO.println $ "type: " ++ env.type - IO.println $ "leanok: " ++ reprStr env.leanok - IO.println $ "uses: " ++ env.uses.toString - IO.println $ "content: " ++ env.content - -def test_splitEnvironment? : IO Unit := do - let stream ← IO.FS.Handle.mk "theorem.tex" IO.FS.Mode.read - let s ← stream.readToEnd - let envs? := split_environments? s - match envs? with - | none => IO.println "No environments found" - | some (env₁, env₂) => do - IO.println env₁ - IO.println env₂ - -def test_parse?_theorem : IO Unit := do - let stream ← IO.FS.Handle.mk "theorem.tex" IO.FS.Mode.read - let s ← stream.readToEnd - let env? := TheoremEnvironment.parse? s - match env? with - | none => IO.println "No theorem found" - | some env => IO.println env - -#eval test_parse_line? -#eval test_parse₁? -#eval test_splitEnvironment? -#eval test_parse?_theorem - -end BlueprintLatex.Test --end diff --git a/FormalTextbookModelTheory.lean b/FormalTextbookModelTheory.lean index 74bd313..3c10936 100644 --- a/FormalTextbookModelTheory.lean +++ b/FormalTextbookModelTheory.lean @@ -1,116 +1,2 @@ -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 (env : Environment) : Array Name := by - let allowedImports := env.allImportedModuleNames.filter (!excludedRootNames.contains ·.getRoot) - exact allowedImports.qsort Name.lt - -def test_userDefinedModules : CommandElabM Unit := do - let env ← getEnv - let modules := userDefinedModules env - 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 env ← getEnv - let modules := userDefinedModules env - let mut fnames := #[] - for module in modules do - fnames := fnames.push (moduleNameToFileName module) - logInfo fnames.toList.toString - -def userDefinedDecls (env : Environment) : Array Name := Id.run do - let mut modIdx : HashSet Nat := .empty - let mut modsSeen : NameSet := .empty - let allowedImports := userDefinedModules env - 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 env ← getEnv - let decls := userDefinedDecls env - logInfo decls.size.repr - logInfo decls.toList.toString - -def getDocstring (env : Environment) (decl : Name) : IO $ Option String := do - return ← findDocString? env decl - -def test_getDocstring : CoreM Unit := do - let env ← getEnv - let doc ← getDocstring env `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) : NameSet := - 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 env - 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 +import FormalTextbookModelTheory.ForMathlib.Matrix +import FormalTextbookModelTheory.ForMathlib.DLO diff --git a/FormalTextbookModelTheory/ForMathlib/DLO.lean b/FormalTextbookModelTheory/ForMathlib/DLO.lean index 83e7352..fb08c28 100644 --- a/FormalTextbookModelTheory/ForMathlib/DLO.lean +++ b/FormalTextbookModelTheory/ForMathlib/DLO.lean @@ -6,31 +6,241 @@ import Mathlib.ModelTheory.Satisfiability import Mathlib.ModelTheory.Bundled import Mathlib.ModelTheory.Order import Mathlib.Order.CountableDenseLinearOrder -import FormalTextbookModelTheory.ForMathlib.Order + +import FormalTextbookModelTheory.ForMathlib.Matrix + open Cardinal -open FirstOrder -open Language -open Order +open FirstOrder Language Structure Theory Order +open Matrix (Vector_eq_VecNotation₂ comp_VecNotation₂) + +namespace FirstOrder.Language.Order --region + +section + +variable {M : Type w} [instStructure : Language.order.Structure M] + +/-- +The interpretation of the unique binary relation symbol of the language `Language.order` on a type `M` gives a +natural binary relation on `M` and it is written with `≤`. +-/ +instance instLE : LE M where + le := fun x y => instStructure.RelMap leSymb ![x, y] + +/-- +Given a type `M` and `𝓜 : Language.order.Structure`, the `Language.order.Structure M` instance induced by the `LE M` +instance which is induced by `𝓜` is equal to `𝓜`. In other words, for a fixed type `M`, `@orderStructure M` is the +left-inverse of `@instLE M`. +-/ +@[simp] +lemma orderStructure_of_LE : @orderStructure M (@instLE M instStructure) = instStructure := by + ext1 + · funext _ r + exfalso + exact IsEmpty.elim (by infer_instance) r + · funext n r x + match n with + | 0 | 1 | _ + 3 => + exfalso + simp only [Language.order, mk₂_Relations, Sequence₂] at r + exact IsEmpty.elim (by infer_instance) r + | 2 => + rw [Vector_eq_VecNotation₂ x, (by apply Subsingleton.allEq : r = leSymb)] + simp only [orderStructure, LE.le, Structure.relMap_apply₂] + +/-- +By definition, the binary relation `≤` is equal to the interpretation of the unique binary relation symbol of the +language `Language.order`. +-/ +instance : @OrderedStructure Language.order M _ instLE instStructure := by + simp only [OrderedStructure, orderLHom_order, orderStructure_of_LE] + exact @LHom.id_isExpansionOn Language.order M instStructure + +end + +section + +variable {M : Type w} [Language.order.Structure M] +variable {N : Type w} [Language.order.Structure N] + +/-- +An order embedding `φ : M ↪o N`, induces and embedding of structures with the same underlying function. +-/ +def toLEmbedding (φ : M ↪o N) : M ↪[Language.order] N where + toEmbedding := φ.toEmbedding + map_fun' := by + intro n f + exfalso + exact IsEmpty.elim (by infer_instance) f + map_rel' := by + intro n r x + match n with + | 0 | 1 | _ + 3 => + exfalso + simp [Language.order, Sequence₂] at r + exact IsEmpty.elim (by infer_instance) r + | 2 => + rw [Vector_eq_VecNotation₂ x, comp_VecNotation₂ φ.toFun, + (by apply Subsingleton.allEq : r = leSymb), relMap_leSymb, relMap_leSymb] + exact φ.map_rel_iff + +/-- +An order isomorphism `φ : M ≃o N`, induces and isomorphism of structures with the same underlying function. +-/ +def toLIso (φ : M ≃o N) : M ≃[Language.order] N where + toEquiv := φ.toEquiv + map_fun' := (toLEmbedding (φ.toOrderEmbedding)).map_fun' + map_rel' := (toLEmbedding (φ.toOrderEmbedding)).map_rel' + +end + +namespace DLO --region + +section + +variable (M : Type w) [Language.order.Structure M] +variable [M ⊨ Language.order.dlo] + +/-- +Models of the theory `Language.order.dlo` satisfies the reflexivity sentence. +-/ +protected lemma realize_reflexive : M ⊨ (leSymb (L := Language.order)).reflexive := by + apply realize_sentence_of_mem Language.order.dlo + unfold dlo linearOrderTheory + left; left; rfl -namespace FirstOrder.Language.Order +/-- +Models of the theory `Language.order.dlo` satisfies the transitivity sentence. +-/ +protected lemma realize_transitive : M ⊨ (leSymb (L := Language.order)).transitive := by + apply realize_sentence_of_mem Language.order.dlo + unfold dlo linearOrderTheory + left; right; right; left; rfl --- def to_Lle_homomorphism {M N : Type w} [L≤.Structure M] [L≤.Structure N] (f : M →o N) : M →[L≤] N := --- by sorry +/-- +Models of the theory `Language.order.dlo` satisfies the antisymmetric sentence. +-/ +protected lemma realize_antisymmetric : M ⊨ (leSymb (L := Language.order)).antisymmetric := by + apply realize_sentence_of_mem Language.order.dlo + unfold dlo linearOrderTheory + left; right; left; rfl -theorem aleph0_categorical_of_dlo : aleph0.Categorical L≤.dlo := by +/-- +Models of the theory `Language.order.dlo` satisfies the totality sentence. +-/ +protected lemma realize_total : M ⊨ (leSymb (L := Language.order)).total := by + apply realize_sentence_of_mem Language.order.dlo + unfold dlo linearOrderTheory + left; right; right; right; rfl + +/-- +Models of the theory `Language.order.dlo` satisfies the densely ordered sentence. +-/ +protected lemma realize_denselyOrderedSentence : M ⊨ Language.order.denselyOrderedSentence := by + apply realize_sentence_of_mem Language.order.dlo + unfold dlo linearOrderTheory + right; right; right; rfl + +/-- +Models of the theory `Language.order.dlo` satisfies the noBotOrder sentence. +-/ +protected lemma realize_noBotOrderSentence : M ⊨ Language.order.noBotOrderSentence := by + apply realize_sentence_of_mem Language.order.dlo + unfold dlo linearOrderTheory + right; right; left; rfl + +/-- +Models of the theory `Language.order.dlo` satisfies the noTopOrder sentence. +-/ +protected lemma realize_noTopOrderSentence : M ⊨ Language.order.noTopOrderSentence := by + apply realize_sentence_of_mem Language.order.dlo + unfold dlo linearOrderTheory + right; left; rfl + +end + +section + +variable {M : Type w} [instStructure : Language.order.Structure M] +variable [instModel : M ⊨ Language.order.dlo] + +instance instPreorder : Preorder M where + le := (@instLE M instStructure).le + le_refl := by + have := DLO.realize_reflexive M + simp only [Relations.realize_reflexive] at this + exact this + le_trans := by + have := DLO.realize_transitive M + simp only [Relations.realize_transitive] at this + exact this + +@[simp] +lemma toLE_of_Preorder + : (@instPreorder M instStructure instModel).toLE = @instLE M instStructure := rfl + +noncomputable instance instLinearOrder : LinearOrder M where + toPreorder := @instPreorder M instStructure instModel + le_antisymm := by + have := DLO.realize_antisymmetric M + simp only [Relations.realize_antisymmetric] at this + exact this + le_total := by + have := DLO.realize_total M + simp only [Relations.realize_total] at this + exact this + decidableLE := by apply Classical.decRel + +@[simp] +lemma toLE_of_LinearOrder + : (@instLinearOrder M instStructure instModel).toLE = @instLE M instStructure := rfl + +instance : @NoMinOrder M instLinearOrder.toLT where + exists_lt := by + have := DLO.realize_noBotOrderSentence M + simp only [noBotOrderSentence] at this + intro a + replace this := this a + simp at this + rcases this with ⟨b, h⟩ + use b + exact h + +instance : @NoMaxOrder M instLinearOrder.toLT where + exists_gt := by + have := DLO.realize_noTopOrderSentence M + simp only [noTopOrderSentence] at this + intro a + replace this := this a + simp at this + rcases this with ⟨b, h⟩ + use b + exact h + +instance : DenselyOrdered M where + dense := by + have := DLO.realize_denselyOrderedSentence M + simp only [denselyOrderedSentence] at this + intro a₁ a₂ h + replace this := this a₁ a₂ + simp only [BoundedFormula.realize_imp, Term.realize_lt, Term.realize_var, + BoundedFormula.realize_ex, BoundedFormula.realize_inf] at this + replace this := this h + rcases this with ⟨a, h₁, h₂⟩ + use a + exact ⟨h₁, h₂⟩ + +end + +theorem aleph0_categorical_of_dlo : aleph0.Categorical Language.order.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 + apply Nonempty.map toLIso + have : Countable M := by apply mk_le_aleph0_iff.mp; rw [hM] + have : Countable N := by apply mk_le_aleph0_iff.mp; rw [hN] + apply iso_of_countable_dense -#check iso_of_countable_dense +end DLO --end -end FirstOrder.Language.Order +end FirstOrder.Language.Order --end diff --git a/FormalTextbookModelTheory/ForMathlib/Language.lean b/FormalTextbookModelTheory/ForMathlib/Language.lean deleted file mode 100644 index 5efd461..0000000 --- a/FormalTextbookModelTheory/ForMathlib/Language.lean +++ /dev/null @@ -1,87 +0,0 @@ -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 diff --git a/FormalTextbookModelTheory/ForMathlib/Matrix.lean b/FormalTextbookModelTheory/ForMathlib/Matrix.lean index 7543902..817b50e 100644 --- a/FormalTextbookModelTheory/ForMathlib/Matrix.lean +++ b/FormalTextbookModelTheory/ForMathlib/Matrix.lean @@ -3,7 +3,7 @@ import Mathlib.Logic.Equiv.Fin namespace Matrix -variable {α : Type*} +variable {α β: Type*} lemma Vector_eq_VecNotation₂ (v : Fin 2 → α) : v = ![v 0, v 1] := by simp only [vecCons] @@ -14,14 +14,12 @@ lemma Vector_eq_VecNotation₂ (v : Fin 2 → α) : v = ![v 0, v 1] := by 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] +@[simp] +lemma comp_VecNotation₂ (f : α → β) (x y : α) : f ∘ ![x, y] = ![f x, f y] := by + ext x + rcases x with ⟨i, h⟩ + match i with + | 0 => rfl + | 1 => rfl - 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 --/ +end Matrix diff --git a/FormalTextbookModelTheory/ForMathlib/Order.lean b/FormalTextbookModelTheory/ForMathlib/Order.lean deleted file mode 100644 index cd6e434..0000000 --- a/FormalTextbookModelTheory/ForMathlib/Order.lean +++ /dev/null @@ -1,324 +0,0 @@ -import Mathlib.SetTheory.Cardinal.Basic -import Mathlib.ModelTheory.Basic -import Mathlib.ModelTheory.Satisfiability -import Mathlib.ModelTheory.Order -import Mathlib.Order.CountableDenseLinearOrder -import Mathlib.Order.Basic -import FormalTextbookModelTheory.ForMathlib.Matrix -import FormalTextbookModelTheory.ForMathlib.Language - -universe u v w - -open Cardinal -open Matrix -open FirstOrder Language Theory Order Structure - -namespace FirstOrder.Language.Order --{{{ - -section Language.order - -scoped notation "L≤" => Language.order - -instance instIsRelational₂: IsRelational₂ L≤ where - empty_functions := Language.instIsRelational.empty_functions - only_rel₂ := by - intro n hn - simp only [Language.order, Language.mk₂, Sequence₂] - match n with - | 0 => exact instIsEmptyPEmpty - | 1 => exact instIsEmptyEmpty - | 2 => contradiction - | _ + 3 => exact instIsEmptyPEmpty - -end Language.order - -section LE - -#check (@orderStructure) - -#check (@orderLHom) - -#check (@OrderedStructure) -/- -tabiki L≤.Structure yapisi orderStructure ile LE M den infer ediliyor. -orderLHom : L≤ →ᴸ L homomorphismasinin expansion oldugunu soyluyor. --/ - -#check (@orderedStructure_LE) -/- -bu baya trivial bir sey. orderLHom : L≤ →ᴸ L≤ zaten identity. bunun bir expansion oldugunu soyluyor. --/ - -def inst_LE_of_IsOrdered - (L : Language.{u, v}) [IsOrdered L] {M : Type w} [L.Structure M] : LE M where - le := fun x y => (@RelMap L M _ 2 leSymb) ![x, y] - -#check (@inst_LE_of_IsOrdered) -/- -burada da ordered bir languageden LE M turetiyoruz. --/ - -@[simp] -lemma orderStructure_of_LE_of_structure {M : Type w} [inst : L≤.Structure M] - : @orderStructure M (inst_LE_of_IsOrdered L≤) = inst := by - ext r₂ m - simp only [orderStructure, inst_LE_of_IsOrdered] - rw [Vector_eq_VecNotation₂ m, relMap_apply₂] - simp only [Nat.succ_eq_add_one, Nat.reduceAdd] - rw [←eq_iff_iff] - apply congrArg (fun s => RelMap s _) - apply Subsingleton.allEq -/- -bu aslinda onemli. L≤.Structure M --(inst_LE_of_IsOrdered)--> LE M --(orderStructure)--> L≤.Structure M isleminin -bizi ayni noktaya getirdigini soyluyor. --/ - -end LE - -section IsOrdered - -variable {L : Language.{u, v}} [instIsOrdered : IsOrdered L] -variable {M : Type w} [instStructure : L.Structure M] - -lemma OrderedStructure_of_IsOrdered - : @OrderedStructure L M instIsOrdered (inst_LE_of_IsOrdered L) instStructure := by - let inst : L≤.Structure M := by exact @orderStructure M (inst_LE_of_IsOrdered L) - simp only [OrderedStructure] - refine { - map_onFunction := by simp only [IsEmpty.forall_iff, implies_true] - map_onRelation := ?map_onRelation - } - intro n - match n with - | 0 | 1 | _ + 3 => - simp only [Language.order, mk₂_Relations, Sequence₂, instIsEmptyPEmpty, IsEmpty.forall_iff] - | 2 => - intro _ x - rw [Vector_eq_VecNotation₂ x] - simp only [inst_LE_of_IsOrdered, orderStructure_of_LE_of_structure, relMap_apply₂] - apply congrArg (fun r => @RelMap L M instStructure 2 r ![x 0, x 1]) - rfl - -section LinearOrder - -lemma linearOrderTheory_subset_dlo : L.linearOrderTheory ⊆ L.dlo := by - simp only [dlo] - exact Set.subset_union_left - -lemma reflexive_in_linearOrderTheory : leSymb.reflexive ∈ L.linearOrderTheory := by - simp only [linearOrderTheory, Set.mem_insert_iff, Set.mem_singleton_iff, true_or] - -lemma transitive_in_linearOrderTheory : leSymb.transitive ∈ L.linearOrderTheory := by - simp only [linearOrderTheory, Set.mem_insert_iff, Set.mem_singleton_iff, true_or, or_true] - -lemma antisymmetric_in_linearOrderTheory : leSymb.antisymmetric ∈ L.linearOrderTheory := by - simp only [linearOrderTheory, Set.mem_insert_iff, Set.mem_singleton_iff, true_or, or_true, or_true] - -lemma total_in_linearOrderTheory : leSymb.total ∈ L.linearOrderTheory := by - simp only [linearOrderTheory, Set.mem_insert_iff, Set.mem_singleton_iff, true_or, or_true, or_true, or_true] - -lemma realize_reflexive_of_model_linearOrderTheory (h : M ⊨ L.linearOrderTheory) - : M ⊨ (leSymb (L := L)).reflexive := by - simp only [model_iff] at h - replace h := h leSymb.reflexive reflexive_in_linearOrderTheory - exact h - -lemma realize_transitive_of_model_linearOrderTheory (h : M ⊨ L.linearOrderTheory) - : M ⊨ (leSymb (L := L)).transitive := by - simp only [model_iff] at h - replace h := h leSymb.transitive transitive_in_linearOrderTheory - exact h - -lemma realize_antisymmetric_of_model_linearOrderTheory (h : M ⊨ L.linearOrderTheory) - : M ⊨ (leSymb (L := L)).antisymmetric := by - simp only [model_iff] at h - replace h := h leSymb.antisymmetric antisymmetric_in_linearOrderTheory - exact h - -lemma realize_total_of_model_linearOrderTheory (h : M ⊨ L.linearOrderTheory) - : M ⊨ (leSymb (L := L)).total := by - simp only [model_iff] at h - replace h := h leSymb.total total_in_linearOrderTheory - exact h - -end LinearOrder - -section DLO - -section - -variable {L : Language.{u, v}} [instIsOrdered : IsOrdered L] - -lemma reflexive_in_dlo : leSymb.reflexive ∈ L.dlo := - linearOrderTheory_subset_dlo reflexive_in_linearOrderTheory - -lemma transitive_in_dlo : leSymb.transitive ∈ L.dlo := - linearOrderTheory_subset_dlo transitive_in_linearOrderTheory - -lemma antisymmetry_in_dlo : leSymb.antisymmetric ∈ L.dlo := - linearOrderTheory_subset_dlo antisymmetric_in_linearOrderTheory - -lemma total_in_dlo : leSymb.total ∈ L.dlo := - linearOrderTheory_subset_dlo total_in_linearOrderTheory - -lemma denselyOrderedSentence_in_dlo : L.denselyOrderedSentence ∈ L.dlo := by - simp only [dlo, Set.union_insert, Set.union_singleton, Set.mem_insert_iff, true_or, or_true] - -end - -section - -variable {L : Language.{u, v}} [instIsOrdered : IsOrdered L] -variable {M : Type w} [instStructure : L.Structure M] - -lemma realize_reflexive_of_model_dlo (h : M ⊨ L.dlo) : M ⊨ (leSymb (L := L)).reflexive := by - simp only [model_iff] at h - replace h := h leSymb.reflexive reflexive_in_dlo - exact h - -lemma realize_transitive_of_model_dlo (h : M ⊨ L.dlo) : M ⊨ (leSymb (L := L)).transitive := by - simp only [model_iff] at h - replace h := h leSymb.transitive transitive_in_dlo - exact h - -lemma model_linearOrderTheory_of_model_dlo (h : M ⊨ L.dlo) : M ⊨ L.linearOrderTheory := by - simp [model_iff] at * - intro φ hφ - exact h φ (linearOrderTheory_subset_dlo hφ) - -lemma realize_denselyOrderedSentence_of_model_dlo (h : M ⊨ L.dlo) : M ⊨ L.denselyOrderedSentence := by - simp only [model_iff] at h - replace h := h L.denselyOrderedSentence denselyOrderedSentence_in_dlo - exact h - -end - -section - -variable (L : Language.{u, v}) [instIsOrdered : IsOrdered L] -variable {M : Type w} [instStructure : L.Structure M] [instModel : M ⊨ L.dlo] - -def inst_Preorder_of_dlo : Preorder M where - le := (inst_LE_of_IsOrdered L).le - le_refl := by - have := realize_reflexive_of_model_dlo instModel - simp only [Relations.realize_reflexive, Reflexive] at this - exact this - le_trans := by - have := realize_transitive_of_model_dlo instModel - simp only [Relations.realize_transitive, Transitive] at this - exact this - -noncomputable def inst_LinearOrder_of_dlo : LinearOrder M where - toPreorder := inst_Preorder_of_dlo L - le_antisymm := by - have := realize_antisymmetric_of_model_linearOrderTheory - (model_linearOrderTheory_of_model_dlo instModel) - simp only [Relations.realize_antisymmetric, Antisymm] at this - exact this - le_total := by - have := realize_total_of_model_linearOrderTheory - (model_linearOrderTheory_of_model_dlo instModel) - simp only [Relations.realize_total, Total] at this - exact this - decidableLE := Classical.decRel _ - -def inst_DenselyOrdered_of_dlo : @DenselyOrdered M (inst_Preorder_of_dlo L).toLT := by - - have : M ⊨ L.denselyOrderedSentence := realize_denselyOrderedSentence_of_model_dlo instModel - - simp only [Sentence.Realize, denselyOrderedSentence, Formula.Realize, BoundedFormula.realize_all, - BoundedFormula.realize_imp, BoundedFormula.realize_ex, BoundedFormula.realize_inf] at this - - let _ : LT M := (inst_Preorder_of_dlo L).toLT - refine { - dense := ?dense - } - - intro a b h - replace this := this a b - simp only [ - @Term.realize_lt L _ M 2 instIsOrdered instStructure (inst_Preorder_of_dlo L) OrderedStructure_of_IsOrdered] at this - replace this := this h - rcases this with ⟨a₂, ⟨h₁, h₂⟩⟩ - use a₂ - simp only [ - @Term.realize_lt L _ M 3 instIsOrdered instStructure (inst_Preorder_of_dlo L) OrderedStructure_of_IsOrdered, - Function.comp_apply] at h₁ h₂ - exact ⟨h₁, h₂⟩ - -end - -end DLO - -end IsOrdered - -end FirstOrder.Language.Order --}}} - -namespace FirstOrder - -namespace Language - -/- -section - -variable {L : Language.{u, v}} [IsOrdered L] {M : Type w} [L.Structure M] - -theorem realize_sentence_of_mem_of_model_theory - {T : Theory L} (h : M ⊨ T) {p : L.Sentence} (hp : p ∈ T) : M ⊨ p := by - simp only [model_iff] at h - exact h p hp - -theorem model_theory_of_subset_of_model_theory {T T' : Theory L} (h : T' ⊆ T) (hT : M ⊨ T) : - M ⊨ T' := by - simp only [model_iff] at * - intro φ hφ - exact hT φ (h hφ) - -theorem realize_reflexive_of_model_linearOrderTheory (h : M ⊨ L.linearOrderTheory) : - M ⊨ (leSymb (L := L)).reflexive := - realize_sentence_of_mem_of_model_theory h reflexive_in_linearOrderTheory - -end --/ - -/- -section -- {{{ - -variable {M : Type w} [inst₁ : L≤.Structure M] - -theorem realize_reflexive_iff : M ⊨ (leSymb (L := L≤)).reflexive ↔ ∀ a : M, a ≤ a := by - simp only [Relations.realize_reflexive, Reflexive] - constructor <;> {intro; assumption} - -theorem realize_transitive_iff - : M ⊨ (leSymb (L := L≤)).transitive ↔ ∀ (a b c : M), a ≤ b → b ≤ c → a ≤ c := by - simp only [Relations.realize_transitive, Transitive] - constructor <;> {intro; assumption} - -instance [inst : M ⊨ L≤.dlo] : Preorder M where - le := (· ≤ ·) - le_refl := by - apply realize_reflexive_iff.1 - apply realize_sentence_of_mem_of_model_theory inst - apply reflexive_in_dlo - le_trans := by - apply realize_transitive_iff.1 - apply realize_sentence_of_mem_of_model_theory inst - apply transitive_in_dlo - -instance [inst : M ⊨ L≤.dlo] : DenselyOrdered M := by - apply realize_denselyOrdered_iff.mp - #check @realize_sentence_of_mem L≤ M inst₁ L≤.dlo inst L≤.denselyOrderedSentence - apply @realize_sentence_of_mem L≤ M inst₁ L≤.dlo inst L≤.denselyOrderedSentence - sorry - -#check realize_denselyOrdered_iff -#check realize_sentence_of_mem - -end -- }}} --/ - -end Language - -end FirstOrder diff --git a/FormalTextbookModelTheory/ForMathlib2/Cardinal.lean b/FormalTextbookModelTheory/ForMathlib2/Cardinal.lean deleted file mode 100644 index 7d4dfff..0000000 --- a/FormalTextbookModelTheory/ForMathlib2/Cardinal.lean +++ /dev/null @@ -1,7 +0,0 @@ -import Mathlib.SetTheory.Cardinal.Basic - -namespace Cardinal - -instance countable_of_mk_eq_aleph0 {α : Type w} (h : #α = ℵ₀) : Countable α := by - apply mk_le_aleph0_iff.mp - rw [h] diff --git a/FormalTextbookModelTheory/ForMathlib2/DLO.lean b/FormalTextbookModelTheory/ForMathlib2/DLO.lean deleted file mode 100644 index e4a228b..0000000 --- a/FormalTextbookModelTheory/ForMathlib2/DLO.lean +++ /dev/null @@ -1,218 +0,0 @@ -import Mathlib.SetTheory.Cardinal.Basic -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.ForMathlib2.Matrix -import FormalTextbookModelTheory.ForMathlib2.Cardinal - -open Cardinal -open FirstOrder Language Structure Theory Order -open Matrix (Vector_eq_VecNotation₂ comp_VecNotation₂) - -namespace FirstOrder.Language.Order --region - -section - -variable {M : Type w} [instStructure : Language.order.Structure M] - -instance instLE : LE M where - le := fun x y => instStructure.RelMap leSymb ![x, y] - -@[simp] -lemma orderStructure_of_LE : @orderStructure M instLE = instStructure := by - ext1 - · funext _ r - exfalso - exact IsEmpty.elim (by infer_instance) r - · funext n r x - match n with - | 0 | 1 | _ + 3 => - exfalso - simp only [Language.order, mk₂_Relations, Sequence₂] at r - exact IsEmpty.elim (by infer_instance) r - | 2 => - rw [Vector_eq_VecNotation₂ x, (by apply Subsingleton.allEq : r = leSymb)] - simp only [orderStructure, LE.le, Structure.relMap_apply₂] - -instance : @OrderedStructure Language.order M _ instLE instStructure := by - simp only [OrderedStructure, orderLHom_order, orderStructure_of_LE] - exact @LHom.id_isExpansionOn Language.order M instStructure - -end - -section - -variable {M : Type w} [Language.order.Structure M] -variable {N : Type w} [Language.order.Structure N] - -def toLEmbedding (φ : M ↪o N) : M ↪[Language.order] N where - toEmbedding := φ.toEmbedding - map_fun' := by - intro n f - exfalso - exact IsEmpty.elim (by infer_instance) f - map_rel' := by - intro n r x - match n with - | 0 | 1 | _ + 3 => - exfalso - simp [Language.order, Sequence₂] at r - exact IsEmpty.elim (by infer_instance) r - | 2 => - rw [Vector_eq_VecNotation₂ x, comp_VecNotation₂ φ.toFun, - (by apply Subsingleton.allEq : r = leSymb), relMap_leSymb, relMap_leSymb] - exact φ.map_rel_iff - -def toLIso (φ : M ≃o N) : M ≃[Language.order] N where - toEquiv := φ.toEquiv - map_fun' := (toLEmbedding (φ.toOrderEmbedding)).map_fun' - map_rel' := (toLEmbedding (φ.toOrderEmbedding)).map_rel' - -end - -namespace DLO --region - -section - -variable (M : Type w) [Language.order.Structure M] -variable [M ⊨ Language.order.dlo] - -protected lemma realize_reflexive : M ⊨ (leSymb (L := Language.order)).reflexive := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - left; left; rfl - -protected lemma realize_transitive : M ⊨ (leSymb (L := Language.order)).transitive := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - left; right; right; left; rfl - -protected lemma realize_antisymmetric : M ⊨ (leSymb (L := Language.order)).antisymmetric := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - left; right; left; rfl - -protected lemma realize_total : M ⊨ (leSymb (L := Language.order)).total := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - left; right; right; right; rfl - -protected lemma realize_denselyOrderedSentence : M ⊨ Language.order.denselyOrderedSentence := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - right; right; right; rfl - -protected lemma realize_noBotOrderSentence : M ⊨ Language.order.noBotOrderSentence := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - right; right; left; rfl - -protected lemma realize_noTopOrderSentence : M ⊨ Language.order.noTopOrderSentence := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - right; left; rfl - -end - -section - -variable {M : Type w} [instStructure : Language.order.Structure M] -variable [instModel : M ⊨ Language.order.dlo] - -instance instPreorder : Preorder M where - le := (@instLE M instStructure).le - le_refl := by - have := DLO.realize_reflexive M - simp only [Relations.realize_reflexive] at this - exact this - le_trans := by - have := DLO.realize_transitive M - simp only [Relations.realize_transitive] at this - exact this - -@[simp] -lemma toLE_of_Preorder - : (@instPreorder M instStructure instModel).toLE = @instLE M instStructure := rfl - -noncomputable instance instLinearOrder : LinearOrder M where - -- le := (@instLE M instStructure).le - -- le_refl := by - -- have := DLO.realize_reflexive M - -- simp only [Relations.realize_reflexive] at this - -- exact this - -- le_trans := by - -- have := DLO.realize_transitive M - -- simp only [Relations.realize_transitive] at this - -- exact this - toPreorder := @instPreorder M instStructure instModel - le_antisymm := by - have := DLO.realize_antisymmetric M - simp only [Relations.realize_antisymmetric] at this - exact this - le_total := by - have := DLO.realize_total M - simp only [Relations.realize_total] at this - exact this - decidableLE := by apply Classical.decRel - -@[simp] -lemma toLE_of_LinearOrder - : (@instLinearOrder M instStructure instModel).toLE = @instLE M instStructure := rfl - -instance : @NoMinOrder M instLinearOrder.toLT where - exists_lt := by - have := DLO.realize_noBotOrderSentence M - simp only [noBotOrderSentence] at this - intro a - replace this := this a - simp at this - rcases this with ⟨b, h⟩ - use b - exact h - -instance : @NoMaxOrder M instLinearOrder.toLT where - exists_gt := by - have := DLO.realize_noTopOrderSentence M - simp only [noTopOrderSentence] at this - intro a - replace this := this a - simp at this - rcases this with ⟨b, h⟩ - use b - exact h - -instance instDenselyOrdered : DenselyOrdered M where - dense := by - have := DLO.realize_denselyOrderedSentence M - simp only [denselyOrderedSentence] at this - intro a₁ a₂ h - replace this := this a₁ a₂ - simp only [BoundedFormula.realize_imp, Term.realize_lt, Term.realize_var, - BoundedFormula.realize_ex, BoundedFormula.realize_inf] at this - replace this := this h - rcases this with ⟨a, h₁, h₂⟩ - use a - exact ⟨h₁, h₂⟩ - -end - -/-- -This is my docstring --/ -theorem aleph0_categorical_of_dlo : aleph0.Categorical Language.order.dlo := by - unfold Categorical - rintro ⟨M⟩ ⟨N⟩ hM hN - simp only at * - apply Nonempty.map toLIso - have := countable_of_mk_eq_aleph0 hM - have := countable_of_mk_eq_aleph0 hN - apply iso_of_countable_dense - -end DLO --end - -end FirstOrder.Language.Order --end diff --git a/FormalTextbookModelTheory/ForMathlib2/Matrix.lean b/FormalTextbookModelTheory/ForMathlib2/Matrix.lean deleted file mode 100644 index 817b50e..0000000 --- a/FormalTextbookModelTheory/ForMathlib2/Matrix.lean +++ /dev/null @@ -1,25 +0,0 @@ -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 - -@[simp] -lemma comp_VecNotation₂ (f : α → β) (x y : α) : f ∘ ![x, y] = ![f x, f y] := by - ext x - rcases x with ⟨i, h⟩ - match i with - | 0 => rfl - | 1 => rfl - -end Matrix diff --git a/blueprint/lean_decls b/blueprint/lean_decls index 5a7a444..baedaa7 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -1,30 +1,16 @@ Matrix.Vector_eq_VecNotation₂ -FirstOrder.Language.Order.linearOrderTheory_subset_dlo -FirstOrder.Language.Order.reflexive_in_linearOrderTheory -FirstOrder.Language.Order.transitive_in_linearOrderTheory -FirstOrder.Language.Order.antisymmetric_in_linearOrderTheory -FirstOrder.Language.Order.total_in_linearOrderTheory -FirstOrder.Language.Order.realize_reflexive_of_model_linearOrderTheory -FirstOrder.Language.Order.realize_transitive_of_model_linearOrderTheory -FirstOrder.Language.Order.realize_antisymmetric_of_model_linearOrderTheory -FirstOrder.Language.Order.realize_total_of_model_linearOrderTheory -FirstOrder.Language.Order.reflexive_in_dlo -FirstOrder.Language.Order.transitive_in_dlo -FirstOrder.Language.Order.antisymmetric_in_dlo -FirstOrder.Language.Order.total_in_dlo -FirstOrder.Language.Order.realize_reflexive_of_model_dlo -FirstOrder.Language.Order.realize_transitive_of_model_dlo -FirstOrder.Language.Order.realize_antisymmetric_of_model_dlo -FirstOrder.Language.Order.realize_total_of_model_dlo -FirstOrder.Language.Order.model_linearOrderTheory_of_model_dlo -FirstOrder.Language.Order.inst_LE_of_IsOrdered -FirstOrder.Language.Order.inst_Preorder_of_dlo -FirstOrder.Language.Order.inst_LinearOrder_of_dlo -FirstOrder.Language.IsRelational₂ -FirstOrder.Language.Order.instIsRelational₂ -FirstOrder.Language.Structure.funMap_eq_funMap_of_relational -FirstOrder.Language.Structure.structure_eq_structure_of_relational_iff -FirstOrder.Language.Structure.RelMap_eq_RelMap_of_relational₂ -FirstOrder.Language.Structure.structure_eq_of_structure_of_relational₂_iff -FirstOrder.Language.Order.orderStructure_of_LE_of_structure -FirstOrder.Language.Order.aleph0_categorical_of_dlo \ No newline at end of file +Matrix.comp_VecNotation₂ +FirstOrder.Language.Order.DLO.realize_reflexive +FirstOrder.Language.Order.DLO.realize_transitive +FirstOrder.Language.Order.DLO.realize_antisymmetric +FirstOrder.Language.Order.DLO.realize_total +FirstOrder.Language.Order.DLO.realize_denselyOrderedSentence +FirstOrder.Language.Order.DLO.realize_noBotOrderSentence +FirstOrder.Language.Order.DLO.realize_noTopOrderSentence +FirstOrder.Language.Order.instLE +FirstOrder.Language.Order.orderStructure_of_LE +FirstOrder.Language.Order.DLO.instPreorder +FirstOrder.Language.Order.DLO.instLinearOrder +FirstOrder.Language.Order.toLEmbedding +FirstOrder.Language.Order.toLIso +FirstOrder.Language.Order.DLO.aleph0_categorical_of_dlo \ No newline at end of file diff --git a/blueprint/print/print.aux b/blueprint/print/print.aux index 6e454d2..4aa5171 100644 --- a/blueprint/print/print.aux +++ b/blueprint/print/print.aux @@ -7,40 +7,29 @@ \@writefile{lof}{\addvspace {10\p@ }} \@writefile{lot}{\addvspace {10\p@ }} \@writefile{toc}{\contentsline {section}{\numberline {1.1}Vectors}{1}{section.1.1}\protected@file@percent } -\newlabel{lem:two-vector-notation}{{1.1.1}{1}{}{theorem.1.1.1}{}} +\newlabel{lem:vector-notation}{{1.1.1}{1}{}{theorem.1.1.1}{}} +\newlabel{lem:vector-notation-under-composition}{{1.1.2}{1}{}{theorem.1.1.2}{}} \@writefile{toc}{\contentsline {section}{\numberline {1.2}Theories}{1}{section.1.2}\protected@file@percent } -\newlabel{lem:linear-order-theory-in-dlo}{{1.2.1}{1}{}{theorem.1.2.1}{}} -\newlabel{lem:reflexive-in-linear-order-theory}{{1.2.2}{1}{}{theorem.1.2.2}{}} -\newlabel{lem:transitive-in-linear-order-theory}{{1.2.3}{1}{}{theorem.1.2.3}{}} -\newlabel{lem:antisymmetric-in-linear-order-theory}{{1.2.4}{1}{}{theorem.1.2.4}{}} -\newlabel{lem:total-in-linear-order-theory}{{1.2.5}{1}{}{theorem.1.2.5}{}} -\newlabel{lem:models-of-linearOrderTheory-realize-reflexive}{{1.2.6}{1}{}{theorem.1.2.6}{}} -\newlabel{lem:models-of-linearOrderTheory-realize-transitive}{{1.2.7}{1}{}{theorem.1.2.7}{}} -\newlabel{lem:models-of-linearOrderTheory-realize-antisymmetric}{{1.2.8}{1}{}{theorem.1.2.8}{}} -\newlabel{lem:models-of-linearOrderTheory-realize-total}{{1.2.9}{2}{}{theorem.1.2.9}{}} -\newlabel{lem:reflexive-in-dlo}{{1.2.10}{2}{}{theorem.1.2.10}{}} -\newlabel{lem:transitive-in-dlo}{{1.2.11}{2}{}{theorem.1.2.11}{}} -\newlabel{lem:antisymmetric-in-dlo}{{1.2.12}{2}{}{theorem.1.2.12}{}} -\newlabel{lem:total-in-dlo}{{1.2.13}{2}{}{theorem.1.2.13}{}} -\newlabel{lem:models-of-dlo-realize-reflexivity}{{1.2.14}{2}{}{theorem.1.2.14}{}} -\newlabel{lem:models-of-dlo-realize-transitivity}{{1.2.15}{2}{}{theorem.1.2.15}{}} -\newlabel{lem:models-of-dlo-realize-antisymmetric}{{1.2.16}{2}{}{theorem.1.2.16}{}} -\newlabel{lem:models-of-dlo-realize-total}{{1.2.17}{2}{}{theorem.1.2.17}{}} -\newlabel{lem:models-of-dlo-models-of-linear-order-theory}{{1.2.18}{2}{}{theorem.1.2.18}{}} -\@writefile{toc}{\contentsline {section}{\numberline {1.3}Instances}{2}{section.1.3}\protected@file@percent } -\newlabel{def:le-instance-ordered-language}{{1.3.1}{2}{}{theorem.1.3.1}{}} -\newlabel{def:preorder-instance-models-of-dlo}{{1.3.2}{2}{}{theorem.1.3.2}{}} -\newlabel{def:linear-order-instance-models-of-dlo}{{1.3.3}{2}{}{theorem.1.3.3}{}} -\newlabel{def:binary-relational-language}{{1.3.4}{2}{}{theorem.1.3.4}{}} -\newlabel{lem:canonical-ordered-language-binary-relational}{{1.3.5}{2}{}{theorem.1.3.5}{}} -\@writefile{toc}{\contentsline {section}{\numberline {1.4}Structures}{3}{section.1.4}\protected@file@percent } -\newlabel{lem:structure-funmap-relational-language}{{1.4.1}{3}{}{theorem.1.4.1}{}} -\newlabel{lem:equality-of-structures-relational-language}{{1.4.2}{3}{}{theorem.1.4.2}{}} -\newlabel{lem:structure-relmap-binary-relational-language}{{1.4.3}{3}{}{theorem.1.4.3}{}} -\newlabel{lem:equality-of-structures-binary-relational-language}{{1.4.4}{3}{}{theorem.1.4.4}{}} -\newlabel{lem:orders-coincide-for-ordered-structures}{{1.4.5}{3}{}{theorem.1.4.5}{}} -\@writefile{toc}{\contentsline {chapter}{\numberline {2}Main Results}{4}{chapter.2}\protected@file@percent } +\newlabel{lem:realize-reflexivity}{{1.2.1}{1}{}{theorem.1.2.1}{}} +\newlabel{lem:realize-transitivity}{{1.2.2}{1}{}{theorem.1.2.2}{}} +\newlabel{lem:realize-antisymmetric}{{1.2.3}{1}{}{theorem.1.2.3}{}} +\newlabel{lem:realize-total}{{1.2.4}{1}{}{theorem.1.2.4}{}} +\newlabel{lem:realize-densely-ordered}{{1.2.5}{1}{}{theorem.1.2.5}{}} +\newlabel{lem:realize-no-min}{{1.2.6}{1}{}{theorem.1.2.6}{}} +\newlabel{lem:realize-no-max}{{1.2.7}{1}{}{theorem.1.2.7}{}} +\@writefile{toc}{\contentsline {chapter}{\numberline {2}Model Theory and The Rest of Mathlib}{2}{chapter.2}\protected@file@percent } \@writefile{lof}{\addvspace {10\p@ }} \@writefile{lot}{\addvspace {10\p@ }} -\newlabel{thm:dlo-aleph0-categorical}{{2.0.1}{4}{}{theorem.2.0.1}{}} -\gdef \@abspage@last{5} +\@writefile{toc}{\contentsline {section}{\numberline {2.1}Instances}{2}{section.2.1}\protected@file@percent } +\newlabel{def:le-instance-language-order}{{2.1.1}{2}{}{theorem.2.1.1}{}} +\newlabel{lem:order-structure-of-le}{{2.1.2}{2}{}{theorem.2.1.2}{}} +\newlabel{def:preorder-dlo}{{2.1.3}{2}{}{theorem.2.1.3}{}} +\newlabel{def:linearorder-dlo}{{2.1.4}{2}{}{theorem.2.1.4}{}} +\@writefile{toc}{\contentsline {section}{\numberline {2.2}Homomorphisms}{2}{section.2.2}\protected@file@percent } +\newlabel{lem:to-embedding}{{2.2.1}{2}{}{theorem.2.2.1}{}} +\newlabel{lem:to-isomorphism}{{2.2.2}{2}{}{theorem.2.2.2}{}} +\@writefile{toc}{\contentsline {chapter}{\numberline {3}Main Result}{3}{chapter.3}\protected@file@percent } +\@writefile{lof}{\addvspace {10\p@ }} +\@writefile{lot}{\addvspace {10\p@ }} +\newlabel{thm:dlo-aleph0-categorical}{{3.0.1}{3}{}{theorem.3.0.1}{}} +\gdef \@abspage@last{4} diff --git a/blueprint/print/print.fdb_latexmk b/blueprint/print/print.fdb_latexmk index ac84b00..372ed95 100644 --- a/blueprint/print/print.fdb_latexmk +++ b/blueprint/print/print.fdb_latexmk @@ -1,7 +1,7 @@ # Fdb version 4 -["pdflatex"] 1722842215.45552 "print.tex" "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.pdf" "print" 1722842216.35635 0 - "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.aux" 1722842216.13454 3389 9986f5bb805a7d456894f1ab84f2a2a4 "pdflatex" - "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.out" 1722842216.13454 684 cd11907768ebb096d11426bf84b99804 "pdflatex" +["pdflatex"] 1723661794.7511 "print.tex" "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.pdf" "print" 1723661795.69292 0 + "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.aux" 1723661795.4694 2232 b6b67c3fcb3329da2c254c2d8baad30a "pdflatex" + "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.out" 1723661795.4694 935 0e20a0f58d1d7838ffc59f27f356d900 "pdflatex" "/usr/local/texlive/2024/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 "" "/usr/local/texlive/2024/texmf-dist/fonts/tfm/adobe/zapfding/pzdr.tfm" 1136768653 1528 f853c4d1b4e0550255e02831fdc8496f "" "/usr/local/texlive/2024/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm" 1246382020 916 f87d7c45f9c908e672703b83b72241a3 "" @@ -83,9 +83,10 @@ "/usr/local/texlive/2024/texmf-dist/web2c/texmf.cnf" 1719785820 42007 0b741a3c21a5ca32b40e3846e75b3548 "" "/usr/local/texlive/2024/texmf-var/web2c/xetex/xelatex.fmt" 1722380463 10868501 e521c25442cce99c56ff9a77d153050d "" "/usr/local/texlive/2024/texmf.cnf" 1722380410.43027 455 5b996dcaa0eb4ef14a83b026bc0a008c "" - "chapters/basics.tex" 1722842210.89455 9444 d7c98278eb22bd3c0fd530b347cabe4f "" - "chapters/main.tex" 1722838314.15515 270 abcdeb6fca3851372d9a5ff1023c4753 "" - "content.tex" 1722838307.94514 917 7d022bbdd7c27336a23d62a729ff0c4b "" + "chapters/basics.tex" 1723659066.66334 2441 b48c6cf0620ad41684aeac4b58dc95e7 "" + "chapters/main.tex" 1723661787.37893 321 18d95ad5a64d5d1a73dc8caacf660dd9 "" + "chapters/model_theory.tex" 1723659684.69707 2076 ed78731b4190e4a400ab523aaea36373 "" + "content.tex" 1723660673.45768 1004 792b81f5308bf1a333bd495ff2e0fd5a "" "macros/common.tex" 1722759673.52174 604 ca3e9443483cfefd693019fb112f2d18 "" "macros/print.tex" 1722422546.45932 1101 87627b2ec24fef68edc71c13f43f7bab "" "print.tex" 1722837065.5925 1131 bf5d368546e76888c21bf562766212eb "" diff --git a/blueprint/print/print.fls b/blueprint/print/print.fls index d7313d4..d5e0134 100644 --- a/blueprint/print/print.fls +++ b/blueprint/print/print.fls @@ -192,6 +192,9 @@ INPUT /usr/local/texlive/2024/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam5 INPUT /usr/local/texlive/2024/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm INPUT /usr/local/texlive/2024/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm7.tfm INPUT /usr/local/texlive/2024/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm5.tfm +INPUT ./chapters/model_theory.tex +INPUT ./chapters/model_theory.tex +INPUT chapters/model_theory.tex INPUT ./chapters/main.tex INPUT ./chapters/main.tex INPUT chapters/main.tex diff --git a/blueprint/print/print.log b/blueprint/print/print.log index 6524026..197a8f2 100644 --- a/blueprint/print/print.log +++ b/blueprint/print/print.log @@ -1,4 +1,4 @@ -This is XeTeX, Version 3.141592653-2.6-0.999996 (TeX Live 2024) (preloaded format=xelatex 2024.7.31) 5 AUG 2024 10:16 +This is XeTeX, Version 3.141592653-2.6-0.999996 (TeX Live 2024) (preloaded format=xelatex 2024.7.31) 14 AUG 2024 21:56 entering extended mode restricted \write18 enabled. %&-line parsing enabled. @@ -683,36 +683,21 @@ LaTeX Font Info: Font shape `TU/latinmodern-math.otf(3)/m/n' will be (Font) scaled to size 6.99925pt on input line 9. LaTeX Font Info: Font shape `TU/latinmodern-math.otf(3)/m/n' will be (Font) scaled to size 4.99947pt on input line 9. - - -LaTeX Warning: Reference `lem:reflexive-in-linearOrderTheory' on page 1 undefin -ed on input line 78. - - -LaTeX Warning: Reference `lem:transitive-in-linearOrderTheory' on page 1 undefi -ned on input line 89. - - -LaTeX Warning: Reference `lem:antisymmetric-in-linearOrderTheory' on page 1 und -efined on input line 100. - - -LaTeX Warning: Reference `lem:total-in-linearOrderTheory' on page 1 undefined o -n input line 111. - - +) [1 ] +Chapter 2. +(./chapters/model_theory.tex) -[2]) +[2 -[3] -Chapter 2. +] +Chapter 3. (./chapters/main.tex)) -[4 +[3 ] (/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.aux) @@ -720,20 +705,17 @@ Chapter 2. LaTeX2e <2024-06-01> patch level 2 L3 programming layer <2024-05-27> *********** - -LaTeX Warning: There were undefined references. - Package rerunfilecheck Info: File `print.out' has not changed. -(rerunfilecheck) Checksum: CD11907768EBB096D11426BF84B99804;684. +(rerunfilecheck) Checksum: 0E20A0F58D1D7838FFC59F27F356D900;935. ) Here is how much of TeX's memory you used: - 16803 strings out of 474240 - 310097 string characters out of 5742353 - 1932557 words of memory out of 5000000 - 39281 multiletter control sequences out of 15000+600000 + 16792 strings out of 474240 + 309351 string characters out of 5742353 + 1929557 words of memory out of 5000000 + 39267 multiletter control sequences out of 15000+600000 563440 words of font info for 85 fonts, out of 8000000 for 9000 1348 hyphenation exceptions out of 8191 - 90i,6n,116p,542b,467s stack positions out of 10000i,1000n,20000p,200000b,200000s + 90i,6n,116p,542b,463s stack positions out of 10000i,1000n,20000p,200000b,200000s Output written on /home/metinersin/projects/FormalTextbookModelTheory/blueprint -/print/print.pdf (5 pages). +/print/print.pdf (4 pages). diff --git a/blueprint/print/print.out b/blueprint/print/print.out index 465edbd..348243c 100644 --- a/blueprint/print/print.out +++ b/blueprint/print/print.out @@ -1,6 +1,7 @@ \BOOKMARK [0][-]{chapter.1}{\376\377\000B\000a\000s\000i\000c\000\040\000D\000e\000f\000i\000n\000i\000t\000i\000o\000n\000s\000\040\000a\000n\000d\000\040\000L\000e\000m\000m\000a\000s}{}% 1 \BOOKMARK [1][-]{section.1.1}{\376\377\000V\000e\000c\000t\000o\000r\000s}{chapter.1}% 2 \BOOKMARK [1][-]{section.1.2}{\376\377\000T\000h\000e\000o\000r\000i\000e\000s}{chapter.1}% 3 -\BOOKMARK [1][-]{section.1.3}{\376\377\000I\000n\000s\000t\000a\000n\000c\000e\000s}{chapter.1}% 4 -\BOOKMARK [1][-]{section.1.4}{\376\377\000S\000t\000r\000u\000c\000t\000u\000r\000e\000s}{chapter.1}% 5 -\BOOKMARK [0][-]{chapter.2}{\376\377\000M\000a\000i\000n\000\040\000R\000e\000s\000u\000l\000t\000s}{}% 6 +\BOOKMARK [0][-]{chapter.2}{\376\377\000M\000o\000d\000e\000l\000\040\000T\000h\000e\000o\000r\000y\000\040\000a\000n\000d\000\040\000T\000h\000e\000\040\000R\000e\000s\000t\000\040\000o\000f\000\040\000M\000a\000t\000h\000l\000i\000b}{}% 4 +\BOOKMARK [1][-]{section.2.1}{\376\377\000I\000n\000s\000t\000a\000n\000c\000e\000s}{chapter.2}% 5 +\BOOKMARK [1][-]{section.2.2}{\376\377\000H\000o\000m\000o\000m\000o\000r\000p\000h\000i\000s\000m\000s}{chapter.2}% 6 +\BOOKMARK [0][-]{chapter.3}{\376\377\000M\000a\000i\000n\000\040\000R\000e\000s\000u\000l\000t}{}% 7 diff --git a/blueprint/print/print.pdf b/blueprint/print/print.pdf index b9f8e31..df19e09 100644 Binary files a/blueprint/print/print.pdf and b/blueprint/print/print.pdf differ diff --git a/blueprint/print/print.synctex.gz b/blueprint/print/print.synctex.gz index 9c8e33b..1371aed 100644 Binary files a/blueprint/print/print.synctex.gz and b/blueprint/print/print.synctex.gz differ diff --git a/blueprint/src/chapters/basics.tex b/blueprint/src/chapters/basics.tex index a2f8fc7..a075b18 100644 --- a/blueprint/src/chapters/basics.tex +++ b/blueprint/src/chapters/basics.tex @@ -3,259 +3,95 @@ \section{Vectors} %%% Really trivial stuff about numbers, vectors, etc. \begin{lemma} - \label{lem:two-vector-notation} + \label{lem:vector-notation} \lean{Matrix.Vector_eq_VecNotation₂} \leanok - For any vector $v : \Fin 2 \to \bbn$, we have $v = ![v(0), v(1)]$. + For any vector $v : \Fin 2 \to X$, we have $v = ![v(0), v(1)]$. \end{lemma} \begin{proof} \leanok \end{proof} -%%% - -\section{Theories} -%%% Really trivial stuff about theories - -\begin{lemma} - \label{lem:linear-order-theory-in-dlo} - \lean{FirstOrder.Language.Order.linearOrderTheory_subset_dlo} - \leanok - The theory of linear orders is a subset of DLO. -\end{lemma} -\begin{proof} - \leanok -\end{proof} - -%%%% LinearOrder -\begin{lemma} - \label{lem:reflexive-in-linear-order-theory} - \lean{FirstOrder.Language.Order.reflexive_in_linearOrderTheory} - \leanok - The theory of linear orders contains the reflexivity sentence. -\end{lemma} -\begin{proof} - \leanok -\end{proof} - -\begin{lemma} - \label{lem:transitive-in-linear-order-theory} - \lean{FirstOrder.Language.Order.transitive_in_linearOrderTheory} - \leanok - The theory of linear orders contains the transitivity sentence. -\end{lemma} -\begin{proof} - \leanok -\end{proof} - -\begin{lemma} - \label{lem:antisymmetric-in-linear-order-theory} - \lean{FirstOrder.Language.Order.antisymmetric_in_linearOrderTheory} - \leanok - The theory of linear orders contains the antisymmetry sentence. -\end{lemma} -\begin{proof} - \leanok -\end{proof} - -\begin{lemma} - \label{lem:total-in-linear-order-theory} - \lean{FirstOrder.Language.Order.total_in_linearOrderTheory} - \leanok - The theory of linear orders contains the totality sentence. -\end{lemma} -\begin{proof} - \leanok -\end{proof} - -\begin{lemma} - \label{lem:models-of-linearOrderTheory-realize-reflexive} - \lean{FirstOrder.Language.Order.realize_reflexive_of_model_linearOrderTheory} - \leanok - Models of the theory of linear orders realize the reflexivity sentence. -\end{lemma} -\begin{proof} - \leanok - \uses{lem:reflexive-in-linearOrderTheory} -\end{proof} - -\begin{lemma} - \label{lem:models-of-linearOrderTheory-realize-transitive} - \lean{FirstOrder.Language.Order.realize_transitive_of_model_linearOrderTheory} - \leanok - Models of the theory of linear orders realize the transitivity sentence. -\end{lemma} -\begin{proof} - \leanok - \uses{lem:transitive-in-linearOrderTheory} -\end{proof} - -\begin{lemma} - \label{lem:models-of-linearOrderTheory-realize-antisymmetric} - \lean{FirstOrder.Language.Order.realize_antisymmetric_of_model_linearOrderTheory} - \leanok - Models of the theory of linear orders realize the antisymmetry sentence. -\end{lemma} -\begin{proof} - \leanok - \uses{lem:antisymmetric-in-linearOrderTheory} -\end{proof} - -\begin{lemma} - \label{lem:models-of-linearOrderTheory-realize-total} - \lean{FirstOrder.Language.Order.realize_total_of_model_linearOrderTheory} - \leanok - Models of the theory of linear orders realize the totality sentence. -\end{lemma} -\begin{proof} - \leanok - \uses{lem:total-in-linearOrderTheory} -\end{proof} - -%%%% -%%%% DLO \begin{lemma} - \label{lem:reflexive-in-dlo} - \lean{FirstOrder.Language.Order.reflexive_in_dlo} + \label{lem:vector-notation-under-composition} + \lean{Matrix.comp_VecNotation₂} \leanok - The theory DLO contains the reflexivity sentence. + For any function $f : X \to Y$ and elements $x_1, x_2 \in X$, we have $f \circ ![x_1, x_2] = ![f(x_1), f(x_2)]$. \end{lemma} \begin{proof} \leanok - \uses{lem:linear-order-theory-in-dlo, lem:reflexive-in-linear-order-theory} \end{proof} -\begin{lemma} - \label{lem:transitive-in-dlo} - \lean{FirstOrder.Language.Order.transitive_in_dlo} - \leanok - The theory DLO contains the transitivity sentence -\end{lemma} -\begin{proof} - \leanok - \uses{lem:linear-order-theory-in-dlo, lem:transitive-in-linear-order-theory} -\end{proof} +%%% -\begin{lemma} - \label{lem:antisymmetric-in-dlo} - \lean{FirstOrder.Language.Order.antisymmetric_in_dlo} - \leanok - The theory DLO contains the antisymmetry sentence. -\end{lemma} -\begin{proof} - \leanok - \uses{lem:linear-order-theory-in-dlo, lem:antisymmetric-in-linear-order-theory} -\end{proof} +\section{Theories} +%%% Really trivial stuff about theories \begin{lemma} - \label{lem:total-in-dlo} - \lean{FirstOrder.Language.Order.total_in_dlo} + \label{lem:realize-reflexivity} + \lean{FirstOrder.Language.Order.DLO.realize_reflexive} \leanok - The theory DLO contains the totality sentence. + Models of the theory of dense linear orders realize the reflexivity sentence. \end{lemma} \begin{proof} \leanok - \uses{lem:linear-order-theory-in-dlo, lem:total-in-linear-order-theory} \end{proof} \begin{lemma} - \label{lem:models-of-dlo-realize-reflexivity} - \lean{FirstOrder.Language.Order.realize_reflexive_of_model_dlo} + \label{lem:realize-transitivity} + \lean{FirstOrder.Language.Order.DLO.realize_transitive} \leanok - Models of the theory DLO realize the reflexivity sentence. + Models of the theory of dense linear orders realize the transitivity sentence. \end{lemma} \begin{proof} \leanok - \uses{lem:reflexive-in-dlo} \end{proof} \begin{lemma} - \label{lem:models-of-dlo-realize-transitivity} - \lean{FirstOrder.Language.Order.realize_transitive_of_model_dlo} + \label{lem:realize-antisymmetric} + \lean{FirstOrder.Language.Order.DLO.realize_antisymmetric} \leanok - Models of the theory DLO realize the transitivity sentence. + Models of the theory of dense linear orders realize the antisymmetry sentence. \end{lemma} \begin{proof} \leanok - \uses{lem:transitive-in-dlo} \end{proof} \begin{lemma} - \label{lem:models-of-dlo-realize-antisymmetric} - \lean{FirstOrder.Language.Order.realize_antisymmetric_of_model_dlo} + \label{lem:realize-total} + \lean{FirstOrder.Language.Order.DLO.realize_total} \leanok - Models of the theory DLO realize the antisymmetry sentence. + Models of the theory of dense linear orders realize the totality sentence. \end{lemma} \begin{proof} \leanok - \uses{lem:antisymmetric-in-dlo} \end{proof} \begin{lemma} - \label{lem:models-of-dlo-realize-total} - \lean{FirstOrder.Language.Order.realize_total_of_model_dlo} + \label{lem:realize-densely-ordered} + \lean{FirstOrder.Language.Order.DLO.realize_denselyOrderedSentence} \leanok - Models of the theory DLO realize the totality sentence. + Models of the theory of dense linear orders realize the densely ordered sentence. \end{lemma} \begin{proof} \leanok - \uses{lem:total-in-dlo} \end{proof} \begin{lemma} - \label{lem:models-of-dlo-models-of-linear-order-theory} - \lean{FirstOrder.Language.Order.model_linearOrderTheory_of_model_dlo} + \label{lem:realize-no-min} + \lean{FirstOrder.Language.Order.DLO.realize_noBotOrderSentence} \leanok - Models of DLO are also models of the theory of linear orders. + Models of the theory of dense linear orders realize no minimum sentence. \end{lemma} \begin{proof} \leanok - \uses{lem:linear-order-theory-in-dlo} \end{proof} -%%%% - -%%% - -\section{Instances} -%%% Simple instances and instance chains - -\begin{definition} - \label{def:le-instance-ordered-language} - \lean{FirstOrder.Language.Order.inst_LE_of_IsOrdered} - \leanok - Any structure of an ordered language is an ordered set. -\end{definition} - -\begin{definition} - \label{def:preorder-instance-models-of-dlo} - \lean{FirstOrder.Language.Order.inst_Preorder_of_dlo} - \leanok - \uses{def:le-instance-ordered-language, lem:models-of-dlo-realize-reflexivity, lem:models-of-dlo-realize-transitivity} - statement of your definition -\end{definition} - -\begin{definition} - \label{def:linear-order-instance-models-of-dlo} - \lean{FirstOrder.Language.Order.inst_LinearOrder_of_dlo} - \leanok - \uses{def:preorder-instance-models-of-dlo, lem:models-of-dlo-realize-antisymmetric, lem:models-of-dlo-realize-total} - statement of your definition -\end{definition} - -\begin{definition} - \label{def:binary-relational-language} - \lean{FirstOrder.Language.IsRelational₂} - \leanok - A language is binary relational if it has onyl binary relation symbols. -\end{definition} - \begin{lemma} - \label{lem:canonical-ordered-language-binary-relational} - \lean{FirstOrder.Language.Order.instIsRelational₂} + \label{lem:realize-no-max} + \lean{FirstOrder.Language.Order.DLO.realize_noTopOrderSentence} \leanok - \uses{def:binary-relational-language} - The canonical ordered language consisting of a single binary relation $\leq$ is a binary relational language. + Models of the theory of dense linear orders realize no maximum sentence. \end{lemma} \begin{proof} \leanok @@ -263,74 +99,4 @@ \section{Instances} %%% -\section{Structures} -%%% Equality of structures for relational languages - -\begin{lemma} - \label{lem:structure-funmap-relational-language} - \lean{FirstOrder.Language.Structure.funMap_eq_funMap_of_relational} - \leanok - Structures of a relational language have equal function maps. -\end{lemma} -\begin{proof} - \leanok -\end{proof} - -\begin{lemma} - \label{lem:equality-of-structures-relational-language} - \lean{FirstOrder.Language.Structure.structure_eq_structure_of_relational_iff} - \leanok - Two structures of a relational language are equal if and only if they agree on the - interpretation of all relation symbols. -\end{lemma} -\begin{proof} - \leanok - \uses{lem:structure-funmap-relational-language} -\end{proof} - -%%% - -%%% Equality of structures for binary relational languages - -\begin{lemma} - \label{lem:structure-relmap-binary-relational-language} - \lean{FirstOrder.Language.Structure.RelMap_eq_RelMap_of_relational₂} - \leanok - \uses{def:binary-relational-language} - Two structures of a binary relational language have equal relation maps if and only - if they agree on the interpretation of all binary relation symbols. -\end{lemma} -\begin{proof} - \leanok -\end{proof} - -\begin{lemma} - \label{lem:equality-of-structures-binary-relational-language} - \lean{FirstOrder.Language.Structure.structure_eq_of_structure_of_relational₂_iff} - \leanok - \uses{def:binary-relational-language} - Two structures of a binary relational language are equal if and only if they agree on the - interpretation of all binary relation symbols. -\end{lemma} -\begin{proof} - \leanok - \uses{lem:structure-relmap-binary-relational-language, lem:equality-of-structures-relational-language} -\end{proof} - -\begin{lemma} - \label{lem:orders-coincide-for-ordered-structures} - \lean{FirstOrder.Language.Order.orderStructure_of_LE_of_structure} - \leanok - \uses{def:le-instance-ordered-language} - statement of your lemma -\end{lemma} -\begin{proof} - \leanok - \uses{def:le-instance-ordered-language, - lem:canonical-ordered-language-binary-relational, - lem:equality-of-structures-binary-relational-language, - lem:two-vector-notation} -\end{proof} - -%%% diff --git a/blueprint/src/chapters/main.tex b/blueprint/src/chapters/main.tex index d49a292..a7ff0ae 100644 --- a/blueprint/src/chapters/main.tex +++ b/blueprint/src/chapters/main.tex @@ -1,10 +1,11 @@ \begin{theorem} \label{thm:dlo-aleph0-categorical} - \lean{FirstOrder.Language.Order.aleph0_categorical_of_dlo} - \notready + \lean{FirstOrder.Language.Order.DLO.aleph0_categorical_of_dlo} + \leanok The theory of dense linear orders without endpoints is $\aleph_0$-categorical. \end{theorem} \begin{proof} - \notready + \leanok + \uses{def:linearorder-dlo, lem:to-isomorphism} \end{proof} diff --git a/blueprint/src/chapters/model_theory.tex b/blueprint/src/chapters/model_theory.tex new file mode 100644 index 0000000..89fd629 --- /dev/null +++ b/blueprint/src/chapters/model_theory.tex @@ -0,0 +1,67 @@ +\section{Instances} +%%% Simple instances + +\begin{definition} + \label{def:le-instance-language-order} + \lean{FirstOrder.Language.Order.instLE} + \leanok + Any structure of the language of orders is an ordered set. +\end{definition} + +\begin{lemma} + \label{lem:order-structure-of-le} + \lean{FirstOrder.Language.Order.orderStructure_of_LE} + \leanok + \uses{def:le-instance-language-order} + The structure induced from $\le$ which is induced from another structure is equal to the original structure. +\end{lemma} +\begin{proof} + \leanok + \uses{def:le-instance-language-order, lem:vector-notation} +\end{proof} + +\begin{definition} + \label{def:preorder-dlo} + \lean{FirstOrder.Language.Order.DLO.instPreorder} + \leanok + \uses{def:le-instance-language-order, lem:realize-reflexivity, lem:realize-transitivity} + Models of the theory of dense linear orders are preorders. +\end{definition} + +\begin{definition} + \label{def:linearorder-dlo} + \lean{FirstOrder.Language.Order.DLO.instLinearOrder} + \leanok + \uses{def:le-instance-language-order, def:preorder-dlo, lem:realize-antisymmetric, lem:realize-total} + Models of the theory of dense linear orders are linear orders. +\end{definition} + +%%% + +\section{Homomorphisms} + +\begin{lemma} + \label{lem:to-embedding} + \lean{FirstOrder.Language.Order.toLEmbedding} + \leanok + \uses{def:le-instance-language-order} + A function which is an order embedding is also an embedding in the model theoretic sense. +\end{lemma} +\begin{proof} + \leanok + \uses{def:le-instance-language-order, lem:vector-notation, lem:vector-notation-under-composition} +\end{proof} + +\begin{lemma} + \label{lem:to-isomorphism} + \lean{FirstOrder.Language.Order.toLIso} + \leanok + \uses{def:le-instance-language-order} + A function which is an order isomorphism is also an isomorphism in the model theoretic sense. +\end{lemma} +\begin{proof} + \leanok + \uses{def:le-instance-language-order, lem:vector-notation, lem:vector-notation-under-composition, lem:to-embedding} +\end{proof} + + diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index 523fdd8..befd653 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -16,15 +16,19 @@ % \end{theorem} % \begin{proof} -% \leanokcd +% \leanok % \uses{thm:open_ample, lem:open_ample_immersion} % This obviously follows from what we did so far. -% \end +% \end{proof} \chapter{Basic Definitions and Lemmas} \input{chapters/basics.tex} -\chapter{Main Results} +\chapter{Model Theory and The Rest of Mathlib} + +\input{chapters/model_theory.tex} + +\chapter{Main Result} \input{chapters/main.tex} \ No newline at end of file diff --git a/blueprint/src/web.paux b/blueprint/src/web.paux index f154504..76313b9 100644 Binary files a/blueprint/src/web.paux and b/blueprint/src/web.paux differ diff --git a/blueprint/web/dep_graph_document.html b/blueprint/web/dep_graph_document.html index eade282..ac32b62 100644 --- a/blueprint/web/dep_graph_document.html +++ b/blueprint/web/dep_graph_document.html @@ -61,25 +61,25 @@

Dependencies

-
+
-