Structural Tactics

Structural tactics manipulate the shape of the goal — introducing variables, splitting conjunctions, pattern-matching on disjunctions.

import logos
import logos.tactics as t
from logos.goal import Goal
from logos.runner import run
from logos.kernel import infer
from logos.helpers import structural_eq

intro(*names)

Strips leading Forall and Implies from the goal, adding the introduced items to the context.

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

# Introduce universally quantified variables
logos.check(logos.prove(
    logos.forall(int, int, lambda x, y: x + y == y + x),
    [
        t.intro("x", "y"),   # strips Forall(x, Forall(y, ...)), adds x,y to context
        t.ring(),
    ],
))
print("Proved with intro")

# Introduce hypothesis from implication
logos.check(logos.prove(
    logos.forall(int, lambda x: (x > logos.lit(0)) >> (x > logos.lit(0))),
    [
        t.intro("x", "h"),   # x from Forall, h: x>0 from Implies
        t.assumption(),       # close with h
    ],
))
print("Proved implication with intro")

Proved with intro
Proved implication with intro

assumption()

Closes the goal if it appears verbatim in the context.

x = logos.var("x", int)
hyp = x > logos.lit(0)

goal = Goal({"h": hyp}, hyp)
proof = run(goal, [t.assumption()])
print("Closed by assumption:", type(proof).__name__)  # HypRef

Closed by assumption: HypRef

exact(term)

Closes the goal with an explicit proof term. For when you know exactly what kernel term to supply.

from logos.kernel import Refl

x = logos.var("x", int)
goal = Goal({}, x == x)
proof = run(goal, [t.exact(Refl(x))])
print("Closed by exact:", type(proof).__name__)  # Refl

Closed by exact: Refl

split()

For conjunction goals A & B — splits into two subgoals, one for A and one for B.

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

logos.check(logos.prove(
    logos.forall(int, int, lambda x, y:
        (x > logos.lit(0)) >> ((y > logos.lit(0)) >> ((x > logos.lit(0)) & (y > logos.lit(0))))
    ),
    [
        t.intro("x", "y", "hx", "hy"),
        t.split(),
        [t.assumption()],   # prove x > 0
        [t.assumption()],   # prove y > 0
    ],
))
print("Proved conjunction")

Proved conjunction

left(right_type) / right(left_type)

For disjunction goals A | B — choose which side to prove.

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

# Prove "x > 0 or x > 0" by proving the left side
logos.check(logos.prove(
    logos.forall(int, lambda x:
        (x > logos.lit(0)) >> ((x > logos.lit(0)) | (x > logos.lit(0)))
    ),
    [
        t.intro("x", "h"),
        t.left(x > logos.lit(0)),   # choose to prove left side; right_type = x > 0
        t.assumption(),
    ],
))
print("Proved disjunction via left")

Proved disjunction via left

witness(val)

For existential goals Exists(x, P(x)) — provide the witness value, reducing to P[x:=val].

logos.check(logos.prove(
    logos.exists(int, lambda x: x > logos.lit(5)),
    [
        t.witness(logos.lit(10)),   # instantiate x := 10
        t.decide(),                  # verify 10 > 5
    ],
))
print("Proved: ∃x > 5  (witness: 10)")

Proved: ∃x > 5  (witness: 10)

contradiction()

Closes the goal if the context contains both P and ~P for some proposition P.

from logos.expr import Not

x = logos.var("x", int)
p = x > logos.lit(0)

# Context has both h: x > 0 and hn: ~(x > 0) — contradiction!
goal = Goal({"h": p, "hn": Not(p)}, x == logos.lit(99))
proof = run(goal, [t.contradiction()])
print("Closed by contradiction:", type(proof).__name__)  # ExFalso

Closed by contradiction: ExFalso

apply(ref)

Applies an Axiom/Theorem object (or a local hypothesis string) whose statement matches the current goal.

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

# Declare and prove a theorem
@logos.theorem
def x_eq_x(x: int):
    return x == x

logos.check(x_eq_x.proof(t.intro("x"), t.refl()))

# Apply it inside another proof using the object
x_inst = logos.var("x", int)
goal = Goal({}, x_inst == x_inst)
proof = run(goal, [t.apply(x_eq_x)])
print("Applied theorem:", type(proof).__name__)

Applied theorem: ForallElim

You can also apply local hypotheses by name:

x = logos.var("x", int)
hyp = x > logos.lit(0)
goal = Goal({"h": hyp}, hyp)
proof = run(goal, [t.apply("h")])
print("Applied hypothesis:", type(proof).__name__)

Applied hypothesis: HypRef