Hoare/Core.lean

View source on GitHub

Triple

A Hoare triple {P} f {Q} means: for every input satisfying P, every possible output of f satisfies Q. The quantification is over the support — the same possibilistic (reachability-based) layer used throughout the framework. Think of it as a contract with a precondition.

def Triple [Monad M] [Support M]
    (P : α → Prop) (f : Kernel M α β) (Q : β → Prop) : Prop :=
  ∀ a : α, P a → ∀ b : β, Support.support (f a) b → Q b

# Hoare triple: {P} f {Q}
# "If input satisfies P, every possible output satisfies Q"

def triple_holds(P, f, Q, test_inputs):
    """Check {P} f {Q} over test inputs"""
    for x in test_inputs:
        if P(x):
            y = f(x)
            if not Q(y):
                return False, x, y
    return True, None, None

# {x > 0} double {y > 0}  -- should hold
P = lambda x: x > 0
Q = lambda y: y > 0
f = lambda x: x * 2

ok, _, _ = triple_holds(P, f, Q, range(-5, 10))
print(f"{{x > 0}} double {{y > 0}}: {ok}")

# {x > 0} negate {y > 0}  -- should FAIL
g = lambda x: -x
ok, cx, cy = triple_holds(P, g, Q, range(-5, 10))
print(f"{{x > 0}} negate {{y > 0}}: {ok}")
print(f"  counterexample: P({cx})=True, but Q({cy})=False")

triple_consequence

Rule of consequence: you can weaken the precondition (accept more inputs) and strengthen the postcondition (promise less about outputs). If the original triple holds, the weakened one does too.

triple_comp

Sequential composition (the COMP rule): if {P} f {R} and {R} g {Q}, then {P} f;g {Q}. Uses support_bind to decompose the composite's support into an intermediate value.

theorem triple_comp [Monad M] [LawfulMonad M] [Support M]
    {P : α → Prop} {R : β → Prop} {Q : γ → Prop}
    {f : Kernel M α β} {g : Kernel M β γ}
    (hf : Triple P f R) (hg : Triple R g Q)
    : Triple P (Kernel.comp f g) Q

# COMP rule: {P} f {R} and {R} g {Q}  =>  {P} f;g {Q}
# The intermediate predicate R bridges the two stages.

P = lambda x: x >= 0          # non-negative input
R = lambda y: y >= 0 and y <= 50  # intermediate: bounded
Q = lambda z: z % 2 == 0      # final output is even

f = lambda x: min(x, 50)      # clamp to [0,50]
g = lambda y: y * 2            # double

# Check each triple individually:
inputs = list(range(0, 100))
pf = all(R(f(x)) for x in inputs if P(x))
rg = all(Q(g(y)) for y in range(51) if R(y))
comp = all(Q(g(f(x))) for x in inputs if P(x))

print(f"{{P}} clamp {{R}}: {pf}")
print(f"{{R}} double {{Q}}: {rg}")
print(f"{{P}} clamp;double {{Q}}: {comp}  (by COMP)")

triple_skip

The skip rule: the identity kernel preserves any predicate. Uses support_pure to show the only possible output is the input itself.

triple_post_and

AND rule: if f preserves Q and R separately, it preserves both simultaneously.

triple_pre_or

OR rule: if the triple holds from precondition P1 and from P2, it holds from their disjunction.

Connections

• Handshake.lean — imported; triples are built on top of the contract/kernel infrastructure
• Hoare/WP.lean — weakest precondition transformer, equivalent to triples
• Hoare/Bridge.lean — connects triples to ContractPreserving
• Hoare/Comp.lean — chains the full pipeline through COMP
• Hoare/Graded.lean — adds cost bounds (grades) to triples