Homotopy Tactics

A tactic language for building proofs interactively — including homotopy-native tactics that exist nowhere else.

What Are Tactics?

A tactic is a function that transforms a proof goal into simpler subgoals. Instead of writing proof terms by hand (which can be enormous and inscrutable), you describe a strategy for finding the proof, and the tactic engine does the rest.

If proof terms are the assembly language of verification, tactics are the high-level programming language. You say what to do ("split into cases", "apply induction", "rewrite using this equality"), and the engine figures out how to build the proof term.

Analogy: Tactics are to proof terms what Python is to machine code. You write apply(lemma) and the engine generates the hundreds of proof constructors needed to complete the step.

The Tactic Monad

Internally, each tactic is a function:

Tactic = Callable[[TacticState], tuple[ProofTerm, TacticState]]

# TacticState contains:
#   - goals:    list of remaining proof goals
#   - context:  current hypotheses (names → types)
#   - env:      global definitions, imported lemmas
#   - fuel:     recursion budget (for termination)

A tactic takes the current state (a list of goals with a proof context) and returns a proof term that solves the current goal, plus a new state with the remaining goals. Tactics compose monadically:

# Sequential composition: do t1, then t2 on the remaining goals
def then(t1: Tactic, t2: Tactic) -> Tactic:
    def composed(state: TacticState) -> (ProofTerm, TacticState):
        proof1, state1 = t1(state)
        proof2, state2 = t2(state1)
        return combine(proof1, proof2), state2
    return composed

Basic Tactics

Deppy provides the standard set of tactics found in any proof assistant, adapted for Python verification:

exact(term) — Provide a Proof Directly

The simplest tactic: you supply the proof term. The engine checks that it has the right type.

# Goal: 42 == 42
# Tactic: just provide the proof
> exact(Refl(42))
# Goal solved! ✅

intro(name?) — Introduce a Variable

When the goal is a universally quantified statement ∀ x:A. P(x), intro moves x into the context and changes the goal to P(x).

# Goal: ∀ x:int. x + 0 = x
> intro("x")
# Context: x : int
# Goal: x + 0 = x

apply(lemma) — Apply a Known Lemma

If you have a lemma L : A → B and the goal is B, apply(L) changes the goal to A.

# Known lemma: add_zero_right : ∀ x:int. x + 0 = x
# Goal: 5 + 0 = 5
> apply(add_zero_right)
# Goal solved! ✅ (auto-instantiates x := 5)

rewrite(path) — Rewrite Using a Path

Given a path p : a = b, rewrite(p) replaces occurrences of a with b in the current goal.

# Goal: (x + 0) * 2 = x * 2
# We have: p : x + 0 = x  (from add_zero_right)
> rewrite(p)
# Goal: x * 2 = x * 2
> exact(Refl(x * 2))
# Goal solved! ✅

split() — Case Split

Splits the current goal into multiple subgoals based on the structure of the input. This generates a Čech cover internally.

# Goal: ∀ x:int. abs(x) >= 0
> split()
# Subgoal 1: x >= 0 → abs(x) >= 0
# Subgoal 2: x < 0 → abs(x) >= 0

induction(var) — Structural Induction

Performs structural induction on a variable. For lists, this generates a base case (empty list) and an inductive step (cons case).

# Goal: ∀ xs:list[int]. len(reverse(xs)) = len(xs)
> induction("xs")
# Subgoal 1 (base):      len(reverse([])) = len([])
# Subgoal 2 (inductive): ∀ x, xs'.
#   len(reverse(xs')) = len(xs')  →  (IH)
#   len(reverse(x :: xs')) = len(x :: xs')

Homotopy-Specific Tactics

These tactics are unique to Deppy. No other verification tool has them because no other tool is built on homotopy type theory.

transport(path) — Carry Proof Along Path

The tactic version of the transport operation. Given a path p : a = b and a goal P(b), replaces the goal with P(a).

# Goal: Sorted(merge_sort(xs))
# We have: p : insertion_sort(xs) = merge_sort(xs)
# We have: proof_isort : Sorted(insertion_sort(xs))
> transport(p)
# Goal: Sorted(insertion_sort(xs))
# (The goal has been "transported back" along p)
> exact(proof_isort)
# Goal solved! ✅

path_induction() — J-Elimination

When the goal involves an arbitrary path p : a = b, path_induction() reduces it to the case where p = refl(a) and b = a.

# Goal: ∀ a b:A. ∀ p:(a = b). Sym(Sym(p)) = p
> intro("a"); intro("b"); intro("p")
# Goal: Sym(Sym(p)) = p
> path_induction()
# Now b = a and p = refl(a)
# Goal: Sym(Sym(refl(a))) = refl(a)
# Sym(refl(a)) = refl(a), so Sym(Sym(refl(a))) = Sym(refl(a)) = refl(a)
> exact(Refl(Refl(a)))
# Goal solved! ✅

cech_decompose(cover) — Čech Strategy

Automatically decomposes the current goal using a Čech cover. Generates one subgoal per patch plus overlap consistency goals.

# Goal: ∀ x:int. classify(x) ∈ {"negative", "zero", "positive"}
> cech_decompose(["x < 0", "x == 0", "x > 0"])
# Subgoal 1: x < 0 → classify(x) ∈ {"negative", "zero", "positive"}
# Subgoal 2: x == 0 → classify(x) ∈ {"negative", "zero", "positive"}
# Subgoal 3: x > 0 → classify(x) ∈ {"negative", "zero", "positive"}
# (No overlaps → no gluing subgoals)

fiber_induction(fibration) — Induction on Fibers

When the goal involves a value from a fibration (e.g., any subclass of an ABC), this tactic generates one subgoal per fiber.

# Goal: ∀ c:Collection. after add(x), contains(x) is True
> fiber_induction(Collection)
# Subgoal 1: c:ListCollection → after add(x), contains(x) is True
# Subgoal 2: c:SetCollection → after add(x), contains(x) is True
# Subgoal 3: c:DictCollection → after add(x), contains(x) is True
# Subgoal 4: c:DequeCollection → after add(x), contains(x) is True
# Subgoal 5: c:SortedCollection → after add(x), contains(x) is True

univalence() — Apply Univalence Axiom

When the goal requires showing two types are equal, univalence() reduces it to showing they are equivalent (have a structure-preserving bijection).

# Goal: list[int] =_Type tuple[int]  (as Sequences)
> univalence()
# Goal: list[int] ≃ tuple[int]  (as Sequences)
# i.e., construct a bijection preserving Sequence operations
> exact(Equiv(
    forward=tuple,          # list → tuple
    backward=list,          # tuple → list
    roundtrip_lr=...,       # tuple(list(t)) = t
    roundtrip_rl=...,       # list(tuple(l)) = l
  ))
# Goal solved! ✅

funext() — Apply Function Extensionality

When the goal is f = g for two functions, funext() reduces it to showing f(x) = g(x) for an arbitrary x.

# Goal: (λ x. x + x) = (λ x. 2 * x)
> funext()
# Intro'd: x : int
# Goal: x + x = 2 * x
> apply(add_self_is_double)
# Goal solved! ✅

duck_path(protocol) — Construct Duck Typing Path

Constructs a path between two objects based on their conformance to a shared protocol. This is Deppy's most Python-specific tactic.

# Goal: PathType(Iterable[int], my_list, my_tuple)
> duck_path(Iterable[int])
# Checks that both my_list and my_tuple implement __iter__
# and yield the same sequence of values.
# Auto-generates the path witness.
# Goal solved! ✅

Tactic Combinators

Tactics compose via combinators — building complex proof strategies from simple pieces:

then(t1, t2) — Sequential Composition

# Do t1 on the current goal, then t2 on whatever remains
strategy = then(
    intro("x"),      # introduce the variable
    apply(lemma)      # then apply a lemma
)

# Chains of 'then' are common — use the >> operator
strategy = intro("x") >> split() >> apply(lemma)

or_else(t1, t2) — Fallback

# Try t1; if it fails, try t2
strategy = or_else(
    apply(specific_lemma),   # try the specific lemma first
    auto()                    # fall back to auto-search
)

# Use the | operator
strategy = apply(lemma1) | apply(lemma2) | auto()

repeat(t) — Apply Until Fixpoint

# Keep applying t until it fails (no more goals it can solve)
strategy = repeat(intro())
# Introduces all universally quantified variables

# Useful for simplification loops:
simplify = repeat(
    rewrite(add_zero) | rewrite(mul_one) | rewrite(mul_zero)
)

all_goals(t) — Apply to Every Open Goal

# After split() creates N subgoals, solve all with same tactic
strategy = split() >> all_goals(auto())

# Or target a specific goal
strategy = split() >> focus(1, apply(lemma_a)) >> focus(2, apply(lemma_b))

Full Combinator Reference

Interactive Tactic Mode

Deppy provides an interactive REPL for developing proofs step-by-step. This is invaluable when automatic verification fails and you need to guide the engine.

$ deppy tactic myfile.py::my_function

Deppy Tactic Mode v0.1
Function: my_function
Guarantee: "returns a sorted list with no duplicates"
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━

Goal 1 of 1:
  ∀ xs:list[int].
    sorted(unique_sorted(xs)) = unique_sorted(xs)
    ∧ len(unique_sorted(xs)) = len(set(xs))

> intro("xs")
  Context: xs : list[int]
  Goal: sorted(unique_sorted(xs)) = unique_sorted(xs)
         ∧ len(unique_sorted(xs)) = len(set(xs))

> split()
  Goal 1 of 2: sorted(unique_sorted(xs)) = unique_sorted(xs)
  Goal 2 of 2: len(unique_sorted(xs)) = len(set(xs))

> focus(1)
  Goal 1: sorted(unique_sorted(xs)) = unique_sorted(xs)
  Hint: unique_sorted returns sorted(list(set(xs)))

> unfold("unique_sorted")
  Goal 1: sorted(sorted(list(set(xs)))) = sorted(list(set(xs)))

> rewrite(sorted_idempotent)
  Goal 1 solved! ✅

> focus(2)
  Goal 2: len(unique_sorted(xs)) = len(set(xs))

> unfold("unique_sorted")
  Goal 2: len(sorted(list(set(xs)))) = len(set(xs))

> rewrite(sorted_preserves_length)
  Goal 2: len(list(set(xs))) = len(set(xs))

> rewrite(list_preserves_length)
  Goal 2: len(set(xs)) = len(set(xs))

> exact(Refl(len(set(xs))))
  Goal 2 solved! ✅

All goals solved! Proof complete. ✅
Proof term saved to myfile.deppy.proof

Full Example: List Reverse Is Involutive

Let's prove that reversing a list twice gives back the original list: reverse(reverse(xs)) = xs for all lists xs.

@guarantee("reverse(reverse(xs)) == xs")
def reverse_involutive(xs: list[int]) -> bool:
    return list(reversed(list(reversed(xs)))) == xs

As a Tactic Script

# The full proof as a tactic script (non-interactive)
proof = (
    intro("xs")
    >> induction("xs")
    >> focus(1, exact(Refl([])))
    >> focus(2,
        rewrite(reverse_cons)
        >> rewrite(reverse_append)
        >> rewrite(reverse_singleton)
        >> rewrite(IH)
        >> rewrite(singleton_append)
        >> exact(Refl(Cons(x, xs_)))
    )
)

The auto() Tactic

auto() is Deppy's most powerful tactic. It searches for a proof by trying a battery of strategies:

def auto(depth: int = 5) -> Tactic:
    """Try everything: Z3, simplification, lemma DB, path search."""
    return or_else(
        z3_discharge(),             # try Z3 directly
        or_else(
            apply_from_db(),         # try known lemmas
            or_else(
                simplify() >> auto(depth - 1),  # simplify, recurse
                or_else(
                    split() >> all_goals(auto(depth - 1)),  # case split
                    or_else(
                        transport_search(),  # look for transportable proofs
                        oracle_query()       # ask the LLM oracle
                    )
                )
            )
        )
    )

The search order matters. auto() tries the cheapest and most trustworthy strategies first (Z3, known lemmas), then moves to more expensive ones (case splitting, transport search), and finally falls back to the LLM oracle as a last resort.

Comparison with F* Meta Tactics

F* has a powerful tactic system called Meta-F*. Deppy's tactics are inspired by Meta-F* but differ in key ways:

The six homotopy-specific tactics (transport, path_induction, cech_decompose, fiber_induction, univalence, duck_path) have no analogue in any other verification tool. They are a direct consequence of building the type theory on homotopy-theoretic foundations.

Writing Custom Tactics

Because Deppy tactics are just Python functions, you can write your own:

from deppy.tactics import Tactic, TacticState, intro, apply, rewrite

# A custom tactic for arithmetic goals
def arith() -> Tactic:
    """Solve arithmetic goals by normalization + Z3."""
    return (
        repeat(
            rewrite(add_zero)
            | rewrite(mul_one)
            | rewrite(mul_zero)
            | rewrite(add_comm)
            | rewrite(mul_comm)
        )
        >> z3_discharge()
    )

# A domain-specific tactic for financial code
def money_tactic() -> Tactic:
    """Handle Decimal arithmetic with rounding."""
    return (
        repeat(rewrite(decimal_add_assoc))
        >> rewrite(decimal_round_monotone)
        >> z3_discharge()
    )

# Use in a guarantee
@guarantee("total = sum of line items", tactic=money_tactic())
def compute_total(items: list[LineItem]) -> Decimal:
    return sum(item.price * item.qty for item in items)

Quick Reference

Standard Tactics

Homotopy Tactics (unique to Deppy)