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. The companion family opE r frames the exception postcondition; the FrameOp class relates op to its companion, derived by the structure of the exception postcondition type.

class Lean.Order.FrameOp {Pred : Type u} [CompleteLattice Pred] {R : Type x} (op : R → Pred → Pred) (EPosts : Type v) [CompleteLattice EPosts] (opE : outParam (R → EPosts → EPosts)) : Prop

Relates a frame operator op on the value channel of a PredTrans Pred EPosts to a companion opE on the exception channel. Both preserve suprema. Instances derive opE from the structure of EPosts: op itself on the assertion type, a pointwise lift under a function layer, and a componentwise lift on a product layer. A low-priority default instance ignores the frame. An instance for a custom exception layer takes precedence.

• preservesSup (r : R) : PreservesSup (op r)

  Each op r preserves suprema, so it has an upper adjoint.

• preservesSupE (r : R) : PreservesSup (opE r)

  Each opE r preserves suprema, so it has an upper adjoint.

def Lean.Order.FrameOp.pointwise {A : Type v} {R : Type x} {ε : Type w} (opE : R → A → A) (r : R) : (ε → A) → ε → A

The frame acts pointwise under a function layer.

Equations

• Lean.Order.FrameOp.pointwise opE r = Function.comp (opE r)

def Lean.Order.FrameOp.prod {A : Type v} {B : Type v'} {R : Type x} (opA : R → A → A) (opB : R → B → B) (r : R) : A × B → A × B

The frame acts componentwise on a product layer.

Equations

• Lean.Order.FrameOp.prod opA opB r = Prod.map (opA r) (opB r)

def Lean.Order.FrameOp.ignore {A : Type v} {R : Type x} : R → A → A

The frame cannot act on the channel, so its companion ignores it.

Equations

• Lean.Order.FrameOp.ignore x✝ = id

instance Lean.Order.instPreservesSupForallPointwise {R : Type x} {EPosts : Type v} [CompleteLattice EPosts] (opE : R → EPosts → EPosts) [∀ (r : R), PreservesSup (opE r)] (r : R) {ε : Type w} : PreservesSup (FrameOp.pointwise opE r)

instance Lean.Order.instPreservesSupProdProd {R : Type x} {EPosts : Type v} [CompleteLattice EPosts] {B : Type v'} [CompleteLattice B] (opA : R → EPosts → EPosts) (opB : R → B → B) [∀ (r : R), PreservesSup (opA r)] [∀ (r : R), PreservesSup (opB r)] (r : R) : PreservesSup (FrameOp.prod opA opB r)

instance Lean.Order.instPreservesSupIgnore {R : Type x} {EPosts : Type v} [CompleteLattice EPosts] (r : R) : PreservesSup (FrameOp.ignore r)

@[instance 10000]

instance Lean.Order.instFrameOpOfPreservesSup {Pred : Type u} [CompleteLattice Pred] {R : Type x} {op : R → Pred → Pred} [∀ (r : R), PreservesSup (op r)] : FrameOp op Pred op

instance Lean.Order.instFrameOpForallPointwise {Pred : Type u} [CompleteLattice Pred] {R : Type x} {op : R → Pred → Pred} {EPosts : Type v} [CompleteLattice EPosts] {ε : Type w} {opE : R → EPosts → EPosts} [FrameOp op EPosts opE] : FrameOp op (ε → EPosts) (FrameOp.pointwise opE)

instance Lean.Order.instFrameOpProdProd {Pred : Type u} [CompleteLattice Pred] {R : Type x} {op : R → Pred → Pred} {EPosts : Type v} [CompleteLattice EPosts] {B : Type v'} [CompleteLattice B] {opA : R → EPosts → EPosts} {opB : R → B → B} [FrameOp op EPosts opA] [FrameOp op B opB] : FrameOp op (EPosts × B) (FrameOp.prod opA opB)

@[instance 100, defaultInstance 1000]

instance Lean.Order.instFrameOpIgnoreOfPreservesSup {Pred : Type u} [CompleteLattice Pred] {R : Type x} {op : R → Pred → Pred} {EPosts : Type v} [CompleteLattice EPosts] [∀ (r : R), PreservesSup (op r)] : FrameOp op EPosts FrameOp.ignore

@[simp]

theorem Lean.Order.FrameOp.pointwise_apply {A : Type u} {R : Type x} {ε : Type w} (opE : R → A → A) (r : R) (E : ε → A) (e : ε) : pointwise opE r E e = opE r (E e)

@[simp]

theorem Lean.Order.FrameOp.prod_fst {A : Type u} {B : Type v} {R : Type x} (opA : R → A → A) (opB : R → B → B) (r : R) (p : A × B) : (prod opA opB r p).fst = opA r p.fst

@[simp]

theorem Lean.Order.FrameOp.prod_snd {A : Type u} {B : Type v} {R : Type x} (opA : R → A → A) (opB : R → B → B) (r : R) (p : A × B) : (prod opA opB r p).snd = opB r p.snd

@[simp]

theorem Lean.Order.FrameOp.ignore_apply {A : Type u} {R : Type x} (r : R) (a : A) : ignore r a = a

theorem Lean.Order.FrameOp.upperAdjoint_pointwise_apply {A : Type u} {R : Type x} {ε : Type w} [CompleteLattice A] (opE : R → A → A) [∀ (r : R), PreservesSup (opE r)] (r : R) (X : ε → A) (e : ε) : PreservesSup.upperAdjoint (pointwise opE r) X e = PreservesSup.upperAdjoint (opE r) (X e)

theorem Lean.Order.FrameOp.upperAdjoint_prod_fst {A : Type u} {B : Type v} {R : Type x} [CompleteLattice A] [CompleteLattice B] (opA : R → A → A) (opB : R → B → B) [∀ (r : R), PreservesSup (opA r)] [∀ (r : R), PreservesSup (opB r)] (r : R) (E : A × B) : (PreservesSup.upperAdjoint (prod opA opB r) E).fst = PreservesSup.upperAdjoint (opA r) E.fst

theorem Lean.Order.FrameOp.upperAdjoint_prod_snd {A : Type u} {B : Type v} {R : Type x} [CompleteLattice A] [CompleteLattice B] (opA : R → A → A) (opB : R → B → B) [∀ (r : R), PreservesSup (opA r)] [∀ (r : R), PreservesSup (opB r)] (r : R) (E : A × B) : (PreservesSup.upperAdjoint (prod opA opB r) E).snd = PreservesSup.upperAdjoint (opB r) E.snd

theorem Lean.Order.FrameOp.upperAdjoint_ignore {A : Type u} {R : Type x} [CompleteLattice A] (r : R) (X : A) : PreservesSup.upperAdjoint (ignore r) X = X

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

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

Equations

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

@[simp]

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

Unfolding frameClosure through apply.

theorem Lean.Order.PredTrans.monotone_frameClosure {Pred : Type u} [CompleteLattice Pred] {EPosts : Type v} [CompleteLattice EPosts] {β : Type w} {R : Type x} {opE : R → EPosts → EPosts} (op : R → Pred → Pred) [FrameOp op EPosts opE] {t : PredTrans Pred EPosts β} (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] {EPosts : Type v} [CompleteLattice EPosts] {β : Type w} {R : Type x} {opE : R → EPosts → EPosts} (op : R → Pred → Pred) [FrameOp op EPosts opE] (comp : R → R → R) (hact : ∀ (r r' : R) (a : Pred), op (comp r r') a = op r (op r' a)) (hactE : ∀ (r r' : R) (E : EPosts), opE (comp r r') E = opE r (opE r' E)) (t : PredTrans Pred EPosts β) (Q : β → Pred) (E : EPosts) (F : R) : PartialOrder.rel (op F ((frameClosure op t).apply Q E)) ((frameClosure op t).apply (fun (a : β) => op F (Q a)) (opE F E))

The frame rule, internalized: for supremum-preserving op r whose resources compose by comp with the action law op (comp r r') = op r ∘ op r', and the matching companion law hactE, op F commutes into the value postcondition of t.frameClosure op while opE F commutes into the exception postcondition.

theorem Lean.Order.PredTrans.le_frameClosure_iff {Pred : Type u} [CompleteLattice Pred] {EPosts : Type v} [CompleteLattice EPosts] {β : Type w} {R : Type x} {opE : R → EPosts → EPosts} (op : R → Pred → Pred) [FrameOp op EPosts opE] (t : PredTrans Pred EPosts β) {Q : β → Pred} {E : EPosts} {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)) (opE r 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)) (opE r E) for every resource r.

theorem Lean.Order.PredTrans.le_frameClosure {Pred : Type u} [CompleteLattice Pred] {EPosts : Type v} [CompleteLattice EPosts] {β : Type w} {R : Type x} {opE : R → EPosts → EPosts} (op : R → Pred → Pred) [FrameOp op EPosts opE] (t : PredTrans Pred EPosts β) {Q : β → Pred} {E : EPosts} {pre : Pred} (hframe : ∀ (r : R) (Q' : β → Pred), PartialOrder.rel (op r (t.apply Q' E)) (t.apply (fun (a : β) => op r (Q' a)) (opE r 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 on both channels, then pre ⊑ (t.frameClosure op).apply Q E.

theorem Lean.Order.PredTrans.frameClosure_le {Pred : Type u} [CompleteLattice Pred] {EPosts : Type v} [CompleteLattice EPosts] {β : Type w} {R : Type x} {opE : R → EPosts → EPosts} (op : R → Pred → Pred) [FrameOp op EPosts opE] (e : R) (hunit : ∀ (a : Pred), op e a = a) (hunitE : ∀ (E : EPosts), opE e E = E) (t : PredTrans Pred EPosts β) (Q : β → Pred) (E : EPosts) : 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 and opE e = id.