Cairn.Layout.Check
lean/Cairn/Layout/Check.lean
Checking Pressable by evaluation
Pressable w l (Bridge.lean) is stated with Laid.Everywhere, an inductive Prop, so it
can't be decided directly. This file gives each condition a Bool twin and proves the twin
sound, so for a concrete view, window and metrics an app proves every control pressable with
by decide +kernel (the kernel evaluates the layout; no compiler, no extra axiom):
theorem pressable : ∀ t ∈ targets (layout m w v), hitTest (layout m w v) t.visible.center = some t.control :=
hitTest_center_of_check (by decide +kernel)
Imports Cairn.Layout.Bridge
Definitions 10
insideB (r o : Rect) : Bool
padB (p : Insets) : Bool
fitsB : Laid → Bool
stackTopB : Laid → Bool
controlLeafB : Laid → Bool
allB (p : Laid → Bool) : Laid → Bool
p holds at every node.
allListB (p : Laid → Bool) : List Laid → Bool
checkPressable (w : Size) (l : Laid) : Bool
Every condition of Pressable, evaluated.
controlsNonempty (l : Laid) : Bool
Every control's visible part (rect ∩ clip) is nonempty.
controlRectsNonempty (l : Laid) : Bool
Every control's rect is nonempty. Its visible part may still be empty under a scroll box
(scrolled out of view), where the fuzzer checks only the controls it can see; anywhere else a
tree that passes checkPressable shows each control whole (visible_eq_rect).
Theorems 8
inside_of_insideB {r o : Rect} (h : insideB r o = true) : r.inside o
everywhere_of_allB {p : Laid → Bool} {P : Laid → Prop}
(hp : ∀ (l : Laid), p l = true → P l) (l : Laid) : allB p l = true → Laid.Everywhere P l
everywhere_of_allListB {p : Laid → Bool} {P : Laid → Prop}
(hp : ∀ (l : Laid), p l = true → P l) (ks : List Laid) :
allListB p ks = true → ∀ (k : Laid), k ∈ ks → Laid.Everywhere P k
fits_of_fitsB (l : Laid) : fitsB l = true → Fits l
stackTop_of_stackTopB (l : Laid) : stackTopB l = true → StackTop l
controlLeaf_of_controlLeafB (l : Laid) : controlLeafB l = true → ControlLeaf l
pressable_of_check {w : Size} {l : Laid} (h : checkPressable w l = true) :
Pressable w lThe checker is sound.
hitTest_center_of_check {m : TextMetrics} {w : Size} {n : Node}
(h : (checkPressable w (layout m w n) && controlsNonempty (layout m w n)) = true)
(t : Runtime.Target) :
t ∈ Runtime.targets (layout m w n) →
Runtime.hitTest (layout m w n) t.visible.center = some t.controlEvery control is pressable at its centre, for a laid-out view the checker accepts: the centre of its visible part, which the checker asks to be nonempty.