The frame closure

The frame closure is an endomap on predicate transformers over a family of supremum-preserving operators op r, one per resource r. It internalizes the frame rule into the transformer it is applied to.

noncomputable def Lean.Order.PredTrans.frameClosure {Pred : Type u} [CompleteLattice Pred] {EPred : Type v} {β : Type w} {R : Type x} (op : R → Pred → Pred) (t : PredTrans Pred EPred β) : PredTrans Pred EPred β

The frame closure of a predicate transformer t with respect to a family of supremum-preserving operators op r: the meet over all resources r of the r-upper-adjoint of t framed by r. It internalizes the frame rule into any t (see PredTrans.frameClosure_frames), with no assumption on t. The exception postcondition is handed to t unchanged.

Equations

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

theorem Lean.Order.PredTrans.apply_frameClosure {Pred : Type u} [CompleteLattice Pred] {EPred : Type v} {β : Type w} {R : Type x} (op : R → Pred → Pred) (t : PredTrans Pred EPred β) (Q : β → Pred) (E : EPred) : (frameClosure op t).apply Q E = iInf fun (r : R) => PreservesSup.upperAdjoint (op r) (t.apply (fun (a : β) => op r (Q a)) E)

Unfolding frameClosure through apply.

theorem Lean.Order.PredTrans.monotone_frameClosure {Pred : Type u} [CompleteLattice Pred] {EPred : Type v} {β : Type w} {R : Type x} [CompleteLattice EPred] (op : R → Pred → Pred) [∀ (r : R), PreservesSup (op r)] {t : PredTrans Pred EPred β} (h : t.monotone) : (frameClosure op t).monotone

The frame closure carries monotonicity: if t is monotone, so is t.frameClosure op.

theorem Lean.Order.PredTrans.frameClosure_frames {Pred : Type u} [CompleteLattice Pred] {EPred : Type v} {β : Type w} {R : Type x} (op : R → Pred → Pred) [∀ (r : R), PreservesSup (op r)] (comp : R → R → R) (hact : ∀ (r r' : R) (a : Pred), op (comp r r') a = op r (op r' a)) (t : PredTrans Pred EPred β) (Q : β → Pred) (E : EPred) (F : R) : PartialOrder.rel (op F ((frameClosure op t).apply Q E)) ((frameClosure op t).apply (fun (a : β) => op F (Q a)) E)

The frame rule, internalized: for a family of supremum-preserving operators op r whose resources compose by comp with the action law op (comp r r') = op r ∘ op r', and any predicate transformer t, op F commutes into the postcondition of t.frameClosure op.

theorem Lean.Order.PredTrans.le_frameClosure_iff {Pred : Type u} [CompleteLattice Pred] {EPred : Type v} {β : Type w} {R : Type x} (op : R → Pred → Pred) [∀ (r : R), PreservesSup (op r)] (t : PredTrans Pred EPred β) {Q : β → Pred} {E : EPred} {pre : Pred} : PartialOrder.rel pre ((frameClosure op t).apply Q E) ↔ ∀ (r : R), PartialOrder.rel (op r pre) (t.apply (fun (a : β) => op r (Q a)) E)

Landing below the frame closure, transposed across the Galois connection: pre ⊑ (t.frameClosure op).apply Q E holds exactly when op r pre ⊑ t.apply (fun a => op r (Q a)) E for every resource r. At a unit resource (op e = id) the r = e conjunct is pre ⊑ t.apply Q E; the remaining conjuncts are the frame conditions on pre, so a pre that cannot frame is forced down to the trivial ⊥.

theorem Lean.Order.PredTrans.le_frameClosure {Pred : Type u} [CompleteLattice Pred] {EPred : Type v} {β : Type w} {R : Type x} (op : R → Pred → Pred) [∀ (r : R), PreservesSup (op r)] (t : PredTrans Pred EPred β) {Q : β → Pred} {E : EPred} {pre : Pred} (hframe : ∀ (r : R) (Q' : β → Pred), PartialOrder.rel (op r (t.apply Q' E)) (t.apply (fun (a : β) => op r (Q' a)) E)) (hpre : PartialOrder.rel pre (t.apply Q E)) : PartialOrder.rel pre ((frameClosure op t).apply Q E)

Landing below the frame closure reduces to landing below the base transformer together with framing: if pre ⊑ t.apply Q E and t frames every op r, then pre ⊑ (t.frameClosure op).apply Q E.

theorem Lean.Order.PredTrans.frameClosure_le {Pred : Type u} [CompleteLattice Pred] {EPred : Type v} {β : Type w} {R : Type x} (op : R → Pred → Pred) [∀ (r : R), PreservesSup (op r)] (e : R) (hunit : ∀ (a : Pred), op e a = a) (t : PredTrans Pred EPred β) (Q : β → Pred) (E : EPred) : PartialOrder.rel ((frameClosure op t).apply Q E) (t.apply Q E)

The frame closure lies below the base transformer, witnessed at a unit resource e with op e = id.