### Install External Solvers

Source: https://github.com/philzook58/knuckledragger/blob/main/tutorial.ipynb

Execute the installation script to download and build the supported external solvers.

```bash
! cd knuckledragger && ./install.sh # get and build external solvers
```

--------------------------------

### Quickcheck Logic Goals

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/short_talk.ipynb

Use the Hypothesis library to verify SMT goals. The second example demonstrates a failing check.

```python
import kdrag.hypothesis as hyp
import kdrag.theories.nat as nat
n = smt.Const("n", nat.Nat)
hyp.quickcheck(smt.ForAll([n], n + nat.Z == n))
```

```python
hyp.quickcheck(smt.ForAll([n], n + nat.Z == n + nat.one))
```

--------------------------------

### Install Knuckledragger

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/nng.ipynb

Download and install the Knuckledragger library. Restart the notebook runtime if the installation fails.

```bash
#git clone https://github.com/philzook58/knuckledragger.git
#cd knuckledragger
#python3 -m pip install -e .
```

--------------------------------

### Utilize Pre-built Mathematical Theories

Source: https://context7.com/philzook58/knuckledragger/llms.txt

Examples of using pre-proven lemmas for natural numbers and performing operations on lists.

```python
import kdrag as kd
import kdrag.smt as smt
import kdrag.theories.nat as nat
import kdrag.theories.list as list_

# Natural numbers with pre-proven lemmas
print(nat.one + nat.two)  # Uses defined addition
n = smt.Const("n", nat.Nat)

# Use pre-proven lemmas
proof = kd.prove(
    smt.ForAll([n], nat.add(n, nat.Z) == n),
    by=[nat.add_Z_r]  # Pre-proven lemma
)

# List operations
IntList = list_.List(smt.IntSort())
l = smt.Const("l", IntList.T)

# List constructors
empty = IntList.Nil
singleton = IntList.Cons(42, IntList.Nil)

# Pattern matching on lists
x = smt.Int("x")
matched = l.match_(
    (IntList.Nil, 0),
    (IntList.Cons(x, l), 1 + x)
)
```

--------------------------------

### Install Knuckledragger

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/short_talk.ipynb

Use pip to install the library directly from the GitHub repository.

```bash
#! python3 -m pip install git+https://github.com/philzook58/knuckledragger.git
```

--------------------------------

### Prove le_3_5 Example

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/soft_found/lf/IndProp.ipynb

Provides an example proof in Coq for the proposition '3 <= 5' using the previously defined 'le' relation.

```Coq
Example le_3_5 : 3 <= 5.
Proof.
  apply le_S. apply le_S. apply le_n. Qed.
```

--------------------------------

### Prove Real and BitVector Theorems

Source: https://github.com/philzook58/knuckledragger/blob/main/tutorial.ipynb

Examples of proving properties for different Z3 data types.

```python
x = smt.Real("x")
real_trich = kd.prove(smt.ForAll([x], smt.Or(x < 0, x == 0, 0 < x)))
real_trich
```

```python
x = smt.BitVec("x", 32)
or_idem = kd.prove(smt.ForAll([x], x | x == x))
or_idem
```

--------------------------------

### Install Knuckledragger

Source: https://github.com/philzook58/knuckledragger/blob/main/docs/index.md

Commands to install the package via uv.

```bash
uv pip install git+https://github.com/philzook58/knuckledragger.git
```

```bash
git clone https://github.com/philzook58/knuckledragger.git
cd knuckledragger
uv pip install -e .
```

```bash
uv pip install -e .[solvers,rust,pypcode,dev]
```

--------------------------------

### Install Knuckledragger

Source: https://github.com/philzook58/knuckledragger/blob/main/tutorial.ipynb

Commands to clone the repository and install the package in a development environment.

```bash
!git clone https://github.com/philzook58/knuckledragger.git
```

```bash
!cd knuckledragger && python3 -m pip install -e .
```

--------------------------------

### Prove Perm3 example in Coq

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/soft_found/lf/IndProp.ipynb

A proof demonstrating that [1;2;3] is a permutation of [2;3;1] using the Perm3 relation.

```coq
Example Perm3_example1 : Perm3 [1;2;3] [2;3;1].
Proof.
  apply perm3_trans with [2;1;3].
  - apply perm3_swap12.
  - apply perm3_swap23.   Qed.
```

--------------------------------

### Example Assembly Code for Verification

Source: https://github.com/philzook58/knuckledragger/blob/main/src/kdrag/contrib/pcode/README.md

This assembly code snippet includes directives for knuckledragger, defining an entry point with a condition and an exit point with a post-condition.

```asm
.include "/tmp/knuckle.s"
.globl myfunc

.text
    kd_entry myfunc "true"
    movq $42, %rax
    kd_exit .Lfunc_end "(= RAX (_ bv42 64))"
ret
```

--------------------------------

### Install knuckledragger with pypcode support

Source: https://github.com/philzook58/knuckledragger/blob/main/src/kdrag/contrib/pcode/README.md

Use this command to install the knuckledragger library with the necessary pypcode extra for assembly checking.

```bash
python3 -m pip install git+https://github.com/philzook58/knuckledragger.git[pypcode]
```

--------------------------------

### Restart Colab Instance

Source: https://github.com/philzook58/knuckledragger/blob/main/tutorial.ipynb

Programmatically restart the Python process to apply installation changes.

```python
import os
os.kill(os.getpid(), 9)
```

--------------------------------

### Create and Apply Rewrite Rules

Source: https://context7.com/philzook58/knuckledragger/llms.txt

Demonstrates creating rewrite rules from proven theorems and applying them to expressions, as well as manual rule definition.

```python
unit_rule = kd.prove(smt.ForAll([x], x + 0 == x))

# Apply rewriting
expr = x + 0 + 0 + 0
simplified = rewrite(expr, [unit_rule])
print(simplified)  # x

# Manual RewriteRule
square_rule = RewriteRule([x], x**2, x * x)
result = rewrite((y**2)**2, [square_rule])
print(result)  # y*y*y*y
```

--------------------------------

### Initialize Lemma for n + Succ(m) == Succ(n + m)

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/nng.ipynb

Initializes an interactive proof for the property `n + Succ(m) == Succ(n + m)` using `kd.Lemma`.

```python
l = kd.Lemma(smt.ForAll([n,m], n + Nat.Succ(m) == Nat.Succ(n + m)))
l
# TODO
```

--------------------------------

### Simple Proofs

Source: https://github.com/philzook58/knuckledragger/blob/main/CLAUDE.md

Using `kd.prove` for straightforward theorem proving with Z3.

```APIDOC
## Simple Proofs

`kd.prove(thm, by=[lemma1, lemma2], timeout=1000)` - Prove a theorem in one Z3 call

- Returns a `kd.Proof` object
- Use `by=[...]` to provide lemmas as assumptions
- Throws `kd.kernel.LemmaError` if unprovable
```

--------------------------------

### Use tactics for proof construction

Source: https://context7.com/philzook58/knuckledragger/llms.txt

Demonstrates basic proof tactics including universal quantifier fixes, conjunction splitting, and intermediate lemma introduction.

```python
l = kd.Lemma(smt.ForAll([x, y], smt.Implies(x > y, x >= y)))
_x, _y = l.fixes()  # Open the forall quantifiers
l.intros()          # Move x > y to context
l.auto()
forall_proof = l.qed()
```

```python
p, q = smt.Bools("p q")
l = kd.Lemma(smt.Implies(smt.And(p, q), smt.And(q, p)))
l.intros()
l.split(at=0)   # Split the And in context
l.split()       # Split the goal And
l.auto()        # First conjunct
l.auto()        # Second conjunct
and_comm = l.qed()
```

```python
l = kd.Lemma(smt.Implies(x > 0, x + 1 > 1))
l.intros()
l.have(x >= 0, by=[])      # Prove and add intermediate fact
l.auto()
intermediate = l.qed()
```

--------------------------------

### Initialize Lemma for n + Zero == n

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/nng.ipynb

Initializes an interactive proof for `n + 0 == n` using `kd.Lemma`.

```python
l = kd.Lemma(smt.ForAll([n], n + Nat.Zero == n))
l
```

--------------------------------

### Check Unsatisfiability with VampireSolver

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/short_talk.ipynb

Initializes a VampireSolver, adds equations and a universal quantifier constraint, and prints the solver's standard output.

```python
s = kd.solvers.VampireSolver()
for eq in E:
    s.add(eq)
s.add(smt.ForAll([x], x * e != x))
s.check()
print(s.res.stdout.decode())
```

--------------------------------

### Prove Succ Injectivity using QForAll

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/nng.ipynb

Prove the injectivity of the 'Succ' constructor using `kd.QForAll` to handle preconditions. This lemma states that if Succ(n) == Succ(m), then n == m.

```python
succ_inj = kd.prove(kd.QForAll([n,m], Nat.Succ(n) == Nat.Succ(m), n == m))
succ_inj
```

--------------------------------

### Lemma Induction and Proof Steps

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/leroy_compiler/IMP.ipynb

Proof steps for a lemma involving store evaluation and free variables.

```python
s1,s2 = smt.Consts("s1 s2", Store)
l = kd.Lemma(kd.QForAll([s1,s2,a], 
                    kd.QForAll([x], free_in_aexp(x,a), s1[x] == s2[x]),
                        aeval(s1, a) == aeval(s2, a)
                         ))
_s1, _s2, _a = l.fixes()
l.induct(_a)

l.fix()
l.intros()
l.simp(unfold=True)
l.auto()

_name = l.fix()
l.intros()
l.simp(unfold=True)
#l.unfold(at=0)
l.have(free_in_aexp(_name, Aexp.VAR(_name)), by=free_in_aexp.defn)
l.auto()

_plus1, _plus2 = l.fixes()
l.intros()
l.intros()
l.unfold()
#l.simp(unfold=False)
l.simp()
```

--------------------------------

### Interactive Proofs with kd.Lemma

Source: https://context7.com/philzook58/knuckledragger/llms.txt

The `kd.Lemma` class facilitates interactive, tactic-based proofs for complex theorems. It allows step-by-step proof construction using tactics like `intros` and `auto`.

```python
import kdrag as kd
import kdrag.smt as smt

x, y = smt.Ints("x y")

# Basic interactive proof with intros and auto
l = kd.Lemma(smt.Implies(x > 0, x >= 0))
l.intros()      # Move hypothesis to context: [x > 0] ?|= x >= 0
l.auto()        # Solve automatically
proof = l.qed()
```

--------------------------------

### Evaluate Arithmetic Expressions

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/soft_found/lf/Imp.ipynb

Defines the recursive function 'aeval' to evaluate arithmetic expressions. It takes an arithmetic expression and returns its numerical value. Includes an example test case.

```python
"""
Fixpoint aeval (a : aexp) : nat :=
  match a with
  | ANum n => n
  | APlus  a1 a2 => (aeval a1) + (aeval a2)
  | AMinus a1 a2 => (aeval a1) - (aeval a2)
  | AMult  a1 a2 => (aeval a1) * (aeval a2)
  end.

Example test_aeval1:
  aeval (APlus (ANum 2) (ANum 2)) = 4.
Proof. reflexivity. Qed.
"""
aeval = smt.Function("aeval", aexp, smt.IntSort())
#aeval = kd.define("aeval", [a], )
```

--------------------------------

### Equational Proofs with Calc Tactic

Source: https://github.com/philzook58/knuckledragger/blob/main/docs/index.md

Demonstrates using the Calc tactic for explicit equational proofs. Requires importing necessary functions like inv, id_left, inv_left, and mul_assoc.

```python
c = kd.Calc([x], x * inv(x))
c.eq(e * (x * inv(x)), by=[id_left])
c.eq((inv(inv(x)) * inv(x)) * (x * inv(x)), by=[inv_left])
c.eq(inv(inv(x)) * ((inv(x) * x) * inv(x)), by=[mul_assoc])
c.eq(inv(inv(x)) * (e * inv(x)), by=[inv_left])
c.eq(inv(inv(x)) * inv(x), by=[id_left])
c.eq(e, by=[inv_left])
inv_right = c.qed()
```

--------------------------------

### Z3 Basics

Source: https://github.com/philzook58/knuckledragger/blob/main/CLAUDE.md

Common functions for interacting with the Z3 SMT solver through the `kdrag.smt` module.

```APIDOC
## Z3 Basics (from `kdrag.smt`)

Common functions:

- `smt.Const(name, sort)` or `smt.Ints("x y z")`, `smt.Reals("x y z")`
- `smt.ForAll(vs, body)`, `smt.Exists(vs, body)`
- `smt.And(...)`, `smt.Or(...)`, `smt.Implies(p, q)`
- `smt.Function(name, *arg_sorts, ret_sort)` - declare uninterpreted function

Operators naturally overload: `+`, `-`, `*`, `/`, `==`, `!=`, `<`, `>`, `<=`, `>=`
```

--------------------------------

### Handle Lemma Proof Failure

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/nng.ipynb

Demonstrates how `kd.prove` raises a `kd.kernel.LemmaError` for unprovable lemmas or those requiring more automation, showing a countermodel.

```python
try:
    succ_succ_disjoint = kd.prove(smt.ForAll([n,m], Nat.Succ(m) == Nat.Succ(n)), timeout=10)
except kd.kernel.LemmaError as e:
    print(e)
```

--------------------------------

### Induction Lemma Proof Steps

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/leroy_compiler/IMP.ipynb

A sequence of proof tactics for an induction lemma involving arithmetic expressions.

```python
# TODO: Induction lemmas should quantify everything at once.
_plus2 = l.fix()
l.intros()
_plus1 = l.fix()
l.intros()
l.intros()
l.unfold()
l.simp()
l.have(smt.Or(free_in_aexp(_name, _plus1), free_in_aexp(_name, _plus2)) ==
                   free_in_aexp(_name, Aexp.PLUS(_plus1, _plus2)), by=[free_in_aexp.defn])
l.newgoal(smt.And(aeval(_s1, _plus1) == aeval(_s2, _plus1), 
             aeval(_s1, _plus2) == aeval(_s2, _plus2)))
l.split()
#l.apply(1)
```

--------------------------------

### kd.Lemma - Interactive Proofs

Source: https://context7.com/philzook58/knuckledragger/llms.txt

The `Lemma` class provides an interactive tactic-based proof environment for complex proofs.

```APIDOC
## kd.Lemma - Interactive Proofs

### Description
Provides an interactive tactic-based proof environment for complex proofs.

### Method
`kd.Lemma`

### Parameters
#### Path Parameters
None

#### Query Parameters
None

#### Request Body
None

### Request Example
```python
import kdrag as kd
import kdrag.smt as smt

x, y = smt.Ints("x y")

# Basic interactive proof with intros and auto
l = kd.Lemma(smt.Implies(x > 0, x >= 0))
l.intros()      # Move hypothesis to context: [x > 0] ?|= x >= 0
l.auto()        # Solve automatically
proof = l.qed()
```

### Response
#### Success Response (200)
Returns a proof object.

#### Response Example
(Proof object)
```

--------------------------------

### Find Counterexample for a False Theorem with Z3

Source: https://github.com/philzook58/knuckledragger/blob/main/tutorial.ipynb

Illustrates how Z3 can provide a counterexample when a theorem is not universally true. It defines an implication `q implies p` and shows that Z3 can find values for `p` and `q` that make the implication false.

```python
q = z3.Bool("q")
my_false_thm = z3.Implies(q, p)
z3.prove(my_false_thm)
```

--------------------------------

### kd.prove - Proving Theorems

Source: https://context7.com/philzook58/knuckledragger/llms.txt

The `prove` function attempts to prove a theorem using Z3's SMT solver. It can optionally use previously proven lemmas as hints and supports timeouts.

```APIDOC
## kd.prove - Proving Theorems

### Description
Attempts to prove a theorem using Z3's SMT solver, optionally with previously proven lemmas as hints.

### Method
`kd.prove`

### Parameters
#### Path Parameters
None

#### Query Parameters
None

#### Request Body
None

### Request Example
```python
import kdrag as kd
import kdrag.smt as smt

p, q = smt.Bools("p q")
tautology = kd.prove(smt.Implies(p, smt.Or(p, q)))

x = smt.Real("x")
trichotomy = kd.prove(smt.ForAll([x], smt.Or(x < 0, x == 0, 0 < x)))

bv = smt.BitVec("bv", 32)
or_idempotent = kd.prove(smt.ForAll([bv], bv | bv == bv))

n = smt.Int("n")
succ = kd.define("succ", [n], n + 1)
succ_positive = kd.prove(
    smt.ForAll([n], smt.Implies(n >= 0, succ(n) > 0)),
    by=[succ.defn]
)

try:
    false_claim = kd.prove(smt.Implies(p, smt.And(p, q)), timeout=100)
except kd.kernel.LemmaError as e:
    print(f"Failed to prove: {e}")
```

### Response
#### Success Response (200)
Returns a proof object or a boolean indicating success.

#### Response Example
(Proof object or True/False)
```

--------------------------------

### Attempt to Prove Addition Property: n + Zero == n (Timeout)

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/nng.ipynb

Demonstrates an attempt to prove `n + 0 == n` using `kd.prove`, which times out, suggesting the need for induction.

```python
try:
    kd.prove(smt.ForAll([n], n + Nat.Zero == n), by=[add.defn], timeout=10)
except TimeoutError as e:
    print(e)
```

--------------------------------

### Perform Interactive Proofs

Source: https://github.com/philzook58/knuckledragger/blob/main/docs/index.md

Using the Lemma object for interactive tactic-based proofs.

```python
# More involved proofs can be more easily done in an interactive tactic
# Under the hood, this boils down to calls to kd.prove
# These proofs are best understood by seeing the interactive output in a Jupyter notebook
l = kd.Lemma(smt.ForAll([n], n + Nat.Zero == n))
# Output: [] ?|= ForAll(n, add(n, Zero) == n)

_n = l.fix()            
# Output: [] ?|= add(n!0, Zero) == n!2213

l.induct(_n)              
# Output: [] ?|= add(Zero, Zero) == Zero

# Base case
l.auto(by=[add.defn])
# Output: [] ?|= ForAll(a!0, Implies(add(a!0, Zero) == a!0, add(Succ(a!0), Zero) == Succ(a!0)))

# Inductive case
l.auto(by=[add.defn])
# Output: Nothing to do!

# Finally the actual Proof is built
add_x_zero = l.qed()
```

--------------------------------

### Prove Theorems with Z3

Source: https://github.com/philzook58/knuckledragger/blob/main/docs/index.md

Basic usage of kd.prove to verify Z3 expressions.

```python
import kdrag as kd
import kdrag.smt as smt # smt is literally a reexporting of z3

# Anything Z3 can do on it's own, we can "prove" with no extra work
p,q = smt.Bools("p q")
simple_taut = kd.prove(smt.Implies(p, smt.Or(p, q)))

# The returned objects are `Proof`, not smt.ExprRef` formulas
assert isinstance(simple_taut, kd.Proof)
assert not isinstance(simple_taut, smt.ExprRef)

# kd.prove will throw an error if the theorem is not provable
try:
    false_lemma = kd.prove(smt.Implies(p, smt.And(p, q)), timeout=10)
    print("This will not be reached")
except kd.kernel.LemmaError as e:
    pass

# Z3 also supports things like Reals, Ints, BitVectors and strings
x = smt.Real("x")
real_trich = kd.prove(smt.ForAll([x], smt.Or(x < 0, x == 0, 0 < x)))

x = smt.BitVec("x", 32)
or_idem = kd.prove(smt.ForAll([x], x | x == x))
```

--------------------------------

### Prove Nil Append and Length Predicate

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/soft_found/lf/Lists.ipynb

Demonstrates proving list properties using SMT constraints and case analysis.

```python
l = smt.Const("l", NatList)
nil_app = kd.prove(smt.ForAll([l], append(NatList.Nil, l) == l), by=append.defn)


l = kd.Lemma(smt.ForAll([l], nat.safe_pred(length(l)) == length(tail(l))))
_l = l.fix()
l.cases(_l)
print(l.goals)
l.auto(by=[length.defn, tail.defn, nat.safe_pred.defn])
l.auto(by=[length.defn, tail.defn, nat.safe_pred.defn])
```

--------------------------------

### Isar-Style Proof Pattern

Source: https://github.com/philzook58/knuckledragger/blob/main/CLAUDE.md

Implements an Isar-style proof using explicit forward reasoning with .have() and .auto(). More verbose but shows explicit steps.

```python
@kd.Theorem(smt.ForAll([l1, l2], sum(append(l1, l2)) == sum(l1) + sum(l2)))
def sum_append(pf):
    _l1, _l2 = pf.fixes()
    pf.induct(_l1)
    # Base case - establish facts with have, finish with auto
    pf.have(append(Nil, _l2) == _l2, by=[append.defn])
    pf.have(sum(Nil) == 0, by=[sum.defn])
    pf.auto(by=[append.defn, sum.defn])  # Discharge accumulated implications
    # Inductive case
    _head, _tail = pf.fixes()
    pf.have(append(Cons(_head, _tail), _l2) == Cons(_head, append(_tail, _l2)), by=[append.defn])
    pf.auto(by=[append.defn, sum.defn])
```

--------------------------------

### Prove Theorems with kd.prove

Source: https://context7.com/philzook58/knuckledragger/llms.txt

Use `kd.prove` to automatically prove theorems using Z3. It can optionally use previously proven lemmas as hints. Supports various logic types including real numbers and bitvectors. Includes timeout and error handling.

```python
import kdrag as kd
import kdrag.smt as smt

# Simple proofs that Z3 can solve directly
p, q = smt.Bools("p q")
tautology = kd.prove(smt.Implies(p, smt.Or(p, q)))

# Using real numbers
x = smt.Real("x")
trichotomy = kd.prove(smt.ForAll([x], smt.Or(x < 0, x == 0, 0 < x)))

# Bitvector properties
bv = smt.BitVec("bv", 32)
or_idempotent = kd.prove(smt.ForAll([bv], bv | bv == bv))

# Using lemmas with the `by` parameter
n = smt.Int("n")
succ = kd.define("succ", [n], n + 1)
succ_positive = kd.prove(
    smt.ForAll([n], smt.Implies(n >= 0, succ(n) > 0)),
    by=[succ.defn]
)

# Timeout and error handling
try:
    false_claim = kd.prove(smt.Implies(p, smt.And(p, q)), timeout=100)
except kd.kernel.LemmaError as e:
    print(f"Failed to prove: {e}")
```

--------------------------------

### Constructing an Equational Proof in Python

Source: https://github.com/philzook58/knuckledragger/blob/main/tutorial.ipynb

Demonstrates how to construct an explicit equational proof for the right inverse law using Knuckledragger's `Calc` tactic. This method allows for step-by-step verification of theorems.

```python
# The Calc tactic can allow one to write explicit equational proofs
c = kd.Calc([x], x * inv(x))
c.eq(e * (x * inv(x)), by=[id_left])
c.eq((inv(inv(x)) * inv(x)) * (x * inv(x)), by=[inv_left])
c.eq(inv(inv(x)) * ((inv(x) * x) * inv(x)), by=[mul_assoc])
c.eq(inv(inv(x)) * (e * inv(x)), by=[inv_left])
c.eq(inv(inv(x)) * inv(x), by=[id_left])
c.eq(e, by=[inv_left])
inv_right = c.qed()
```

--------------------------------

### Interactive Proof Tactic

Source: https://github.com/philzook58/knuckledragger/blob/main/tutorial.ipynb

Demonstrates an interactive proof process using the Lemma object.

```python
# More involved proofs can be more easily done in an interactive tactic
# Under the hood, this boils down to calls to kd.prove
# These proofs are best understood by seeing the interactive output in a Jupyter notebook
l = kd.Lemma(smt.ForAll([n], n + Nat.Zero == n))

# [] ?|= ForAll(n, add(n, Zero) == n)
_n = l.fix()            

# [] ?|= add(n!0, Zero) == n!2213
l.induct(_n)              

# Case n!0 == Nat.Zero
# [] ?|= add(Zero, Zero) == Zero
l.auto(by=[add.defn])

# Case n!0 == Nat.Succ(n.pred)
# [] ?|= ForAll(a!0, Implies(add(a!0, Zero) == a!0, add(Succ(a!0), Zero) == Succ(a!0)))
l.auto(by=[add.defn])

# Finally the actual Proof is built
add_x_zero = l.qed()
```

--------------------------------

### Tactics Reference

Source: https://github.com/philzook58/knuckledragger/blob/main/CLAUDE.md

A comprehensive list of tactics available on the `ProofState` object for manipulating proofs.

```APIDOC
### Tactics Reference

Tactics are methods on `ProofState` (returned by `kd.Lemma` or passed to `@Theorem`):

**Opening quantifiers/assumptions:**

- `l.fix()` - open one \(orall\), returns the fresh variable
- `l.fixes()` - open multiple \(orall\)s, returns list
- `l.intros()` - move implication hypothesis into context. Returns that new context formula
- `l.obtain(n)` - open \(\exists\) in hypothesis `n`, returns witness constants

**Proving subgoals:**

- `l.auto(**kwargs)` - call Z3 on current goal with context
- `l.show(thm, by=[...])` - prove goal equals `thm` using lemmas
- `l.exact(pf)` - close goal with proof `pf`

**Manipulating context/goal:**

- `l.have(thm, by=[...])` - add lemma to context (must be implied by context)
- `l.rw(rule, at=None, rev=False)` - rewrite using equality `rule` (at goal or hyp index)
- `l.unfold(*decls, at=None)` - unfold definitions
- `l.split()` - split `\wedge` in goal or `\vee` in hypotheses
- `l.apply(n)` - apply implication from hypothesis `n`
- `l.exists(*ts)` - provide witnesses for \(\exists\) goal

**Induction:**

- `l.induct(x, using=None)` - induct on variable `x` (auto-detects or use custom principle)
  - **Important**: After `l.induct(x)` on an inductive datatype, the constructor case generates `ForAll` for ALL constructor fields
  - For `Cons(head, tail)` you must use `head, tail = l.fixes()` not `l.fix()`
  - Example: After inducting on a list, the `Cons` case needs `fixes()` to open both head and tail

**Advanced:**

- `l.specialize(n, *ts)` - instantiate universal in hypothesis `n` with terms
- `with l.sub() as l1: ...` - create subgoal

**Finish:**

- `l.qed()` - complete proof and return `kd.Proof`
```

--------------------------------

### Z3 BitVector Proof

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/short_talk.ipynb

Demonstrates a basic proof of idempotence for bitwise OR using Z3.

```python
import z3
x = z3.BitVec("x", 64)
or_idem = z3.ForAll([x], x | x == x)
or_idem
```

```python
z3.prove(or_idem)
```

--------------------------------

### Coq Proof Tactics for Aexp

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/leroy_compiler/IMP.ipynb

Tactics for handling PLUS and MINUS cases in a formal proof.

```Coq
(* Case a = PLUS a1 a2 *)
  rewrite IHa1, IHa2. auto. auto. auto.
- (* Case a = MINUS a1 a2 *)
  rewrite IHa1, IHa2; auto.
Qed.
```

--------------------------------

### Declare Axioms with kd.axiom

Source: https://context7.com/philzook58/knuckledragger/llms.txt

Use `kd.axiom` to assert formulas as true without proof, useful for defining foundational properties like group theory axioms. Use with caution to avoid logical inconsistencies.

```python
import kdrag as kd
import kdrag.smt as smt

# Declare a custom sort and axioms for group theory
G = smt.DeclareSort("G")
mul = smt.Function("mul", G, G, G)
e = smt.Const("e", G)
inv = smt.Function("inv", G, G)

# Register multiplication for operator overloading
kd.notation.mul.register(G, mul)

x, y, z = smt.Consts("x y z", G)

# Group axioms
mul_assoc = kd.axiom(smt.ForAll([x, y, z], x * (y * z) == (x * y) * z))
id_left = kd.axiom(smt.ForAll([x], e * x == x))
inv_left = kd.axiom(smt.ForAll([x], inv(x) * x == e))

# Now prove theorems using these axioms
id_right = kd.prove(smt.ForAll([x], x * e == x), by=[mul_assoc, id_left, inv_left])
```

--------------------------------

### Proof State Tactics (Old Style)

Source: https://github.com/philzook58/knuckledragger/blob/main/CLAUDE.md

An alternative, less preferred method for defining and proving theorems using `kd.Lemma`.

```APIDOC
**Old style** (less preferred):

```python
l = kd.Lemma(smt.ForAll([x], x + 0 == x))
x = l.fix()
l.auto()
add_zero = l.qed()
```
```

--------------------------------

### ASMC PCode Checker Help

Source: https://github.com/philzook58/knuckledragger/blob/main/src/kdrag/contrib/pcode/README.md

View the help information for the ASMC PCode checker to see available options and usage.

```bash
python3 -m kdrag.contrib.pcode --help
```

--------------------------------

### Perform Equational Reasoning with Calc

Source: https://github.com/philzook58/knuckledragger/blob/main/CLAUDE.md

Demonstrates chained equational reasoning using the Calc object. Supports chained .eq, .le, .lt, .ge, .gt methods.

```python
c = kd.Calc([x], lhs)
c.eq(rhs1, by=[lemma1])
c.eq(rhs2, by=[lemma2])
result = c.qed()
```

--------------------------------

### Apply Induction to Variable

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/nng.ipynb

Applies the `induct` tactic to the variable `_n` in the `kd.Lemma` proof, setting up the base case for induction.

```python
l.induct(_n)
```

--------------------------------

### Prove le_3_5 using kdrag Equivalence

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/soft_found/lf/IndProp.ipynb

Demonstrates proving '3 <= 5' using the kdrag equivalence of the 'le' relation, showcasing different proof strategies.

```Python
# But is this cheating? I'm using
l = kd.Lemma(le(3,5))
l.auto(by=le_equiv)
le_3_5 = l.qed()

l = kd.Lemma(le(3,5))
for i in range(2):
    l.apply(le_S1)
    l.split()
    l.auto()
l.simp(unfold=False)
l.apply(le_n)
l.qed()

l = kd.Lemma(le(3, S(S(3))))
l.apply(le_S2)
l.apply(le_S2)
l.apply(le_n)
le_3_5 = l.qed()
```

--------------------------------

### Knuckledragger Kernel Axioms

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/short_talk.ipynb

Demonstrates using the kernel to prove statements based on axioms.

```python
x = smt.Int("x")
xpos = kd.kernel.axiom(x > 0)
# ---------------------------
kd.kernel.prove(x > -1, by=[xpos])
```

```python
kd.kernel.prove(x > -1, by=[xpos]).reason
```

--------------------------------

### Simplify Goal

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/nng.ipynb

Simplifies the current goal using the `simp` tactic within the `kd.Lemma` proof after unfolding the addition definition.

```python
# l.auto() would finish the goal here
l.simp()
```

--------------------------------

### Prove Addition Property: Two + n == Succ(Succ(n))

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/nng.ipynb

Proves the property `2 + n == 2 + n` for all natural numbers `n` using `kd.prove`, requiring definitions of `one`, `two`, and `add`.

```python
add_two_x = kd.prove(smt.ForAll([n], add(two, n) == Nat.Succ(Nat.Succ(n))), by=[one.defn, two.defn, add.defn])
add_two_x
```

--------------------------------

### Import Z3 Library

Source: https://github.com/philzook58/knuckledragger/blob/main/tutorial.ipynb

Imports the Z3 SMT solver library, which is the foundation for Knuckledragger's functionality. This is a standard first step when using Z3 or Knuckledragger.

```python
import z3
```

--------------------------------

### Access Theorem from Proof Object

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/nng.ipynb

Access the underlying Z3 theorem (QuantifierRef) from the `kd.Proof` object.

```python
type(zero_succ_disjoint.thm)
```

--------------------------------

### Complete Proof for n + Zero == n in Single Cell

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/nng.ipynb

Demonstrates a complete interactive proof for `n + 0 == n` within a single cell using `kd.Lemma` and its tactics.

```python
l = kd.Lemma(smt.ForAll([n], n + Nat.Zero == n))
_n = l.fix()
l.induct(_n)
l.auto(by=[add.defn])
l.auto(by=[add.defn])
add_x_zero = l.qed()
add_x_zero
```

--------------------------------

### Prove a Tautology with Z3

Source: https://github.com/philzook58/knuckledragger/blob/main/tutorial.ipynb

Demonstrates how to prove a simple theorem (a tautology) using Z3's `prove` function. It defines a boolean variable `p` and asserts the implication `p implies p`.

```python
p = z3.Bool("p")
my_true_thm = z3.Implies(p, p)
z3.prove(my_true_thm)
```

--------------------------------

### Prove Aexp Property with Knuckledragger

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/leroy_compiler/IMP.ipynb

Demonstrates using kd.prove to verify properties of free variables in arithmetic expressions.

```python
print(a2.sort())
kd.prove(kd.QForAll([x,a1,a2], 
                    smt.Or(free_in_aexp(x, a1), 
                    free_in_aexp(x, a2)) ==    
                    free_in_aexp(x, Aexp.PLUS(a1, a2))),
                    by=[free_in_aexp.defn])
```

--------------------------------

### Prove Lemmas with Definitions

Source: https://github.com/philzook58/knuckledragger/blob/main/tutorial.ipynb

Uses function definitions to prove properties about the custom addition function.

```python
# The definitional lemma is not available to the solver unless you give it
add_zero_x = kd.prove(smt.ForAll([n], Nat.Zero + n == n), by=[add.defn])
add_succ_x = kd.prove(smt.ForAll([n,m], Nat.Succ(n) + m == Nat.Succ(n + m)), by=[add.defn])
```

--------------------------------

### Knuckledragger Basic Proof

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/short_talk.ipynb

Initializes a proof using the Knuckledragger library.

```python
import kdrag as kd
import kdrag.smt as smt # smt is literally a reexporting of z3

x = smt.BitVec("x", 32)
or_idem = kd.prove(smt.ForAll([x], x | x == x))
or_idem
```

--------------------------------

### Prove properties of pairs

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/soft_found/lf/Lists.ipynb

Defining a swap function and proving its properties using SMT solvers.

```Python


swap_pair = kd.define("swap_pair", [p], NatProd(p.n2, p.n1))

nat_prod_surj = kd.prove(smt.ForAll([n, m], swap_pair(NatProd(n, m)) == NatProd(m, n)), by=swap_pair.defn)
```

--------------------------------

### Prove Zero and Succ Disjointness

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/nng.ipynb

Prove the lemma that 'Zero' is not equal to 'Succ(n)' for any 'n'. The result is a 'kd.Proof' object.

```python
zero_succ_disjoint = kd.prove(smt.ForAll([n], Nat.Zero != Nat.Succ(n)))
zero_succ_disjoint
```

--------------------------------

### Solve Integer Constraints with Z3

Source: https://github.com/philzook58/knuckledragger/blob/main/tutorial.ipynb

Declares integer variables, defines a set of constraints, and uses Z3's `solve` function to find a solution that satisfies all constraints. This is useful for constraint satisfaction problems.

```python
x = z3.Int('x')
y = z3.Int('y')
z3.solve(x > 2, y < 10, x + 2*y == 7)
```

--------------------------------

### Simplify expressions with kd.simp and kd.full_simp

Source: https://context7.com/philzook58/knuckledragger/llms.txt

Simplification functions that unfold definitions and apply Z3's simplifier, with support for tracing and conditional logic.

```python
import kdrag as kd
import kdrag.smt as smt
import kdrag.theories.nat as nat

# full_simp repeatedly unfolds and simplifies
result = kd.full_simp(nat.one + nat.one + nat.S(nat.one))
print(result)  # S(S(S(S(Z))))

# simp with trace to see what happened
trace = []
simplified = kd.simp(nat.Z + nat.one, trace=trace)
print(trace)   # List of lemmas used

# Conditional simplification (won't fully reduce)
p = smt.Bool("p")
partial = kd.full_simp(smt.If(p, 42, 3))
print(partial)  # If(p, 42, 3)
```

--------------------------------

### Prove Simple Tautology

Source: https://github.com/philzook58/knuckledragger/blob/main/tutorial.ipynb

Demonstrates basic proof functionality using Z3Py expressions.

```python
import kdrag as kd
import kdrag.smt as smt # smt is literally a reexporting of z3


p,q = smt.Bools("p q")
simple_taut = kd.prove(smt.Implies(p, smt.Or(p, q)))
simple_taut
```

--------------------------------

### Implement list operations and proofs

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/soft_found/lf/Lists.ipynb

Defining repeat, length, and append functions for lists, and proving properties about them.

```Python
n,count = smt.Consts("n count", nat.Nat)
repeat = smt.Function("repeat", nat.Nat, nat.Nat, NatList)
kd.define("repeat", [n,count], smt.If(count.is_Z, NatList.Nil, NatList.Cons(n, repeat(n, count.pred))))

length = smt.Function("length", NatList, nat.Nat)
l = smt.Const("l", NatList)
kd.define("length", [l], smt.If(l.is_Nil, nat.Nat.Z, nat.Nat.S(length(l.tail))))

append = smt.Function("append", NatList, NatList, NatList)
l1,l2 = smt.Consts("l1 l2", NatList)
kd.define("append", [l1,l2], smt.If(l1.is_Nil, l2, NatList.Cons(l1.head, append(l1.tail, l2))))

kd.notation.add.register(NatList, append)

x = list(nat.from_int(i) for i in range(1,10))
kd.prove(natlist(x[0], x[1], x[2]) + natlist(x[4], x[5]) == natlist(x[0], x[1], x[2], x[4], x[5]), by=append.defn)
kd.prove(NatList.Nil + natlist(x[4], x[5]) == natlist(x[4], x[5]), by=append.defn)
kd.prove(natlist(x[0], x[1], x[2]) + NatList.Nil == natlist(x[0], x[1], x[2]), by=append.defn)
```

```text
Result:
|= append(Cons(from_int(1),
            Cons(from_int(2), Cons(from_int(3), Nil))),
       Nil) ==
Cons(from_int(1), Cons(from_int(2), Cons(from_int(3), Nil)))
```

--------------------------------

### Perform equational reasoning with kd.Calc

Source: https://context7.com/philzook58/knuckledragger/llms.txt

The Calc class facilitates structured equational proofs with explicit intermediate steps and support for inequalities.

```python
import kdrag as kd
import kdrag.smt as smt

# Example: prove that x * inv(x) = e in a group
G = smt.DeclareSort("G")
mul = smt.Function("mul", G, G, G)
e = smt.Const("e", G)
inv = smt.Function("inv", G, G)
kd.notation.mul.register(G, mul)

x, y, z = smt.Consts("x y z", G)
mul_assoc = kd.axiom(smt.ForAll([x, y, z], x * (y * z) == (x * y) * z))
id_left = kd.axiom(smt.ForAll([x], e * x == x))
inv_left = kd.axiom(smt.ForAll([x], inv(x) * x == e))

# Calc proof: x * inv(x) = e
c = kd.Calc([x], x * inv(x))
c.eq(e * (x * inv(x)), by=[id_left])
c.eq((inv(inv(x)) * inv(x)) * (x * inv(x)), by=[inv_left])
c.eq(inv(inv(x)) * ((inv(x) * x) * inv(x)), by=[mul_assoc])
c.eq(inv(inv(x)) * (e * inv(x)), by=[inv_left])
c.eq(inv(inv(x)) * inv(x), by=[id_left])
c.eq(e, by=[inv_left])
inv_right = c.qed()

# Calc with inequalities
x = smt.Real("x")
c = kd.Calc([x], x * x)
c.ge(0)  # x*x >= 0
square_nonneg = c.qed()
```

--------------------------------

### Lemma Proof Output and Result

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/leroy_compiler/IMP.ipynb

Intermediate proof state and final result for the lemma induction.

```text
Output:
[s1!52, s2!53, a!54, name!63];
[ForAll(x,
       Implies(free_in_aexp(x, VAR(name!63)),
               s1!52[x] == s2!53[x]))]
?|= s1!52[name!63] == s2!53[name!63]
```

```text
Result:
[s1!52, s2!53, a!54, plus1!70, plus2!71];
[And(Implies(ForAll(x,
                   Implies(free_in_aexp(x, plus1!70),
                           s1!52[x] == s2!53[x])),
            aeval(s1!52, plus1!70) == aeval(s2!53, plus1!70)),
    Implies(ForAll(x,
                   Implies(free_in_aexp(x, plus2!71),
                           s1!52[x] == s2!53[x])),
            aeval(s1!52, plus2!71) == aeval(s2!53, plus2!71))),
 ForAll(x,
       Implies(free_in_aexp(x, PLUS(plus1!70, plus2!71)),
               s1!52[x] == s2!53[x]))]
?|= aeval(s1!52, plus1!70) + aeval(s1!52, plus2!71) ==
aeval(s2!53, plus1!70) + aeval(s2!53, plus2!71)
```

--------------------------------

### Define Abstract Numerals with Definitions

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/nng.ipynb

Define abstract numerals (one, two, three) using `kd.define`. This allows for manipulation at an abstract level and creates definitional theorems.

```python
one = kd.define("one", [], Nat.Succ(Nat.Zero))
two = kd.define("two", [], Nat.Succ(one))
three = kd.define("three", [], Nat.Succ(two))
one,two,three
```

--------------------------------

### Prove Addition Property: Zero + n == n

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/nng.ipynb

Proves the property `0 + n == n` for all natural numbers `n` using `kd.prove` and the definition of `add`.

```python
add_zero_x = kd.prove(smt.ForAll([n], Nat.Zero + n == n), by=[add.defn])
add_zero_x
```

--------------------------------

### Define Addition with kd.cond

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/nng.ipynb

Defines addition using `kd.cond` for a more structured definition, which expands into chained `smt.If` statements.

```python
add = smt.Function("add", Nat, Nat, Nat)
add = kd.define("add", [n,m], kd.cond(
    (n.is_Zero, m),
    (n.is_Succ, Nat.Succ(add(n.pred, m)))
))
```

--------------------------------

### Prove Addition Property: Zero + One == One

Source: https://github.com/philzook58/knuckledragger/blob/main/examples/nng.ipynb

Proves the property `0 + 1 == 1` for natural numbers using `kd.prove` with definitions of `one` and `add`.

```python
add_zero_one = kd.prove(Nat.Zero + one == one, by=[one.defn, add.defn])
add_zero_one
```

--------------------------------

### Handle Unprovable Lemmas

Source: https://github.com/philzook58/knuckledragger/blob/main/tutorial.ipynb

Demonstrates error handling when a theorem cannot be proven within the specified constraints.

```python
try:
    false_lemma = kd.prove(smt.Implies(p, smt.And(p, q)), timeout=10)
    print("This will not be reached")
except kd.kernel.LemmaError as _:
    pass
```