diff options
Diffstat (limited to '')
| -rw-r--r-- | AGENT.md | 221 |
1 files changed, 132 insertions, 89 deletions
@@ -1,165 +1,208 @@ # 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. +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` CLI. Every addition is type-checked by Lean's kernel at `check`/`commit` time. --- -## 1. Key Design Principle: Explicit Domains +## 1. Key Design Principles -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. +**Explicit domains.** Every declaration belongs to a domain you name with `in <Domain>`. Each domain is a `<Domain>.lean` file. Load only the domain(s) you need for a given task. -**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 +**Persistent state.** The KB stores a `--@kb` metadata header before every Lean declaration in each domain file. On startup, `kb` scans all domain files and reconstructs the full declaration list automatically — no state is lost between sessions. -An agent loading only `People` facts into its context window would run: `kb list all of People`. +**Exit codes.** Every command returns exit code `0` on success or `1` on error. Scripts can detect failure without parsing output. --- ## 2. Session Start Protocol -```bash -# Orient yourself: see what domains and declarations exist -kb list all -kb domains stats +State is loaded automatically from domain files on startup. There is no need to re-add anything between sessions. -# Recall declarations in a specific domain -kb list all of Ontology -kb list all of People +```bash +kb status # git status + domain summary +kb domains stats # declaration counts per domain and kind +kb list all # full declaration list ``` --- ## 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` | +Every `add` command requires `in <Domain>` at the end. Both `→` and `->` are accepted as type arrows. -### Notes +| Command | Example | +|---------|---------| +| `add type <n> [extends <P>] in <D>` | `kb add type Person extends Entity in People` | +| `add instance <n> : <Type> in <D>` | `kb add instance socrates : Person in People` | +| `add prop <n> : <DomType> -> <Range> in <D>` | `kb add prop birthYear : Person -> Nat in People` | +| `add rel <n> : <D1> -> <D2> -> Prop in <D>` | `kb add rel bornIn : Person -> Place -> Prop in People` | +| `add fact <fact> in <D>` | `kb add fact birthYear(socrates) = 470 in People` | +| `add rule <n> : <stmt> in <D>` | `kb add rule anc : ∀ x y z, parentOf x y → parentOf y z → ancestorOf x z in People` | +| `add def <n> <params> : <Type> := <body> in <D>` | `kb add def ytd (r : Float) : Float := Float.log 2 / r in Finance` | -- 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. +**Fact syntax:** `prop(inst) = value` or `rel(inst1, inst2)`. --- -## 4. Querying the Knowledge Base +## 4. Reading 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` | +| Command | Description | +|---------|-------------| +| `list all [of <Domain>]` | List all declarations, optionally restricted to one domain | +| `list types / instances / props / rels / facts / rules / defs [of <D>]` | Filter by kind | +| `show def <n>` | Print the full Lean source of a declaration | +| `get <prop>(<inst>)` | Retrieve a property value — runs `#eval prop inst` in Lean | +| `search <text>` | Full-text search across declaration names, Lean source, and domain names | +| `deps <n>` | Show what `<n>` uses (forward) and what uses `<n>` (reverse) | + +### Examples + +```bash +kb get birthYear(socrates) # → 470 +kb get atomicNumber(gold) # → 79 -### Query semantics +kb search socrates # all decls mentioning socrates +kb search "-> Nat" # all props/facts mapping to Nat -- `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`. +kb deps birthYear +# Dependencies of [prop] birthYear (People): +# uses: [type] Person (People) +# used by: [fact] fact_birthYear_socrates (People) +``` --- -## 5. Checking Consistency and Committing +## 5. Querying -Add all facts first, then verify and commit in one step: +### Basic query (default tactics: `first | decide | aesop | simp`) ```bash -kb check -kb commit "Added Socrates and basic ontology" +kb query "even (2 + 2)" +# Status: Yes +# Tactic: first | decide | aesop | simp +# Proof: +# theorem _kb_proof : even (2 + 2) := ... ``` -`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. +### Query with custom tactic script -**Do not check after each individual fact.** Batch your additions, then check once. +```bash +kb query "birthYear socrates = 470" using decide +kb query "∀ n : Nat, n + 0 = n" using simp +kb query "Nat.Prime 17" using native_decide +kb query "x + y = y + x" using ring +``` ---- +Returns: +- `Status: Yes` + proof term — proposition is provable with the given tactics +- `Status: No` + Lean output — a contradiction was found +- `Status: Unknown` + Lean output — tactics ran out without a result -## 6. Example Workflow +### Eval ```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 +kb eval "yearsToDouble 0.07" +kb eval "List.length [1, 2, 3]" +``` -# 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 +## 6. Removing Declarations -# Verify and commit everything at once -kb check -kb commit "Added Socrates and basic person/place ontology" +```bash +kb rm birthYear +# Warning: the following declarations reference 'birthYear': +# [fact] fact_birthYear_socrates (People) +# Consider removing dependents first. +# Removed 'birthYear'. ``` +`rm` is metadata-block aware — it removes the exact `--@kb` block and its Lean source for the named declaration, regardless of how many lines the source spans. + --- -## 7. Removing Declarations +## 7. Verifying and Committing + +Add a batch of declarations, then check and commit once: ```bash -kb rm <name> +kb check +kb commit "Added Socrates and basic ontology" ``` -The tool warns if other declarations depend on the one being removed. Remove dependents first. +`check` syncs cross-domain imports and runs `lake build` to verify the entire KB. `commit` does the same before running `git commit`. **Do not check after every individual addition** — batch your additions and check once. --- -## 8. Reusable Definitions +## 8. Example Workflow ```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 +# Base types +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 + +# Inspect +kb deps birthYear +kb search athens +kb get birthYear(socrates) + +# Query +kb query "birthYear socrates = 470" using decide + +# Verify and persist +kb check +kb commit "Added Socrates and basic person/place ontology" + +# Next session: kb loads all of the above automatically from People.lean ``` --- ## 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. +- **Batch additions, check once.** `lake build` is slow; don't call `check` after every fact. +- **Use `deps` before `rm`** to understand what will break. +- **Use `search` before `add`** to avoid duplicate declarations. +- **Choose tactics deliberately**: `native_decide` for decidable propositions, `omega` for linear arithmetic, `norm_num` for numeric computations, `ring` for ring equalities. +- **Put base types in a shared domain** so dependent domains can import them cleanly. +- **Use meaningful domain names** matching the planned structure: `People`, `Physics`, `MoneyFinance`, `EarthSciences`, etc. --- ## 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 +kb check # verify everything compiles +kb commit "Session: what was added" # persist to git +kb domains stats # confirm final counts ``` --- -## 11. Need Help? +## 11. Error Handling -```bash -kb help +All errors print a one-line summary and return exit code `1`: + +``` +Error: type 'Person' already exists. +Error: 'birthYear' not found. +Error: unknown command 'add type Person'. + Hint: add commands require `in <Domain>`. Run 'help' for usage. ``` -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. +Check exit codes in scripts: +```bash +kb add type Person in People || echo "Add failed, continuing..." +``` |