Hoare/Bridge.lean

View source on GitHub

contract_is_triple

Contract preservation is exactly a Hoare triple with trivial precondition. ContractPreserving f Q is the same as {True} f {Q}. Both unfold to: for all inputs, all reachable outputs satisfy Q.

theorem contract_is_triple [Monad M] [Support M]
    {f : Kernel M α β} {Q : Contract β}
    : ContractPreserving f Q ↔ Triple (fun _ => True) f Q

# contract_is_triple: ContractPreserving f Q  <=>  {True} f {Q}
# A contract with no precondition IS a Hoare triple.

def contract_preserving(f, Q, inputs):
    """Check: for ALL inputs, every output satisfies Q"""
    return all(Q(f(x)) for x in inputs)

def triple(P, f, Q, inputs):
    """Check: for inputs where P holds, outputs satisfy Q"""
    return all(Q(f(x)) for x in inputs if P(x))

is_positive = lambda y: y > 0
always_true = lambda x: True
abs_fn = lambda x: abs(x) + 1

inputs = range(-10, 10)

cp = contract_preserving(abs_fn, is_positive, inputs)
tr = triple(always_true, abs_fn, is_positive, inputs)

print(f"ContractPreserving(abs+1, positive): {cp}")
print(f"Triple(True, abs+1, positive):       {tr}")
print(f"They're the same thing:              {cp == tr}")

handshake_enables_comp

Handshake-compatible stages compose. If f establishes the handshake's postcondition and g requires the handshake's precondition, sequential composition carries P to R. The handshake's compatibility lemma (post implies pre) bridges the gap via the rule of consequence.

theorem handshake_enables_comp [Monad M] [LawfulMonad M] [Support M]
    {P : α → Prop} {R : γ → Prop}
    {f : Kernel M α β} {k : Kernel M β γ}
    (h : Handshake β)
    (hf : Triple P f h.post) (hk : Triple h.pre k R)
    : Triple P (Kernel.comp f k) R

triple_counterexample

Nontriviality: not every kernel satisfies every triple. A specific bad kernel (mapping unit to false) fails the triple {True} badKernel {b = true}. This demonstrates the proof system has teeth — it can reject kernels.

theorem triple_counterexample :
    ¬ Triple (fun (_ : Unit) => True) badKernel (· = true)

Connections

• Hoare/Core.lean — imported; provides Triple and triple_comp
• Contracts.lean — ContractPreserving is the bridge target
• Handshake.lean — the Handshake structure that enables composition
• Hoare/Comp.lean — uses handshake_enables_comp to chain the full pipeline
• Hoare/Graded.lean — graded_contract_bridge lifts this to graded triples