PSDL: Python-syntax Tactics

A tactic language whose source is Python — every line maps to a kernel ProofTerm.

Why Another Tactic Language?

Most proof assistants ship their own tactic language: Coq has Ltac, Lean has its tactic mode, Isabelle has Isar. Deppy's twist is that its tactic language is just Python. Every PSDL proof body is parsed by Python's ast module and translated to a kernel ProofTerm — no separate grammar, no separate file format, full IDE support for free.

The translation is total: every Python statement maps to some kernel construct (often Structural(…) when the statement has no proof-theoretic content). The combination of ordinary expressions, function calls, control flow, and a small set of operator-overloading conventions gives PSDL the same expressive power as a hand-written tactic monad — while being syntactically indistinguishable from Python.

The simplest possible PSDL block

from deppy.proofs.psdl import compile_psdl
res = compile_psdl("qed()", foundations={})
print(res.term_repr, res.ok)
# Refl True

qed() is a closer that emits Refl — the reflexivity proof. It's how you say "the obligation is exactly the goal we already have." All eight closer functions emit Refl with different debug labels: qed, auto, done, omega, rfl_, decide, trivial, simp.

How a PSDL Block Compiles

compile_psdl(src, *, foundations=None, ctx=None) takes a Python source string whose top-level statements are PSDL tactics and returns a PSDLCompileResult:

from deppy.proofs.psdl import compile_psdl

res = compile_psdl("""
def add_comm(x, y):
    return x + y
""", foundations={})

print(res.proof_term)        # the kernel term
print(res.term_repr)         # a string view (Refl)
print(res.lean_tactic)       # Lean tactic source
print(res.errors)            # []
print(res.ok)                # True
print(res.final_epoch)       # heap epoch at end of block
print(res.effect_sequence)   # list of (line, kind, target)

The Cubical-Effect Mapping Table

Every Python construct maps to a specific kernel object. The table below is exhaustive for the constructs PSDL understands; the compiler emits Structural(…) for the rest.

Syntactic Sugar

PSDL adds a small set of conventions that make tactics read more naturally than direct kernel-term construction.

Postfix navigation on equalities

res = compile_psdl("""
eq.lhs
eq.rhs
eq.cong(f)
eq.symm
eq.trans(eq2)
""", foundations={})
print(res.ok)             # True
print(res.term_repr)      # Cong, Sym, Trans, …

The compiler produces:

• eq.lhs / eq.rhs → Structural('eq.lhs') / Structural('eq.rhs') (left/right component accessors).
• eq.cong(f) → Cong(f, AxiomInvocation(eq)).
• eq.symm → Sym(AxiomInvocation(eq)).
• eq.trans(eq2) → Trans(eq, eq2).

Operator overloading

res = compile_psdl("(p @ q)", foundations={})
print(res.term_repr)      # PathComp(…)

res = compile_psdl("~p", foundations={})
print(res.term_repr)      # Sym(…)

res = compile_psdl("p ** 3", foundations={})
print(res.term_repr)      # PathComp(…)  three-fold composition

Walrus binding

res = compile_psdl("(h := apply(F))",
    foundations={"F": {"statement": "foo"}})
print(res.term_repr)
# Cut(h, AxiomInvocation(F), Refl)

The walrus operator gives a name to the application of a foundation or lemma so subsequent steps can cite it.

Sequential >> composition

res = compile_psdl("apply(F) >> apply(G)",
    foundations={"F": {"statement": "foo"},
                 "G": {"statement": "bar"}})
print(res.term_repr)
# Cut(_chain_1, AxiomInvocation(F), AxiomInvocation(G))

Boolean ops as proof composition

res = compile_psdl("apply(P) or apply(Q)",
    foundations={"P": {"statement": "p"},
                 "Q": {"statement": "q"}})
print(res.term_repr)
# Cases(Var(name='_or_1'), 2 branches)

Closer functions

res = compile_psdl("""
qed()
auto()
rfl_()
""", foundations={})
print(res.term_repr)
# Cut(_psdl_step_1, Refl, Cut(_psdl_step_2, Refl, Refl))

Assert with goal label

res = compile_psdl("""
assert x == y, "qed"
assert x > 0, "omega"
assert P, "rfl"
""", foundations={})
print(res.ok)             # True

The string after the comma is the proof tactic to apply: one of "qed" / "omega" / "rfl" / "trivial" / "decide" / "simp" / "auto" / "done".

Context managers for goal scoping

res = compile_psdl("""
with goal("P(x)"):
    apply(F)
""", foundations={"F": {"statement": "foo"}})
print(res.term_repr)
# AxiomInvocation(F)

res = compile_psdl("""
with hypothesis(h, int):
    pass
""", foundations={})
print(res.term_repr)
# Cut(h, Assume(…), Structural('trivial'))

Comprehensions are induction

res = compile_psdl("[refl(x) for x in xs]", foundations={})
print(res.term_repr)
# ListInduction(x, nil=Refl, cons=Refl)

Quantifiers

res = compile_psdl("forall(x, int, x >= 0)", foundations={})
print(res.term_repr)
# Cut(x, Assume(…), Z3(x >= 0))

forall and exists pass their type as a SynType rather than stuffing the type into the refinement predicate (a soundness fix landed in the latest release).

Soundness Fixes Worth Knowing

A handful of constructs used to silently drop information; the current PSDL compiler handles them honestly. If you saw earlier docs claiming any of these worked differently, the new behaviour is correct.

• break / continue invalidate the surrounding ListInduction / NatInduction and register a PSDLError. The proof term still compiles, but res.ok is False.
• try / finally / else chains properly via nested Cuts — earlier versions dropped the finally and else blocks.
• Match-case guards wrap the body in Cut(Z3Proof(guard), …, body). Earlier versions dropped the guard entirely.
• raise Exc uses EffectWitness("exception:NAME", …) with correct semantics — earlier versions used a ConditionalEffectWitness with inverted polarity.
• Multi-handler try / except chains every handler plus the value witness via Cut; earlier versions only kept the last handler.
• P or Q compiles to Cases([("or_0", left), ("or_1", right)]); earlier versions dropped the right disjunct.
• while <cond>: extracts the induction variable from the condition's AST; earlier versions always hard-coded "n".
• kan_fill emits Patch(cls, method, impl, contract_proof); earlier versions emitted a generic Cut.

Runtime-Semantics Lint

PSDL also runs a lint pass over the source and registers a PSDLError for runtime-semantics traps that would otherwise let an unsound proof slip through:

res = compile_psdl("""
def f():
    x = 1 is 1
    return x
""", foundations={})
print(res.ok)            # False
print(res.errors[0].message)
# 'runtime-semantics lint: ``is``/``is not`` against a literal (int) — 
#  CPython interning quirk; use ``==`` for value equality'

The lint covers:

• Late closure binding (loop-variable capture).
• Mutable default arguments.
• Iterator exhaustion (zip / map / filter consumed twice).
• is / is not on literals.
• Truthiness checks on falsy literals.
• int / int using float division.
• Mutation of one alias when proof depends on another in the same group.

Citing Foundations & Lemmas

compile_psdl(src, foundations=…) takes a dict of named facts the proof is allowed to cite. Inside the source, apply(NAME) resolves NAME in foundations and emits an AxiomInvocation:

res = compile_psdl("apply(comm) >> apply(assoc)",
    foundations={
        "comm":  {"statement": "a + b == b + a"},
        "assoc": {"statement": "(a+b)+c == a+(b+c)"},
    })
print(res.term_repr)
# Cut(_chain_1, AxiomInvocation(comm), AxiomInvocation(assoc))

End-to-End: PSDL Proof in a Sidecar

In a .deppy file, the psdl_proof: block carries the same source text:

verify dist_nonneg:
  function: Point.distance
  property: "Point.distance(p, q) >= 0"
  via: "foundation Real_sqrt_nonneg"
  binders: { p: Point, q: Point }
  psdl_proof: |
    if isinstance(other, Point):
        inline(Point.distance, sqrt(sum_zip_sub_sq(self, other)))
        apply(Real_sqrt_nonneg)
        assert sum_zip_sub_sq(self, other) >= 0, "z3"
    else:
        raise NotImplementedError

The same source goes through the same compiler whether it comes from a sidecar file or a @psdl_proof("…") decorator on a Python method — see Decorator Form.

What's Next

Homotopy Tactics covers the broader tactic engine (the one running inside the kernel after PSDL has produced its term). The combination — PSDL on the outside, homotopy tactics on the inside — is what makes Deppy practical for large proof bodies.