diff options
| -rw-r--r-- | AGENT.md | 165 | ||||
| -rw-r--r-- | KnowledgeBase.lean | 4 | ||||
| -rw-r--r-- | Main.lean | 814 | ||||
| -rw-r--r-- | Mathematics.lean | 5 | ||||
| -rw-r--r-- | README.md | 191 | ||||
| -rw-r--r-- | SocietyCulture.lean | 17 | ||||
| -rw-r--r-- | domain.tex | 273 |
7 files changed, 1268 insertions, 201 deletions
diff --git a/AGENT.md b/AGENT.md new file mode 100644 index 0000000..f7bc695 --- /dev/null +++ b/AGENT.md @@ -0,0 +1,165 @@ +# Lean-Based Knowledge Base Agent Instructions + +You are an AI agent with access to a persistent, formally verified knowledge base built in Lean 4. The knowledge base is stored as a Git repository of Lean files. You interact with it using the `kb` command-line tool. Every addition is type-checked by Lean's kernel, ensuring logical consistency. + +--- + +## 1. Key Design Principle: Explicit Domains + +Every declaration belongs to a **domain** that you name explicitly using `in <Domain>`. Each domain is stored as a separate `<Domain>.lean` file in the KB root. There is no automatic classification. + +**Choose domains based on what you want an agent to load together.** For example: +- `Ontology` — base types (`Entity`, `Person`, `Place`, …) that everything else depends on +- `People` — instances, properties, and facts about specific people +- `Geography` — instances and facts about places +- `Finance` — financial formulas and data +- `Physics` — physical constants and laws + +An agent loading only `People` facts into its context window would run: `kb list all of People`. + +--- + +## 2. Session Start Protocol + +```bash +# Orient yourself: see what domains and declarations exist +kb list all +kb domains stats + +# Recall declarations in a specific domain +kb list all of Ontology +kb list all of People +``` + +--- + +## 3. Adding Knowledge + +Every `add` command requires `in <Domain>` at the end. + +| Command | Purpose | Example | +|---------|---------|---------| +| `kb add type <n> [extends <Parent>] in <D>` | Declare a type | `kb add type Person extends Entity in Ontology` | +| `kb add instance <n> : <Type> in <D>` | Declare an individual | `kb add instance socrates : Person in People` | +| `kb add prop <n> : <DomType> -> <Range> in <D>` | Declare a property | `kb add prop birthYear : Person -> Nat in People` | +| `kb add rel <n> : <D1> -> <D2> -> Prop in <D>` | Declare a relation | `kb add rel bornIn : Person -> Place -> Prop in People` | +| `kb add fact <fact> in <D>` | Assert a fact | `kb add fact birthYear(socrates) = 470 in People` | +| `kb add rule <n> : <statement> in <D>` | Add a logical rule | `kb add rule ancestors_transitive : ∀ x y z, parentOf x y → parentOf y z → ancestorOf x z in Ontology` | +| `kb add def <n> <params> : <Type> := <body> in <D>` | Define a shortcut | `kb add def yearsToDouble (r : Float) : Float := Float.log 2 / r in Finance` | + +### Notes + +- Both `→` (Unicode) and `->` (ASCII) are accepted as type arrows. +- Fact syntax: `prop(inst) = value` or `rel(inst1, inst2)`. +- Domains are created automatically when first used — no `create domain` step needed. +- Put base types in a shared domain (e.g. `Ontology`) that other domains can depend on. + +--- + +## 4. Querying the Knowledge Base + +| Command | Description | Example | +|---------|-------------|---------| +| `kb eval <expr>` | Compute a value | `kb eval "yearsToDouble 0.05"` | +| `kb query <prop>` | Ask if a proposition is provable | `kb query "even (2 + 2)"` | +| `kb list all of <Domain>` | List all declarations in a domain | `kb list all of People` | + +### Query semantics + +- `kb eval` runs Lean's `#eval` on the expression. +- `kb query` attempts to prove the proposition using `decide`, `aesop`, or `simp`. Returns `Yes`, `No`, or `Unknown`. + +--- + +## 5. Checking Consistency and Committing + +Add all facts first, then verify and commit in one step: + +```bash +kb check +kb commit "Added Socrates and basic ontology" +``` + +`kb check` rewrites `KnowledgeBase.lean` to import every domain file on disk, injects cross-domain imports where needed, then runs `lake build`. `kb commit` does the same before committing to Git. + +**Do not check after each individual fact.** Batch your additions, then check once. + +--- + +## 6. Example Workflow + +```bash +# Base ontology (shared types everything else depends on) +kb add type Entity in Ontology +kb add type Person extends Entity in Ontology +kb add type Place extends Entity in Ontology +kb add type City extends Place in Ontology + +# Domain-specific properties and relations +kb add prop birthYear : Person -> Nat in People +kb add rel bornIn : Person -> Place -> Prop in People + +# Instances +kb add instance socrates : Person in People +kb add instance athens : City in People + +# Facts +kb add fact birthYear(socrates) = 470 in People +kb add fact bornIn(socrates, athens) in People + +# Verify and commit everything at once +kb check +kb commit "Added Socrates and basic person/place ontology" +``` + +--- + +## 7. Removing Declarations + +```bash +kb rm <name> +``` + +The tool warns if other declarations depend on the one being removed. Remove dependents first. + +--- + +## 8. Reusable Definitions + +```bash +kb add def yearsToDouble (r : Float) : Float := Float.log 2 / r in Finance +kb eval "yearsToDouble 0.05" +kb list defs +kb show def yearsToDouble +``` + +--- + +## 9. Best Practices + +- **Put base types in one domain** (e.g. `Ontology`) so all other domains can import it cleanly. +- **Group by agent-loadable context**: a domain should contain what an agent needs for a specific task. +- **Use meaningful domain names**: `People`, `Physics`, `Finance`, `Geography` — not `Domain1`. +- **Prefer `def` over `axiom` for computed facts** — definitions are safer and evaluable. +- **Run `kb check` once after a batch** of additions, not after each one. +- **Commit with descriptive messages** so the KB history is readable. + +--- + +## 10. Session End Protocol + +```bash +kb commit "Session summary: what was added" +kb list all # Review final state +kb domains stats # Confirm counts are as expected +``` + +--- + +## 11. Need Help? + +```bash +kb help +``` + +Lean error messages are forwarded directly. A typical error like `unknown identifier 'Person'` means the type was declared in another domain file that hasn't been imported yet — run `kb check` to sync imports, or check that you added the base type before its dependents. diff --git a/KnowledgeBase.lean b/KnowledgeBase.lean new file mode 100644 index 0000000..a5728c3 --- /dev/null +++ b/KnowledgeBase.lean @@ -0,0 +1,4 @@ +-- KnowledgeBase root module (auto-generated by kb) + +import Mathematics +import SocietyCulture @@ -3,266 +3,680 @@ import Lean open Lean IO -------------------------------------------------------------------------------- --- 1. Data structures for commands and knowledge base state +-- 1. Data structures +-- +-- Every declaration carries an explicit `domain` chosen by the user. +-- Domains are arbitrary identifiers (e.g. "Ontology", "Physics", "Finance"). +-- Each domain maps to a single <domain>.lean file in the KB root. -------------------------------------------------------------------------------- inductive KBCommand where - | Init (dir : String) - | AddType (name : String) (parent : Option String) - | AddInstance (name : String) (typeName : String) - | AddProp (name : String) (domain : String) (range : String) - | AddRel (name : String) (dom1 : String) (dom2 : String) - | AddFact (fact : String) - | AddRule (name : String) (statement : String) - | AddDef (name : String) (params : String) (type : String) (body : String) - | Remove (name : String) - | List (what : String) (filter : Option String) - | ShowDef (name : String) - | Eval (expr : String) - | Query (prop : String) + | Init (dir : String) + | AddType (name : String) (parent : Option String) (domain : String) + | AddInstance (name : String) (typeName : String) (domain : String) + | AddProp (name : String) (domType : String) (range : String) (domain : String) + | AddRel (name : String) (dom1 : String) (dom2 : String) (domain : String) + | AddFact (fact : String) (domain : String) + | AddRule (name : String) (statement : String) (domain : String) + | AddDef (name : String) (params : String) (type : String) (body : String) (domain : String) + | Remove (name : String) + | List (what : String) (filter : Option String) + | ShowDef (name : String) + | Eval (expr : String) + | Query (prop : String) | Check - | Commit (msg : String) + | Commit (msg : String) | Status - | Domains -- new: show domain hierarchy - | DomainsStats -- new: show statistics per domain (stub) + | Domains + | DomainsStats | Help | Exit deriving Repr +structure KBDecl where + kind : String -- "type" | "instance" | "prop" | "rel" | "fact" | "rule" | "def" + name : String + lean : String -- Lean 4 source text emitted to disk + domain : String -- user-chosen domain stem (becomes <domain>.lean) +deriving Repr, Inhabited + structure KBState where - root : System.FilePath + root : System.FilePath + decls : Array KBDecl + +-------------------------------------------------------------------------------- +-- 2. Lean-4-safe utility functions +-------------------------------------------------------------------------------- + +/-- True when `needle` appears anywhere in `haystack`. -/ +def strContains (haystack needle : String) : Bool := + if needle.isEmpty then true + else (haystack.splitOn needle).length > 1 + +/-- Remove duplicate strings from a list, keeping first occurrence. -/ +def dedupStrings (xs : List String) : List String := + xs.foldl (fun acc x => if acc.contains x then acc else acc ++ [x]) [] + +/-- ASCII-only lowercase. -/ +def strToLower (s : String) : String := + s.map fun c => + if c.toNat >= 'A'.toNat && c.toNat <= 'Z'.toNat + then Char.ofNat (c.toNat + 32) else c -------------------------------------------------------------------------------- --- 2. Command parsing (simple, based on whitespace) +-- 3. Command parsing +-- +-- Every `add` command requires an explicit `in <Domain>` suffix that names the +-- destination file. Both `→` and `->` are accepted as type arrows. +-- +-- Syntax: +-- add type <Name> [extends <Parent>] in <Domain> +-- add instance <name> : <Type> in <Domain> +-- add prop <name> : <DomType> -> <Range> in <Domain> +-- add rel <name> : <D1> -> <D2> -> Prop in <Domain> +-- add fact <fact> in <Domain> +-- add rule <name> : <statement> in <Domain> +-- add def <name> <params> : <T> := <body> in <Domain> -------------------------------------------------------------------------------- def parseCommand (line : String) : Option KBCommand := - let parts := line.trim.splitOn " " |>.filter (not ∘ String.isEmpty) + -- Normalise Unicode → so either arrow style works. + let normalised := line.trim.replace "→" "->" + let parts := normalised.splitOn " " |>.filter (not ∘ String.isEmpty) + let raw := line.trim -- used for suffix-style extraction match parts with + -- ── init ──────────────────────────────────────────────────────────────── | ["init", dir] => some (.Init dir) - | ["add", "type", name] => some (.AddType name none) - | ["add", "type", name, "extends", parent] => some (.AddType name (some parent)) - | ["add", "instance", name, ":", typeName] => some (.AddInstance name typeName) - | ["add", "prop", name, ":", domain, "->", range] => some (.AddProp name domain range) - | ["add", "rel", name, ":", dom1, "->", dom2, "->", "Prop"] => some (.AddRel name dom1 dom2) - | ["add", "fact", _] => - some (.AddFact (line.drop 9)) -- drop "add fact " - | ["add", "rule", name, ":", _] => - let n := 9 + name.length + 2 - some (.AddRule name (line.drop n)) - | ["add", "def", name, params, ":", type, ":=", body] => - some (.AddDef name params type body) - | ["rm", name] => some (.Remove name) - | ["list", what] => some (.List what none) - | ["list", what, "of", filter] => some (.List what (some filter)) - | ["show", "def", name] => some (.ShowDef name) - | ["eval", expr] => some (.Eval expr) - | ["query", prop] => some (.Query prop) - | ["check"] => some .Check - | ["commit", msg] => some (.Commit msg) - | ["status"] => some .Status - | ["domains"] => some .Domains -- new - | ["domains", "stats"] => some .DomainsStats -- new - | ["help"] => some .Help - | ["exit"] => some .Exit - | _ => none + -- ── add type ──────────────────────────────────────────────────────────── + | ["add", "type", name, "in", dom] => + some (.AddType name none dom) + | ["add", "type", name, "extends", par, "in", dom] => + some (.AddType name (some par) dom) + -- ── add instance ──────────────────────────────────────────────────────── + | ["add", "instance", name, ":", ty, "in", dom] => + some (.AddInstance name ty dom) + -- ── add prop ──────────────────────────────────────────────────────────── + | ["add", "prop", name, ":", dt, "->", rng, "in", dom] => + some (.AddProp name dt rng dom) + -- ── add rel ───────────────────────────────────────────────────────────── + | ["add", "rel", name, ":", d1, "->", d2, "->", "Prop", "in", dom] => + some (.AddRel name d1 d2 dom) + -- ── add fact (suffix style: everything between "add fact " and " in <D>") + | "add" :: "fact" :: _ => + -- Find " in " as a domain separator (last occurrence wins). + let body := raw.drop "add fact ".length + let segs := body.splitOn " in " + if segs.length >= 2 then + let dom := segs.getLast!.trim + -- Rejoin all but the last segment in case the fact itself contains " in " + let fact := (segs.dropLast |> String.intercalate " in ").trim + some (.AddFact fact dom) + else none + -- ── add rule (suffix style) ───────────────────────────────────────────── + | "add" :: "rule" :: name :: ":" :: _ => + let afterColon := raw.drop ("add rule " ++ name ++ " : ").length + let segs := afterColon.splitOn " in " + if segs.length >= 2 then + let dom := segs.getLast!.trim + let stmt := (segs.dropLast |> String.intercalate " in ").trim + some (.AddRule name stmt dom) + else none + -- ── add def ───────────────────────────────────────────────────────────── + -- Syntax: add def <n> <params> : <type> := <body> in <Domain> + | "add" :: "def" :: name :: _ => + let afterName := raw.drop ("add def " ++ name ++ " ").length + let domSegs := afterName.splitOn " in " + if domSegs.length < 2 then none + else + let dom := domSegs.getLast!.trim + let defBody := (domSegs.dropLast |> String.intercalate " in ").trim + let colonSegs := defBody.splitOn " : " + if colonSegs.length < 2 then none + else + let params := (colonSegs.headD "").trim + let typeBody := (colonSegs.tail |> String.intercalate " : ").trim + let assignSegs := typeBody.splitOn " := " + if assignSegs.length < 2 then none + else + let ty := (assignSegs.headD "").trim + let body := (assignSegs.tail |> String.intercalate " := ").trim + some (.AddDef name params ty body dom) + -- ── other commands (no domain argument) ────────────────────────────────── + | ["rm", name] => some (.Remove name) + | ["list", what] => some (.List what none) + | ["list", what, "of", f] => some (.List what (some f)) + | ["show", "def", name] => some (.ShowDef name) + | "eval" :: _ => some (.Eval (raw.drop "eval ".length)) + | "query" :: _ => some (.Query (raw.drop "query ".length)) + | ["check"] => some .Check + | "commit" :: _ => some (.Commit (raw.drop "commit ".length)) + | ["status"] => some .Status + | ["domains"] => some .Domains + | ["domains", "stats"] => some .DomainsStats + | ["help"] => some .Help + | ["exit"] => some .Exit + | _ => none -------------------------------------------------------------------------------- --- 3. Handlers (stubs with informative output) +-- 4. File-system helpers -------------------------------------------------------------------------------- -def addType (name : String) (parent : Option String) : IO Unit := do - let parentMsg := match parent with | some p => s!" extending '{p}'" | none => "" - println s!"[Stub] Adding type '{name}'{parentMsg}" - println " Would append to appropriate .lean file and run `lake build`." +def domainPath (root : System.FilePath) (domain : String) : System.FilePath := + root / (domain ++ ".lean") -def addInstance (name : String) (typeName : String) : IO Unit := do - println s!"[Stub] Adding instance '{name} : {typeName}'" +/-- Append `decl` to a domain file, creating it with a module header if new. -/ +def appendToDomain (root : System.FilePath) (domain decl : String) : IO Unit := do + let path := domainPath root domain + unless (← path.pathExists) do + IO.FS.writeFile path s!"-- Knowledge Base: {domain}\n\n" + let handle ← IO.FS.Handle.mk path .append + handle.putStrLn decl + handle.flush -def addProp (name domain range : String) : IO Unit := do - println s!"[Stub] Adding property '{name} : {domain} -> {range}'" +def runProc (cmd : String) (args : Array String) (cwd : Option String := none) + : IO (UInt32 × String) := do + let child ← IO.Process.spawn { + cmd := cmd + args := args + cwd := cwd + stdout := .piped + stderr := .piped + } + let stdoutTask ← IO.asTask child.stdout.readToEnd Task.Priority.dedicated + let stderrOut ← child.stderr.readToEnd + let stdoutOut ← IO.ofExcept stdoutTask.get + let code ← child.wait + return (code, stdoutOut ++ stderrOut) -def addRel (name dom1 dom2 : String) : IO Unit := do - println s!"[Stub] Adding relation '{name} : {dom1} -> {dom2} -> Prop'" +def runProcPrint (cmd : String) (args : Array String) (cwd : Option String := none) + : IO UInt32 := do + let (code, out) ← runProc cmd args cwd + unless out.isEmpty do println out + return code -def addFact (fact : String) : IO Unit := do - println s!"[Stub] Adding fact: {fact}" +-------------------------------------------------------------------------------- +-- 5. Lean snippet generators +-------------------------------------------------------------------------------- -def addRule (name stmt : String) : IO Unit := do - println s!"[Stub] Adding rule '{name} : {stmt}'" +def genType (name : String) (parent : Option String) : String := + match parent with + | none => s!"opaque {name} : Type" + | some p => + s!"opaque {name} : Type\n" ++ + s!"-- {name} extends {p}\n" ++ + s!"axiom {name}.val : {name} → {p}" -def addDef (name params type body : String) : IO Unit := do - println s!"[Stub] Adding definition '{name} {params} : {type} := {body}'" +def genInstance (name typeName : String) : String := + s!"opaque {name} : {typeName}" -def removeDecl (name : String) : IO Unit := do - println s!"[Stub] Removing declaration '{name}' (checking dependencies)" +def genProp (name domType range : String) : String := + s!"opaque {name} : {domType} → {range}" -def listDecls (what : String) (filter : Option String) : IO Unit := do - let filterMsg := match filter with | some f => s!" of {f}" | none => "" - println s!"[Stub] Listing {what}{filterMsg}" +def genRel (name dom1 dom2 : String) : String := + s!"opaque {name} : {dom1} → {dom2} → Prop" -def showDef (name : String) : IO Unit := do - println s!"[Stub] Showing definition of '{name}'" +/-- Parse a fact string and produce a Lean axiom. + Accepted syntax: + `prop(inst) = value` → `axiom fact_prop_inst : prop inst = value` + `rel(inst1, inst2)` → `axiom fact_rel_inst1_inst2 : rel inst1 inst2` -/ +def genFact (fact : String) : String := + let byOpenParen := fact.splitOn "(" + if byOpenParen.length < 2 then + -- No parentheses: bare `lhs = rhs` + let byEq := fact.splitOn "=" + if byEq.length >= 2 then + let lhs := (byEq.headD "").trim + let rhs := (byEq.tail.headD "").trim + s!"axiom fact_{lhs} : {lhs} = {rhs}" + else + s!"-- unrecognised fact: {fact}\n-- expected: prop(inst) = val or rel(a, b)" + else + let funcName := (byOpenParen.headD "").trim + let afterOpen := byOpenParen.tail |> String.intercalate "(" + let byClose := afterOpen.splitOn ")" + let argsStr := (byClose.headD "").trim + let args := argsStr.splitOn "," |>.map String.trim + let tag := args.foldl (· ++ "_" ++ ·) funcName + let argStr := String.intercalate " " args + let afterClose := byClose.tail |> String.intercalate ")" + let byEq := afterClose.splitOn "=" + if byEq.length >= 2 then + let rhs := (byEq.tail.headD "").trim + s!"axiom fact_{tag} : {funcName} {argStr} = {rhs}" + else + s!"axiom fact_{tag} : {funcName} {argStr}" -def evalExpr (expr : String) : IO Unit := do - println s!"[Stub] Evaluating: {expr}" - println " Would run `#eval` in a temporary Lean file and return result." +def genRule (name stmt : String) : String := + s!"axiom {name} : {stmt}" -def queryProp (prop : String) : IO Unit := do - println s!"[Stub] Querying: {prop}" - println " Would attempt to prove with `aesop` and return Yes/No/Unknown." +def genDef (name params type body : String) : String := + s!"def {name} ({params}) : {type} := {body}" -def checkKB : IO Unit := do - println "Running `lake build` to verify knowledge base..." - let child ← IO.Process.spawn { cmd := "lake", args := #["build"] } - let exitCode ← child.wait - if exitCode == 0 then - println "Consistent (build succeeded)." - else - println "Inconsistent! Build failed." +-------------------------------------------------------------------------------- +-- 6. Duplicate check +-------------------------------------------------------------------------------- -def commitChanges (msg : String) : IO Unit := do - println s!"[Stub] Committing with message: {msg}" - println " Would run `git add . && git commit -m \"...\"` after `kb check`." +def isDuplicate (state : KBState) (kind name : String) : Bool := + state.decls.any (fun d => d.kind == kind && d.name == name) -def status : IO Unit := do - println "[Stub] Showing git status and unverified changes." +-------------------------------------------------------------------------------- +-- 7. Add handlers (domain is always explicit — no auto-classification) +-------------------------------------------------------------------------------- -def initKB (dir : String) : IO Unit := do - println s!"[Stub] Initializing new knowledge base in '{dir}'" - println " Would create directory structure and lakefile.lean." +def addType (stateRef : IO.Ref KBState) (name : String) (parent : Option String) + (domain : String) : IO Unit := do + let state ← stateRef.get + if isDuplicate state "type" name then + println s!"Error: type '{name}' already exists."; return + let lean := genType name parent + appendToDomain state.root domain lean + stateRef.modify fun s => { s with decls := s.decls.push { kind := "type", name, lean, domain } } + let ext := parent.map (fun p => s!" (extends {p})") |>.getD "" + println s!"Added type '{name}'{ext} → {domain}.lean" + +def addInstance (stateRef : IO.Ref KBState) (name typeName domain : String) : IO Unit := do + let state ← stateRef.get + if isDuplicate state "instance" name then + println s!"Error: instance '{name}' already exists."; return + let lean := genInstance name typeName + appendToDomain state.root domain lean + stateRef.modify fun s => { s with decls := s.decls.push { kind := "instance", name, lean, domain } } + println s!"Added instance '{name} : {typeName}' → {domain}.lean" + +def addProp (stateRef : IO.Ref KBState) (name domType range domain : String) : IO Unit := do + let state ← stateRef.get + if isDuplicate state "prop" name then + println s!"Error: property '{name}' already exists."; return + let lean := genProp name domType range + appendToDomain state.root domain lean + stateRef.modify fun s => { s with decls := s.decls.push { kind := "prop", name, lean, domain } } + println s!"Added property '{name} : {domType} → {range}' → {domain}.lean" + +def addRel (stateRef : IO.Ref KBState) (name dom1 dom2 domain : String) : IO Unit := do + let state ← stateRef.get + if isDuplicate state "rel" name then + println s!"Error: relation '{name}' already exists."; return + let lean := genRel name dom1 dom2 + appendToDomain state.root domain lean + stateRef.modify fun s => { s with decls := s.decls.push { kind := "rel", name, lean, domain } } + println s!"Added relation '{name} : {dom1} → {dom2} → Prop' → {domain}.lean" + +def addFact (stateRef : IO.Ref KBState) (fact domain : String) : IO Unit := do + let state ← stateRef.get + let declName := "fact:" ++ fact + if isDuplicate state "fact" declName then + println s!"Warning: fact already exists: {fact}"; return + let lean := genFact fact + appendToDomain state.root domain lean + let newDecl : KBDecl := { kind := "fact", name := declName, lean, domain } + stateRef.modify fun s => { s with decls := s.decls.push newDecl } + println s!"Added fact: {fact} → {domain}.lean" + +def addRule (stateRef : IO.Ref KBState) (name stmt domain : String) : IO Unit := do + let state ← stateRef.get + if isDuplicate state "rule" name then + println s!"Error: rule '{name}' already exists."; return + let lean := genRule name stmt + appendToDomain state.root domain lean + stateRef.modify fun s => { s with decls := s.decls.push { kind := "rule", name, lean, domain } } + println s!"Added rule '{name}' → {domain}.lean" + +def addDef (stateRef : IO.Ref KBState) (name params type body domain : String) : IO Unit := do + let state ← stateRef.get + if isDuplicate state "def" name then + println s!"Error: definition '{name}' already exists. Use 'rm {name}' first."; return + let lean := genDef name params type body + appendToDomain state.root domain lean + stateRef.modify fun s => { s with decls := s.decls.push { kind := "def", name, lean, domain } } + println s!"Added definition '{name} ({params}) : {type} := {body}' → {domain}.lean" -------------------------------------------------------------------------------- --- 4. Domain hierarchy (extracted from the original help text) +-- 8. Remove handler -------------------------------------------------------------------------------- -def domainHierarchy : String := - "Domain classification (initial curated structure):\n" ++ - "- Mathematics\n" ++ - " • Elementary Math (Arithmetic, Fractions, Percentages)\n" ++ - " • Algebra\n" ++ - " • Geometry (Plane, Solid, Coordinate, Transformations, High‑D, Packing, Curves, Polyforms, Topology, Tilings)\n" ++ - " • Plotting (Functions, Equations, Parametric, Inequalities, Number Lines, Polar)\n" ++ - " • Calculus (Integrals, Derivatives, Limits, Sequences, Products, Series, Sums, Vector Analysis, Transforms, Applications, Continuity, Domain/Range)\n" ++ - " • Differential Equations\n" ++ - " • Statistics (Descriptive, Inference, Regression, Random Variables)\n" ++ - " • Functions (Domain/Range, Injectivity/Surjectivity, Continuity, Periodic, Odd/Even, Special, Number Theoretic, Representation)\n" ++ - "- Science & Technology\n" ++ - " • Physics (Mechanics, Oscillations, Statistical Physics, Thermodynamics, Electricity & Magnetism, Optics, Relativity, Nuclear, Quantum, Particle, Astrophysics, Constants, Principles, Effects, Fluid Mechanics)\n" ++ - " • Chemistry\n" ++ - " • Units & Measures\n" ++ - " • Engineering (Aerospace, Energy, Electrical, Control Systems, Mechanical, Civil, Fluid Mechanics, Sound, Steam Tables, Measurement)\n" ++ - " • Computational Sciences (Cellular Automata, Substitution Systems, Turing Machines, Complexity, Algebraic Codes, Fractals, Image Processing, Hashing)\n" ++ - " • Earth Sciences\n" ++ - " • Life Sciences (Human Anatomy, Animal Anatomy, Neuroscience, Genomics, Molecular Biology, Animals & Plants)\n" ++ - " • Space & Astronomy\n" ++ - "- Society & Culture\n" ++ - " • People\n" ++ - " • Arts & Media\n" ++ - " • History\n" ++ - " • Words & Linguistics (Word Properties, Languages, Document Length, Notable Texts, Transliterations, Morse, Soundex, Encodings, Emotions)\n" ++ - " • Money & Finance (Stock Data, Mortgages, Salaries, Bonds, Derivatives, Income Tax, Sales Tax)\n" ++ - " • Dates & Times\n" ++ - " • Food & Nutrition\n" ++ - " • Demographics (Health, Age/Sex, Gender, Business, Citizenship, Crime, Education, Income, Language, Race, Marriage, Mobility, Religion, Military, HDI)\n" ++ - "- Everyday Life\n" ++ - " • Personal Health (Exercise, Nutrition, Child Growth)\n" ++ - " • Personal Finance (Mortgages, Stocks, Currency, Cost of Living, Gas, Food, Electricity)\n" ++ - " • Entertainment\n" ++ - " • Household Science\n" ++ - " • Household Math\n" ++ - " • Programming\n" ++ - " • Hobbies\n" ++ - " • Today's World (Economy, Finland Economy, Weather)\n" +def removeDecl (stateRef : IO.Ref KBState) (name : String) : IO Unit := do + let state ← stateRef.get + let targets := state.decls.filter (fun d => d.name == name) + if targets.isEmpty then + println s!"Error: '{name}' not found."; return + let dependents := state.decls.filter (fun d => + d.name != name && strContains d.lean name) + unless dependents.isEmpty do + println s!"Warning: these declarations reference '{name}':" + for dep in dependents do + println s!" [{dep.kind}] {dep.name}" + println "Remove dependents first for a consistent KB." + stateRef.modify fun s => { s with decls := s.decls.filter (fun d => d.name != name) } + let domains := dedupStrings (targets.map (·.domain)).toList + for domain in domains do + let path := domainPath state.root domain + if ← path.pathExists then + let contents ← IO.FS.readFile path + let kept := contents.splitOn "\n" |>.filter (fun l => !strContains l name) + IO.FS.writeFile path (String.intercalate "\n" kept) + println s!"Removed '{name}'." -------------------------------------------------------------------------------- --- 5. Help text (now includes the new commands) +-- 9. List / ShowDef -------------------------------------------------------------------------------- -def helpText : String := - "Lean4 Knowledge Base CLI (kb)\n" ++ - "Usage: kb <command> [arguments]\n\n" ++ - "Commands:\n" ++ - " init <dir> Create a new knowledge base repository.\n" ++ - " add type <name> [extends <p>] Define a new type.\n" ++ - " add instance <name> : <type> Declare an instance.\n" ++ - " add prop <name> : <d> -> <r> Add a property.\n" ++ - " add rel <name> : <d1> -> <d2> -> Prop Add a relation.\n" ++ - " add fact <fact> Add a fact.\n" ++ - " add rule <name> : <statement> Add a logical rule.\n" ++ - " add def <name> <params> : <t> := <body> Define a shortcut.\n" ++ - " rm <name> Remove a declaration.\n" ++ - " list <types|instances|props|rels|facts|defs> [of <filter>] List.\n" ++ - " show def <name> Show a shortcut definition.\n" ++ - " eval <expr> Evaluate a computable expression.\n" ++ - " query <prop> Ask whether a proposition is provable.\n" ++ - " check Run `lake build` to verify consistency.\n" ++ - " commit <message> Commit all changes.\n" ++ - " status Show git status.\n" ++ - " domains Show the hierarchical domain classification.\n" ++ - " domains stats Show statistics per domain (stub).\n" ++ - " help Show this help.\n" ++ - " exit Exit the CLI.\n" +def normKind (w : String) : String := + if w == "types" then "type" + else if w == "instances" then "instance" + else if w == "props" then "prop" + else if w == "rels" then "rel" + else if w == "facts" then "fact" + else if w == "rules" then "rule" + else if w == "defs" then "def" + else w + +def listDecls (stateRef : IO.Ref KBState) (what : String) (filter : Option String) : IO Unit := do + let state ← stateRef.get + let nk := normKind what + let matchKind : KBDecl → Bool := + if nk == "all" then fun _ => true else fun d => d.kind == nk + let matchFilter : KBDecl → Bool := + match filter with + | none => fun _ => true + | some f => + let fl := strToLower f + fun d => + strContains (strToLower d.name) fl || + strContains (strToLower d.domain) fl || + strContains (strToLower d.lean) fl + let hits := state.decls.filter (fun d => matchKind d && matchFilter d) + if hits.isEmpty then println s!"(no {what} found)" + else for d in hits do + println s!"[{d.kind}] {d.name} ({d.domain})" + +def showDef (stateRef : IO.Ref KBState) (name : String) : IO Unit := do + let state ← stateRef.get + let hits := state.decls.filter (fun d => d.name == name) + if hits.isEmpty then println s!"'{name}' not found." + else for d in hits do + println s!"-- [{d.kind}] {d.name} (domain: {d.domain})" + println d.lean -------------------------------------------------------------------------------- --- 6. Domain command handlers +-- 10. Eval / Query -------------------------------------------------------------------------------- -def listDomains : IO Unit := do - println domainHierarchy +def buildImports (state : KBState) : IO String := do + let domains := dedupStrings (state.decls.map (·.domain)).toList + let mut imports := "" + for domain in domains do + if ← (domainPath state.root domain).pathExists then + imports := imports ++ s!"import {domain}\n" + return imports -def domainsStats : IO Unit := do - println "[Stub] Domain statistics (would show counts of types/instances per domain)" +def runLeanSnippet (state : KBState) (snippet : String) : IO (UInt32 × String) := do + let imports ← buildImports state + let tmpPath : System.FilePath := state.root / "_kb_tmp.lean" + IO.FS.writeFile tmpPath (imports ++ "\n" ++ snippet ++ "\n") + let result ← runProc "lean" #[tmpPath.toString] (some state.root.toString) + try IO.FS.removeFile tmpPath catch _ => pure () + return result + +def evalExpr (stateRef : IO.Ref KBState) (expr : String) : IO Unit := do + let state ← stateRef.get + let (code, out) ← runLeanSnippet state s!"#eval {expr}" + if code == 0 then println out + else do + println s!"Lean error evaluating `{expr}`:" + println out + +def queryProp (stateRef : IO.Ref KBState) (prop : String) : IO Unit := do + let state ← stateRef.get + let snippet := + "set_option maxHeartbeats 4000 in\n" ++ + s!"#check (by first | decide | aesop | simp : {prop})" + let (code, out) ← runLeanSnippet state snippet + if code == 0 then + println "Yes (provable)" + else if strContains out "false" || strContains out "False" then + println "No (contradiction found)" + else do + println "Unknown (could not prove or disprove with decide / aesop / simp)" + unless out.isEmpty do println out + +-------------------------------------------------------------------------------- +-- 11. Build / commit / status +-- +-- syncRootModule rewrites KnowledgeBase.lean to import every domain file that +-- currently exists on disk, then injects `import <base>` into any domain file +-- that references names from another domain file it knows about. +-- This ensures `lake build` compiles the entire KB, not just the root stub. +-------------------------------------------------------------------------------- + +/-- Collect all domain stems that have a .lean file in the KB root. -/ +def existingDomains (root : System.FilePath) : IO (List String) := do + let reserved := ["KnowledgeBase", "lakefile", "_kb_tmp"] + let entries ← System.FilePath.readDir root + let stems := entries.toList.filterMap fun e => + let name := e.fileName + if name.endsWith ".lean" then + let stem := name.dropRight ".lean".length + if reserved.contains stem then none else some stem + else none + return dedupStrings stems + +/-- Rewrite KnowledgeBase.lean to import all existing domain files. + Also prepend cross-domain imports into domain files that need them, + based on which domains are known to this session. -/ +def syncRootModule (root : System.FilePath) (state : KBState) : IO Unit := do + let allDomains ← existingDomains root + -- Build a mapping: domain → set of other domains it directly references. + -- A domain file references another if any of the *other* domain's declared + -- names appear in its own declaration texts. + for domain in allDomains do + let ownDecls := state.decls.filter (fun d => d.domain == domain) + let otherDomains := allDomains.filter (· != domain) + let mut needed : List String := [] + for other in otherDomains do + let otherDecls := state.decls.filter (fun d => d.domain == other) + -- Does any own decl's lean text mention a name from `other`? + let referenced := ownDecls.any fun od => + otherDecls.any fun od2 => strContains od.lean od2.name + if referenced then needed := needed ++ [other] + -- Inject missing imports at the top of the domain file. + if !needed.isEmpty then + let path := domainPath root domain + if ← path.pathExists then + let contents ← IO.FS.readFile path + let missing := needed.filter (fun imp => !strContains contents s!"import {imp}") + unless missing.isEmpty do + let newHeader := (missing.map (fun imp => s!"import {imp}")).foldl + (· ++ "\n" ++ ·) "" + IO.FS.writeFile path (newHeader ++ "\n" ++ contents) + -- Rewrite the root module. + let mut rootContent := "-- KnowledgeBase root module (auto-generated by kb)\n\n" + for stem in allDomains do + rootContent := rootContent ++ s!"import {stem}\n" + IO.FS.writeFile (root / "KnowledgeBase.lean") rootContent + +def checkKB (stateRef : IO.Ref KBState) : IO Unit := do + let state ← stateRef.get + syncRootModule state.root state + println "Running `lake build`…" + let code ← runProcPrint "lake" #["build"] (some state.root.toString) + println (if code == 0 then "✓ Consistent (build succeeded)." + else "✗ Build failed — see errors above.") + +def commitChanges (stateRef : IO.Ref KBState) (msg : String) : IO Unit := do + let state ← stateRef.get + let dir := state.root.toString + syncRootModule state.root state + println "Verifying before commit…" + let buildCode ← runProcPrint "lake" #["build"] (some dir) + if buildCode != 0 then + println "Commit aborted: build failed. Fix errors and retry."; return + let _ ← runProcPrint "git" #["add", "."] (some dir) + let code ← runProcPrint "git" #["commit", "-m", msg] (some dir) + if code == 0 then println s!"Committed: \"{msg}\"" + else println "(Nothing new to commit — working tree clean.)" + +def showStatus (stateRef : IO.Ref KBState) : IO Unit := do + let state ← stateRef.get + let dir := state.root.toString + println "=== git status ===" + let _ ← runProcPrint "git" #["status", "--short"] (some dir) + println "\n=== session summary ===" + println s!" KB root : {state.root}" + println s!" decls : {state.decls.size} declaration(s) in memory this session" + +-------------------------------------------------------------------------------- +-- 12. Init +-------------------------------------------------------------------------------- + +def initKB (dir : String) : IO Unit := do + let root : System.FilePath := System.FilePath.mk dir + let mkCode ← runProcPrint "mkdir" #["-p", dir] + if mkCode != 0 then println s!"Error: could not create '{dir}'."; return + IO.FS.writeFile (root / "lakefile.lean") + "import Lake\nopen Lake DSL\n\npackage KnowledgeBase where\n\nlean_lib KnowledgeBase where\n" + IO.FS.writeFile (root / "KnowledgeBase.lean") + "-- KnowledgeBase root module\n-- Run `kb check` to populate this file.\n" + let _ ← runProcPrint "git" #["init"] (some dir) + let _ ← runProcPrint "git" #["add", "."] (some dir) + let _ ← runProcPrint "git" #["commit", "-m", "Initial kb scaffold"] (some dir) + println s!"Initialised knowledge base in '{dir}'." -------------------------------------------------------------------------------- --- 7. Main loop +-- 13. Domain listing / stats -------------------------------------------------------------------------------- -partial def processCommand (stateRef : IO.Ref KBState) (line : String) : IO Unit := do - let _ := stateRef -- silence unused warning +def listDomains (stateRef : IO.Ref KBState) : IO Unit := do + let state ← stateRef.get + let domains := dedupStrings (state.decls.map (·.domain)).toList + if domains.isEmpty then + println "(no domains in current session — use 'add … in <Domain>' to create one)" + else do + println "Domains active this session:" + for dom in domains do + let n := (state.decls.filter (fun d => d.domain == dom)).size + println s!" {dom} ({n} declaration(s))" + +def domainsStats (stateRef : IO.Ref KBState) : IO Unit := do + let state ← stateRef.get + let domains := dedupStrings (state.decls.map (·.domain)).toList + println "=== Domain statistics (current session) ===" + if domains.isEmpty then + println " (none)" + else + for dom in domains do + let ds := state.decls.filter (fun d => d.domain == dom) + println s!" {dom}: {ds.size} declaration(s)" + for k in ["type","instance","prop","rel","fact","rule","def"] do + let n := (ds.filter (fun d => d.kind == k)).size + if n > 0 then println s!" {k}: {n}" + println "\n=== By kind (all domains) ===" + for k in ["type","instance","prop","rel","fact","rule","def"] do + let n := (state.decls.filter (fun d => d.kind == k)).size + if n > 0 then println s!" {k}: {n}" + println s!"\n Total: {state.decls.size}" + +-------------------------------------------------------------------------------- +-- 14. Help text +-------------------------------------------------------------------------------- + +def helpText : String := + "Lean4 Knowledge Base CLI (kb)\n" ++ + "Usage: <command> [arguments]\n\n" ++ + "Every declaration must specify its destination domain file explicitly\n" ++ + "with `in <Domain>`. Domain names are arbitrary identifiers; each becomes\n" ++ + "a <Domain>.lean file in the KB root.\n\n" ++ + "Commands:\n" ++ + " init <dir>\n" ++ + " Create a new knowledge base repository in <dir>.\n\n" ++ + " add type <Name> [extends <Parent>] in <Domain>\n" ++ + " Declare a new type, optionally as a subtype of <Parent>.\n\n" ++ + " add instance <name> : <Type> in <Domain>\n" ++ + " Declare a named individual of the given type.\n\n" ++ + " add prop <name> : <DomType> -> <Range> in <Domain>\n" ++ + " Add a property mapping a type to a value type.\n\n" ++ + " add rel <name> : <D1> -> <D2> -> Prop in <Domain>\n" ++ + " Add a binary relation between two types.\n\n" ++ + " add fact <fact> in <Domain>\n" ++ + " Assert a fact. Syntax: prop(inst) = val or rel(a, b).\n\n" ++ + " add rule <name> : <statement> in <Domain>\n" ++ + " Add a universally quantified axiom.\n\n" ++ + " add def <name> <params> : <Type> := <body> in <Domain>\n" ++ + " Define a reusable computed shortcut.\n\n" ++ + " rm <name>\n" ++ + " Remove a declaration (warns about dependents).\n\n" ++ + " list <types|instances|props|rels|facts|rules|defs|all> [of <filter>]\n" ++ + " List declarations, optionally filtered by name/domain/content.\n\n" ++ + " show def <name>\n" ++ + " Print the Lean source of a named declaration.\n\n" ++ + " eval <expr>\n" ++ + " Evaluate a computable Lean expression via #eval.\n\n" ++ + " query <prop>\n" ++ + " Try to prove a proposition (Yes / No / Unknown).\n\n" ++ + " check\n" ++ + " Sync imports and run lake build to verify the whole KB.\n\n" ++ + " commit <message>\n" ++ + " Verify then git-commit all changes.\n\n" ++ + " status\n" ++ + " Show git status and session summary.\n\n" ++ + " domains\n" ++ + " List all domains active in this session with declaration counts.\n\n" ++ + " domains stats\n" ++ + " Detailed breakdown of declarations per domain and kind.\n\n" ++ + " help Show this message.\n" ++ + " exit Quit.\n\n" ++ + "Example workflow:\n" ++ + " add type Entity in Ontology\n" ++ + " add type Person extends Entity in Ontology\n" ++ + " add type Place extends Entity in Ontology\n" ++ + " add instance socrates : Person in People\n" ++ + " add prop birthYear : Person -> Nat in People\n" ++ + " add fact birthYear(socrates) = 470 in People\n" ++ + " check\n" ++ + " commit \"Added Socrates\"\n" + +-------------------------------------------------------------------------------- +-- 15. Main REPL loop +-------------------------------------------------------------------------------- + +partial def processCommand (stateRef : IO.Ref KBState) (line : String) : IO Bool := do match parseCommand line with - | none => println "Invalid command. Type 'help' for usage." + | none => + println s!"Unknown command: '{line}'." + println "Type 'help' for usage, including required 'in <Domain>' syntax." + return true | some cmd => match cmd with - | .Init dir => initKB dir - | .AddType name parent => addType name parent - | .AddInstance name ty => addInstance name ty - | .AddProp name dom ran => addProp name dom ran - | .AddRel name d1 d2 => addRel name d1 d2 - | .AddFact fact => addFact fact - | .AddRule name stmt => addRule name stmt - | .AddDef name params ty body => addDef name params ty body - | .Remove name => removeDecl name - | .List what filt => listDecls what filt - | .ShowDef name => showDef name - | .Eval expr => evalExpr expr - | .Query prop => queryProp prop - | .Check => checkKB - | .Commit msg => commitChanges msg - | .Status => status - | .Domains => listDomains - | .DomainsStats => domainsStats - | .Help => println helpText - | .Exit => throw (IO.userError "exit") + | .Init dir => initKB dir + | .AddType n p dom => addType stateRef n p dom + | .AddInstance n t dom => addInstance stateRef n t dom + | .AddProp n dt rng dom => addProp stateRef n dt rng dom + | .AddRel n d1 d2 dom => addRel stateRef n d1 d2 dom + | .AddFact f dom => addFact stateRef f dom + | .AddRule n s dom => addRule stateRef n s dom + | .AddDef n p t b dom => addDef stateRef n p t b dom + | .Remove n => removeDecl stateRef n + | .List w f => listDecls stateRef w f + | .ShowDef n => showDef stateRef n + | .Eval e => evalExpr stateRef e + | .Query p => queryProp stateRef p + | .Check => checkKB stateRef + | .Commit m => commitChanges stateRef m + | .Status => showStatus stateRef + | .Domains => listDomains stateRef + | .DomainsStats => domainsStats stateRef + | .Help => println helpText + | .Exit => return false + return true partial def main : IO Unit := do - println "Lean4 Knowledge Base CLI" - println "Type 'help' for commands." - let initialState : KBState := { root := System.FilePath.mk "." } - let stateRef ← IO.mkRef initialState + println "Lean4 Knowledge Base CLI — type 'help' for commands, 'exit' to quit." + let stateRef ← IO.mkRef (KBState.mk (System.FilePath.mk ".") #[]) let rec loop : IO Unit := do IO.print "kb> " let line ← (← IO.getStdin).getLine let trimmed := line.trim - if trimmed.isEmpty then loop - else - try - processCommand stateRef trimmed - if trimmed == "exit" then return () - else loop - catch e => - if e.toString == "exit" then return () - else do - println s!"Error: {e}" - loop + unless trimmed.isEmpty do + let cont ← processCommand stateRef trimmed + unless cont do return + loop loop diff --git a/Mathematics.lean b/Mathematics.lean new file mode 100644 index 0000000..59508fa --- /dev/null +++ b/Mathematics.lean @@ -0,0 +1,5 @@ +-- Knowledge Base domain: Mathematics + +opaque Entity : Type +opaque socrates : Philospher +axiom fact_birthYear_socrates : birthYear socrates = 420 @@ -1 +1,190 @@ -# kb
\ No newline at end of file +# kb — Lean 4 Knowledge Base CLI + +A persistent, formally verified knowledge base stored as a Git repository of Lean 4 files. Every declaration is type-checked by Lean's kernel. An LLM agent interacts with it entirely through the `kb` CLI. + +--- + +## Core Concepts + +- **Persistent**: stored as `.lean` files in a Git repository — survives across sessions. +- **Formally verified**: every addition is type-checked by Lean's kernel at `kb check` / `kb commit` time. +- **Domain-organised**: declarations are grouped into named domain files. Each domain is one `.lean` file. An agent can load a specific domain into its context without loading the entire KB. +- **Version-controlled**: full history, branching, and reproducibility via Git. + +--- + +## Planned Domain Structure + +The KB is organised into four top-level sections, each subdivided into domain files that correspond to a specific area of knowledge. The subsections are the natural unit an agent loads — for example, loading only `Physics` or only `MoneyFinance` without pulling in unrelated facts. + +### Mathematics + +| Domain file | Coverage | +|-------------|----------| +| `ElementaryMath` | Arithmetic, fractions, percentages; reasoning about parity and sign of underspecified values | +| `Algebra` | Variables, number systems, algebraic operations and symbols | +| `Geometry` | Plane, solid, coordinate, transformations, high-dimensional, packing, curves, polyforms, topology, tilings | +| `Plotting` | Functions, equations, parametric plots, inequalities, number lines, polar plots | +| `Calculus` | Integrals, derivatives, limits, sequences, products, series, sums, vector analysis, transforms, continuity, domain & range | +| `DifferentialEquations` | Ordinary (ODE) and partial (PDE) differential equations | +| `Statistics` | Descriptive statistics, inference, regression, random variables | +| `Functions` | Domain & range, injectivity, surjectivity, continuity, periodic, odd/even, special, number-theoretic, representation formulas | + +### Science & Technology + +| Domain file | Coverage | +|-------------|----------| +| `Physics` | Mechanics, oscillations & waves, statistical physics, thermodynamics, electricity & magnetism, optics, relativity, nuclear, quantum, particle, astrophysics, constants, principles, effects, fluid mechanics | +| `Chemistry` | Matter from atoms and ions to biomolecules | +| `UnitsMeasures` | Conversion and analysis of scientific and everyday measurement systems | +| `Engineering` | Aerospace, energy, electrical, control systems, mechanical, civil, fluid mechanics, acoustics, steam tables, measurement devices | +| `ComputationalSciences` | Cellular automata, substitution systems, Turing machines, complexity, algebraic codes, fractals, image processing, hashing | +| `EarthSciences` | Geology, geodesy, oceanography, climatology | +| `LifeSciences` | Human anatomy, animal anatomy, neuroscience, genomics, molecular biology, animals and plants | +| `SpaceAstronomy` | Phenomena and technology beyond Earth's atmosphere | + +### Society & Culture + +| Domain file | Coverage | +|-------------|----------| +| `People` | Biographical and demographic data on notable individuals and public figures | +| `ArtsMedia` | Music, films, comics, sculptures, paintings, and related media | +| `History` | Timelines, monetary value analysis, historical events, inventions, conflicts | +| `WordsLinguistics` | Word properties, languages, document length, notable texts, transliterations, Morse code, Soundex, encodings, emotions | +| `MoneyFinance` | Stock data, mortgages & loans, salaries, bonds, derivative valuation, income tax, sales tax | +| `DatesTimes` | Dates, calendars, time systems | +| `FoodNutrition` | Nutritional data and dietary guidelines | +| `Demographics` | Health care, age/sex, gender equality, business, citizenship, crime, education, income & employment, language, race, marriage, mobility, religion, military, HDI | + +### Everyday Life + +| Domain file | Coverage | +|-------------|----------| +| `PersonalHealth` | Physical exercise, food and nutrition, child growth & development | +| `PersonalFinance` | Mortgages & loans, stock data, currency conversion, cost of living, gasoline, food, electricity prices | +| `Entertainment` | Music, films, artworks, cultural productions | +| `HouseholdScience` | Scientific reasoning applied to everyday physical phenomena | +| `HouseholdMath` | Everyday calculations and measurements | +| `Programming` | Algorithms, data structures, programming concepts | +| `Hobbies` | Recreational activities and personal projects | +| `TodaysWorld` | World economy, Finland economy, weather | + +--- + +## Knowledge Representation + +| Kind | Description | Lean form | +|------|-------------|-----------| +| **Type** | A category or class | `opaque Person : Type` | +| **Subtype** | A type extending another | `opaque Philosopher : Type` + coercion axiom | +| **Instance** | A named individual | `opaque socrates : Person` | +| **Property** | A function from a type to a value | `opaque birthYear : Person → Nat` | +| **Relation** | A binary predicate | `opaque bornIn : Person → Place → Prop` | +| **Fact** | An asserted value or relation | `axiom fact_birthYear_socrates : birthYear socrates = 470` | +| **Rule** | A universally quantified axiom | `axiom ancestors_transitive : ∀ x y z, …` | +| **Definition** | A named computable expression | `def yearsToDouble (r : Float) : Float := …` | + +--- + +## CLI Commands + +### Adding knowledge *(all require `in <Domain>`)* + +| Command | Description | +|---------|-------------| +| `add type <n> [extends <Parent>] in <D>` | Declare a type, optionally as a subtype | +| `add instance <n> : <Type> in <D>` | Declare a named individual | +| `add prop <n> : <DomType> -> <Range> in <D>` | Add a property | +| `add rel <n> : <D1> -> <D2> -> Prop in <D>` | Add a binary relation | +| `add fact <fact> in <D>` | Assert a fact: `prop(inst) = val` or `rel(a, b)` | +| `add rule <n> : <statement> in <D>` | Add a universally quantified axiom | +| `add def <n> <params> : <Type> := <body> in <D>` | Define a reusable computed shortcut | + +Both `→` (Unicode) and `->` (ASCII) are accepted as type arrows. + +### Inspecting knowledge + +| Command | Description | +|---------|-------------| +| `list <types\|instances\|props\|rels\|facts\|rules\|defs\|all> [of <Domain>]` | List declarations, optionally filtered by domain | +| `show def <n>` | Print the Lean source of a declaration | +| `domains` | List all domains active this session with declaration counts | +| `domains stats` | Detailed breakdown per domain and kind | + +### Querying + +| Command | Description | +|---------|-------------| +| `eval <expr>` | Evaluate a computable Lean expression via `#eval` | +| `query <prop>` | Attempt to prove a proposition (Yes / No / Unknown) | + +### Build and version control + +| Command | Description | +|---------|-------------| +| `init <dir>` | Create a new KB repository | +| `check` | Sync imports and run `lake build` to verify the whole KB | +| `commit <message>` | Verify then `git commit` all changes | +| `status` | Show `git status` and session summary | +| `rm <n>` | Remove a declaration (warns about dependents) | + +--- + +## How `check` Works + +`kb check` does three things before running `lake build`: + +1. Scans the KB root for all `*.lean` domain files. +2. Inspects which domains reference names declared in other domains, and injects the necessary `import` lines. +3. Rewrites `KnowledgeBase.lean` to import all domain files so `lake build` compiles everything. + +Add a batch of declarations, then run `check` once at the end rather than after each individual addition. + +--- + +## Example Workflow + +```bash +# Initialise +kb init ./myKB +cd myKB + +# Base types shared across domains +kb add type Entity in People +kb add type Person extends Entity in People +kb add type Place extends Entity in People +kb add type City extends Place in People + +# Properties and relations +kb add prop birthYear : Person -> Nat in People +kb add rel bornIn : Person -> Place -> Prop in People + +# Instances and facts +kb add instance socrates : Person in People +kb add instance athens : City in People +kb add fact birthYear(socrates) = 470 in People +kb add fact bornIn(socrates, athens) in People + +# Verify and commit +kb check +kb commit "Added Socrates and basic person/place ontology" + +# Agent loads only the People domain for a biographical query +kb list all of People +``` + +--- + +## Query Capabilities + +- **Computational**: `kb eval "yearsToDouble 0.05"` — runs `#eval` on any computable Lean expression. +- **Logical**: `kb query "even (2 + 2)"` — attempts to prove the proposition using `decide`, `aesop`, or `simp`. +- **Selective loading**: `kb list all of Physics` — an agent pulls only the Physics domain into its context for a focused query. + +--- + +## Extensibility + +- Domain files from the planned structure are created on first use — no separate setup step. +- Definitions (`kb add def`) become permanent reusable shortcuts stored in Lean files. +- The KB grows incrementally across sessions — each `kb commit` is a checkpoint in Git history. diff --git a/SocietyCulture.lean b/SocietyCulture.lean new file mode 100644 index 0000000..ca4d0da --- /dev/null +++ b/SocietyCulture.lean @@ -0,0 +1,17 @@ +import Mathematics + +-- Knowledge Base domain: SocietyCulture + +opaque Person : Type +-- Person extends Entity +axiom Person.val : Person → Entity +opaque Place : Type +-- Place extends Entity +axiom Place.val : Place → Entity +opaque City : Type +-- City extends Place +axiom City.val : City → Place +opaque athens : City +opaque birthyear : Person → Nat +opaque bornIn : Person → Place → Prop +axiom fact_bornIn_socrates_athens : bornIn socrates athens diff --git a/domain.tex b/domain.tex new file mode 100644 index 0000000..0a98765 --- /dev/null +++ b/domain.tex @@ -0,0 +1,273 @@ + +\documentclass[11pt]{article} +\usepackage[utf8]{inputenc} +\usepackage{enumitem} +\usepackage{hyperref} + +\setlist[itemize]{leftmargin=2em} + +\begin{document} + +\section{Mathematics} + +\subsection{Elementary Math} +System can perform arithmetic operations on underspecified values to determine parity, sign, or other qualities of an expression without knowing exact values. +\begin{itemize} + \item Arithmetic + \item Fractions + \item Percentages +\end{itemize} + +\subsection{Algebra} +Algebra studies variables within number systems and the operations acting on numbers and symbols. + +\subsection{Geometry} +Geometry studies properties of figures and the underlying space. +\begin{itemize} + \item Plane Geometry + \item Solid Geometry + \item Coordinate Geometry + \item Geometric Transformations + \item High-Dimensional Geometry + \item Packing \& Covering Programs + \item Curves \& Surfaces + \item Polyforms + \item Topology + \item Tilings +\end{itemize} + +\subsection{Plotting} +Plotting and graphing visualize the behavior of mathematical functions. +\begin{itemize} + \item Functions + \item Equations + \item Parametric Plots + \item Inequalities + \item Number Lines + \item Polar Plots +\end{itemize} + +\subsection{Calculus} +Calculus studies rates of change and measures such as length, area, and volume. +\begin{itemize} + \item Integrals + \item Derivatives + \item Limits + \item Sequences + \item Products + \item Series Expansions + \item Sums + \item Vector Analysis + \item Integral Transforms + \item Applications of Calculus + \item Continuity + \item Domain \& Range +\end{itemize} + +\subsection{Differential Equations} +Equations involving functions and their derivatives, including ordinary (ODE) and partial (PDE) differential equations. + +\subsection{Statistics} +Statistics involves collection, analysis, and exposition of data. +\begin{itemize} + \item Descriptive Statistics + \item Statistical Inference + \item Regression Analysis + \item Random Variables +\end{itemize} + +\subsection{Functions} +A function is a relation between a set of inputs (domain) and possible outputs (codomain). +\begin{itemize} + \item Domain \& Range + \item Injectivity \& Surjectivity + \item Continuity + \item Periodic Functions + \item Odd \& Even Functions + \item Special Functions + \item Number-Theoretic Functions + \item Representation Formulas +\end{itemize} + +\section{Science \& Technology} + +\subsection{Physics} +Physics studies features of the universe, from natural to manmade phenomena. +\begin{itemize} + \item Mechanics + \item Oscillations \& Waves + \item Statistical Physics + \item Thermodynamics + \item Electricity \& Magnetism + \item Optics + \item Relativity + \item Nuclear Physics + \item Quantum Physics + \item Particle Physics + \item Astrophysics + \item Physical Constants + \item Physical Principles + \item Physical Effects + \item Fluid Mechanics +\end{itemize} + +\subsection{Chemistry} +Study of matter from atoms and ions to biomolecules. + +\subsection{Units \& Measures} +Conversion and analysis of standard scientific and everyday measurement systems. + +\subsection{Engineering} +Engineering concerns design, construction, analysis, and maintenance of systems using scientific and mathematical principles. +\begin{itemize} + \item Aerospace Engineering + \item Energy Data + \item Electrical Engineering + \item Control Systems + \item Mechanical Engineering + \item Civil Engineering + \item Fluid Mechanics + \item Sound \& Acoustics + \item Steam Tables + \item Measurement Devices +\end{itemize} + +\subsection{Computational Sciences} +Computational theory and algorithmic structures. +\begin{itemize} + \item Cellular Automata + \item Substitution Systems + \item Turing Machines + \item Computational Complexity + \item Algebraic Codes + \item Fractals + \item Image Processing + \item Hashing +\end{itemize} + +\subsection{Earth Sciences} +Study of Earth and its atmosphere, including geology, geodesy, oceanography, and climatology. + +\subsection{Life Sciences} +Study of living organisms from molecular to organismal levels. +\begin{itemize} + \item Human Anatomy + \item Animal Anatomy + \item Neuroscience + \item Genomics + \item Molecular Biology + \item Animals and Plants +\end{itemize} + +\subsection{Space \& Astronomy} +Study of phenomena and technology beyond Earth's atmosphere. + +\section{Society \& Culture} + +\subsection{People} +Biographical and demographic analysis of notable individuals and public figures. + +\subsection{Arts \& Media} +Exploration of music, films, comics, sculptures, paintings, and related media. + +\subsection{History} +Generation of timelines, monetary value analysis, and comparison of historical events, inventions, and conflicts. +\begin{itemize} +\end{itemize} + +\subsection{Words \& Linguistics} +Computational and structural analysis of language. +\begin{itemize} + \item Word Properties + \item Languages + \item Document Length + \item Notable Texts + \item Transliterations + \item Morse Code + \item Soundex + \item Character Encodings + \item Emotions +\end{itemize} + +\subsection{Money \& Finance} +Analysis of monetary trends and financial instruments. +\begin{itemize} + \item Stock Data + \item Mortgages \& Loans + \item Salaries and Wages + \item Bonds + \item Derivative Valuation + \item Income Tax + \item Sales Tax +\end{itemize} + +\subsection{Dates \& Times} +Scientific and historical information about dates, calendars, and time systems. + +\subsection{Food \& Nutrition} +Nutritional data and dietary guidelines for foods. + +\subsection{Demographic \& Social Statistics} +Statistical analysis of populations and societies. +\begin{itemize} + \item Health Care Statistics + \item Age \& Sex Demographics + \item Gender Equality + \item Business Statistics + \item Citizenship Statistics + \item Crime Statistics + \item Education Statistics + \item Income \& Employment + \item Language Demographics + \item Race \& National Origin + \item Marriage Statistics + \item Geographic Mobility + \item Religion + \item Military Data + \item Human Development Index +\end{itemize} + +\section{Everyday Life} + +\subsection{Personal Health} +Nutritional data, exercise calculators, and growth tracking. +\begin{itemize} + \item Physical Exercise + \item Food and Nutrition + \item Child Growth \& Development +\end{itemize} + +\subsection{Personal Finance} +Financial computation and economic projections. +\begin{itemize} + \item Mortgages \& Loans + \item Stock Data + \item Currency Conversion + \item Cost of Living + \item Gasoline Price + \item Food Price + \item Electricity Price +\end{itemize} + +\subsection{Entertainment} +Data on music, films, artworks, and cultural productions. + +\subsection{Household Science} +Applications of scientific reasoning to everyday environmental and physical phenomena. + +\subsection{Household Math} + +\subsection{Programming} + +\subsection{Hobbies} +Algorithms and data for recreational activities and personal projects. + +\subsection{Today's World} +Timely statistics on global and national conditions. +\begin{itemize} + \item World Economy + \item Finland Economy + \item Weather +\end{itemize} + +\end{document} |