|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Lean FRO LLC. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Sebastian Graf |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +prelude |
| 9 | +public import Std.Internal.Do.Order.Basic |
| 10 | + |
| 11 | +@[expose] public section |
| 12 | + |
| 13 | +namespace Lean.Order |
| 14 | + |
| 15 | +universe u v w |
| 16 | + |
| 17 | +variable {α : Type u} [CompleteLattice α] |
| 18 | + |
| 19 | +/-- |
| 20 | +`f : α → α` *preserves `Sup`* if it distributes over arbitrary joins: |
| 21 | +`f (sup s) = sup { f x | x ∈ s }`. Equivalently `f` is a lower adjoint, so it has an upper adjoint |
| 22 | +`PreservesSup.upperAdjoint f`. |
| 23 | +
|
| 24 | +A frame operator acts by a `Sup`-preserving map for each resource `r`: the lattice meet `(a ⊓ ·)`, |
| 25 | +or a cost combinator `(costConj r)` for a counter resource. The upper adjoint is the corresponding |
| 26 | +implication: Heyting `⇨` for the meet, a magic wand for separating conjunction. |
| 27 | +-/ |
| 28 | +class PreservesSup {α : Type u} [CompleteLattice α] (f : α → α) : Prop where |
| 29 | + /-- `f` preserves joins. -/ |
| 30 | + map_sup (s : α → Prop) : |
| 31 | + f (CompleteLattice.sup s) = CompleteLattice.sup (fun y => ∃ x, s x ∧ y = f x) |
| 32 | + |
| 33 | +namespace PreservesSup |
| 34 | + |
| 35 | +/-- The upper adjoint of `f`: the join of all `x` with `f x ⊑ b`. For `f = (a ⊓ ·)` this is Heyting |
| 36 | +implication `a ⇨ ·`. -/ |
| 37 | +noncomputable def upperAdjoint (f : α → α) (b : α) : α := CompleteLattice.sup (fun x => f x ⊑ b) |
| 38 | + |
| 39 | +/-- `upperAdjoint f b` is the least upper bound of `{x | f x ⊑ b}` by definition. -/ |
| 40 | +theorem upperAdjoint_spec (f : α → α) (b : α) : is_sup (fun x : α => f x ⊑ b) (upperAdjoint f b) := |
| 41 | + CompleteLattice.sup_spec (fun x : α => f x ⊑ b) |
| 42 | + |
| 43 | +/-- Unit, free from the definition of `upperAdjoint`: `f x ⊑ b → x ⊑ upperAdjoint f b`. Needs only |
| 44 | +`CompleteLattice`. -/ |
| 45 | +theorem le_upperAdjoint (f : α → α) {b x : α} (h : f x ⊑ b) : x ⊑ upperAdjoint f b := |
| 46 | + le_sup (c := fun x : α => f x ⊑ b) h |
| 47 | + |
| 48 | +/-- Counit (modus ponens), from join preservation: `f (upperAdjoint f b) ⊑ b`. -/ |
| 49 | +theorem upperAdjoint_le (f : α → α) [PreservesSup f] (b : α) : f (upperAdjoint f b) ⊑ b := by |
| 50 | + unfold upperAdjoint |
| 51 | + rw [PreservesSup.map_sup (f := f)] |
| 52 | + apply sup_le |
| 53 | + rintro y ⟨x, hx, rfl⟩ |
| 54 | + exact hx |
| 55 | + |
| 56 | +/-- Monotonicity of a `Sup`-preserving `f`, derived from join preservation. -/ |
| 57 | +theorem map_mono (f : α → α) [PreservesSup f] {b b' : α} (h : b ⊑ b') : f b ⊑ f b' := by |
| 58 | + have hsup : (CompleteLattice.sup (fun y => y ⊑ b')) = b' := |
| 59 | + is_sup_unique (CompleteLattice.sup_spec _) |
| 60 | + (fun x => ⟨fun hb' y hy => PartialOrder.rel_trans hy hb', |
| 61 | + fun hy => hy b' PartialOrder.rel_refl⟩) |
| 62 | + calc f b ⊑ f (CompleteLattice.sup (fun y => y ⊑ b')) := by |
| 63 | + rw [PreservesSup.map_sup (f := f)]; exact le_sup _ ⟨b, h, rfl⟩ |
| 64 | + _ = f b' := by rw [hsup] |
| 65 | + |
| 66 | +/-- The **frame closure** of a post-transformer `k` with respect to a family of `Sup`-preserving |
| 67 | +operators `op r`: the meet over all resources `r` of the `r`-upper-adjoint of `k` framed by `r`. It |
| 68 | +internalizes the frame rule into any `k` (see `frameClosure_frames`), with no assumption on `k`. A |
| 69 | +weakest precondition built as `frameClosure op (fun Q => bwp x Q E)` satisfies the `op`-frame rule by |
| 70 | +construction. -/ |
| 71 | +noncomputable def frameClosure {R : Type v} {β : Type w} (op : R → α → α) |
| 72 | + (k : (β → α) → α) (Q : β → α) : α := |
| 73 | + ⨅ r, upperAdjoint (op r) (k (fun a => op r (Q a))) |
| 74 | + |
| 75 | +/-- The frame rule, internalized: for a family of `Sup`-preserving operators `op r` whose resources |
| 76 | +compose by `comp` with the action law `op (comp r r') = op r ∘ op r'`, and any post-transformer `k`, |
| 77 | +`op F (frameClosure op k Q) ⊑ frameClosure op k (fun a => op F (Q a))`. -/ |
| 78 | +theorem frameClosure_frames {R : Type v} {β : Type w} (op : R → α → α) [∀ r, PreservesSup (op r)] |
| 79 | + (comp : R → R → R) (hact : ∀ r r' a, op (comp r r') a = op r (op r' a)) |
| 80 | + (k : (β → α) → α) (Q : β → α) (F : R) : |
| 81 | + op F (frameClosure op k Q) ⊑ frameClosure op k (fun a => op F (Q a)) := by |
| 82 | + apply le_iInf |
| 83 | + intro F' |
| 84 | + apply le_upperAdjoint (op F') |
| 85 | + rw [← hact F' F (frameClosure op k Q)] |
| 86 | + refine PartialOrder.rel_trans (map_mono (op (comp F' F)) (iInf_le _ (comp F' F))) ?_ |
| 87 | + refine PartialOrder.rel_trans (upperAdjoint_le (op (comp F' F)) _) ?_ |
| 88 | + apply PartialOrder.rel_of_eq |
| 89 | + congr 1 |
| 90 | + funext a |
| 91 | + rw [hact F' F (Q a)] |
| 92 | + |
| 93 | +end PreservesSup |
| 94 | + |
| 95 | +end Lean.Order |
| 96 | + |
| 97 | +end -- public section |
0 commit comments