RCompOk: the success-restricted Kleisli relation

RComp (Integrations/ParamTripleTransfer.lean) relates two computations in one monad by wp-refinement with a shared failure barrel. This module relates a computation c : M α in a monad whose Std.Do postcondition shape may carry exception components (a model that fails, for example on arithmetic overflow or an out-of-range index) to a computation c' : N α' in a monad of shape .pure (a total model, for example Id):

RCompOk Rα c c' := ∀ Q', (⊢ₛ wp⟦c'⟧ (⇓ a' => ⌜Q' a'⌝)) → ⊢ₛ wp⟦c⟧ (⇓? a => ⌜∃ a', Rα a a' ∧ Q' a'⌝)

Every postcondition that c' establishes is established, up to Rα, by every successful execution of c; a failing execution of c is unconstrained. At N = Id this is the statement "if c returns a, then Rα a c'.run" (RCompOk.id_iff). The relation is stated through wp for M only, so it applies to any M with a WPMonad instance.

Rules

• RCompOk.pure, RCompOk.bind — the Kleisli rules; bind composes;
• RCompOk.mono — weakening of the value relation;
• RCompOk.ite, RCompOk.dite — conditionals on both sides, with equivalent conditions; RCompOk.ite_left, RCompOk.dite_left — a conditional on the M side only (a runtime check with no counterpart in N);
• RCompOk.bind_left — a computation on the M side only, described by a partial-correctness postcondition;
• RCompOk.of_wp_false — a computation that never succeeds relates to anything;
• RCompOk.forIn_list, RCompOk.forIn_range, RCompOk.forIn_rco — for loops over List.Forall₂-related lists, over [a:b] and over a...b, with early exit through RForInStep.

Transfer

RCompOk.transfer moves a total-correctness fact about c' to a partial-correctness fact about c: if every result of c' satisfies Q', and Rα a a' → Q' a' → Q a, then every successful result of c satisfies Q. RCompOk.triple_transfer is the same statement in Std.Do triple notation. The converse direction does not hold: a computation that always fails is RCompOk-related to every c' and satisfies every partial-correctness postcondition (Examples/RCompOkExamples.lean, transfer_reverse_false).

Containers

ArrayRel R is the pointwise relation on arrays, List.Forall₂ R on the underlying lists (the relation R_array of Combinators/ParamArray.lean is ArrayRel at a Param relation, R_array_eq_arrayRel). ArrayRel.iff_getElem states it by size and index; ArrayRel.ofFn_iff states agreement of an array with an indexed family Fin n → α.

The rcomp_ok tactic

rcomp_ok walks both programs of an RCompOk goal and applies the rule matching the head of the M side, leaving the value-relation leaves as goals. See rcompOkCore.

def Transfer.Param.RCompOk {M : Type u → Type v} {ps : Std.Do.PostShape} [Std.Do.WP M ps] {N : Type u → Type w} [Std.Do.WP N Std.Do.PostShape.pure] {α α' : Type u} (Rα : α → α' → Prop) (c : M α) (c' : N α') : Prop

The success-restricted Kleisli lift of a value relation. RCompOk Rα c c' holds when every postcondition Q' that the total computation c' establishes is established, up to Rα, by every successful execution of c: each value a that c returns without an exception has a partner a' with Rα a a' and Q' a'. The monad N has postcondition shape .pure, so wp⟦c'⟧ (⇓ a' => ⌜Q' a'⌝) states that every result of c' satisfies Q'.

Equations

• One or more equations did not get rendered due to their size.

theorem Transfer.Param.RCompOk.pure {M : Type u → Type v} {ps : Std.Do.PostShape} [Monad M] [Std.Do.WPMonad M ps] {N : Type u → Type w} [Monad N] [Std.Do.WPMonad N Std.Do.PostShape.pure] {α α' : Type u} (Rα : α → α' → Prop) {a : α} {a' : α'} (h : Rα a a') : RCompOk Rα (Pure.pure a) (Pure.pure a')

pure rule: related values give related pure computations.

theorem Transfer.Param.RCompOk.bind {M : Type u → Type v} {ps : Std.Do.PostShape} [Monad M] [Std.Do.WPMonad M ps] {N : Type u → Type w} [Monad N] [Std.Do.WPMonad N Std.Do.PostShape.pure] {α α' β β' : Type u} {Rα : α → α' → Prop} {Rβ : β → β' → Prop} {c : M α} {c' : N α'} {f : α → M β} {f' : α' → N β'} (hc : RCompOk Rα c c') (hf : ∀ (a : α) (a' : α'), Rα a a' → RCompOk Rβ (f a) (f' a')) : RCompOk Rβ (c >>= f) (c' >>= f')

bind rule: related heads and pointwise related continuations give related sequential compositions. The intermediate relation Rα is arbitrary.

theorem Transfer.Param.RCompOk.mono {M : Type u → Type v} {ps : Std.Do.PostShape} {N : Type u → Type w} {α α' : Type u} [Std.Do.WP M ps] [Std.Do.WP N Std.Do.PostShape.pure] {R S : α → α' → Prop} (hRS : ∀ (a : α) (a' : α'), R a a' → S a a') {c : M α} {c' : N α'} (h : RCompOk R c c') : RCompOk S c c'

Weakening: RCompOk is monotone in the value relation.

theorem Transfer.Param.RCompOk.of_wp_false {M : Type u → Type v} {ps : Std.Do.PostShape} {N : Type u → Type w} {α α' : Type u} [Std.Do.WP M ps] [Std.Do.WP N Std.Do.PostShape.pure] {R : α → α' → Prop} {c : M α} (c' : N α') (h : ⊢ₛ (Std.Do.wp c).apply (Std.Do.PostCond.mayThrow fun (x : α) => ⌜False⌝)) : RCompOk R c c'

A computation with no successful execution (its partial-correctness wp at the postcondition False holds) is RCompOk-related to every c'.

theorem Transfer.Param.RCompOk.bind_left {M : Type u → Type v} {ps : Std.Do.PostShape} {N : Type u → Type w} {α α' β : Type u} [Monad M] [Std.Do.WPMonad M ps] [Std.Do.WP N Std.Do.PostShape.pure] {R : β → α' → Prop} {c : M α} {f : α → M β} {c' : N α'} (P : α → Prop) (hc : ⊢ₛ (Std.Do.wp c).apply (Std.Do.PostCond.mayThrow fun (a : α) => ⌜P a⌝)) (hf : ∀ (a : α), P a → RCompOk R (f a) c') : RCompOk R (c >>= f) c'

One-sided bind: a computation c on the M side with no counterpart on the N side, whose successful results satisfy P, followed by continuations each related to c'.

theorem Transfer.Param.RCompOk.ite {M : Type u → Type v} {ps : Std.Do.PostShape} {N : Type u → Type w} {α α' : Type u} [Std.Do.WP M ps] [Std.Do.WP N Std.Do.PostShape.pure] {R : α → α' → Prop} {b b' : Prop} [Decidable b] [Decidable b'] (hb : b ↔ b') {t e : M α} {t' e' : N α'} (ht : RCompOk R t t') (he : RCompOk R e e') : RCompOk R (if b then t else e) (if b' then t' else e')

ite rule: conditionals with equivalent conditions and branchwise related arms are related.

theorem Transfer.Param.RCompOk.dite {M : Type u → Type v} {ps : Std.Do.PostShape} {N : Type u → Type w} {α α' : Type u} [Std.Do.WP M ps] [Std.Do.WP N Std.Do.PostShape.pure] {R : α → α' → Prop} {b b' : Prop} [Decidable b] [Decidable b'] (hb : b ↔ b') {t : b → M α} {e : ¬b → M α} {t' : b' → N α'} {e' : ¬b' → N α'} (ht : ∀ (h : b) (h' : b'), RCompOk R (t h) (t' h')) (he : ∀ (h : ¬b) (h' : ¬b'), RCompOk R (e h) (e' h')) : RCompOk R (if h : b then t h else e h) (if h' : b' then t' h' else e' h')

dite rule: dependent conditionals with equivalent conditions and branchwise related arms are related.

theorem Transfer.Param.RCompOk.ite_left {M : Type u → Type v} {ps : Std.Do.PostShape} {N : Type u → Type w} {α α' : Type u} [Std.Do.WP M ps] [Std.Do.WP N Std.Do.PostShape.pure] {R : α → α' → Prop} {b : Prop} [Decidable b] {t e : M α} {c' : N α'} (ht : b → RCompOk R t c') (he : ¬b → RCompOk R e c') : RCompOk R (if b then t else e) c'

One-sided ite: a conditional on the M side whose arms are each related to c' under the corresponding case hypothesis.

theorem Transfer.Param.RCompOk.dite_left {M : Type u → Type v} {ps : Std.Do.PostShape} {N : Type u → Type w} {α α' : Type u} [Std.Do.WP M ps] [Std.Do.WP N Std.Do.PostShape.pure] {R : α → α' → Prop} {b : Prop} [Decidable b] {t : b → M α} {e : ¬b → M α} {c' : N α'} (ht : ∀ (h : b), RCompOk R (t h) c') (he : ∀ (h : ¬b), RCompOk R (e h) c') : RCompOk R (if h : b then t h else e h) c'

One-sided dite: a dependent conditional on the M side whose arms are each related to c'.

theorem Transfer.Param.RCompOk.forIn_list {M : Type u → Type v} {ps : Std.Do.PostShape} {N : Type u → Type w} {β β' : Type u} [Monad M] [Std.Do.WPMonad M ps] [Monad N] [Std.Do.WPMonad N Std.Do.PostShape.pure] {A : Type x} {A' : Type y} (RA : A → A' → Prop) (Rβ : β → β' → Prop) (body : A → β → M (ForInStep β)) (body' : A' → β' → N (ForInStep β')) (hbody : ∀ (a : A) (a' : A') (b : β) (b' : β'), RA a a' → Rβ b b' → RCompOk (RForInStep Rβ) (body a b) (body' a' b')) {l : List A} {l' : List A'} (hl : List.Forall₂ RA l l') {init : β} {init' : β'} (hinit : Rβ init init') : RCompOk Rβ (forIn l init body) (forIn l' init' body')

forIn rule over lists: a loop body mapping related elements and related accumulators to RForInStep-related steps, folded over List.Forall₂-related lists from related initial accumulators, gives related loops. A done step must meet a done step, so early exit is matched.

theorem Transfer.Param.RCompOk.forIn_range {M : Type u → Type v} {ps : Std.Do.PostShape} {N : Type u → Type w} {β β' : Type u} [Monad M] [Std.Do.WPMonad M ps] [Monad N] [Std.Do.WPMonad N Std.Do.PostShape.pure] (Rβ : β → β' → Prop) (r : Std.Legacy.Range) (body : ℕ → β → M (ForInStep β)) (body' : ℕ → β' → N (ForInStep β')) (hbody : ∀ (i : ℕ) (b : β) (b' : β'), Rβ b b' → RCompOk (RForInStep Rβ) (body i b) (body' i b')) {init : β} {init' : β'} (hinit : Rβ init init') : RCompOk Rβ (forIn r init body) (forIn r init' body')

forIn rule over a range [a:b] (Std.Legacy.Range) iterated on both sides, with the same index passed to both bodies.

theorem Transfer.Param.RCompOk.forIn_rco {M N : Type → Type} {ps : Std.Do.PostShape} [Monad M] [Std.Do.WPMonad M ps] [Monad N] [Std.Do.WPMonad N Std.Do.PostShape.pure] {β β' : Type} (Rβ : β → β' → Prop) (r : Std.Rco ℕ) (body : ℕ → β → M (ForInStep β)) (body' : ℕ → β' → N (ForInStep β')) (hbody : ∀ (i : ℕ) (b : β) (b' : β'), Rβ b b' → RCompOk (RForInStep Rβ) (body i b) (body' i b')) {init : β} {init' : β'} (hinit : Rβ init init') : RCompOk Rβ (forIn r init body) (forIn r init' body')

forIn rule over a half-open range a...b (Std.Rco Nat) iterated on both sides, with the same index passed to both bodies. The range's ForIn instance places the accumulator in Type.

theorem Transfer.Param.RCompOk.transfer {M : Type u → Type v} {ps : Std.Do.PostShape} {N : Type u → Type w} {α α' : Type u} [Std.Do.WP M ps] [Std.Do.WP N Std.Do.PostShape.pure] {R : α → α' → Prop} {c : M α} {c' : N α'} (h : RCompOk R c c') {Q : α → Prop} {Q' : α' → Prop} (hQ : ∀ (a : α) (a' : α'), R a a' → Q' a' → Q a) (ht : ⊢ₛ (Std.Do.wp c').apply (Std.Do.PostCond.noThrow fun (a' : α') => ⌜Q' a'⌝)) : ⊢ₛ (Std.Do.wp c).apply (Std.Do.PostCond.mayThrow fun (a : α) => ⌜Q a⌝)

Transfer from the total side to the successful executions of the partial side. If every result of c' satisfies Q' and R a a' → Q' a' → Q a, then every result that c returns without an exception satisfies Q. The converse direction, from a partial-correctness fact about c to a fact about c', does not hold, since a c that always fails is related to every c'.

theorem Transfer.Param.RCompOk.triple_transfer {M : Type u → Type v} {ps : Std.Do.PostShape} {N : Type u → Type w} {α α' : Type u} [Std.Do.WP M ps] [Std.Do.WP N Std.Do.PostShape.pure] {R : α → α' → Prop} {c : M α} {c' : N α'} (h : RCompOk R c c') {Q : α → Prop} {Q' : α' → Prop} (hQ : ∀ (a : α) (a' : α'), R a a' → Q' a' → Q a) (P : Std.Do.Assertion ps) (ht : ⦃⌜True⌝⦄ c' ⦃Std.Do.PostCond.noThrow fun (a' : α') => ⌜Q' a'⌝⦄) : ⦃P⦄ c ⦃Std.Do.PostCond.mayThrow fun (a : α) => ⌜Q a⌝⦄

RCompOk.transfer in triple notation: a total-correctness triple for c' gives a partial-correctness triple for c under any precondition.

theorem Transfer.Param.RCompOk.id_iff {M : Type u → Type v} {ps : Std.Do.PostShape} {α α' : Type u} [Std.Do.WP M ps] {R : α → α' → Prop} {c : M α} {c' : Id α'} : RCompOk R c c' ↔ ⊢ₛ (Std.Do.wp c).apply (Std.Do.PostCond.mayThrow fun (a : α) => ⌜R a c'.run⌝)

At N = Id, RCompOk R c c' states that every successful result of c is R-related to c'.run.

def Transfer.Param.ArrayRel {α : Type x} {β : Type y} (R : α → β → Prop) (a : Array α) (b : Array β) : Prop

The pointwise relation on arrays: a and b have the same size and corresponding entries are R-related, stated as List.Forall₂ R on the underlying lists.

Equations

• Transfer.Param.ArrayRel R a b = List.Forall₂ R a.toList b.toList

theorem Transfer.Param.R_array_eq_arrayRel {mA nA : MapClass} {A A' : Type u} (PA : Param mA nA A A') : R_array PA = ArrayRel PA.R

The Param array relation R_array PA is ArrayRel at the relation of PA.

theorem Transfer.Param.ArrayRel.iff_getElem {α : Type x} {β : Type y} {R : α → β → Prop} {a : Array α} {b : Array β} : ArrayRel R a b ↔ a.size = b.size ∧ ∀ (i : ℕ) (h : i < a.size) (h' : i < b.size), R a[i] b[i]

ArrayRel by size and index.

theorem Transfer.Param.ArrayRel.size_eq {α : Type x} {β : Type y} {R : α → β → Prop} {a : Array α} {b : Array β} (h : ArrayRel R a b) : a.size = b.size

Related arrays have equal size.

theorem Transfer.Param.ArrayRel.getElem {α : Type x} {β : Type y} {R : α → β → Prop} {a : Array α} {b : Array β} (h : ArrayRel R a b) (i : ℕ) (hi : i < a.size) (hi' : i < b.size) : R a[i] b[i]

Entries of related arrays at the same in-range index are related.

theorem Transfer.Param.ArrayRel.push {α : Type x} {β : Type y} {R : α → β → Prop} {a : Array α} {b : Array β} (h : ArrayRel R a b) {x : α} {y : β} (hxy : R x y) : ArrayRel R (a.push x) (b.push y)

Pushing related entries onto related arrays gives related arrays.

theorem Transfer.Param.ArrayRel.set {α : Type x} {β : Type y} {R : α → β → Prop} {a : Array α} {b : Array β} (h : ArrayRel R a b) (i : ℕ) (hi : i < a.size) (hi' : i < b.size) {x : α} {y : β} (hxy : R x y) : ArrayRel R (a.set i x hi) (b.set i y hi')

Writing related entries at the same in-range index of related arrays gives related arrays.

theorem Transfer.Param.ArrayRel.ofFn_iff {α : Type x} {β : Type y} {R : α → β → Prop} {n : ℕ} (f : Fin n → α) (b : Array β) : ArrayRel R (Array.ofFn f) b ↔ b.size = n ∧ ∀ (k : Fin n) (hk : ↑k < b.size), R (f k) b[↑k]

Agreement of an array with an indexed family: Array.ofFn f is related to b exactly when b has size n and position k of b is related to f k.

Axiom audit

partial def Transfer.Param.rcompOkIntros : Lean.Elab.Tactic.TacticM Unit

Introduce every leading binder of the main goal with a fresh name.

partial def Transfer.Param.rcompOkCore (userRels rels lemmas : Array Lean.Term) : Lean.Elab.Tactic.TacticM Unit

Structural RCompOk descent. On a goal RCompOk R c c' (after introducing leading binders and dsimp only, which removes have and β-redexes left by do-elaboration) it tries, in order:

1. each supplied lemma, by exact and then by apply;
2. by the head of c: Bind.bind ↦ RCompOk.bind, with the intermediate relation taken from userRels, then from the relations of the enclosing goals (innermost first, including R of an RForInStep R goal), then equality; ite / dite ↦ RCompOk.ite / RCompOk.dite when c' has the same head and RCompOk.ite_left / RCompOk.dite_left otherwise; ForIn.forIn ↦ RCompOk.forIn_range, RCompOk.forIn_rco, RCompOk.forIn_list at equality (same list) or at a relation from userRels;
3. otherwise RCompOk.pure.

It recurses into every resulting RCompOk goal. Condition equivalences b ↔ b' are closed by Iff.rfl when possible; an RForInStep R leaf on two yield (or two done) steps is reduced to R. Value-relation leaves and goals that match no rule are left to the caller.

def Transfer.Param.rcompOkTac : Lean.ParserDescr

rcomp_ok assembles an RCompOk witness by structural descent over both programs (see rcompOkCore) and leaves the value-relation leaves as goals. rcomp_ok using R₁, …, Rₙ supplies intermediate relations for bind and forIn, tried before the relations of the enclosing goals; rcomp_ok [h₁, …, hₘ] supplies RCompOk lemmas for sub-programs (a called function, a failing primitive), tried at each node before the structural rules. It fails on a goal that is not RCompOk _ _ _.

Equations

• One or more equations did not get rendered due to their size.