Hoare/Effects.lean

View source on GitHub

Effect

An effect on type b: a function assigning a natural number value to each element, bounded above. When the bound is 1, this is a Boolean predicate (true/false). This approximates the [0,1]-valued effects of Cho-Jacobs using natural numbers.

structure Effect (β : Type) where
  eval : β → Nat
  bound : Nat
  bounded : ∀ b : β, eval b ≤ bound

booleanEffect

Embed a decidable Boolean contract (b → Bool) as a {0,1}-valued effect. True maps to 1, false maps to 0, bound is 1.

effectPreserving

A kernel preserves an effect if every reachable output has effect value equal to the bound (fully satisfied). For Boolean effects this means eval b = 1 for all outputs — exactly ContractPreserving.

boolean_effect_bridge

The key equivalence: for Boolean effects, effectPreserving is exactly ContractPreserving. Boolean contracts are the {0,1} case of effect algebra predicates.

theorem boolean_effect_bridge [Monad M] [Support M]
    {f : Kernel M α β} {Q : β → Bool}
    : effectPreserving f (booleanEffect Q) ↔
      ContractPreserving f (fun b => Q b = true)

Effect.top / Effect.bot / Effect.and

Basic effect algebra operations: top (always 1), bottom (always 0), conjunction (min of two effects). These are the building blocks, though the full Cho-Jacobs effect algebra (partial addition, orthocomplement) is not formalized here.

effectPreserving_comp

Closure under precomposition: if g preserves an effect, then f;g preserves it for any f. Only the last kernel's effect matters.

Connections

• Hoare/Core.lean — imported; effects are checked via the same support quantification as triples
• Contracts.lean — ContractPreserving is the bridge target
• Hoare/Graded.lean — grades are a different quantitative extension of triples