|
2 | 2 |
|
3 | 3 | - Try to follow the style that already exists in the repo |
4 | 4 | - Simple and non verbose is much preferred |
| 5 | +- Recommend changes to improve clarity of error messages |
| 6 | +- Recommend changes to make more consistent with Lean/Rocq/Isabelle/ACL2 conventions |
| 7 | +- Recommend new features that this system is missing that Lean/Rocq/Isabelle/ACL2/Mizar might have |
| 8 | +- Record new learnings in this file to avoid repeating failures |
| 9 | +- I am worried about proof instability and solve time. So try to keep track of those. |
| 10 | +- DO NOT try to be sneaky to get a proof though (mutating stuff, using python craziness). Knuckledragger relies on proper usage to remain sound. |
5 | 11 |
|
6 | 12 | ## Library Usage |
7 | 13 |
|
8 | | -Knuckledragger is python library for interactive theorem proving. |
| 14 | +Knuckledragger is a python library for interactive theorem proving backed by Z3. |
9 | 15 |
|
10 | | -The theorem `smt.BoolRef` and formula `smt.ExprRef` are those reexported from z3py in the module `kdrag.smt`. |
11 | | -Commonly used z3py functions are |
| 16 | +### Core Types |
12 | 17 |
|
13 | | -- `smt.Const(name, sort)` |
14 | | -- `smt.ForAll(vs, body)` |
15 | | -- `smt.Exists(vs, body)` |
16 | | -- `smt.And` `smt.Or` `smt.Implies` |
| 18 | +- `kd.Proof` - A proven theorem (frozen dataclass with `thm: smt.BoolRef`) |
| 19 | +- `smt.BoolRef` - Z3 boolean formula (theorems/propositions) |
| 20 | +- `smt.ExprRef` - Z3 expression (terms) |
| 21 | +- `smt.SortRef` - Z3 sorts/types (e.g., `smt.IntSort()`, `smt.RealSort()`) |
17 | 22 |
|
18 | | -Many things ave natural operator overloading available for them |
| 23 | +### Z3 Basics (from `kdrag.smt`) |
19 | 24 |
|
20 | | -It has a tactics system available in `kdrag.tactics`. Tactics are methods attached to a `kd.tactics.ProofState` object which can be made `l = kd.Lemma(my_to_be_proven_formula)`. This moves around the proof state in a manner similar to Lean or Rocq or Isabelle. |
| 25 | +Common functions: |
21 | 26 |
|
22 | | -Common tactics include |
| 27 | +- `smt.Const(name, sort)` or `smt.Ints("x y z")`, `smt.Reals("x y z")` |
| 28 | +- `smt.ForAll(vs, body)`, `smt.Exists(vs, body)` |
| 29 | +- `smt.And(...)`, `smt.Or(...)`, `smt.Implies(p, q)` |
| 30 | +- `smt.Function(name, *arg_sorts, ret_sort)` - declare uninterpreted function |
23 | 31 |
|
24 | | -- `l.intros` - bring an implication into the context |
25 | | -- `l.fix()` or `l.fixes` - open a forall quantifier |
26 | | -- `l.obtain(n)` will open an existential in the context. This function returns the fresh constants produces |
27 | | -- `l.have(mythm)` where mythm is implied by the current context will add mythm into the context |
28 | | -- `l.rw(add_assoc)` to apply a rewrite rule lemma |
29 | | -- `l.exists` to fill in a existential at the top level of the current goal |
| 32 | +Operators naturally overload: `+`, `-`, `*`, `/`, `==`, `!=`, `<`, `>`, `<=`, `>=` |
30 | 33 |
|
31 | | -`l.qed()` is the call that actually produces a |
| 34 | +### Simple Proofs |
32 | 35 |
|
33 | | -Proofs dischargeable by a single z3 call can be discharged via `kd.prove(thm, by=[lemma1, lemma2, lemma3])` which returns a `kd.Proof` object |
| 36 | +`kd.prove(thm, by=[lemma1, lemma2], timeout=1000)` - Prove a theorem in one Z3 call |
34 | 37 |
|
35 | | -Good examples of usage can be found in `kdrag.theories.real`, `kdrag.theories.logic.zf` |
| 38 | +- Returns a `kd.Proof` object |
| 39 | +- Use `by=[...]` to provide lemmas as assumptions |
| 40 | +- Throws `kd.kernel.LemmaError` if unprovable |
| 41 | + |
| 42 | +### Proof State Tactics (Preferred: `@Theorem` decorator) |
| 43 | + |
| 44 | +**Modern style** (preferred): |
| 45 | + |
| 46 | +```python |
| 47 | +@kd.Theorem(smt.ForAll([x], x + 0 == x)) |
| 48 | +def add_zero(l): |
| 49 | + """x + 0 == x""" |
| 50 | + x = l.fix() |
| 51 | + l.auto() |
| 52 | +``` |
| 53 | + |
| 54 | +**Old style** (less preferred): |
| 55 | + |
| 56 | +```python |
| 57 | +l = kd.Lemma(smt.ForAll([x], x + 0 == x)) |
| 58 | +x = l.fix() |
| 59 | +l.auto() |
| 60 | +add_zero = l.qed() |
| 61 | +``` |
| 62 | + |
| 63 | +For development, use `@kd.PTheorem` which prints next goal instead of erroring. |
| 64 | + |
| 65 | +### Tactics Reference |
| 66 | + |
| 67 | +Tactics are methods on `ProofState` (returned by `kd.Lemma` or passed to `@Theorem`): |
| 68 | + |
| 69 | +**Opening quantifiers/assumptions:** |
| 70 | + |
| 71 | +- `l.fix()` - open one ∀, returns the fresh variable |
| 72 | +- `l.fixes()` - open multiple ∀s, returns list |
| 73 | +- `l.intros()` - move implication hypothesis into context |
| 74 | +- `l.obtain(n)` - open ∃ in hypothesis `n`, returns witness constants |
| 75 | + |
| 76 | +**Proving subgoals:** |
| 77 | + |
| 78 | +- `l.auto(**kwargs)` - call Z3 on current goal with context |
| 79 | +- `l.show(thm, by=[...])` - prove goal equals `thm` using lemmas |
| 80 | +- `l.exact(pf)` - close goal with proof `pf` |
| 81 | + |
| 82 | +**Manipulating context/goal:** |
| 83 | + |
| 84 | +- `l.have(thm, by=[...])` - add lemma to context (must be implied by context) |
| 85 | +- `l.rw(rule, at=None, rev=False)` - rewrite using equality `rule` (at goal or hyp index) |
| 86 | +- `l.unfold(*decls, at=None)` - unfold definitions |
| 87 | +- `l.split()` - split `∧` in goal or `∨` in hypotheses |
| 88 | +- `l.apply(n)` - apply implication from hypothesis `n` |
| 89 | +- `l.exists(*ts)` - provide witnesses for ∃ goal |
| 90 | + |
| 91 | +**Induction:** |
| 92 | + |
| 93 | +- `l.induct(x, using=None)` - induct on variable `x` (auto-detects or use custom principle) |
| 94 | + - **Important**: After `l.induct(x)` on an inductive datatype, the constructor case generates `ForAll` for ALL constructor fields |
| 95 | + - For `Cons(head, tail)` you must use `head, tail = l.fixes()` not `l.fix()` |
| 96 | + - Example: After inducting on a list, the `Cons` case needs `fixes()` to open both head and tail |
| 97 | + |
| 98 | +**Advanced:** |
| 99 | + |
| 100 | +- `l.specialize(n, *ts)` - instantiate universal in hypothesis `n` with terms |
| 101 | +- `with l.sub() as l1: ...` - create subgoal |
| 102 | + |
| 103 | +**Finish:** |
| 104 | + |
| 105 | +- `l.qed()` - complete proof and return `kd.Proof` |
| 106 | + |
| 107 | +### Definitions and Axioms |
| 108 | + |
| 109 | +- `kd.define(name, vars, body)` - Define a function. Returns function with `.defn` attribute |
| 110 | +- `kd.axiom(thm)` - Assert axiom (use sparingly!) |
| 111 | +- `kd.FreshVar(name, sort)` or `kd.FreshVars("x y z", sort)` - Create schema variables |
| 112 | + |
| 113 | +### Algebraic Datatypes |
| 114 | + |
| 115 | +```python |
| 116 | +List = kd.Inductive("List") |
| 117 | +List.declare("Nil") |
| 118 | +List.declare("Cons", ("head", smt.IntSort()), ("tail", List)) |
| 119 | +List = List.create() |
| 120 | +``` |
| 121 | + |
| 122 | +- `kd.Struct(name, *fields)` - Product types |
| 123 | +- `kd.NewType(name, basesort, pred)` - Refinement types |
| 124 | +- `kd.Enum(name, *constructors)` - Simple enums |
| 125 | +- `kd.InductiveRel(name, *params)` - Inductively defined relations |
| 126 | + |
| 127 | +### Quantifier Helpers |
| 128 | + |
| 129 | +- `kd.QForAll([x], hyp, body)` → `ForAll([x], Implies(hyp, body))` |
| 130 | +- `kd.QExists([x], hyp, body)` → `Exists([x], And(hyp, body))` |
| 131 | +- `kd.QImplies(hyp, conc)` → sugar for conditional implications |
| 132 | + |
| 133 | +### Calc (Equational Reasoning) |
| 134 | + |
| 135 | +```python |
| 136 | +c = kd.Calc([x], lhs) |
| 137 | +c.eq(rhs1, by=[lemma1]) |
| 138 | +c.eq(rhs2, by=[lemma2]) |
| 139 | +result = c.qed() |
| 140 | +``` |
| 141 | + |
| 142 | +Supports `.eq`, `.le`, `.lt`, `.ge`, `.gt` for chained reasoning. |
| 143 | + |
| 144 | +### Common Proof Patterns |
| 145 | + |
| 146 | +**Tactic-style (Lean/Rocq): Simple and direct** |
| 147 | + |
| 148 | +```python |
| 149 | +@kd.Theorem(smt.ForAll([l], my_property(l))) |
| 150 | +def my_lemma(pf): |
| 151 | + _l = pf.fix() |
| 152 | + pf.induct(_l) |
| 153 | + # Base case (e.g., Nil) |
| 154 | + pf.auto(by=[relevant_defns]) |
| 155 | + # Constructor case (e.g., Cons) - use fixes() for all fields! |
| 156 | + _head, _tail = pf.fixes() |
| 157 | + pf.auto(by=[relevant_defns, helper_lemmas]) |
| 158 | +``` |
| 159 | + |
| 160 | +**Isar-style (Isabelle): Explicit forward reasoning with have/show** |
| 161 | + |
| 162 | +```python |
| 163 | +@kd.Theorem(smt.ForAll([l1, l2], sum(append(l1, l2)) == sum(l1) + sum(l2))) |
| 164 | +def sum_append(pf): |
| 165 | + _l1, _l2 = pf.fixes() |
| 166 | + pf.induct(_l1) |
| 167 | + # Base case - establish facts with have, finish with auto |
| 168 | + pf.have(append(Nil, _l2) == _l2, by=[append.defn]) |
| 169 | + pf.have(sum(Nil) == 0, by=[sum.defn]) |
| 170 | + pf.auto(by=[append.defn, sum.defn]) # Discharge accumulated implications |
| 171 | + # Inductive case |
| 172 | + _head, _tail = pf.fixes() |
| 173 | + pf.have(append(Cons(_head, _tail), _l2) == Cons(_head, append(_tail, _l2)), by=[append.defn]) |
| 174 | + pf.auto(by=[append.defn, sum.defn]) |
| 175 | +``` |
| 176 | + |
| 177 | +**Important about `have` and `show`:** |
| 178 | + |
| 179 | +- `pf.have(fact, by=[...])` adds `fact -> goal` as the new goal (forward reasoning) |
| 180 | +- After multiple `have` statements, use `pf.auto()` to discharge all accumulated implications |
| 181 | +- `pf.show(exact_goal, by=[...])` checks the goal matches exactly, then proves it |
| 182 | +- Isar-style is more verbose but shows explicit reasoning steps |
| 183 | +- Tactic-style is more concise and lets Z3 do more work |
| 184 | + |
| 185 | +**Passing lemmas to `by=`:** |
| 186 | + |
| 187 | +- Use `by=[lemma1, lemma2]` to provide previously proved theorems |
| 188 | +- Z3 will use these as assumptions |
| 189 | +- Sometimes you need to pass helper lemmas that seem "obvious" to help Z3 find the proof |
| 190 | +- Order can matter - Z3 may need earlier lemmas to prove later steps |
| 191 | + |
| 192 | +**When proofs timeout:** |
| 193 | + |
| 194 | +- Break into smaller lemmas |
| 195 | +- Prove helper lemmas first and use them in `by=` |
| 196 | +- Check if you need identity lemmas (e.g., `append(l, Nil) == l` before `rev_append`) |
| 197 | +- Consider increasing `timeout` parameter to `l.auto(by=[...], timeout=5000)` |
| 198 | + |
| 199 | +### Theory Status |
| 200 | + |
| 201 | +**Stable/Mature** (good examples): |
| 202 | + |
| 203 | +- `kdrag.theories.int` - integer arithmetic with induction |
| 204 | +- `kdrag.theories.nat` - Peano naturals (excellent induction examples) |
| 205 | +- `kdrag.theories.logic.zf` - ZF set theory (excellent proof examples) |
| 206 | +- `kdrag.theories.seq` - sequences |
| 207 | +- `kdrag.theories.list` - polymorphic lists (use only if needed, prefer monomorphic versions) |
| 208 | +- `examples/intlist.py` - pedagogical example of integer lists with many proofs |
| 209 | + |
| 210 | +**Experimental** (avoid for examples): |
| 211 | + |
| 212 | +- `kdrag.theories.algebra.*` - category theory, groups, etc. |
| 213 | +- `kdrag.theories.real.calc` - needs updating |
36 | 214 |
|
37 | 215 | ## Commands |
38 | 216 |
|
|
0 commit comments