Cairn · module
Cairn.Text.WrapProofs
lean/Cairn/Text/WrapProofs.lean
Theorems about line breaking (Cairn.Text.Wrap)
For every text cs, width W and offsets o (any function: nothing here assumes the offsets
are monotone, so it holds for every TextMetrics, valid or not):
- Lines fit.
allLines_fit: every line is at mostWwide, or is a single scalar (a scalar wider than the line, which no break could help). - Lines tile the text.
allLines_coverandallLines_tiles: the lines are nonempty ranges in order, and the text isg₀ ++ l₀ ++ g₁ ++ l₁ ++ … ++ lₖ ++ gₖ₊₁with every gapgᵢmade of break spaces only (possibly empty, where an over-wide word was cut). - Line count.
lines_length_le: at mostmaxLineslines. - Keep.
lines_tail,lines_head:tailkeeps exactly the lastmin n kof theklines,headthe first.
Imports Cairn.Text.Wrap
Order
Inductive types 2
Cover (sp : Nat → Prop) (len : Nat) : Nat → List (Nat × Nat) → Prop
Cover sp len p rs: the ranges rs are nonempty and in order, the first starts at or
after p, the last ends by len, and every index in [p, len) outside them satisfies sp.
Constructors
nil {sp : Nat → Prop} {len p : Nat} :
p ≤ len → (∀ (i : Nat), p ≤ i → i < len → sp i) → Cover sp len p []cons {sp : Nat → Prop} {len p a b : Nat} {rs : List (Nat × Nat)} :
p ≤ a →
a < b →
(∀ (i : Nat), p ≤ i → i < a → sp i) →
Cover sp len b rs → Cover sp len p ((a, b) :: rs)Tiles : List Char → List (List Char) → Prop
Tiles cs ls: cs = g₀ ++ l₀ ++ g₁ ++ l₁ ++ … ++ lₖ ++ gₖ₊₁ where ls = [l₀, …, lₖ], every
line is nonempty and every gap is break spaces.
Constructors
last {g : List Char} : (∀ (c : Char), c ∈ g → c = ' ') → Tiles g []line {g l rest : List Char} {ls : List (List Char)} :
(∀ (c : Char), c ∈ g → c = ' ') →
l ≠ [] → Tiles rest ls → Tiles (g ++ l ++ rest) (l :: ls)Definitions 1
Good (o : Nat → Int) (W : Int) (p : Nat × Nat) : Prop
A piece or line is good if it fits or is at most one scalar.
Theorems 27
cutGo_spec (o : Nat → Int) (W : Int) (a b fuel c : Nat) : o c - o a ≤ W ∨ c = a + 1 → a + 1 ≤ c → (o (cutGo o W a b fuel c) - o a ≤ W ∨ cutGo o W a b fuel c = a + 1) ∧ c ≤ cutGo o W a b fuel c ∧ (cutGo o W a b fuel c ≤ b ∨ cutGo o W a b fuel c = c)
cut_spec (o : Nat → Int) (W : Int) (a b : Nat) : (o (cut o W a b) - o a ≤ W ∨ cut o W a b = a + 1) ∧ a + 1 ≤ cut o W a b ∧ (cut o W a b ≤ b ∨ cut o W a b = a + 1)
chunkGo_good (o : Nat → Int) (W : Int) (b fuel a : Nat) : b ≤ a + fuel → (∀ (p : Nat × Nat), p ∈ (chunkGo o W b fuel a).fst → Good o W p) ∧ Good o W (chunkGo o W b fuel a).snd
chunk_good (o : Nat → Int) (W : Int) (w : Nat × Nat) : (∀ (p : Nat × Nat), p ∈ (chunk o W w).fst → Good o W p) ∧ Good o W (chunk o W w).snd
fill_good (o : Nat → Int) (W : Int) (ws : List (Nat × Nat)) (cur : Nat × Nat) : Good o W cur → ∀ (l : Nat × Nat), l ∈ fill o W cur ws → Good o W l
breakAll_good (o : Nat → Int) (W : Int) (ws : List (Nat × Nat)) (l : Nat × Nat) : l ∈ breakAll o W ws → Good o W l
allLines_fit (o : Nat → Int) (W : Int) (cs : List Char) (l : Nat × Nat) : l ∈ allLines o W cs → o l.snd - o l.fst ≤ W ∨ l.snd ≤ l.fst + 1
Lines fit. Every line is at most W wide, or is a single scalar.
le {sp : Nat → Prop} {len p : Nat} {rs : List (Nat × Nat)}
(h : Cover sp len p rs) : p ≤ len
wordsFrom_cover (cs rest : List Char) (i : Nat) : i + rest.length = cs.length → (∀ (k : Nat), rest[k]? = cs[i + k]?) → ∀ (cur : Option Nat) (p : Nat), (match cur with | none => p ≤ i ∧ ∀ (k : Nat), p ≤ k → k < i → cs[k]? = some ' ' | some a => p ≤ a ∧ a < i ∧ ∀ (k : Nat), p ≤ k → k < a → cs[k]? = some ' ') → Cover (fun k => cs[k]? = some ' ') cs.length p (wordsFrom rest i cur)
Words cover the text: what lies between and around them is break spaces.
words_cover (cs : List Char) :
Cover (fun k => cs[k]? = some ' ') cs.length 0 (words cs)
chunkGo_cover {sp : Nat → Prop} {len : Nat} (o : Nat → Int) (W : Int)
(b : Nat) (rs : List (Nat × Nat)) (fuel a p : Nat) :
Cover sp len p ((a, b) :: rs) →
Cover sp len p ((chunkGo o W b fuel a).fst ++ (chunkGo o W b fuel a).snd :: rs)
chunk_cover {sp : Nat → Prop} {len : Nat} (o : Nat → Int) (W : Int)
(w : Nat × Nat) (rs : List (Nat × Nat)) {p : Nat} (h : Cover sp len p (w :: rs)) :
Cover sp len p ((chunk o W w).fst ++ (chunk o W w).snd :: rs)
append {sp : Nat → Prop} {len : Nat} {x : Nat × Nat}
{ws F : List (Nat × Nat)} (hF : ∀ (q : Nat), Cover sp len q (x :: ws) → Cover sp len q F)
(pre : List (Nat × Nat)) (p : Nat) :
Cover sp len p (pre ++ x :: ws) → Cover sp len p (pre ++ F)Replacing what follows a prefix keeps a cover, if it keeps the cover from where the prefix ends.
merge {sp : Nat → Prop} {len p a b c d : Nat} {rs : List (Nat × Nat)}
(h : Cover sp len p ((a, b) :: (c, d) :: rs)) : Cover sp len p ((a, d) :: rs)
fill_cover {sp : Nat → Prop} {len : Nat} (o : Nat → Int) (W : Int)
(ws : List (Nat × Nat)) (cur : Nat × Nat) (p : Nat) :
Cover sp len p (cur :: ws) → Cover sp len p (fill o W cur ws)
breakAll_cover {sp : Nat → Prop} {len : Nat} (o : Nat → Int) (W : Int)
{p : Nat} {ws : List (Nat × Nat)} : Cover sp len p ws → Cover sp len p (breakAll o W ws)
allLines_cover (o : Nat → Int) (W : Int) (cs : List Char) : Cover (fun k => cs[k]? = some ' ') cs.length 0 (allLines o W cs)
Lines cover the text. The lines are nonempty, in order, within the text, and every scalar outside them is a break space.
spaces_of_gap {cs : List Char} {p q : Nat}
(h : ∀ (i : Nat), p ≤ i → i < q → cs[i]? = some ' ') (c : Char) :
c ∈ List.take (q - p) (List.drop p cs) → c = ' '
tiles {cs : List Char} {p : Nat} {rs : List (Nat × Nat)}
(h : Cover (fun k => cs[k]? = some ' ') cs.length p rs) :
Tiles (List.drop p cs) (List.map (slice cs) rs)
allLines_tiles (o : Nat → Int) (W : Int) (cs : List Char) : Tiles cs (List.map (slice cs) (allLines o W cs))
Lines tile the text. Put back between and around the lines, break spaces alone rebuild the text.
keepLines_length_le {α : Type} (n : Nat) (k : Keep) (ls : List α) :
(keepLines (some n) k ls).length ≤ n
lines_length_le (o : Nat → Int) (W : Int) (wr : Wrap) (cs : List Char) (n : Nat) (h : wr.maxLines = some n) : (lines o W wr cs).length ≤ n
Line count. At most maxLines lines.
lines_tail (o : Nat → Int) (W : Int) (wr : Wrap) (cs : List Char) (n : Nat) (hm : wr.maxLines = some n) (hk : wr.keep = Keep.tail) : ∃ pre, pre ++ lines o W wr cs = allLines o W cs ∧ (lines o W wr cs).length = min n (allLines o W cs).length
Keep tail. The lines shown are exactly the last min n k of all k lines.
lines_head (o : Nat → Int) (W : Int) (wr : Wrap) (cs : List Char) (n : Nat) (hm : wr.maxLines = some n) (hk : wr.keep = Keep.head) : ∃ post, lines o W wr cs ++ post = allLines o W cs ∧ (lines o W wr cs).length = min n (allLines o W cs).length
Keep head. The lines shown are exactly the first min n k.
lines_none (o : Nat → Int) (W : Int) (wr : Wrap) (cs : List Char) (hm : wr.maxLines = none) : lines o W wr cs = allLines o W cs
Without maxLines, every line is shown.
mem_lines (o : Nat → Int) (W : Int) (wr : Wrap) (cs : List Char) {l : Nat × Nat} (h : l ∈ lines o W wr cs) : l ∈ allLines o W cs
Every line shown is one of the lines, so it fits.
lines_fit (o : Nat → Int) (W : Int) (wr : Wrap) (cs : List Char) (l : Nat × Nat) : l ∈ lines o W wr cs → o l.snd - o l.fst ≤ W ∨ l.snd ≤ l.fst + 1