Rewrite Tactics

Rewrite tactics transform the goal by unfolding definitions, applying equational lemmas, or evaluating sub-expressions.

import logos
import logos.tactics as t

refl()

Closes a == a goals — when both sides are structurally identical.

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

logos.check(logos.prove(logos.forall(int, lambda x: x == x),
            [t.intro("x"), t.refl()]))
print("x = x ✓")

# Also works on expressions
logos.check(logos.prove(
    logos.forall(int, int, lambda x, y: x + y == x + y),
    [t.intro("x", "y"), t.refl()],
))
print("x + y = x + y ✓")

x = x ✓
x + y = x + y ✓

refl fails when the sides differ — even if they’re equivalent:

from logos.theorem import LogosProofError

try:
    logos.check(logos.prove(logos.forall(int, int, lambda x, y: x + y == y + x),
                [t.intro("x", "y"), t.refl()]))
except LogosProofError:
    print("refl cannot prove x + y = y + x (use ring instead)")

refl cannot prove x + y = y + x (use ring instead)

unfold(*refs)

Replaces function applications with their definition bodies. Pass Function objects (from @logos.define).

@logos.define
def triple(x: int):
    return x + x + x

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

# After unfold, triple(x) becomes x + x + x
@logos.theorem
def triple_is_3x(x: int):
    return triple(x) == logos.lit(3) * x

logos.check(triple_is_3x.proof(t.intro("x"), t.unfold(triple), t.ring()))
print("Proved: triple(x) = 3x")

# Unfold multiple at once
@logos.define
def quad(x: int):
    return triple(x) + x

@logos.theorem
def quad_is_4x(x: int):
    return quad(x) == logos.lit(4) * x

logos.check(quad_is_4x.proof(t.intro("x"), t.unfold(quad), t.unfold(triple), t.ring()))
print("Proved: quad(x) = 4x")

Proved: triple(x) = 3x
Proved: quad(x) = 4x

rewrite(ref) / rewrite_rev(ref)

Rewrites the goal using an Axiom or Theorem object. rewrite applies left-to-right; rewrite_rev applies right-to-left.

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

# Prove a useful lemma
@logos.theorem
def triple_def(x: int):
    return triple(x) == x + x + x

logos.check(triple_def.proof(t.intro("x"), t.unfold(triple), t.refl()))

# Use it to rewrite inside another goal
logos.check(logos.prove(
    logos.forall(int, lambda x: triple(x) + x == logos.lit(4) * x),
    [
        t.intro("x"),
        t.rewrite(triple_def),   # replaces triple(x) with x+x+x
        t.ring(),
    ],
))
print("Proved via rewrite")

Proved via rewrite

eval_()

Evaluates ground arithmetic sub-expressions (no variables) within the goal.

logos.check(logos.prove(
    logos.lit(2) + logos.lit(3) == logos.lit(5),
    [t.eval_()],
))
print("2 + 3 = 5 ✓ (via eval)")

logos.check(logos.prove(
    logos.lit(10) - logos.lit(4) == logos.lit(6),
    [t.eval_()],
))
print("10 - 4 = 6 ✓")

2 + 3 = 5 ✓ (via eval)
10 - 4 = 6 ✓

norm_num()

Normalizes numeric expressions and closes numeric ground goals. Similar to eval_ but more aggressive:

logos.check(logos.prove(logos.lit(6) == logos.lit(2) * logos.lit(3), [t.norm_num()]))
print("6 = 2 * 3 ✓")

logos.check(logos.prove(logos.lit(100) == logos.lit(10) ** logos.lit(2), [t.norm_num()]))
print("100 = 10² ✓")

6 = 2 * 3 ✓
100 = 10² ✓

Chaining Rewrites

Rewrite tactics can be chained to progressively transform a goal:

@logos.define
def square(x: int):
    return x * x

@logos.theorem
def sq_comm_example(x: int, y: int):
    return square(x) + square(y) == square(y) + square(x)

logos.check(sq_comm_example.proof(
    t.intro("x", "y"),
    t.unfold(square),   # square(x) → x*x, square(y) → y*y
    t.ring(),            # x*x + y*y = y*y + x*x (commutativity)
))
print("Proved: x² + y² = y² + x²")

Proved: x² + y² = y² + x²