Cairn.UI.Grid
lean/Cairn/UI/Grid.lean
Grids that follow their box
A Grid lays equal cards out in rows, as many columns as fit the box's width. It is plain
arithmetic on the box's size, so a view builds it from the window size the runtime keeps
(UI.size, updated by every resize event): the host only reports the size and Lean decides
every rect. Resizing the window changes the size, the view runs again and the cards reflow.
- Columns are as many cards of
minWidthas fit with the gaps between them, and at least one (columns). The cards then share the width equally, so they grow until another column fits. - Cards keep their aspect ratio (
ratioW : ratioH), plus a fixedcaptionheight under it that doesn't scale. When the rows would be taller than the box, every card shrinks so they fit: nothing scrolls, and nothing is drawn outside the box. - Gaps are fixed:
gapbetween columns and between rows. (Only when the gaps between rows alone are taller than the box are the rows packed with none.) - Reading order: card
iis in rowi / columns, columni % columns, so the cards keep their order on every resize; only where the rows break changes. - The used width is centred in the box; rows start at its top.
Grid.node builds the view: a column of rows of fixed-size cells, each clipping its card, laid
out by the ordinary layout pass. The geometry's theorems are at the end of this file: the
column count is the largest that fits and at least one, the cells never overlap and stay inside
the box, in reading order. They live here, not with the layout proofs, so an app's claims can
cite them. Cairn.Layout.Grid proves the cells land exactly on Grid.rects and that hit
testing a point in a cell answers from that cell alone.
Imports Cairn.UI.Node
Structures 1
Grid : Type
A grid of equal cards whose column count follows the width of its box.
minWidth : NatThe narrowest a card is laid out when there's room for it: there are as many columns as cards of this width fit (at least one; taken as 1 when 0).
ratioW : NatThe cards' aspect ratio, width to height (each taken as 1 when 0).
ratioH : Natgap : NatPoints between columns and between rows.
caption : NatA fixed height under the scaled part of each card (a caption), not scaled with it.
Definitions 24
minW (g : Grid) : Nat
rw (g : Grid) : Nat
rh (g : Grid) : Nat
Fits (g : Grid) (W k : Nat) : Prop
k cards of the minimum width, with the gaps between them, fit in W.
columns (g : Grid) (W : Nat) : Nat
Columns: the most cards of the minimum width that fit in W with their gaps, and at
least one (columns_fits, le_columns).
rows (g : Grid) (W n : Nat) : Nat
Rows for n cards.
vgap (g : Grid) (W H n : Nat) : Nat
The gap between rows: gap, unless the gaps alone are taller than the box.
cardW (g : Grid) (W H n : Nat) : Nat
A card's width: its share of the width, or less if the rows would be too tall.
cardH (g : Grid) (W H n : Nat) : Nat
A card's height: its width at the aspect ratio, plus the caption (cardH_aspect).
usedW (g : Grid) (W H n : Nat) : Nat
The width the columns take, gaps included.
offset (g : Grid) (W H n : Nat) : Nat
Where the first column starts, centring the used width.
cell (g : Grid) (x y : Int) (W H n i : Nat) : Rect
Card i's rect, of n in the W × H box at (x, y): row i / columns, column
i % columns.
rects (g : Grid) (x y : Int) (W H n : Nat) : List Rect
Every card's rect, in order.
minCardH (g : Grid) : Nat
The least height of a card minWidth wide: its scaled part rounded up, plus the caption.
minBox (g : Grid) (n cols : Nat) : Nat × Nat
The smallest box with cols columns in which every one of n cards is at least
minWidth wide, as width and height (minW_le_cardW).
chunksAux {α : Type} (c : Nat) : Nat → List α → List (List α)xs in runs of c (the last may be shorter). fuel bounds the recursion; chunks gives
enough.
chunks {α : Type} (c : Nat) (xs : List α) : List (List α)
cellNode (w h : Nat) (card : Node) : Node
A cell: exactly the card's rect, clipping the card to it, so nothing in one cell paints or takes a click in another.
rowStyle (g : Grid) (W H n : Nat) : Style
A row's box: the used width, a card high, cells gap apart.
rowNode (g : Grid) (W H n : Nat) (cells : List Node) : Node
A row of cells.
style (g : Grid) (W H n : Nat) : Style
The grid's box: W × H, rows vgap apart, the used width centred.
node {α : Type} (g : Grid) (W H : Nat) (card : Nat → Nat → α → Node)
(xs : List α) : NodeThe grid as a view: W × H points (a fixed box), card i drawn by card w h xs[i]
at w × h points in its cell. The cards keep the order of xs.
Theorems 34
minW_pos (g : Grid) : 1 ≤ g.minW
rw_pos (g : Grid) : 1 ≤ g.rw
rh_pos (g : Grid) : 1 ≤ g.rh
columns_pos (g : Grid) (W : Nat) : 1 ≤ g.columns W
fits_iff (g : Grid) (W k : Nat) (hk : 1 ≤ k) : g.Fits W k ↔ k * (g.minW + g.gap) ≤ W + g.gap
k columns fit exactly when k cards and their gaps fit in the width plus one gap.
columns_fits (g : Grid) (W : Nat) : g.columns W = 1 ∨ g.Fits W (g.columns W)
The column count fits: one column, or that many cards of the minimum width fit.
le_columns (g : Grid) (W k : Nat) (h : g.Fits W k) : k ≤ g.columns W
No column count that fits is larger.
not_fits_succ (g : Grid) (W : Nat) : ¬g.Fits W (g.columns W + 1)
One more column would not fit.
gaps_le_W (g : Grid) (W : Nat) : g.gap * (g.columns W - 1) ≤ W
usedW_le (g : Grid) (W H n : Nat) : g.usedW W H n ≤ W
The columns and their gaps fit the width.
offset_usedW_le (g : Grid) (W H n : Nat) : g.offset W H n + g.usedW W H n ≤ W
vgaps_le (g : Grid) (W H n : Nat) : g.vgap W H n * (g.rows W n - 1) ≤ H
rows_le (g : Grid) (W H n : Nat) (hn : 0 < g.rows W n) : (g.rows W n - 1) * (g.cardH W H n + g.vgap W H n) + g.cardH W H n ≤ H
The rows and their gaps fit the height.
cardH_aspect (g : Grid) (W H n : Nat) (h : g.caption ≤ g.heightShare W H n) : g.cardH W H n = g.cardW W H n * g.rh / g.rw + g.caption
Aspect kept: when the box is tall enough for the captions, a card is as tall as its width at the aspect ratio, plus the caption.
vgap_eq (g : Grid) (W H n : Nat) (h : g.gap * (g.rows W n - 1) ≤ H) : g.vgap W H n = g.gap
Gaps fixed: whenever the gaps between rows fit the height, rows are gap apart.
row_lt_rows (g : Grid) (W n i : Nat) (hi : i < n) : i / g.columns W < g.rows W n
mul_le_of_le {a b s : Nat} (h : a ≤ b) : a * s ≤ b * s
pitch_lt {a b s w : Nat} (h : a < b) (hw : w ≤ s) : a * s + w ≤ b * sa < b rows (or columns) of pitch s ≥ w apart: the earlier ends before the later starts.
cell_inside (g : Grid) (x y : Int) (W H n i : Nat) (hi : i < n) : (g.cell x y W H n i).inside { x := x, y := y, w := ↑W, h := ↑H }
Inside: every card's rect is inside the grid's box.
cell_before (g : Grid) (x y : Int) (W H n i j : Nat) (hij : i < j) : have a := g.cell x y W H n i; have b := g.cell x y W H n j; a.y + a.h ≤ b.y ∨ a.y = b.y ∧ a.x + a.w ≤ b.x
Reading order: a later card is in a lower row (it starts below the earlier one's bottom), or in the same row and to the right.
cell_disjoint (g : Grid) (x y : Int) (W H n i j : Nat) (hij : i ≠ j) : (g.cell x y W H n i).disjoint (g.cell x y W H n j)
No overlap: two different cards' rects are disjoint.
rects_length (g : Grid) (x y : Int) (W H n : Nat) : (g.rects x y W H n).length = n
rects_getElem (g : Grid) (x y : Int) (W H n i : Nat) (h : i < (g.rects x y W H n).length) : (g.rects x y W H n)[i] = g.cell x y W H n i
rects_pairwise (g : Grid) (x y : Int) (W H n : Nat) : List.Pairwise (fun a b => a.disjoint b ∧ (a.y + a.h ≤ b.y ∨ a.y = b.y ∧ a.x + a.w ≤ b.x)) (g.rects x y W H n)
The rects in order: pairwise disjoint, and each in reading order before the next.
rects_inside (g : Grid) (x y : Int) (W H n : Nat) (r : Rect) : r ∈ g.rects x y W H n → r.inside { x := x, y := y, w := ↑W, h := ↑H }
ceil_spec (a b : Nat) (hb : 1 ≤ b) :
a ≤ (a + b - 1) / b * b ∧ (0 < a → ((a + b - 1) / b - 1) * b < a)Rounding up: q = ⌈a / b⌉ covers a (a ≤ q * b) and one less doesn't ((q - 1) * b < a
when a > 0).
ceil_div_anti (n c C : Nat) (hc : 1 ≤ c) (hC : c ≤ C) :
(n + C - 1) / C ≤ (n + c - 1) / cRows only get fewer with more columns: ⌈n / C⌉ ≤ ⌈n / c⌉ when 1 ≤ c ≤ C.
le_columns_minBox (g : Grid) (n cols W : Nat) (hW : (g.minBox n cols).fst ≤ W) : max 1 cols ≤ g.columns W
The columns of a box at least minBox's width: at least cols.
minW_le_cardW (g : Grid) (n cols W H : Nat) (hn : 0 < n) (hW : (g.minBox n cols).fst ≤ W) (hH : (g.minBox n cols).snd ≤ H) : g.minW ≤ g.cardW W H n
minBox_cells (g : Grid) (x y : Int) (n cols W H : Nat) (hW : (g.minBox n cols).fst ≤ W) (hH : (g.minBox n cols).snd ≤ H) (r : Rect) : r ∈ g.rects x y W H n → ↑g.minW ≤ r.w
columns_minBox (g : Grid) (n cols : Nat) : g.columns (g.minBox n cols).fst = max 1 cols
minBox has exactly cols columns (at least one).
minBox_narrower (g : Grid) (n cols W H : Nat) (hW : W < (g.minBox n cols).fst) : g.columns W < max 1 cols ∨ g.cardW W H n < g.minW
minBox_shorter (g : Grid) (n cols W H : Nat) (hn : 0 < n) (hcols : g.columns W = max 1 cols) (hgap : g.gap ≤ g.minCardH) (hH : H < (g.minBox n cols).snd) : g.cardW W H n < g.minW
Instances 4
instReprGrid : Repr Grid
instDecidableEqGrid : DecidableEq Grid
instInhabitedGrid : Inhabited Grid
instDecidableFits (g : Grid) (W k : Nat) : Decidable (g.Fits W k)
The smallest box
minBox n cols is the smallest box with cols columns (at least one) in which every one of n
cards is at least minWidth wide: cols cards of the minimum width and their gaps across, and
as many rows of the least card height (minCardH) and their gaps down. An app hands it, plus
whatever it lays out around the grid, to the host as the window's minimum size
(App.minSize), so the cards never shrink below minWidth. Its theorems are at the end of the
file.
The view
The geometry's theorems
That the layout pass puts the cells on these rects, and hit testing, are in
Cairn.Layout.Grid.
Columns
Sizes
Cells
The smallest box
- At or above it, every card is at least
minWidthwide (minW_le_cardW,minBox_cells): a wider box has as many columns or more, so no more rows, and a taller one only more room. - It is the smallest: it has exactly
colscolumns (columns_minBox); a narrower box has fewer columns, or with one column cards narrower thanminWidth(minBox_narrower); a shorter box withcolscolumns has cards narrower thanminWidth(minBox_shorter, when the gap is no taller than a card).