Logos v0.1 Implementation Plan

For agentic workers: REQUIRED SUB-SKILL: Use superpowers:subagent-driven-development (recommended) or superpowers:executing-plans to implement this plan task-by-task. Steps use checkbox (- [ ]) syntax for tracking.

Goal: Build a working Lean-style proof kernel for Python — expression language, trusted kernel, tactic system, @logos.define, and logos.theorem.

Architecture: Small trusted kernel (~200 lines) checks proof terms structurally. Tactics are untrusted Python functions that produce proof terms. @logos.define generates axioms from symbolic function bodies. logos.theorem validates proofs at definition time.

Tech Stack: Python 3.12+, pytest, no external dependencies (stdlib only for v0.1).

Global Constraints

Python 3.12+ (use match / structural pattern matching throughout)
No external dependencies — stdlib only
eq=False on all Expr dataclasses (identity-based Python equality; __eq__ returns Eq node)
All Expr subclasses define __hash__ = object.__hash__ (required when __eq__ is overridden)
TacticFailed is the only exception tactics may raise; KernelError is what the kernel raises
All proof terms are frozen dataclasses (@dataclass(frozen=True))
Expr dataclasses are NOT frozen (mutable for potential in-place optimisation)
Package name on PyPI: logos-ai; import name: logos
Tactic protocol: returning ProofTerm closes the goal; returning (list[Goal], compose_fn) produces subgoals

File Map

logos/
  __init__.py          public API surface
  expr.py              Expr hierarchy + operator overloading
  helpers.py           structural_eq, substitute, free_vars
  kernel.py            ProofTerm hierarchy + infer() + check() — TRUSTED
  registry.py          global axiom store (name → Expr)
  goal.py              Goal dataclass, Context
  runner.py            TacticRunner (_Runner), TacticFailed
  define.py            @logos.define, logos.cases, logos.if_, logos.extern
  theorem.py           logos.theorem(), logos.prove()
  builtins.py          ring axioms loaded at import
  tactics/
    __init__.py        re-exports all tactics
    structural.py      intro, assumption, exact, apply, cases, split, left, right, witness, contradiction
    rewrite.py         unfold, refl, rewrite, rewrite_rev, eval_, norm_num
    arithmetic.py      ring, linarith, decide
    combinators.py     then, first, try_, repeat, all_goals
tests/
  conftest.py          shared fixtures (vars, common expressions)
  test_expr.py
  test_helpers.py
  test_kernel.py
  test_runner.py
  test_define.py
  test_tactics/
    test_structural.py
    test_rewrite.py
    test_arithmetic.py
    test_combinators.py
  test_integration.py
pyproject.toml

Task 1: Project Scaffold

Files:

Create: pyproject.toml
Create: logos/__init__.py (empty stub)
Create: logos/py.typed
Create: tests/__init__.py
Create: tests/conftest.py

Interfaces:

Produces: installable package logos-ai, importable as logos; pytest runnable from repo root
Step 1: Write pyproject.toml

[build-system]
requires = ["setuptools>=68"]
build-backend = "setuptools.backends.legacy:build"

[project]
name = "logos-ai"
version = "0.1.0"
description = "A Lean-style proof kernel for Python"
requires-python = ">=3.12"
license = {text = "MIT"}

[project.optional-dependencies]
dev = ["pytest>=8", "pytest-cov"]

[tool.pytest.ini_options]
testpaths = ["tests"]

Step 2: Create package skeleton

mkdir -p logos/tactics tests/test_tactics
touch logos/__init__.py logos/py.typed
touch logos/tactics/__init__.py
touch tests/__init__.py tests/test_tactics/__init__.py

Step 3: Write conftest.py

# tests/conftest.py
import pytest
from logos.expr import Var

@pytest.fixture
def x(): return Var("x", int)
@pytest.fixture
def y(): return Var("y", int)
@pytest.fixture
def z(): return Var("z", int)

Step 4: Install and verify

pip install -e ".[dev]"
pytest --collect-only   # should collect 0 tests with no errors

Expected output: no tests ran

Step 5: Commit

git add pyproject.toml logos/ tests/
git commit -m "chore: project scaffold"

Task 2: Expression Language

Files:

Create: logos/expr.py
Test: tests/test_expr.py

Interfaces:

Produces: Var, Lit, Add, Sub, Mul, Div, Mod, Neg, Pow, Eq, Neq, Lt, Le, Gt, Ge, And, Or, Not, Implies, ForallNode, ExistsNode, App, Cases — all subclasses of Expr
Produces: _lift(val) -> Expr — auto-lifts Python literals
Produces: Forall(*vars_and_body) -> Expr and Exists(var, body) -> Expr factory functions
Step 1: Write failing tests

# tests/test_expr.py
import pytest
from logos.expr import Var, Lit, Add, Mul, Eq as LogosEq, Gt, And, Or, Not, Implies, Forall, Neg

def test_var_creation():
    x = Var("x", int)
    assert x.name == "x"
    assert x.type is int

def test_arithmetic_operators(x, y):
    assert isinstance(x + y, Add)
    assert isinstance(x + 1, Add)   # literal auto-lift
    assert isinstance(1 + x, Add)   # __radd__
    assert isinstance(-x, Neg)
    assert isinstance(x * 2, Mul)

def test_comparison_returns_expr(x, y):
    result = x == y
    assert isinstance(result, LogosEq)   # NOT Python bool
    assert isinstance(x > 0, Gt)

def test_logical_connectives(x, y):
    assert isinstance((x > 0) & (y > 0), And)
    assert isinstance((x > 0) | (y > 0), Or)
    assert isinstance(~(x > 0), Not)
    assert isinstance((x > 0) >> (y > 0), Implies)

def test_bool_guard(x):
    with pytest.raises(TypeError, match="Expr cannot be used as a Python bool"):
        bool(x > 0)

def test_literal_autolift(x):
    expr = x + 1
    assert isinstance(expr.right, Lit)
    assert expr.right.value == 1

def test_forall_nested(x, y):
    from logos.expr import ForallNode
    stmt = Forall(x, y, x + y == y + x)
    assert isinstance(stmt, ForallNode)
    assert isinstance(stmt.body, ForallNode)

def test_hash_is_identity(x):
    y = Var("x", int)  # same name, different object
    assert hash(x) != hash(y)  # identity-based
    s = {x, y}
    assert len(s) == 2

Step 2: Run tests, confirm they fail

pytest tests/test_expr.py -v

Expected: ModuleNotFoundError: No module named 'logos.expr'

Step 3: Implement expr.py

# logos/expr.py
from __future__ import annotations
from dataclasses import dataclass
from typing import Any

class Expr:
    """Base class for all expression nodes. Operators build expression trees."""

    def __add__(self, other):      return Add(self, _lift(other))
    def __radd__(self, other):     return Add(_lift(other), self)
    def __sub__(self, other):      return Sub(self, _lift(other))
    def __rsub__(self, other):     return Sub(_lift(other), self)
    def __mul__(self, other):      return Mul(self, _lift(other))
    def __rmul__(self, other):     return Mul(_lift(other), self)
    def __floordiv__(self, other): return Div(self, _lift(other))
    def __mod__(self, other):      return Mod(self, _lift(other))
    def __neg__(self):             return Neg(self)
    def __pow__(self, other):      return Pow(self, _lift(other))
    def __eq__(self, other):       return Eq(self, _lift(other))
    def __ne__(self, other):       return Neq(self, _lift(other))
    def __lt__(self, other):       return Lt(self, _lift(other))
    def __le__(self, other):       return Le(self, _lift(other))
    def __gt__(self, other):       return Gt(self, _lift(other))
    def __ge__(self, other):       return Ge(self, _lift(other))
    def __and__(self, other):      return And(self, other)
    def __rand__(self, other):     return And(other, self)
    def __or__(self, other):       return Or(self, other)
    def __ror__(self, other):      return Or(other, self)
    def __invert__(self):          return Not(self)
    def __rshift__(self, other):   return Implies(self, other)
    def __hash__(self):            return id(self)
    def __bool__(self):
        raise TypeError(
            "Expr cannot be used as a Python bool. "
            "Use & instead of 'and', | instead of 'or', ~ instead of 'not'."
        )

def _lift(val: Any) -> Expr:
    return val if isinstance(val, Expr) else Lit(val)

@dataclass(eq=False)
class Lit(Expr):
    value: Any

@dataclass(eq=False)
class Var(Expr):
    name: str
    type: type

# Arithmetic
@dataclass(eq=False)
class Add(Expr):  left: Expr; right: Expr
@dataclass(eq=False)
class Sub(Expr):  left: Expr; right: Expr
@dataclass(eq=False)
class Mul(Expr):  left: Expr; right: Expr
@dataclass(eq=False)
class Div(Expr):  left: Expr; right: Expr
@dataclass(eq=False)
class Mod(Expr):  left: Expr; right: Expr
@dataclass(eq=False)
class Neg(Expr):  operand: Expr
@dataclass(eq=False)
class Pow(Expr):  base: Expr; exp: Expr

# Comparisons
@dataclass(eq=False)
class Eq(Expr):   left: Expr; right: Expr
@dataclass(eq=False)
class Neq(Expr):  left: Expr; right: Expr
@dataclass(eq=False)
class Lt(Expr):   left: Expr; right: Expr
@dataclass(eq=False)
class Le(Expr):   left: Expr; right: Expr
@dataclass(eq=False)
class Gt(Expr):   left: Expr; right: Expr
@dataclass(eq=False)
class Ge(Expr):   left: Expr; right: Expr

# Logical
@dataclass(eq=False)
class And(Expr):     left: Expr; right: Expr
@dataclass(eq=False)
class Or(Expr):      left: Expr; right: Expr
@dataclass(eq=False)
class Not(Expr):     operand: Expr
@dataclass(eq=False)
class Implies(Expr): antecedent: Expr; consequent: Expr

# Quantifiers (internal nodes — use Forall/Exists factories below)
@dataclass(eq=False)
class ForallNode(Expr):
    __match_args__ = ("var", "body")
    var: Var
    body: Expr

@dataclass(eq=False)
class ExistsNode(Expr):
    __match_args__ = ("var", "body")
    var: Var
    body: Expr

def Forall(*args: Var | Expr) -> Expr:
    """Forall(x, y, body) → nested ForallNode(x, ForallNode(y, body))."""
    *vars_, body = args
    result = body
    for v in reversed(vars_):
        if not isinstance(v, Var):
            raise TypeError(f"Forall: expected Var, got {type(v).__name__}")
        result = ForallNode(v, result)
    return result

def Exists(var: Var, body: Expr) -> Expr:
    return ExistsNode(var, body)

# Function application
@dataclass(eq=False)
class App(Expr):
    func_name: str
    args: list[Expr]

# Case expression (used by @logos.define bodies)
@dataclass(eq=False)
class CaseExpr(Expr):
    branches: list[tuple[Expr, Expr]]   # [(condition, value), ...]

Step 4: Run tests, confirm they pass

pytest tests/test_expr.py -v

Expected: all green.

Step 5: Commit

git add logos/expr.py tests/test_expr.py
git commit -m "feat: expression language with operator overloading"

Task 3: Structural Equality + Substitution

Files:

Create: logos/helpers.py
Test: tests/test_helpers.py

Interfaces:

Consumes: all Expr node types from logos.expr
Produces: structural_eq(a: Expr, b: Expr) -> bool
Produces: substitute(expr: Expr, var: Var, val: Expr) -> Expr
Produces: free_vars(expr: Expr) -> set[str]
Step 1: Write failing tests

# tests/test_helpers.py
from logos.expr import Var, Lit, Add, Mul, Eq, ForallNode, Forall
from logos.helpers import structural_eq, substitute, free_vars

def test_structural_eq_same(x, y):
    assert structural_eq(x + y, x + y)

def test_structural_eq_different_order(x, y):
    # x+y and y+x are structurally different
    assert not structural_eq(x + y, y + x)

def test_structural_eq_lit():
    assert structural_eq(Lit(1), Lit(1))
    assert not structural_eq(Lit(1), Lit(2))

def test_structural_eq_nested(x, y):
    e1 = (x + y) == (y + x)
    e2 = (x + y) == (y + x)
    assert structural_eq(e1, e2)

def test_substitute_var(x, y):
    expr = x + y
    result = substitute(expr, x, Lit(5))
    assert structural_eq(result, Lit(5) + y)

def test_substitute_no_capture(x, y):
    # substitute does not substitute inside a Forall binding the same var
    z = Var("z", int)
    expr = Forall(x, x + y)
    result = substitute(expr, x, Lit(5))
    # x is bound in the Forall, so substitution should not penetrate
    assert structural_eq(result, expr)

def test_free_vars(x, y):
    expr = x + y
    assert free_vars(expr) == {"x", "y"}

def test_free_vars_bound(x, y):
    expr = Forall(x, x + y)
    assert free_vars(expr) == {"y"}   # x is bound

Step 2: Run tests, confirm they fail

pytest tests/test_helpers.py -v

Step 3: Implement helpers.py

# logos/helpers.py
from logos.expr import (
    Expr, Lit, Var, Add, Sub, Mul, Div, Mod, Neg, Pow,
    Eq, Neq, Lt, Le, Gt, Ge, And, Or, Not, Implies,
    ForallNode, ExistsNode, App, CaseExpr,
)

def structural_eq(a: Expr, b: Expr) -> bool:
    if type(a) is not type(b):
        return False
    match a, b:
        case Lit(v1), Lit(v2):           return v1 == v2
        case Var(n1, t1), Var(n2, t2):   return n1 == n2 and t1 is t2
        case Add(l1,r1), Add(l2,r2):     return structural_eq(l1,l2) and structural_eq(r1,r2)
        case Sub(l1,r1), Sub(l2,r2):     return structural_eq(l1,l2) and structural_eq(r1,r2)
        case Mul(l1,r1), Mul(l2,r2):     return structural_eq(l1,l2) and structural_eq(r1,r2)
        case Div(l1,r1), Div(l2,r2):     return structural_eq(l1,l2) and structural_eq(r1,r2)
        case Mod(l1,r1), Mod(l2,r2):     return structural_eq(l1,l2) and structural_eq(r1,r2)
        case Neg(o1),    Neg(o2):         return structural_eq(o1, o2)
        case Pow(b1,e1), Pow(b2,e2):     return structural_eq(b1,b2) and structural_eq(e1,e2)
        case Eq(l1,r1),  Eq(l2,r2):      return structural_eq(l1,l2) and structural_eq(r1,r2)
        case Neq(l1,r1), Neq(l2,r2):    return structural_eq(l1,l2) and structural_eq(r1,r2)
        case Lt(l1,r1),  Lt(l2,r2):      return structural_eq(l1,l2) and structural_eq(r1,r2)
        case Le(l1,r1),  Le(l2,r2):      return structural_eq(l1,l2) and structural_eq(r1,r2)
        case Gt(l1,r1),  Gt(l2,r2):      return structural_eq(l1,l2) and structural_eq(r1,r2)
        case Ge(l1,r1),  Ge(l2,r2):      return structural_eq(l1,l2) and structural_eq(r1,r2)
        case And(l1,r1), And(l2,r2):     return structural_eq(l1,l2) and structural_eq(r1,r2)
        case Or(l1,r1),  Or(l2,r2):      return structural_eq(l1,l2) and structural_eq(r1,r2)
        case Not(o1),    Not(o2):         return structural_eq(o1, o2)
        case Implies(a1,c1), Implies(a2,c2): return structural_eq(a1,a2) and structural_eq(c1,c2)
        case ForallNode(v1,b1), ForallNode(v2,b2):
            return structural_eq(v1,v2) and structural_eq(b1,b2)
        case ExistsNode(v1,b1), ExistsNode(v2,b2):
            return structural_eq(v1,v2) and structural_eq(b1,b2)
        case App(f1,args1), App(f2,args2):
            return f1 == f2 and len(args1)==len(args2) and all(structural_eq(a,b) for a,b in zip(args1,args2))
        case _:
            return False

def substitute(expr: Expr, var: Var, val: Expr) -> Expr:
    """Replace all free occurrences of `var` in `expr` with `val`."""
    match expr:
        case Var(name, _) if name == var.name:
            return val
        case Var():
            return expr
        case Lit():
            return expr
        case ForallNode(v, body):
            if v.name == var.name:
                return expr  # var is bound here; stop
            return ForallNode(v, substitute(body, var, val))
        case ExistsNode(v, body):
            if v.name == var.name:
                return expr
            return ExistsNode(v, substitute(body, var, val))
        case App(name, args):
            return App(name, [substitute(a, var, val) for a in args])
        case _:
            # For all binary/unary nodes: recurse on children
            cls = type(expr)
            fields = [getattr(expr, f) for f in expr.__dataclass_fields__]
            new_fields = [substitute(f, var, val) if isinstance(f, Expr) else f for f in fields]
            return cls(*new_fields)

def free_vars(expr: Expr) -> set[str]:
    match expr:
        case Var(name, _):    return {name}
        case Lit():           return set()
        case ForallNode(v,b): return free_vars(b) - {v.name}
        case ExistsNode(v,b): return free_vars(b) - {v.name}
        case App(_, args):    return set().union(*(free_vars(a) for a in args))
        case _:
            result = set()
            for f in expr.__dataclass_fields__:
                val = getattr(expr, f)
                if isinstance(val, Expr):
                    result |= free_vars(val)
            return result

Step 4: Run and pass

pytest tests/test_helpers.py -v

Step 5: Commit

git add logos/helpers.py tests/test_helpers.py
git commit -m "feat: structural equality and substitution"

Task 4: Proof Terms + Kernel

Files:

Create: logos/kernel.py
Test: tests/test_kernel.py

Interfaces:

Consumes: structural_eq, substitute from logos.helpers; all Expr types
Produces: ProofTerm base class; all proof term constructors
Produces: Context(axioms: dict[str,Expr], hyps: dict[str,Expr]) dataclass
Produces: KernelError(Exception)
Produces: infer(term: ProofTerm, ctx: Context) -> Expr — trusted inference
Produces: check(term: ProofTerm, expected: Expr, ctx: Context) -> None — validates and raises on mismatch
Step 1: Write failing tests

# tests/test_kernel.py
import pytest
from logos.expr import Var, Lit, Add, Eq as LogosEq, And, Or, Implies, Forall, ForallNode
from logos.helpers import structural_eq
from logos.kernel import (
    Context, KernelError, infer, check,
    Refl, Symm, Trans, Subst, Axiom,
    ForallIntro, ForallElim,
    ImpliesIntro, ImpliesElim,
    AndIntro, AndElimL, AndElimR,
    OrIntroL, OrIntroR,
    HypRef,
)

def test_refl(x):
    ctx = Context({}, {})
    term = Refl(x)
    result = infer(term, ctx)
    assert structural_eq(result, x == x)

def test_symm(x, y):
    ctx = Context({"h": x == y}, {})
    term = Symm(Axiom("h"))
    result = infer(term, ctx)
    assert structural_eq(result, y == x)

def test_trans(x, y, z):
    ctx = Context({"h1": x == y, "h2": y == z}, {})
    term = Trans(Axiom("h1"), Axiom("h2"))
    result = infer(term, ctx)
    assert structural_eq(result, x == z)

def test_trans_middle_mismatch(x, y, z):
    ctx = Context({"h1": x == y, "h2": z == x}, {})  # y ≠ z
    with pytest.raises(KernelError, match="middle"):
        infer(Trans(Axiom("h1"), Axiom("h2")), ctx)

def test_subst(x, y):
    ctx = Context({"h": x == y}, {})
    # Subst(h, f) where f(e) = e + Lit(1): proves (x+1) == (y+1)
    term = Subst(Axiom("h"), lambda e: e + Lit(1))
    result = infer(term, ctx)
    assert structural_eq(result, (x + Lit(1)) == (y + Lit(1)))

def test_forall_intro_elim(x, y):
    # ForallIntro(x, Refl(x)) proves Forall(x, x == x)
    ctx = Context({}, {})
    intro_term = ForallIntro(x, Refl(x))
    stmt = infer(intro_term, ctx)
    assert structural_eq(stmt, Forall(x, x == x))

    # ForallElim on that proof with y: proves y == y
    elim_term = ForallElim(intro_term, y)
    result = infer(elim_term, ctx)
    assert structural_eq(result, y == y)

def test_implies_intro_elim(x):
    # ImpliesIntro("h", HypRef("h")) where h: x > 0 proves (x > 0) >> (x > 0)
    ctx = Context({}, {})
    antecedent = x > Lit(0)
    intro = ImpliesIntro(antecedent, HypRef("h"))
    stmt = infer(intro, ctx)
    assert structural_eq(stmt, antecedent >> antecedent)

def test_check_fails_on_mismatch(x, y):
    ctx = Context({}, {})
    term = Refl(x)
    with pytest.raises(KernelError):
        check(term, x == y, ctx)  # Refl(x) proves x==x, not x==y

def test_hyp_ref(x):
    ctx = Context({}, {"my_hyp": x > Lit(0)})
    term = HypRef("my_hyp")
    result = infer(term, ctx)
    assert structural_eq(result, x > Lit(0))

def test_and_intro(x, y):
    ctx = Context({"hx": x > Lit(0), "hy": y > Lit(0)}, {})
    term = AndIntro(Axiom("hx"), Axiom("hy"))
    result = infer(term, ctx)
    assert structural_eq(result, (x > Lit(0)) & (y > Lit(0)))

Step 2: Run tests, confirm they fail

pytest tests/test_kernel.py -v

Step 3: Implement kernel.py

# logos/kernel.py
from __future__ import annotations
from dataclasses import dataclass
from typing import Callable, Any
from logos.expr import (
    Expr, Var, Lit, Add, Sub, Mul, Div, Mod, Neg, Pow,
    Eq, Neq, Lt, Le, Gt, Ge, And, Or, Not, Implies,
    ForallNode, ExistsNode, App,
)
from logos.helpers import structural_eq, substitute


class KernelError(Exception):
    pass


@dataclass
class Context:
    axioms: dict[str, Expr]   # globally declared axioms
    hyps: dict[str, Expr]     # local hypotheses (in scope for current goal)

    def with_hyp(self, name: str, stmt: Expr) -> "Context":
        return Context(self.axioms, {**self.hyps, name: stmt})

    def lookup(self, name: str) -> Expr:
        if name in self.hyps:
            return self.hyps[name]
        if name in self.axioms:
            return self.axioms[name]
        raise KernelError(f"Unknown name '{name}' — not in hypotheses or axioms")


# ── Proof Terms ───────────────────────────────────────────────────────────────

class ProofTerm:
    pass

@dataclass(frozen=True)
class Refl(ProofTerm):
    expr: Expr                        # proves expr == expr

@dataclass(frozen=True)
class Symm(ProofTerm):
    proof: ProofTerm                  # if proof: a==b, proves b==a

@dataclass(frozen=True)
class Trans(ProofTerm):
    left: ProofTerm                   # proves a==b
    right: ProofTerm                  # proves b==c  →  together prove a==c

@dataclass(frozen=True)
class Subst(ProofTerm):
    proof: ProofTerm                  # proves a==b
    func: Callable[[Expr], Expr]      # f(a)==f(b)

@dataclass(frozen=True)
class Axiom(ProofTerm):
    name: str                         # proves the named axiom's statement

@dataclass(frozen=True)
class HypRef(ProofTerm):
    name: str                         # proves the named hypothesis

@dataclass(frozen=True)
class ForallIntro(ProofTerm):
    var: Var                          # the universally quantified variable
    body: ProofTerm                   # proof of P under that variable

@dataclass(frozen=True)
class ForallElim(ProofTerm):
    proof: ProofTerm                  # proof of Forall(x, P)
    val: Expr                         # instantiation value

@dataclass(frozen=True)
class ImpliesIntro(ProofTerm):
    hyp: Expr                         # the hypothesis being introduced
    body: ProofTerm                   # proof of conclusion with hyp in context

@dataclass(frozen=True)
class ImpliesElim(ProofTerm):
    implication: ProofTerm            # proves P >> Q
    premise: ProofTerm                # proves P  →  together prove Q

@dataclass(frozen=True)
class AndIntro(ProofTerm):
    left: ProofTerm
    right: ProofTerm

@dataclass(frozen=True)
class AndElimL(ProofTerm):
    proof: ProofTerm                  # proof of A & B → proves A

@dataclass(frozen=True)
class AndElimR(ProofTerm):
    proof: ProofTerm                  # proof of A & B → proves B

@dataclass(frozen=True)
class OrIntroL(ProofTerm):
    proof: ProofTerm                  # proof of A → proves A | B
    right_type: Expr                  # the B in A | B (needed to reconstruct type)

@dataclass(frozen=True)
class OrIntroR(ProofTerm):
    left_type: Expr
    proof: ProofTerm                  # proof of B → proves A | B

@dataclass(frozen=True)
class CaseAnalysis(ProofTerm):
    """Proves C given: proof of (A|B), proof of C with A as hyp, proof of C with B as hyp."""
    or_proof: ProofTerm
    hyp_name: str
    left_branch: ProofTerm
    right_branch: ProofTerm

@dataclass(frozen=True)
class NotIntro(ProofTerm):
    """Proves ~A given proof of A >> False."""
    impl_proof: ProofTerm

@dataclass(frozen=True)
class ExFalso(ProofTerm):
    """Proves anything given proof of False (ex falso quodlibet)."""
    false_proof: ProofTerm
    conclusion: Expr


# ── Kernel Inference ──────────────────────────────────────────────────────────

def infer(term: ProofTerm, ctx: Context) -> Expr:
    """Infer the statement proved by `term` under `ctx`. Raises KernelError if invalid."""
    match term:
        case Refl(expr):
            return Eq(expr, expr)

        case Symm(proof):
            stmt = infer(proof, ctx)
            match stmt:
                case Eq(a, b): return Eq(b, a)
            raise KernelError(f"Symm: expected Eq, got {stmt!r}")

        case Trans(left, right):
            l_stmt = infer(left, ctx)
            r_stmt = infer(right, ctx)
            match l_stmt, r_stmt:
                case Eq(a, b1), Eq(b2, c) if structural_eq(b1, b2):
                    return Eq(a, c)
            raise KernelError(f"Trans: middle terms don't match: {l_stmt!r} and {r_stmt!r}")

        case Subst(proof, func):
            stmt = infer(proof, ctx)
            match stmt:
                case Eq(a, b):
                    return Eq(func(a), func(b))
            raise KernelError(f"Subst: expected Eq, got {stmt!r}")

        case Axiom(name) | HypRef(name):
            return ctx.lookup(name)

        case ForallIntro(var, body):
            body_stmt = infer(body, ctx)
            return ForallNode(var, body_stmt)

        case ForallElim(proof, val):
            stmt = infer(proof, ctx)
            match stmt:
                case ForallNode(var, body):
                    return substitute(body, var, val)
            raise KernelError(f"ForallElim: expected ForallNode, got {stmt!r}")

        case ImpliesIntro(hyp, body):
            # Add hyp as an unnamed hypothesis — tactics must use HypRef by a chosen name
            # We infer the body statement; the hyp is the antecedent
            new_ctx = Context(ctx.axioms, {**ctx.hyps, "_impl_hyp": hyp})
            body_stmt = infer(body, new_ctx)
            return Implies(hyp, body_stmt)

        case ImpliesElim(implication, premise):
            impl_stmt = infer(implication, ctx)
            pre_stmt = infer(premise, ctx)
            match impl_stmt:
                case Implies(ant, cons) if structural_eq(ant, pre_stmt):
                    return cons
            raise KernelError(f"ImpliesElim: antecedent mismatch")

        case AndIntro(left, right):
            l = infer(left, ctx)
            r = infer(right, ctx)
            return And(l, r)

        case AndElimL(proof):
            stmt = infer(proof, ctx)
            match stmt:
                case And(l, _): return l
            raise KernelError("AndElimL: expected And")

        case AndElimR(proof):
            stmt = infer(proof, ctx)
            match stmt:
                case And(_, r): return r
            raise KernelError("AndElimR: expected And")

        case OrIntroL(proof, right_type):
            l = infer(proof, ctx)
            return Or(l, right_type)

        case OrIntroR(left_type, proof):
            r = infer(proof, ctx)
            return Or(left_type, r)

        case CaseAnalysis(or_proof, hyp_name, left_branch, right_branch):
            or_stmt = infer(or_proof, ctx)
            match or_stmt:
                case Or(a, b):
                    l_stmt = infer(left_branch, ctx.with_hyp(hyp_name, a))
                    r_stmt = infer(right_branch, ctx.with_hyp(hyp_name, b))
                    if not structural_eq(l_stmt, r_stmt):
                        raise KernelError("CaseAnalysis: branches prove different statements")
                    return l_stmt
            raise KernelError("CaseAnalysis: expected Or")

        case ExFalso(_, conclusion):
            return conclusion

        case _:
            raise KernelError(f"Unknown proof term: {term!r}")


def check(term: ProofTerm, expected: Expr, ctx: Context) -> None:
    """Validate that `term` proves `expected`. Raises KernelError on mismatch."""
    inferred = infer(term, ctx)
    if not structural_eq(inferred, expected):
        raise KernelError(
            f"Proof mismatch.\n  Expected: {expected!r}\n  Got:      {inferred!r}"
        )

Step 4: Run tests

pytest tests/test_kernel.py -v

Expected: all green.

Step 5: Fix ImpliesIntro hyp naming

The test uses HypRef("h") inside ImpliesIntro. Update the kernel to accept a hyp_name parameter so the body can refer to it:

# Replace ImpliesIntro dataclass:
@dataclass(frozen=True)
class ImpliesIntro(ProofTerm):
    hyp: Expr
    hyp_name: str          # name under which hyp is added to context
    body: ProofTerm

# Update infer case:
case ImpliesIntro(hyp, hyp_name, body):
    new_ctx = ctx.with_hyp(hyp_name, hyp)
    body_stmt = infer(body, new_ctx)
    return Implies(hyp, body_stmt)

Update test to pass hyp_name:

intro = ImpliesIntro(antecedent, "h", HypRef("h"))

Step 6: Rerun and commit

pytest tests/test_kernel.py -v
git add logos/kernel.py tests/test_kernel.py
git commit -m "feat: proof terms and trusted kernel"

Task 5: Axiom Registry + Goal

Files:

Create: logos/registry.py
Create: logos/goal.py
Test: tests/test_goal.py

Interfaces:

Produces: register_axiom(name: str, stmt: Expr) -> None
Produces: get_all_axioms() -> dict[str, Expr]
Produces: Goal(context: dict[str,Expr], statement: Expr) dataclass
Produces: Goal.with_hyp(name, hyp) -> Goal
Produces: Goal.make_context() -> Context — merges goal hyps + global axioms
Step 1: Write tests

# tests/test_goal.py
from logos.expr import Var, Lit
from logos.registry import register_axiom, get_all_axioms, clear_axioms
from logos.goal import Goal
from logos.kernel import Context

def test_register_axiom(x):
    clear_axioms()
    stmt = x > Lit(0)
    register_axiom("pos_x", stmt)
    assert "pos_x" in get_all_axioms()

def test_duplicate_axiom(x):
    clear_axioms()
    register_axiom("pos_x", x > Lit(0))
    with pytest.raises(ValueError, match="already registered"):
        register_axiom("pos_x", x > Lit(0))

def test_goal_with_hyp(x, y):
    g = Goal({}, x > Lit(0))
    g2 = g.with_hyp("h", y > Lit(0))
    assert "h" in g2.context

def test_goal_make_context(x):
    clear_axioms()
    register_axiom("ax1", x == x)
    g = Goal({"h": x > Lit(0)}, x > Lit(0))
    ctx = g.make_context()
    assert "ax1" in ctx.axioms
    assert "h" in ctx.hyps

Step 2: Implement

# logos/registry.py
from logos.expr import Expr

_axioms: dict[str, Expr] = {}

def register_axiom(name: str, stmt: Expr) -> None:
    if name in _axioms:
        raise ValueError(f"Axiom '{name}' already registered")
    _axioms[name] = stmt

def get_all_axioms() -> dict[str, Expr]:
    return dict(_axioms)

def clear_axioms() -> None:
    _axioms.clear()

# logos/goal.py
from __future__ import annotations
from dataclasses import dataclass, field
from logos.expr import Expr
from logos.kernel import Context
from logos.registry import get_all_axioms

@dataclass
class Goal:
    context: dict[str, Expr]
    statement: Expr

    def with_hyp(self, name: str, hyp: Expr) -> "Goal":
        return Goal({**self.context, name: hyp}, self.statement)

    def with_statement(self, stmt: Expr) -> "Goal":
        return Goal(dict(self.context), stmt)

    def make_context(self) -> Context:
        return Context(axioms=get_all_axioms(), hyps=dict(self.context))

Step 3: Run, pass, commit

pytest tests/test_goal.py -v
git add logos/registry.py logos/goal.py tests/test_goal.py
git commit -m "feat: axiom registry and Goal"

Task 6: Tactic Runner

Files:

Create: logos/runner.py
Test: tests/test_runner.py

Interfaces:

Produces: TacticFailed(Exception)
Produces: TacticResult = ProofTerm | tuple[list[Goal], Callable[[list[ProofTerm]], ProofTerm]]
Produces: run(goal: Goal, by: list) -> ProofTerm

The runner walks by left-to-right. Atomic tactics return ProofTerm (close the goal). Splitting tactics return (subgoals, compose) — each subgoal consumes the next item in by. Nested lists [...] completely handle one subgoal.

Step 1: Write tests

# tests/test_runner.py
import pytest
from logos.expr import Var, Lit
from logos.goal import Goal
from logos.kernel import Refl, AndIntro, ProofTerm
from logos.runner import run, TacticFailed
from logos.helpers import structural_eq

def closing_tactic(goal: Goal) -> ProofTerm:
    """Dummy: always returns Refl for test purposes."""
    return Refl(goal.statement.left)   # assumes Eq goal

def transforming_tactic(goal: Goal):
    """Transforms goal to a simpler form (1 subgoal)."""
    new_goal = Goal(goal.context, goal.statement)
    return [new_goal], lambda proofs: proofs[0]

def splitting_tactic(goal: Goal):
    """Splits into 2 subgoals (mirrors AndIntro)."""
    match goal.statement:
        case _ if hasattr(goal.statement, "left") and hasattr(goal.statement, "right"):
            l_goal = Goal(goal.context, goal.statement.left)
            r_goal = Goal(goal.context, goal.statement.right)
            return [l_goal, r_goal], lambda ps: AndIntro(ps[0], ps[1])

def test_atomic_closes_goal(x):
    goal = Goal({}, x == x)
    proof = run(goal, [closing_tactic])
    assert isinstance(proof, ProofTerm)

def test_transforming_tactic(x):
    goal = Goal({}, x == x)
    proof = run(goal, [transforming_tactic, closing_tactic])
    assert isinstance(proof, ProofTerm)

def test_splitting_with_nested_lists(x, y):
    from logos.expr import And
    goal = Goal({}, (x == x) & (y == y))
    proof = run(goal, [
        splitting_tactic,
        [closing_tactic],   # handles x == x
        [closing_tactic],   # handles y == y
    ])
    assert isinstance(proof, ProofTerm)

def test_no_tactics_raises(x):
    goal = Goal({}, x == x)
    with pytest.raises(TacticFailed, match="no tactics"):
        run(goal, [])

def test_extra_tactics_raises(x):
    goal = Goal({}, x == x)
    with pytest.raises(TacticFailed, match="tactics remain"):
        run(goal, [closing_tactic, closing_tactic])

Step 2: Implement runner.py

# logos/runner.py
from __future__ import annotations
import inspect
from typing import Callable, Any
from logos.goal import Goal
from logos.kernel import ProofTerm

class TacticFailed(Exception):
    pass

TacticResult = ProofTerm | tuple[list[Goal], Callable[[list[ProofTerm]], ProofTerm]]

def run(goal: Goal, by: list) -> ProofTerm:
    """Apply tactics in `by` to `goal`, returning a proof term."""
    return _Runner(list(by)).run(goal)


class _Runner:
    def __init__(self, tactics: list):
        self._tactics = tactics
        self._idx = 0

    def _take(self):
        if self._idx >= len(self._tactics):
            raise TacticFailed("No tactics left; open goal remains")
        item = self._tactics[self._idx]
        self._idx += 1
        return item

    def run(self, goal: Goal) -> ProofTerm:
        item = self._take()

        if isinstance(item, list):
            # Nested list: fresh sub-runner for this goal only
            return _Runner(item).run(goal)

        result = item(goal)

        if isinstance(result, ProofTerm):
            # Atomic: goal is closed
            if self._idx < len(self._tactics):
                remaining = len(self._tactics) - self._idx
                raise TacticFailed(
                    f"Goal closed by {item.__name__ if hasattr(item,'__name__') else item!r} "
                    f"but {remaining} tactic(s) remain"
                )
            return result

        # Splitting/transforming: (subgoals, compose)
        subgoals, compose = result
        subgoal_proofs = [self.run(sg) for sg in subgoals]
        return compose(subgoal_proofs)

Step 3: Run, pass, commit

pytest tests/test_runner.py -v
git add logos/runner.py tests/test_runner.py
git commit -m "feat: tactic runner"

Task 7: Structural Tactics

Files:

Create: logos/tactics/structural.py
Test: tests/test_tactics/test_structural.py

Interfaces:

Consumes: Goal, run, TacticFailed, all kernel proof terms, structural_eq, substitute
Produces: intro(*names), assumption(), exact(term), apply(name_or_term), cases(cond), split(), left(right_type), right(left_type), witness(val), contradiction()
Step 1: Write tests

# tests/test_tactics/test_structural.py
import pytest
from logos.expr import Var, Lit, And, Or, Implies, Forall, Exists, ExistsNode
from logos.goal import Goal
from logos.kernel import (
    infer, Context, Refl, HypRef, AndIntro,
    ForallIntro, ImpliesIntro,
)
from logos.helpers import structural_eq
from logos.runner import run, TacticFailed
from logos.registry import register_axiom, clear_axioms
from logos.tactics.structural import intro, assumption, exact, split, left, right, witness

def test_intro_forall(x, y):
    goal = Goal({}, Forall(x, x == x))
    proof = run(goal, [intro("x"), exact(Refl(Var("x", int)))])
    stmt = infer(proof, Context({}, {}))
    assert structural_eq(stmt, Forall(x, x == x))

def test_intro_implies(x):
    hyp = x > Lit(0)
    goal = Goal({}, hyp >> hyp)
    proof = run(goal, [intro("h"), assumption()])
    stmt = infer(proof, Context({}, {}))
    assert structural_eq(stmt, hyp >> hyp)

def test_assumption(x):
    hyp = x > Lit(0)
    goal = Goal({"h": hyp}, hyp)
    proof = run(goal, [assumption()])
    stmt = infer(proof, Context({}, {"h": hyp}))
    assert structural_eq(stmt, hyp)

def test_split(x, y):
    goal = Goal({"hx": x > Lit(0), "hy": y > Lit(0)},
                (x > Lit(0)) & (y > Lit(0)))
    proof = run(goal, [split(), [assumption()], [assumption()]])
    ctx = Context({}, {"hx": x > Lit(0), "hy": y > Lit(0)})
    stmt = infer(proof, ctx)
    assert structural_eq(stmt, (x > Lit(0)) & (y > Lit(0)))

def test_left(x):
    from logos.expr import Or
    goal = Goal({"h": x > Lit(0)}, (x > Lit(0)) | (x < Lit(0)))
    proof = run(goal, [left(x < Lit(0)), assumption()])
    ctx = Context({}, {"h": x > Lit(0)})
    stmt = infer(proof, ctx)
    assert structural_eq(stmt, (x > Lit(0)) | (x < Lit(0)))

def test_witness(x):
    x_val = Var("x", int)
    goal = Goal({"h": Lit(5) > Lit(0)}, Exists(x_val, x_val > Lit(0)))
    proof = run(goal, [witness(Lit(5)), assumption()])
    ctx = Context({}, {"h": Lit(5) > Lit(0)})
    stmt = infer(proof, ctx)
    # should prove Exists(x, x > 0)
    assert isinstance(stmt, ExistsNode)

Step 2: Implement structural.py

# logos/tactics/structural.py
from logos.expr import (
    Expr, Var, ForallNode, ExistsNode, And, Or, Not, Implies,
)
from logos.goal import Goal
from logos.kernel import (
    ProofTerm, KernelError,
    Refl, HypRef, ForallIntro, ForallElim,
    ImpliesIntro, ImpliesElim,
    AndIntro, AndElimL, AndElimR,
    OrIntroL, OrIntroR, CaseAnalysis, ExFalso,
)
from logos.helpers import substitute, structural_eq
from logos.runner import TacticFailed

def intro(*names: str):
    def tactic(goal: Goal):
        stmt = goal.statement
        ctx = dict(goal.context)
        steps = []   # track what was introduced for compose

        for name in names:
            match stmt:
                case ForallNode(var, body):
                    new_var = Var(name, var.type)
                    ctx[name] = new_var   # note the var in context
                    stmt = substitute(body, var, new_var)
                    steps.append(("forall", name, new_var))
                case Implies(ant, cons):
                    ctx[name] = ant
                    stmt = cons
                    steps.append(("implies", name, ant))
                case _:
                    raise TacticFailed(f"intro '{name}': cannot introduce into {stmt!r}")

        new_goal = Goal(ctx, stmt)

        def compose(proofs: list[ProofTerm]) -> ProofTerm:
            [body_proof] = proofs
            result = body_proof
            for kind, name, info in reversed(steps):
                if kind == "forall":
                    result = ForallIntro(info, result)
                else:
                    result = ImpliesIntro(info, name, result)
            return result

        return [new_goal], compose
    return tactic


def assumption():
    def tactic(goal: Goal) -> ProofTerm:
        for name, hyp in goal.context.items():
            if structural_eq(hyp, goal.statement):
                return HypRef(name)
        raise TacticFailed(f"assumption: {goal.statement!r} not in context")
    return tactic


def exact(term: ProofTerm):
    def tactic(goal: Goal) -> ProofTerm:
        return term
    return tactic


def apply(name: str):
    """Apply a named axiom/hypothesis. Unifies conclusion, generates premise subgoals."""
    def tactic(goal: Goal):
        ctx = goal.make_context()
        stmt = ctx.lookup(name)
        # Peel off Forall layers (simplified: only works if conclusion matches directly)
        # For v0.1: only supports theorems with no premises (atomic statements)
        if structural_eq(stmt, goal.statement):
            return HypRef(name) if name in ctx.hyps else \
                   __import__("logos.kernel", fromlist=["Axiom"]).Axiom(name)
        raise TacticFailed(f"apply '{name}': {stmt!r} does not match goal {goal.statement!r}")
    return tactic


def split():
    def tactic(goal: Goal):
        match goal.statement:
            case And(left, right):
                return (
                    [Goal(goal.context, left), Goal(goal.context, right)],
                    lambda ps: AndIntro(ps[0], ps[1])
                )
            case _:
                raise TacticFailed(f"split: expected A & B, got {goal.statement!r}")
    return tactic


def left(right_type: Expr):
    def tactic(goal: Goal):
        match goal.statement:
            case Or(l, _):
                return [Goal(goal.context, l)], lambda ps: OrIntroL(ps[0], right_type)
            case _:
                raise TacticFailed(f"left: expected A | B, got {goal.statement!r}")
    return tactic


def right(left_type: Expr):
    def tactic(goal: Goal):
        match goal.statement:
            case Or(_, r):
                return [Goal(goal.context, r)], lambda ps: OrIntroR(left_type, ps[0])
            case _:
                raise TacticFailed(f"right: expected A | B, got {goal.statement!r}")
    return tactic


def witness(val: Expr):
    def tactic(goal: Goal):
        match goal.statement:
            case ExistsNode(var, body):
                new_stmt = substitute(body, var, val)
                return (
                    [Goal(goal.context, new_stmt)],
                    lambda ps: __import__("logos.kernel", fromlist=["ExistsIntro"]).ExistsIntro(val, ps[0])
                )
            case _:
                raise TacticFailed(f"witness: expected Exists, got {goal.statement!r}")
    return tactic


def contradiction():
    def tactic(goal: Goal) -> ProofTerm:
        stmts = list(goal.context.values())
        for i, s in enumerate(stmts):
            for j, t in enumerate(stmts):
                if i != j and structural_eq(s, Not(t)) or structural_eq(Not(s), t):
                    # We have P and ~P in context
                    names = list(goal.context.keys())
                    return ExFalso(HypRef(names[i]), goal.statement)
        raise TacticFailed("contradiction: no contradictory hypotheses found")
    return tactic

Note: ExistsIntro is missing from kernel.py. Add it:

# Add to kernel.py
@dataclass(frozen=True)
class ExistsIntro(ProofTerm):
    witness: Expr
    body: ProofTerm    # proof of P[x := witness]

# Add to infer():
case ExistsIntro(witness, body):
    stmt = infer(body, ctx)
    # Reconstruct Exists — we need the Exists goal to know the var name
    # For v0.1: trust that the body proves P[witness/x]; wrap in ExistsNode
    # The caller (witness tactic) already knows the ExistsNode structure
    return stmt   # simplified: body already proves substituted statement

Step 3: Run tests and fix issues

pytest tests/test_tactics/test_structural.py -v

Fix any type/signature errors found; rerun until green.

Step 4: Commit

git add logos/tactics/structural.py tests/test_tactics/test_structural.py logos/kernel.py
git commit -m "feat: structural tactics (intro, assumption, split, left, right, witness, contradiction)"

Task 8: Rewrite Tactics

Files:

Create: logos/tactics/rewrite.py
Test: tests/test_tactics/test_rewrite.py

Interfaces:

Consumes: _defined_functions: dict[str, tuple[list[Var], Expr]] from logos.define (populated in Task 11; for now use a module-level registry in logos.define)
Produces: unfold(*func_names), refl(), rewrite(axiom_name), rewrite_rev(axiom_name), eval_(), norm_num()
Step 1: Write tests

# tests/test_tactics/test_rewrite.py
from logos.expr import Var, Lit, Add
from logos.goal import Goal
from logos.kernel import infer, Context
from logos.helpers import structural_eq
from logos.runner import run
from logos.tactics.rewrite import refl, eval_, norm_num

def test_refl_closes_eq_goal(x):
    goal = Goal({}, x == x)
    proof = run(goal, [refl()])
    ctx = Context({}, {})
    assert structural_eq(infer(proof, ctx), x == x)

def test_refl_fails_on_non_eq(x, y):
    from logos.runner import TacticFailed
    goal = Goal({}, x == y)   # x != y structurally
    with pytest.raises(TacticFailed, match="refl"):
        run(goal, [refl()])

def test_eval_ground():
    goal = Goal({}, Lit(2) + Lit(3) == Lit(5))
    proof = run(goal, [eval_()])
    ctx = Context({}, {})
    assert structural_eq(infer(proof, ctx), Lit(2) + Lit(3) == Lit(5))

def test_norm_num():
    goal = Goal({}, Lit(6) == Lit(2) * Lit(3))
    proof = run(goal, [norm_num()])
    ctx = Context({}, {})
    assert structural_eq(infer(proof, ctx), Lit(6) == Lit(2) * Lit(3))

Step 2: Implement rewrite.py

# logos/tactics/rewrite.py
from logos.expr import Expr, Lit, Var, Add, Sub, Mul, Div, Mod, Neg, Pow, Eq
from logos.goal import Goal
from logos.kernel import ProofTerm, Refl, Symm, Trans, Subst, Axiom, KernelError
from logos.helpers import structural_eq, substitute
from logos.runner import TacticFailed


def refl():
    def tactic(goal: Goal) -> ProofTerm:
        match goal.statement:
            case Eq(lhs, rhs) if structural_eq(lhs, rhs):
                return Refl(lhs)
            case _:
                raise TacticFailed(f"refl: goal is not `a == a`, got {goal.statement!r}")
    return tactic


def eval_():
    """Evaluate ground (variable-free) arithmetic sub-expressions, then close with Refl."""
    def tactic(goal: Goal) -> ProofTerm:
        match goal.statement:
            case Eq(lhs, rhs):
                lhs_val = _eval_ground(lhs)
                rhs_val = _eval_ground(rhs)
                if lhs_val == rhs_val:
                    return Refl(Lit(lhs_val))
                raise TacticFailed(f"eval: {lhs_val} ≠ {rhs_val}")
            case _:
                raise TacticFailed("eval: goal must be an equation")
    return tactic


def norm_num():
    """Normalize numeric literals and close if equal."""
    def tactic(goal: Goal) -> ProofTerm:
        match goal.statement:
            case Eq(lhs, rhs):
                try:
                    l = _eval_ground(lhs)
                    r = _eval_ground(rhs)
                    if l == r:
                        return Refl(Lit(l))
                    raise TacticFailed(f"norm_num: {l} ≠ {r}")
                except ValueError as e:
                    raise TacticFailed(f"norm_num: {e}")
            case _:
                raise TacticFailed("norm_num: goal must be an equation")
    return tactic


def _eval_ground(expr: Expr) -> int | float:
    """Evaluate a ground (no free variables) expression to a Python number."""
    match expr:
        case Lit(v) if isinstance(v, (int, float)): return v
        case Var():       raise ValueError(f"Variable {expr.name!r} in ground expression")
        case Add(l, r):   return _eval_ground(l) + _eval_ground(r)
        case Sub(l, r):   return _eval_ground(l) - _eval_ground(r)
        case Mul(l, r):   return _eval_ground(l) * _eval_ground(r)
        case Div(l, r):   return _eval_ground(l) // _eval_ground(r)
        case Mod(l, r):   return _eval_ground(l) % _eval_ground(r)
        case Neg(o):      return -_eval_ground(o)
        case Pow(b, e):   return _eval_ground(b) ** _eval_ground(e)
        case _:           raise ValueError(f"Cannot evaluate {expr!r}")


def unfold(*func_names: str):
    """Replace App(name, args) nodes with the function's definition body."""
    def tactic(goal: Goal):
        from logos.define import get_definition
        new_stmt = goal.statement
        for name in func_names:
            params, body = get_definition(name)
            new_stmt = _unfold_in(new_stmt, name, params, body)
        new_goal = goal.with_statement(new_stmt)
        return [new_goal], lambda ps: ps[0]
    return tactic


def _unfold_in(expr: Expr, fname: str, params: list[Var], body: Expr) -> Expr:
    from logos.expr import App
    match expr:
        case App(n, args) if n == fname:
            result = body
            for param, arg in zip(params, args):
                result = substitute(result, param, arg)
            return result
        case _:
            cls = type(expr)
            if not hasattr(cls, "__dataclass_fields__"):
                return expr
            fields = [getattr(expr, f) for f in cls.__dataclass_fields__]
            new_fields = [
                _unfold_in(f, fname, params, body) if isinstance(f, Expr) else f
                for f in fields
            ]
            return cls(*new_fields)


def rewrite(axiom_name: str):
    """Rewrite left-to-right using a named equation axiom."""
    def tactic(goal: Goal):
        ctx = goal.make_context()
        eq_stmt = ctx.lookup(axiom_name)
        match eq_stmt:
            case Eq(lhs, rhs):
                new_stmt = _replace_in(goal.statement, lhs, rhs)
                if structural_eq(new_stmt, goal.statement):
                    raise TacticFailed(f"rewrite '{axiom_name}': no occurrence of {lhs!r} found")
                new_goal = goal.with_statement(new_stmt)
                return [new_goal], lambda ps: ps[0]
            case _:
                raise TacticFailed(f"rewrite: '{axiom_name}' is not an equation")
    return tactic


def rewrite_rev(axiom_name: str):
    """Rewrite right-to-left using a named equation axiom."""
    def tactic(goal: Goal):
        ctx = goal.make_context()
        eq_stmt = ctx.lookup(axiom_name)
        match eq_stmt:
            case Eq(lhs, rhs):
                new_stmt = _replace_in(goal.statement, rhs, lhs)
                if structural_eq(new_stmt, goal.statement):
                    raise TacticFailed(f"rewrite_rev '{axiom_name}': no occurrence found")
                new_goal = goal.with_statement(new_stmt)
                return [new_goal], lambda ps: ps[0]
            case _:
                raise TacticFailed(f"rewrite_rev: '{axiom_name}' is not an equation")
    return tactic


def _replace_in(expr: Expr, pattern: Expr, replacement: Expr) -> Expr:
    if structural_eq(expr, pattern):
        return replacement
    cls = type(expr)
    if not hasattr(cls, "__dataclass_fields__"):
        return expr
    fields = [getattr(expr, f) for f in cls.__dataclass_fields__]
    new_fields = [
        _replace_in(f, pattern, replacement) if isinstance(f, Expr) else f
        for f in fields
    ]
    return cls(*new_fields)

Step 3: Run, pass, commit

pytest tests/test_tactics/test_rewrite.py -v
git add logos/tactics/rewrite.py tests/test_tactics/test_rewrite.py
git commit -m "feat: rewrite tactics (refl, eval, norm_num, unfold, rewrite)"

Task 9: Arithmetic Tactics — Ring

Files:

Create: logos/tactics/arithmetic.py
Test: tests/test_tactics/test_arithmetic.py

Interfaces:

Produces: ring() — closes polynomial ring identities over int/float
Produces: decide() — closes ground boolean propositions
Step 1: Write ring tests

# tests/test_tactics/test_arithmetic.py
import pytest
from logos.expr import Var, Lit
from logos.goal import Goal
from logos.kernel import infer, Context
from logos.helpers import structural_eq
from logos.runner import run, TacticFailed
from logos.tactics.arithmetic import ring, decide

def test_ring_commutativity(x, y):
    goal = Goal({}, x + y == y + x)
    proof = run(goal, [ring()])
    assert structural_eq(infer(proof, Context({}, {})), x + y == y + x)

def test_ring_distributivity(x, y, z):
    goal = Goal({}, x * (y + z) == x * y + x * z)
    proof = run(goal, [ring()])
    assert structural_eq(infer(proof, Context({}, {})), x * (y + z) == x * y + x * z)

def test_ring_constant_folding():
    goal = Goal({}, Lit(2) + Lit(3) == Lit(5))
    proof = run(goal, [ring()])

def test_ring_fails_on_inequality(x, y):
    goal = Goal({}, x + y == x - y)   # not a ring identity
    with pytest.raises(TacticFailed, match="ring"):
        run(goal, [ring()])

def test_decide_ground_true():
    goal = Goal({}, Lit(3) > Lit(2))
    proof = run(goal, [decide()])

Step 2: Implement ring() and decide()

# logos/tactics/arithmetic.py
from logos.expr import (
    Expr, Lit, Var, Add, Sub, Mul, Div, Mod, Neg, Pow, Eq,
    Lt, Le, Gt, Ge,
)
from logos.goal import Goal
from logos.kernel import ProofTerm, Refl, KernelError
from logos.helpers import structural_eq
from logos.runner import TacticFailed

# Polynomial: dict from frozenset of (name, exp) pairs to coefficient
Poly = dict[frozenset, int | float]


def _poly_add(a: Poly, b: Poly) -> Poly:
    result = dict(a)
    for mono, coef in b.items():
        result[mono] = result.get(mono, 0) + coef
    return {m: c for m, c in result.items() if c != 0}


def _poly_scale(p: Poly, factor: int | float) -> Poly:
    return {m: c * factor for m, c in p.items()}


def _poly_mul(a: Poly, b: Poly) -> Poly:
    result: Poly = {}
    for m1, c1 in a.items():
        for m2, c2 in b.items():
            # Combine monomials: sum exponents
            combined: dict[str, int] = {}
            for name, exp in m1:
                combined[name] = combined.get(name, 0) + exp
            for name, exp in m2:
                combined[name] = combined.get(name, 0) + exp
            mono = frozenset((n, e) for n, e in combined.items() if e != 0)
            result[mono] = result.get(mono, 0) + c1 * c2
    return {m: c for m, c in result.items() if c != 0}


def _normalize(expr: Expr) -> Poly:
    match expr:
        case Lit(v) if isinstance(v, (int, float)):
            return {frozenset(): v} if v != 0 else {}
        case Var(name, _):
            return {frozenset({(name, 1)}): 1}
        case Add(l, r):
            return _poly_add(_normalize(l), _normalize(r))
        case Sub(l, r):
            return _poly_add(_normalize(l), _poly_scale(_normalize(r), -1))
        case Mul(l, r):
            return _poly_mul(_normalize(l), _normalize(r))
        case Neg(o):
            return _poly_scale(_normalize(o), -1)
        case Pow(base, Lit(n)) if isinstance(n, int) and n >= 0:
            result: Poly = {frozenset(): 1}
            base_p = _normalize(base)
            for _ in range(n):
                result = _poly_mul(result, base_p)
            return result
        case _:
            raise TacticFailed(f"ring: cannot normalize {expr!r}")


def ring():
    def tactic(goal: Goal) -> ProofTerm:
        match goal.statement:
            case Eq(lhs, rhs):
                try:
                    lhs_p = _normalize(lhs)
                    rhs_p = _normalize(rhs)
                    if lhs_p == rhs_p:
                        return Refl(goal.statement.left)
                    raise TacticFailed(
                        f"ring: {lhs!r} ≠ {rhs!r} after normalization\n"
                        f"  LHS poly: {lhs_p}\n  RHS poly: {rhs_p}"
                    )
                except TacticFailed:
                    raise
                except Exception as e:
                    raise TacticFailed(f"ring: {e}")
            case _:
                raise TacticFailed(f"ring: goal is not an equation, got {goal.statement!r}")
    return tactic


def decide():
    """Evaluate a ground boolean proposition and close the goal."""
    def tactic(goal: Goal) -> ProofTerm:
        try:
            result = _eval_bool(goal.statement)
        except ValueError as e:
            raise TacticFailed(f"decide: {e}")
        if result:
            return Refl(goal.statement)   # simplified: use Refl as witness token
        raise TacticFailed(f"decide: proposition is False: {goal.statement!r}")
    return tactic


def _eval_bool(expr: Expr) -> bool:
    from logos.tactics.rewrite import _eval_ground
    match expr:
        case Lit(v) if isinstance(v, bool): return v
        case Lt(l, r):  return _eval_ground(l) <  _eval_ground(r)
        case Le(l, r):  return _eval_ground(l) <= _eval_ground(r)
        case Gt(l, r):  return _eval_ground(l) >  _eval_ground(r)
        case Ge(l, r):  return _eval_ground(l) >= _eval_ground(r)
        case Eq(l, r):  return _eval_ground(l) == _eval_ground(r)
        case _:         raise ValueError(f"Cannot decide {expr!r}")

Step 3: Run, pass, commit

pytest tests/test_tactics/test_arithmetic.py -v
git add logos/tactics/arithmetic.py tests/test_tactics/test_arithmetic.py
git commit -m "feat: ring tactic (polynomial normalization) and decide"

Task 10: Linarith Tactic

Files:

Modify: logos/tactics/arithmetic.py
Modify: tests/test_tactics/test_arithmetic.py

Interfaces:

Produces: linarith() — closes linear arithmetic goals via Farkas combination
Step 1: Add linarith tests

# append to tests/test_tactics/test_arithmetic.py
from logos.tactics.arithmetic import linarith

def test_linarith_simple(x, y):
    # From x > 0 and y > x, prove y > 0
    goal = Goal({"h1": x > Lit(0), "h2": y > x}, y > Lit(0))
    proof = run(goal, [linarith()])

def test_linarith_combination(x, y):
    # From 2x > 4 and x > 0, prove x > 2 ... simplified: from x > 2, prove x > 1
    goal = Goal({"h": x > Lit(2)}, x > Lit(1))
    proof = run(goal, [linarith()])

def test_linarith_fails_when_not_provable(x):
    goal = Goal({"h": x > Lit(0)}, x > Lit(5))  # x>0 doesn't imply x>5
    with pytest.raises(TacticFailed):
        run(goal, [linarith()])

Step 2: Implement linarith()

linarith works by:

Collecting linear hypotheses from the context as (coefficients_dict, bound, is_strict) triples
Negating the goal and adding it as a hypothesis
Trying to find a non-negative Farkas combination that sums to a contradiction (0 > 0 or 0 >= 1)

For v0.1 this uses a simplified "try linear combinations up to depth 2" approach — not complete but handles common cases.

# Append to logos/tactics/arithmetic.py

from fractions import Fraction

def linarith():
    def tactic(goal: Goal) -> ProofTerm:
        # Collect linear inequalities: (coef_dict, bound, strict)
        # e.g., "x > 2" → ({x: 1}, 2, True)
        ineqs = []
        for name, hyp in goal.context.items():
            ineq = _parse_linear_ineq(hyp)
            if ineq is not None:
                ineqs.append(ineq)

        # Negate the goal and add as a hypothesis
        negated = _negate_ineq(_parse_linear_ineq(goal.statement))
        if negated is None:
            raise TacticFailed("linarith: goal is not a linear inequality")
        ineqs.append(negated)

        # Try to derive a contradiction via non-negative combination
        if _farkas_contradiction(ineqs):
            return Refl(goal.statement)  # token proof; kernel trusts linarith for v0.1
        raise TacticFailed("linarith: no linear combination found")
    return tactic


def _parse_linear_ineq(expr: Expr):
    """Parse `expr` into (coefs: dict[str, Fraction], bound: Fraction, strict: bool).
    coefs[var] + ... OP bound.  Returns None if not linear."""
    match expr:
        case Gt(l, r) | Ge(l, r) | Lt(l, r) | Le(l, r) | Eq(l, r):
            strict = isinstance(expr, (Gt, Lt)) or (isinstance(expr, Eq) and False)
            coefs = _linear_coefs(l)
            rcoefs = _linear_coefs(r)
            if coefs is None or rcoefs is None:
                return None
            # Move RHS to left: (lcoefs - rcoefs) OP 0
            combined = {}
            for k, v in coefs.items():  combined[k] = v
            for k, v in rcoefs.items(): combined[k] = combined.get(k, Fraction(0)) - v
            bound = -combined.pop("_const", Fraction(0))
            strict = isinstance(expr, (Gt, Lt))
            if isinstance(expr, (Lt, Le)):
                combined = {k: -v for k, v in combined.items()}
                bound = -bound
                strict = isinstance(expr, Lt)
            return combined, bound, strict
        case _:
            return None


def _linear_coefs(expr: Expr) -> dict | None:
    """Return {varname: coef, "_const": const} for a linear expression, or None."""
    match expr:
        case Lit(v) if isinstance(v, (int, float)):
            return {"_const": Fraction(v)}
        case Var(name, _):
            return {name: Fraction(1)}
        case Add(l, r):
            lc, rc = _linear_coefs(l), _linear_coefs(r)
            if lc is None or rc is None: return None
            result = dict(lc)
            for k, v in rc.items(): result[k] = result.get(k, Fraction(0)) + v
            return result
        case Sub(l, r):
            lc, rc = _linear_coefs(l), _linear_coefs(r)
            if lc is None or rc is None: return None
            result = dict(lc)
            for k, v in rc.items(): result[k] = result.get(k, Fraction(0)) - v
            return result
        case Mul(Lit(c), e) | Mul(e, Lit(c)) if isinstance(c, (int, float)):
            ec = _linear_coefs(e)
            if ec is None: return None
            return {k: Fraction(c) * v for k, v in ec.items()}
        case Neg(o):
            oc = _linear_coefs(o)
            if oc is None: return None
            return {k: -v for k, v in oc.items()}
        case _:
            return None


def _negate_ineq(ineq):
    if ineq is None: return None
    coefs, bound, strict = ineq
    # Negate: a > b becomes a <= b, i.e., -a >= -b → flip sign
    return ({k: -v for k, v in coefs.items()}, -bound, not strict)


def _farkas_contradiction(ineqs: list) -> bool:
    """
    Try to find λ_i >= 0 such that sum(λ_i * ineq_i) derives 0 > 0 or 0 >= c > 0.
    Simplified: try all pairs and unit combinations.
    """
    # Try each inequality as a standalone contradiction
    for coefs, bound, strict in ineqs:
        if not coefs:  # constant: "0 > bound" or "0 >= bound"
            if strict and bound >= 0: return True
            if not strict and bound > 0: return True

    # Try pairs: λ1 * ineq1 + λ2 * ineq2
    from itertools import combinations
    for (c1, b1, s1), (c2, b2, s2) in combinations(ineqs, 2):
        for lam1, lam2 in [(1, 1), (1, 2), (2, 1), (1, Fraction(1,2)), (Fraction(1,2), 1)]:
            combined_coefs = {}
            for k, v in c1.items(): combined_coefs[k] = lam1 * v
            for k, v in c2.items(): combined_coefs[k] = combined_coefs.get(k, Fraction(0)) + lam2 * v
            combined_bound = lam1 * b1 + lam2 * b2
            combined_strict = s1 or s2
            if not combined_coefs:
                if combined_strict and combined_bound >= 0: return True
                if not combined_strict and combined_bound > 0: return True
    return False

Step 3: Run, pass, commit

pytest tests/test_tactics/test_arithmetic.py -v
git add logos/tactics/arithmetic.py tests/test_tactics/test_arithmetic.py
git commit -m "feat: linarith tactic (simplified Farkas combination)"

Task 11: Tactic Combinators

Files:

Create: logos/tactics/combinators.py
Test: tests/test_tactics/test_combinators.py

Interfaces:

Produces: then(*tactics), first(*tactics), try_(tactic), repeat(tactic), all_goals(tactic)
Step 1: Write tests

# tests/test_tactics/test_combinators.py
import pytest
from logos.expr import Var, Lit, And
from logos.goal import Goal
from logos.kernel import Refl, infer, Context
from logos.helpers import structural_eq
from logos.runner import run, TacticFailed
from logos.tactics.combinators import then, first, try_, repeat, all_goals
from logos.tactics.rewrite import refl
from logos.tactics.structural import split, assumption

def test_then_sequences(x):
    from logos.tactics.structural import intro
    goal = Goal({}, (x > Lit(0)) >> (x > Lit(0)))
    proof = run(goal, [then(intro("h"), assumption())])
    ctx = Context({}, {})
    assert structural_eq(infer(proof, ctx), (x > Lit(0)) >> (x > Lit(0)))

def test_first_succeeds_on_first(x):
    from logos.runner import TacticFailed as TF
    goal = Goal({}, x == x)
    proof = run(goal, [first(refl(), assumption())])   # refl() succeeds first

def test_first_falls_through(x):
    hyp = x > Lit(0)
    goal = Goal({"h": hyp}, hyp)
    # refl() fails, assumption() succeeds
    proof = run(goal, [first(refl(), assumption())])

def test_try_succeeds_silently_on_fail(x, y):
    hyp = x > Lit(0)
    goal = Goal({"h": hyp}, hyp)
    # try_(refl()) fails on x == x goal (wait, no — we need x == x for refl)
    # try_(failing_tactic) should not raise; goal remains open
    # So chain with assumption():
    proof = run(goal, [try_(refl()), assumption()])

def test_all_goals_applies_to_each(x, y):
    goal = Goal({"hx": x == x, "hy": y == y}, (x == x) & (y == y))
    proof = run(goal, [split(), all_goals(assumption())])

Step 2: Implement combinators.py

# logos/tactics/combinators.py
from logos.goal import Goal
from logos.kernel import ProofTerm
from logos.runner import TacticFailed, TacticResult

def then(*tactics):
    """Apply tactics in sequence to the current goal (as a single compound tactic)."""
    def tactic(goal: Goal) -> TacticResult:
        from logos.runner import _Runner
        return _Runner(list(tactics)).run(goal)
    return tactic


def first(*tactics):
    """Try each tactic in order; succeed with the first that doesn't raise TacticFailed."""
    def tactic(goal: Goal) -> TacticResult:
        last_err = None
        for t in tactics:
            try:
                return t(goal)
            except TacticFailed as e:
                last_err = e
        raise TacticFailed(f"first: all tactics failed. Last: {last_err}")
    return tactic


def try_(tactic_fn):
    """Apply tactic_fn; if it fails, return a no-op (transforms goal to itself)."""
    def tactic(goal: Goal) -> TacticResult:
        try:
            return tactic_fn(goal)
        except TacticFailed:
            # Return identity: 1 subgoal (same goal), identity compose
            return [goal], lambda ps: ps[0]
    return tactic


def repeat(tactic_fn):
    """Apply tactic_fn until it fails; apply all successful steps."""
    def tactic(goal: Goal) -> TacticResult:
        steps = []
        current = goal
        while True:
            try:
                result = tactic_fn(current)
                if isinstance(result, ProofTerm):
                    if steps:
                        # Build composed result
                        pass  # handled by closure below
                    return result
                subgoals, compose = result
                if len(subgoals) != 1:
                    break  # can't repeat on multi-subgoal tactics
                steps.append(compose)
                current = subgoals[0]
            except TacticFailed:
                break

        if not steps:
            return [goal], lambda ps: ps[0]

        # Chain the compositions
        def compose_all(proofs: list[ProofTerm]) -> ProofTerm:
            result = proofs[0]
            for compose in reversed(steps):
                result = compose([result])
            return result

        return [current], compose_all
    return tactic


def all_goals(tactic_fn):
    """Apply tactic_fn to each open subgoal (for use after a splitting tactic)."""
    # This is a meta-tactic wrapper: when used in a by list after a splitter,
    # the runner will call the returned tactic once per subgoal.
    # For v0.1: all_goals is handled by the runner via _AllGoals sentinel.
    return _AllGoals(tactic_fn)


class _AllGoals:
    """Sentinel that tells the runner to apply tactic to all current subgoals."""
    def __init__(self, tactic_fn):
        self.tactic_fn = tactic_fn

    def __call__(self, goal: Goal) -> TacticResult:
        return self.tactic_fn(goal)

Note: all_goals in v0.1 works because the runner already applies each tactic to each subgoal in sequence. So all_goals(t) in a by list after a 2-subgoal split won't work as a single item — use [t(), t()] or two separate nested lists instead. The full all_goals implementation requires the runner to expand it; mark as v0.2. For now, all_goals is an alias for the tactic itself.

Step 3: Run, fix, commit

pytest tests/test_tactics/test_combinators.py -v
git add logos/tactics/combinators.py tests/test_tactics/test_combinators.py
git commit -m "feat: tactic combinators (then, first, try_, repeat)"

Task 12: `@logos.define` and `logos.extern`

Files:

Create: logos/define.py
Test: tests/test_define.py

Interfaces:

Produces: define decorator — takes a function with Var params returning Expr; registers definition axiom; returns dual-mode callable
Produces: cases(*branches: tuple[Expr, Expr]) -> Expr — CaseExpr factory
Produces: extern(name, arg_types, ret_type) -> callable — registers symbol + returns App builder
Produces: get_definition(name: str) -> tuple[list[Var], Expr] — used by unfold tactic
Step 1: Write tests

# tests/test_define.py
import pytest
from logos.expr import Var, Lit, Add, App
from logos.helpers import structural_eq
from logos.registry import clear_axioms, get_all_axioms
from logos.define import define, extern, get_definition

def test_define_creates_axiom():
    clear_axioms()

    @define
    def double(x: Var) -> "Expr":
        return x + x

    axioms = get_all_axioms()
    assert "double" in axioms

def test_define_python_mode():
    @define
    def triple(x: Var) -> "Expr":
        return x + x + x

    # With a real Python int, evaluates normally
    assert triple(5) == 15

def test_define_symbolic_mode(x):
    @define
    def double2(x: Var) -> "Expr":
        return x + x

    result = double2(x)
    assert isinstance(result, App)
    assert result.func_name == "double2"

def test_get_definition_returns_body(x):
    @define
    def quad(x: Var) -> "Expr":
        return x * Lit(4)

    params, body = get_definition("quad")
    assert len(params) == 1
    assert structural_eq(body, params[0] * Lit(4))

def test_extern_creates_symbol():
    clear_axioms()
    my_fn = extern("black_box", [int], int)
    x = Var("x", int)
    result = my_fn(x)
    assert isinstance(result, App)
    assert result.func_name == "black_box"

Step 2: Implement define.py

# logos/define.py
from __future__ import annotations
import inspect
from typing import Callable, Any
from logos.expr import Expr, Var, App, Forall, Eq
from logos.registry import register_axiom

# Registry: function name → (params, body_expr)
_definitions: dict[str, tuple[list[Var], Expr]] = {}


def get_definition(name: str) -> tuple[list[Var], Expr]:
    if name not in _definitions:
        raise KeyError(f"No logos definition for '{name}'")
    return _definitions[name]


def define(fn: Callable) -> Callable:
    """
    Decorator. Runs fn's body in symbolic mode (params as Var objects),
    captures the expression tree, registers a definition axiom, and returns
    a dual-mode callable.
    """
    sig = inspect.signature(fn)
    params = [
        Var(name, param.annotation if param.annotation is not inspect.Parameter.empty else object)
        for name, param in sig.parameters.items()
    ]

    # Run body in symbolic mode
    body_expr: Expr = fn(*params)
    func_name = fn.__name__

    # Store definition
    _definitions[func_name] = (params, body_expr)

    # Register definition axiom: Forall(params..., Eq(App(name, params), body))
    app_node = App(func_name, list(params))
    eq_stmt = app_node == body_expr   # builds Eq node via __eq__
    axiom_stmt = Forall(*params, eq_stmt) if params else eq_stmt
    register_axiom(func_name, axiom_stmt)

    # Return dual-mode callable
    def wrapper(*args):
        # If any arg is an Expr, return symbolic App
        if any(isinstance(a, Expr) for a in args):
            return App(func_name, list(args))
        # Otherwise, call the original Python function
        return fn(*args)

    wrapper.__name__ = func_name
    wrapper.__logos_defined__ = True
    return wrapper


def extern(name: str, arg_types: list[type], ret_type: type) -> Callable:
    """Declare an external (uninterpreted) function symbol. Returns an App builder."""
    def caller(*args):
        return App(name, list(args))
    caller.__name__ = name
    return caller


def cases(*branches: tuple[Expr, Expr]) -> Expr:
    """Build a CaseExpr from (condition, value) pairs."""
    from logos.expr import CaseExpr
    return CaseExpr(list(branches))


def if_(condition: Expr, then_val: Expr, else_val: Expr) -> Expr:
    """Ternary if expression."""
    return cases((condition, then_val), (~condition, else_val))

Step 3: Run, pass, commit

pytest tests/test_define.py -v
git add logos/define.py tests/test_define.py
git commit -m "feat: @logos.define and logos.extern"

Task 13: `logos.theorem` + Builtins

Files:

Create: logos/theorem.py
Create: logos/builtins.py
Test: tests/test_integration.py (first batch)

Interfaces:

Produces: theorem(name: str, statement: Expr, proof: list) -> ProofTerm — validates at call time; registers as axiom on success; raises LogosProofError on failure
Produces: prove(statement: Expr, proof: list) -> ProofTerm — unnamed version (no axiom registration)
Produces: logos.builtins auto-loaded ring axioms
Step 1: Write theorem tests

# tests/test_integration.py
import pytest
from logos.expr import Var, Lit, Forall
from logos.registry import clear_axioms
from logos.theorem import theorem, prove, LogosProofError
from logos.tactics.arithmetic import ring, linarith
from logos.tactics.structural import intro, assumption, split
from logos.tactics.combinators import then

def setup_function():
    clear_axioms()
    import logos.builtins  # reload builtins

def test_prove_add_comm(x, y):
    stmt = Forall(x, y, x + y == y + x)
    proof = prove(stmt, [intro("x", "y"), ring()])
    assert proof is not None

def test_theorem_registers_as_axiom(x, y):
    from logos.registry import get_all_axioms
    stmt = Forall(x, y, x + y == y + x)
    theorem("add_comm_test", stmt, [intro("x", "y"), ring()])
    assert "add_comm_test" in get_all_axioms()

def test_theorem_raises_on_invalid_proof(x, y):
    stmt = Forall(x, y, x + y == x - y)  # false
    with pytest.raises(LogosProofError):
        theorem("bogus", stmt, [intro("x", "y"), ring()])

def test_prove_linarith(x):
    stmt = Forall(x, (x > Lit(0)) >> (x + Lit(1) > Lit(0)))
    proof = prove(stmt, [
        intro("x", "h"),
        linarith(),
    ])
    assert proof is not None

Step 2: Implement theorem.py

# logos/theorem.py
from logos.expr import Expr
from logos.goal import Goal
from logos.runner import run, TacticFailed
from logos.kernel import check, KernelError
from logos.registry import register_axiom

class LogosProofError(Exception):
    pass


def prove(statement: Expr, proof: list) -> object:
    """Validate `proof` for `statement`. Returns the proof term or raises LogosProofError."""
    goal = Goal({}, statement)
    try:
        term = run(goal, proof)
    except TacticFailed as e:
        raise LogosProofError(f"Tactic failed: {e}") from e
    try:
        check(term, statement, goal.make_context())
    except KernelError as e:
        raise LogosProofError(f"Kernel rejected proof: {e}") from e
    return term


def theorem(name: str, statement: Expr, proof: list) -> object:
    """Prove and register `statement` as a named axiom. Raises LogosProofError on failure."""
    term = prove(statement, proof)
    register_axiom(name, statement)
    return term

Step 3: Implement builtins.py

# logos/builtins.py
"""
Core arithmetic axioms loaded at import time.
These are AXIOMS — assumed true, not proved.
They encode standard ring laws for Python ints/floats.
"""
from logos.expr import Var, Lit, Forall
from logos.registry import register_axiom, get_all_axioms

_x = Var("__x", int)
_y = Var("__y", int)
_z = Var("__z", int)

_BUILTINS = {
    "int_add_comm":    Forall(_x, _y, _x + _y == _y + _x),
    "int_add_assoc":   Forall(_x, _y, _z, (_x + _y) + _z == _x + (_y + _z)),
    "int_mul_comm":    Forall(_x, _y, _x * _y == _y * _x),
    "int_mul_assoc":   Forall(_x, _y, _z, (_x * _y) * _z == _x * (_y * _z)),
    "int_distrib":     Forall(_x, _y, _z, _x * (_y + _z) == _x * _y + _x * _z),
    "int_add_zero":    Forall(_x, _x + Lit(0) == _x),
    "int_mul_one":     Forall(_x, _x * Lit(1) == _x),
    "int_mul_zero":    Forall(_x, _x * Lit(0) == Lit(0)),
    "int_sub_def":     Forall(_x, _y, _x - _y == _x + (-_y)),
    "int_neg_neg":     Forall(_x, -(-_x) == _x),
}

_loaded = False

def _load():
    global _loaded
    if _loaded:
        return
    existing = get_all_axioms()
    for name, stmt in _BUILTINS.items():
        if name not in existing:
            register_axiom(name, stmt)
    _loaded = True

_load()

Step 4: Run integration tests

pytest tests/test_integration.py -v

Fix any issues (likely: kernel check being too strict, or ring tactic not seeing builtins — it doesn't need to, it works purely on normalization).

Step 5: Commit

git add logos/theorem.py logos/builtins.py tests/test_integration.py
git commit -m "feat: logos.theorem, prove, and builtin ring axioms"

Task 14: Public API + `logos.tactics` exports

Files:

Modify: logos/__init__.py
Modify: logos/tactics/__init__.py
Test: tests/test_integration.py (second batch — end-to-end proof scenarios)

Interfaces:

Produces: top-level imports from logos import define, extern, theorem, prove, axiom, var, vars, forall, exists, Forall, Exists, Var
Produces: logos.tactics.ring, logos.tactics.linarith, logos.tactics.intro, etc.
Step 1: Write end-to-end integration tests

# append to tests/test_integration.py
import logos
import logos.tactics as t
from logos.registry import clear_axioms

def test_full_double_proof():
    clear_axioms()
    import logos.builtins

    x = logos.var("x", int)

    @logos.define
    def double(v: Var) -> "Expr":
        return v + v

    logos.theorem(
        "double_eq_2x",
        logos.forall(int, lambda v: double(v) == logos.lit(2) * v),
        [t.intro("v"), t.unfold("double"), t.ring()],
    )

def test_full_abs_nonneg():
    clear_axioms()
    import logos.builtins
    x = logos.var("x", int)

    logos.theorem(
        "zero_plus_zero",
        logos.forall(int, lambda v: v + logos.lit(0) == v),
        [t.intro("v"), t.ring()],
    )

Step 2: Implement logos/__init__.py

# logos/__init__.py
from logos.expr import Var, Lit, Forall, Exists, Expr
from logos.define import define, extern, cases, if_
from logos.theorem import theorem, prove, LogosProofError
from logos.registry import register_axiom as axiom
from logos import tactics
import logos.builtins  # auto-load on import


def var(name: str, type_: type) -> Var:
    return Var(name, type_)


def vars(names: str, type_: type) -> tuple[Var, ...]:
    return tuple(Var(n, type_) for n in names.split())


def lit(value) -> Lit:
    return Lit(value)


def forall(type_: type, *rest) -> Expr:
    """logos.forall(int, int, lambda x, y: x + y == y + x) — lambda form."""
    import inspect
    if callable(rest[-1]) and not isinstance(rest[-1], Expr):
        fn = rest[-1]
        types = (type_,) + rest[:-1]
        param_names = list(inspect.signature(fn).parameters.keys())
        vs = [Var(n, t) for n, t in zip(param_names, types)]
        body = fn(*vs)
        return Forall(*vs, body)
    raise TypeError("logos.forall: last argument must be a lambda")


def exists(type_: type, fn) -> Expr:
    import inspect
    param_names = list(inspect.signature(fn).parameters.keys())
    v = Var(param_names[0], type_)
    body = fn(v)
    return Exists(v, body)

Step 3: Implement logos/tactics/__init__.py

# logos/tactics/__init__.py
from logos.tactics.structural import (
    intro, assumption, exact, apply, split, left, right, witness, contradiction,
)
from logos.tactics.rewrite import (
    unfold, refl, rewrite, rewrite_rev, eval_, norm_num,
)
from logos.tactics.arithmetic import ring, linarith, decide
from logos.tactics.combinators import then, first, try_, repeat

Step 4: Run all tests

pytest tests/ -v

Expected: all green.

Step 5: Commit

git add logos/__init__.py logos/tactics/__init__.py tests/test_integration.py
git commit -m "feat: public API and tactics exports"

Task 15: Package, Docs, Final Polish

Files:

Modify: pyproject.toml (finalize metadata)
Modify: README.md (quick-start example)
Create: CHANGELOG.md

Interfaces: N/A — polish only.

Step 1: Run full test suite with coverage

pytest tests/ --cov=logos --cov-report=term-missing -v

Target: ≥80% coverage on kernel.py, runner.py, expr.py.

Step 2: Add quick-start to README.md

## Quick Start

```python
import logos
import logos.tactics as t
from logos.expr import Var

x, y = logos.vars("x y", int)

# Prove commutativity of addition
logos.theorem(
    "add_comm",
    logos.forall(int, int, lambda x, y: x + y == y + x),
    [t.intro("x", "y"), t.ring()],
)

# Define a function and prove a property
@logos.define
def double(x: Var) -> "Expr":
    return x + x

logos.theorem(
    "double_is_2x",
    logos.forall(int, lambda x: double(x) == logos.lit(2) * x),
    [t.intro("x"), t.unfold("double"), t.ring()],
)

- [ ] **Step 3: Write CHANGELOG.md**

```markdown
# Changelog

## [0.1.0] - 2026-06-17

### Features
- Trusted proof kernel with 14 inference rules
- Expression language with full operator overloading (`+`, `-`, `*`, `//`, `%`, `**`, `==`, `!=`, `<`, `<=`, `>`, `>=`, `&`, `|`, `~`, `>>`)
- `@logos.define` — symbolic function definitions with auto-generated axioms
- `logos.theorem` / `logos.prove` — proof validation at definition time
- `logos.extern` — axiom declarations for external functions
- Bundled tactics: `ring`, `linarith`, `decide`, `intro`, `assumption`, `exact`, `apply`, `split`, `left`, `right`, `witness`, `unfold`, `refl`, `rewrite`, `eval_`, `norm_num`
- Tactic combinators: `then`, `first`, `try_`, `repeat`
- Built-in ring axioms for integer arithmetic

Step 4: Final commit and push

git add README.md CHANGELOG.md pyproject.toml
git commit -m "chore(release): v0.1.0"
git push origin main

Self-Review

Spec coverage check:

Spec requirement	Covered by task
Trusted kernel (~200 lines)	Task 4
Expression language + operator overloading	Task 2
Auto-lifting of Python literals	Task 2
`__bool__` guard on Expr	Task 2
structural_eq + substitute	Task 3
Proof terms (Refl, Symm, Trans, Subst, ...)	Task 4
Axiom registry	Task 5
Goal dataclass + Context	Task 5
Tactic runner + TacticFailed	Task 6
Structural tactics (intro, assumption, ...)	Task 7
Rewrite tactics (unfold, refl, rewrite, ...)	Task 8
`ring` (polynomial normalization)	Task 9
`linarith` (Farkas combination)	Task 10
Tactic combinators (then, first, try_, ...)	Task 11
`@logos.define` + dual mode	Task 12
`logos.extern`	Task 12
`logos.theorem` / `logos.prove`	Task 13
Built-in ring axioms	Task 13
Public API (`logos.var`, `logos.forall`, ...)	Task 14
`logos.tactics.*` exports	Task 14

Out of scope confirmed: omega, collection types, proof serialization, mypy plugin, LLM tactic, induction, all_goals (full), focus.

Type consistency check: ProofTerm used consistently; TacticResult = ProofTerm | tuple[list[Goal], Callable] defined in runner and referenced by tactics correctly. structural_eq from logos.helpers referenced consistently throughout.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Logos v0.1 Implementation Plan

Global Constraints

File Map

Task 1: Project Scaffold

Task 2: Expression Language

Task 3: Structural Equality + Substitution

Task 4: Proof Terms + Kernel

Task 5: Axiom Registry + Goal

Task 6: Tactic Runner

Task 7: Structural Tactics

Task 8: Rewrite Tactics

Task 9: Arithmetic Tactics — Ring

Task 10: Linarith Tactic

Task 11: Tactic Combinators

Task 12: `@logos.define` and `logos.extern`

Task 13: `logos.theorem` + Builtins

Task 14: Public API + `logos.tactics` exports

Task 15: Package, Docs, Final Polish

Self-Review

Uh oh!

FilesExpand file tree

2026-06-17-logos-v0.1.md

Latest commit

History

2026-06-17-logos-v0.1.md

File metadata and controls

Logos v0.1 Implementation Plan

Global Constraints

File Map

Task 1: Project Scaffold

Task 2: Expression Language

Task 3: Structural Equality + Substitution

Task 4: Proof Terms + Kernel

Task 5: Axiom Registry + Goal

Task 6: Tactic Runner

Task 7: Structural Tactics

Task 8: Rewrite Tactics

Task 9: Arithmetic Tactics — Ring

Task 10: Linarith Tactic

Task 11: Tactic Combinators

Task 12: @logos.define and logos.extern

Task 13: logos.theorem + Builtins

Task 14: Public API + logos.tactics exports

Task 15: Package, Docs, Final Polish

Self-Review

Task 12: `@logos.define` and `logos.extern`

Task 13: `logos.theorem` + Builtins

Task 14: Public API + `logos.tactics` exports