Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+β Ctrl+β to navigate,
Ctrl+π±οΈ to focus.
On Mac, use
Cmd instead of
Ctrl .
import Pretty.Defs.Basic
import Pretty.Tactic
/-!
## Theorems about the rendering relation ($β_\mathcal{R}$)
-/
/--
Determinism of the rendering relation (Section 3.3)
-/
theorem Render_deterministic : β {d : Doc } {c i : β } {Lβ Lβ : Layout }, Render d c i Lβ Render d c i Lβ Lβ = Lβ Render_deterministic ( hβ : Render d c i Lβ ) ( hβ : Render d c i Lβ ) : Lβ = Lβ := by
induction hβ generalizing Lβ text { fst := sβ , rst := [] } = Lβ nl concat_one { fst := sβ ++ tβ rst := tsβ } = Lβ concat_multi nest align
case text =>
{ fst := sβ , rst := [] } = Lβ dwi { { fst := sβ , rst := [] } = Lβ cases hβ text { fst := sβ , rst := [] } = { fst := sβ , rst := [] } }
case nl =>
dwi { cases hβ }
case nest ih : ?m.117 dβ cβ (iβ + nβ Lβ hβ ih =>
cases hβ
case nest h : Render dβ cβ (iβ + nβ Lβ h => exact ih : ?m.117 dβ cβ (iβ + nβ Lβ hβ ih h : Render dβ cβ (iβ + nβ Lβ h
case align ih : ?m.117 dβ cβ cβ Lβ hβ
ih =>
cases hβ
case align h => exact ih : ?m.117 dβ cβ cβ Lβ hβ
ih h
case concat_one ihβ : ?m.117 dββ cβ iβ { fst := sβ , rst := [] } hββ
ihβ ihβ : ?m.117 dββ (cβ + String.length sβ iβ { fst := tβ , rst := tsβ } hββ ihβ =>
{ fst := sβ ++ tβ rst := tsβ } = Lβ cases hβ d : Doc c, i : β Lβ : Layout dββ : Doc cβ, iβ : β sβΒΉ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String hββΒΉ : Render dββ cβ iβ { fst := sβΒΉ , rst := [] } hββΒΉ : Render dββ (cβ + String.length sβΒΉ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβΒΉ , rst := [] } = Lβ ihβ : β {Lβ : Layout }, Render dββ (cβ + String.length sβΒΉ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ sβ, tβ : String tsβ : List String hββ : Render dββ cβ iβ { fst := sβ , rst := [] } hββ : Render dββ (cβ + String.length sβ iβ { fst := tβ , rst := tsβ } concat_one { fst := sβΒΉ ++ tβΒΉ rst := tsβΒΉ } = { fst := sβ ++ tβ rst := tsβ } d : Doc c, i : β Lβ : Layout dββ : Doc cβ, iβ : β sβΒΉ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String hββΒΉ : Render dββ cβ iβ { fst := sβΒΉ , rst := [] } hββΒΉ : Render dββ (cβ + String.length sβΒΉ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβΒΉ , rst := [] } = Lβ ihβ : β {Lβ : Layout }, Render dββ (cβ + String.length sβΒΉ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ ssβ : List String slastβ, sβ, tβ : String tsβ : List String h_non_emptyβ : ssβ β [] h_lastβ : slastβ = List.getLast ssβ h_non_emptyβ hββ : Render dββ (String.length slastβ iβ { fst := tβ , rst := tsβ } hββ : Render dββ cβ iβ { fst := sβ , rst := ssβ } concat_multi { fst := sβΒΉ ++ tβΒΉ rst := tsβΒΉ } = { fst := sβ , rst := List.dropLast ssβ ++ [slastβ ++ tβ ++ tsβ
{ fst := sβ ++ tβ rst := tsβ } = Lβ case concat_one hβ : Render dββ cβ iβ { fst := sβ , rst := [] } hβ hβ =>
d : Doc c, i : β Lβ : Layout dββ : Doc cβ, iβ : β sβΒΉ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String hββ : Render dββ cβ iβ { fst := sβΒΉ , rst := [] } hββ : Render dββ (cβ + String.length sβΒΉ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβΒΉ , rst := [] } = Lβ ihβ : β {Lβ : Layout }, Render dββ (cβ + String.length sβΒΉ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ sβ, tβ : String tsβ : List String hβ : Render dββ cβ iβ { fst := sβ , rst := [] } hβ : Render dββ (cβ + String.length sβ iβ { fst := tβ , rst := tsβ } { fst := sβΒΉ ++ tβΒΉ rst := tsβΒΉ } = { fst := sβ ++ tβ rst := tsβ } cases ihβ : ?m.117 dββ cβ iβ { fst := sβΒΉ , rst := [] } hββ
ihβ hβ : Render dββ cβ iβ { fst := sβ , rst := [] } hβ d : Doc c, i : β Lβ : Layout dββ : Doc cβ, iβ : β sβ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String hββ : Render dββ cβ iβ { fst := sβ , rst := [] } hββ : Render dββ (cβ + String.length sβ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβ , rst := [] } = Lβ ihβ : β {Lβ : Layout }, Render dββ (cβ + String.length sβ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ tβ : String tsβ : List String hβ : Render dββ cβ iβ { fst := sβ , rst := [] } hβ : Render dββ (cβ + String.length sβ iβ { fst := tβ , rst := tsβ } refl { fst := sβ ++ tβΒΉ rst := tsβΒΉ } = { fst := sβ ++ tβ rst := tsβ }
d : Doc c, i : β Lβ : Layout dββ : Doc cβ, iβ : β sβΒΉ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String hββ : Render dββ cβ iβ { fst := sβΒΉ , rst := [] } hββ : Render dββ (cβ + String.length sβΒΉ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβΒΉ , rst := [] } = Lβ ihβ : β {Lβ : Layout }, Render dββ (cβ + String.length sβΒΉ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ sβ, tβ : String tsβ : List String hβ : Render dββ cβ iβ { fst := sβ , rst := [] } hβ : Render dββ (cβ + String.length sβ iβ { fst := tβ , rst := tsβ } { fst := sβΒΉ ++ tβΒΉ rst := tsβΒΉ } = { fst := sβ ++ tβ rst := tsβ } cases ihβ : ?m.117 dββ (cβ + String.length sβ iβ { fst := tβΒΉ , rst := tsβΒΉ } hββ ihβ hβ d : Doc c, i : β Lβ : Layout dββ : Doc cβ, iβ : β sβ : String dββ : Doc tβ : String tsβ : List String hββ : Render dββ cβ iβ { fst := sβ , rst := [] } hββ : Render dββ (cβ + String.length sβ iβ { fst := tβ , rst := tsβ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβ , rst := [] } = Lβ ihβ : β {Lβ : Layout }, Render dββ (cβ + String.length sβ iβ Lβ { fst := tβ , rst := tsβ } = Lβ hβ : Render dββ cβ iβ { fst := sβ , rst := [] } hβ : Render dββ (cβ + String.length sβ iβ { fst := tβ , rst := tsβ } refl.refl { fst := sβ ++ tβ rst := tsβ } = { fst := sβ ++ tβ rst := tsβ }
d : Doc c, i : β Lβ : Layout dββ : Doc cβ, iβ : β sβΒΉ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String hββ : Render dββ cβ iβ { fst := sβΒΉ , rst := [] } hββ : Render dββ (cβ + String.length sβΒΉ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβΒΉ , rst := [] } = Lβ ihβ : β {Lβ : Layout }, Render dββ (cβ + String.length sβΒΉ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ sβ, tβ : String tsβ : List String hβ : Render dββ cβ iβ { fst := sβ , rst := [] } hβ : Render dββ (cβ + String.length sβ iβ { fst := tβ , rst := tsβ } { fst := sβΒΉ ++ tβΒΉ rst := tsβΒΉ } = { fst := sβ ++ tβ rst := tsβ } rfl
{ fst := sβ ++ tβ rst := tsβ } = Lβ case concat_multi hβ : Render dββ cβ iβ { fst := sβ , rst := ssβ } hβ =>
d : Doc c, i : β Lβ : Layout dββ : Doc cβ, iβ : β sβΒΉ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String hββ : Render dββ cβ iβ { fst := sβΒΉ , rst := [] } hββΒΉ : Render dββ (cβ + String.length sβΒΉ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβΒΉ , rst := [] } = Lβ ihβ : β {Lβ : Layout }, Render dββ (cβ + String.length sβΒΉ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ ssβ : List String slastβ, sβ, tβ : String tsβ : List String h_non_emptyβ : ssβ β [] h_lastβ : slastβ = List.getLast ssβ h_non_emptyβ hββ : Render dββ (String.length slastβ iβ { fst := tβ , rst := tsβ } hβ : Render dββ cβ iβ { fst := sβ , rst := ssβ } { fst := sβΒΉ ++ tβΒΉ rst := tsβΒΉ } = { fst := sβ , rst := List.dropLast ssβ ++ [slastβ ++ tβ ++ tsβ dwi { d : Doc c, i : β Lβ : Layout dββ : Doc cβ, iβ : β sβΒΉ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String hββ : Render dββ cβ iβ { fst := sβΒΉ , rst := [] } hββΒΉ : Render dββ (cβ + String.length sβΒΉ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβΒΉ , rst := [] } = Lβ ihβ : β {Lβ : Layout }, Render dββ (cβ + String.length sβΒΉ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ ssβ : List String slastβ, sβ, tβ : String tsβ : List String h_non_emptyβ : ssβ β [] h_lastβ : slastβ = List.getLast ssβ h_non_emptyβ hββ : Render dββ (String.length slastβ iβ { fst := tβ , rst := tsβ } hβ : Render dββ cβ iβ { fst := sβ , rst := ssβ } { fst := sβΒΉ ++ tβΒΉ rst := tsβΒΉ } = { fst := sβ , rst := List.dropLast ssβ ++ [slastβ ++ tβ ++ tsβ cases ihβ : ?m.117 dββ cβ iβ { fst := sβΒΉ , rst := [] } hββ
ihβ hβ : Render dββ cβ iβ { fst := sβ , rst := ssβ } hβ d : Doc c, i : β Lβ : Layout dββ : Doc cβ, iβ : β sβ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String hββ : Render dββ cβ iβ { fst := sβ , rst := [] } hββΒΉ : Render dββ (cβ + String.length sβ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβ , rst := [] } = Lβ ihβ : β {Lβ : Layout }, Render dββ (cβ + String.length sβ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ slastβ, tβ : String tsβ : List String hββ : Render dββ (String.length slastβ iβ { fst := tβ , rst := tsβ } h_non_emptyβ : [] β [] h_lastβ : slastβ = List.getLast [] h_non_emptyβ hβ : Render dββ cβ iβ { fst := sβ , rst := [] } refl { fst := sβ ++ tβΒΉ rst := tsβΒΉ } = { fst := sβ , rst := List.dropLast [] ++ [slastβ ++ tβ ++ tsβ }
case concat_multi h_lastβ _ _ ihβ : ?m.117 dββ cβ iβ { fst := sβ , rst := ssβ } hββ
ihβ ihβ : ?m.117 dββ (String.length slastβ iβ { fst := tβ , rst := tsβ } hββ ihβ =>
cases hβ d : Doc c, i : β Lβ : Layout ssβ : List String slastβ : String dββ : Doc cβ, iβ : β sβΒΉ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String h_non_emptyβ : ssβ β [] h_lastβ : slastβ = List.getLast ssβ h_non_emptyβ hββΒΉ : Render dββ cβ iβ { fst := sβΒΉ , rst := ssβ } hββΒΉ : Render dββ (String.length slastβ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβΒΉ , rst := ssβ } = Lβ ihβ : β {Lβ : Layout }, Render dββ (String.length slastβ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ sβ, tβ : String tsβ : List String hββ : Render dββ cβ iβ { fst := sβ , rst := [] } hββ : Render dββ (cβ + String.length sβ iβ { fst := tβ , rst := tsβ } concat_one { fst := sβΒΉ , rst := List.dropLast ssβ ++ [slastβ ++ tβΒΉ ++ tsβΒΉ = { fst := sβ ++ tβ rst := tsβ } d : Doc c, i : β Lβ : Layout ssβΒΉ : List String slastβΒΉ : String dββ : Doc cβ, iβ : β sβΒΉ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String h_non_emptyβΒΉ : ssβΒΉ β [] h_lastβ : slastβΒΉ = List.getLast ssβΒΉ h_non_emptyβΒΉ hββΒΉ : Render dββ cβ iβ { fst := sβΒΉ , rst := ssβΒΉ } hββΒΉ : Render dββ (String.length slastβΒΉ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβΒΉ , rst := ssβΒΉ } = Lβ ihβ : β {Lβ : Layout }, Render dββ (String.length slastβΒΉ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ ssβ : List String slastβ, sβ, tβ : String tsβ : List String h_non_emptyβ : ssβ β [] h_lastβ : slastβ = List.getLast ssβ h_non_emptyβ hββ : Render dββ (String.length slastβ iβ { fst := tβ , rst := tsβ } hββ : Render dββ cβ iβ { fst := sβ , rst := ssβ } concat_multi
case concat_one hβ : Render dββ cβ iβ { fst := sβ , rst := [] } hβ _ =>
d : Doc c, i : β Lβ : Layout ssβ : List String slastβ : String dββ : Doc cβ, iβ : β sβΒΉ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String h_non_emptyβ : ssβ β [] h_lastβ : slastβ = List.getLast ssβ h_non_emptyβ hββ : Render dββ cβ iβ { fst := sβΒΉ , rst := ssβ } hββΒΉ : Render dββ (String.length slastβ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβΒΉ , rst := ssβ } = Lβ ihβ : β {Lβ : Layout }, Render dββ (String.length slastβ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ sβ, tβ : String tsβ : List String hβ : Render dββ cβ iβ { fst := sβ , rst := [] } hββ : Render dββ (cβ + String.length sβ iβ { fst := tβ , rst := tsβ } { fst := sβΒΉ , rst := List.dropLast ssβ ++ [slastβ ++ tβΒΉ ++ tsβΒΉ = { fst := sβ ++ tβ rst := tsβ } dwi { d : Doc c, i : β Lβ : Layout ssβ : List String slastβ : String dββ : Doc cβ, iβ : β sβΒΉ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String h_non_emptyβ : ssβ β [] h_lastβ : slastβ = List.getLast ssβ h_non_emptyβ hββ : Render dββ cβ iβ { fst := sβΒΉ , rst := ssβ } hββΒΉ : Render dββ (String.length slastβ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβΒΉ , rst := ssβ } = Lβ ihβ : β {Lβ : Layout }, Render dββ (String.length slastβ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ sβ, tβ : String tsβ : List String hβ : Render dββ cβ iβ { fst := sβ , rst := [] } hββ : Render dββ (cβ + String.length sβ iβ { fst := tβ , rst := tsβ } { fst := sβΒΉ , rst := List.dropLast ssβ ++ [slastβ ++ tβΒΉ ++ tsβΒΉ = { fst := sβ ++ tβ rst := tsβ } cases ihβ : ?m.117 dββ cβ iβ { fst := sβΒΉ , rst := ssβ } hββ
ihβ hβ : Render dββ cβ iβ { fst := sβ , rst := [] } hβ d : Doc c, i : β Lβ : Layout slastβ : String dββ : Doc cβ, iβ : β sβ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String hββΒΉ : Render dββ (String.length slastβ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ (String.length slastβ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ tβ : String tsβ : List String hβ : Render dββ cβ iβ { fst := sβ , rst := [] } hββ : Render dββ (cβ + String.length sβ iβ { fst := tβ , rst := tsβ } h_non_emptyβ : [] β [] h_lastβ : slastβ = List.getLast [] h_non_emptyβ hββ : Render dββ cβ iβ { fst := sβ , rst := [] } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβ , rst := [] } = Lβ refl { fst := sβ , rst := List.dropLast [] ++ [slastβ ++ tβΒΉ ++ tsβΒΉ = { fst := sβ ++ tβ rst := tsβ } }
case concat_multi h_lastβ hβ hβ : Render dββ cβ iβ { fst := sβ , rst := ssβ } hβ =>
d : Doc c, i : β Lβ : Layout ssβΒΉ : List String slastβΒΉ : String dββ : Doc cβ, iβ : β sβΒΉ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String h_non_emptyβΒΉ : ssβΒΉ β [] h_lastβ : slastβΒΉ = List.getLast ssβΒΉ h_non_emptyβΒΉ hββ : Render dββ cβ iβ { fst := sβΒΉ , rst := ssβΒΉ } hββ : Render dββ (String.length slastβΒΉ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβΒΉ , rst := ssβΒΉ } = Lβ ihβ : β {Lβ : Layout }, Render dββ (String.length slastβΒΉ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ ssβ : List String slastβ, sβ, tβ : String tsβ : List String h_non_emptyβ : ssβ β [] h_lastβ : slastβ = List.getLast ssβ h_non_emptyβ hβ : Render dββ (String.length slastβ iβ { fst := tβ , rst := tsβ } hβ : Render dββ cβ iβ { fst := sβ , rst := ssβ } cases ihβ : ?m.117 dββ cβ iβ { fst := sβΒΉ , rst := ssβΒΉ } hββ
ihβ hβ : Render dββ cβ iβ { fst := sβ , rst := ssβ } hβ d : Doc c, i : β Lβ : Layout ssβ : List String slastβΒΉ : String dββ : Doc cβ, iβ : β sβ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String h_non_emptyβΒΉ : ssβ β [] h_lastβ : slastβΒΉ = List.getLast ssβ h_non_emptyβΒΉ hββ : Render dββ cβ iβ { fst := sβ , rst := ssβ } hββ : Render dββ (String.length slastβΒΉ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβ , rst := ssβ } = Lβ ihβ : β {Lβ : Layout }, Render dββ (String.length slastβΒΉ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ slastβ, tβ : String tsβ : List String hβ : Render dββ (String.length slastβ iβ { fst := tβ , rst := tsβ } h_non_emptyβ : ssβ β [] h_lastβ : slastβ = List.getLast ssβ h_non_emptyβ hβ : Render dββ cβ iβ { fst := sβ , rst := ssβ } refl
d : Doc c, i : β Lβ : Layout ssβΒΉ : List String slastβΒΉ : String dββ : Doc cβ, iβ : β sβΒΉ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String h_non_emptyβΒΉ : ssβΒΉ β [] h_lastβ : slastβΒΉ = List.getLast ssβΒΉ h_non_emptyβΒΉ hββ : Render dββ cβ iβ { fst := sβΒΉ , rst := ssβΒΉ } hββ : Render dββ (String.length slastβΒΉ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβΒΉ , rst := ssβΒΉ } = Lβ ihβ : β {Lβ : Layout }, Render dββ (String.length slastβΒΉ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ ssβ : List String slastβ, sβ, tβ : String tsβ : List String h_non_emptyβ : ssβ β [] h_lastβ : slastβ = List.getLast ssβ h_non_emptyβ hβ : Render dββ (String.length slastβ iβ { fst := tβ , rst := tsβ } hβ : Render dββ cβ iβ { fst := sβ , rst := ssβ } subst h_lastβ h_lastβ d : Doc c, i : β Lβ : Layout ssβ : List String dββ : Doc cβ, iβ : β sβ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String h_non_emptyβΒΉ : ssβ β [] hββ : Render dββ cβ iβ { fst := sβ , rst := ssβ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβ , rst := ssβ } = Lβ tβ : String tsβ : List String h_non_emptyβ : ssβ β [] hβ : Render dββ cβ iβ { fst := sβ , rst := ssβ } hββ : Render dββ (String.length (List.getLast ssβ h_non_emptyβΒΉ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ (String.length (List.getLast ssβ h_non_emptyβΒΉ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ hβ : Render dββ (String.length (List.getLast ssβ h_non_emptyβ iβ { fst := tβ , rst := tsβ } refl
d : Doc c, i : β Lβ : Layout ssβΒΉ : List String slastβΒΉ : String dββ : Doc cβ, iβ : β sβΒΉ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String h_non_emptyβΒΉ : ssβΒΉ β [] h_lastβ : slastβΒΉ = List.getLast ssβΒΉ h_non_emptyβΒΉ hββ : Render dββ cβ iβ { fst := sβΒΉ , rst := ssβΒΉ } hββ : Render dββ (String.length slastβΒΉ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβΒΉ , rst := ssβΒΉ } = Lβ ihβ : β {Lβ : Layout }, Render dββ (String.length slastβΒΉ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ ssβ : List String slastβ, sβ, tβ : String tsβ : List String h_non_emptyβ : ssβ β [] h_lastβ : slastβ = List.getLast ssβ h_non_emptyβ hβ : Render dββ (String.length slastβ iβ { fst := tβ , rst := tsβ } hβ : Render dββ cβ iβ { fst := sβ , rst := ssβ } cases ihβ hβ d : Doc c, i : β Lβ : Layout ssβ : List String dββ : Doc cβ, iβ : β sβ : String dββ : Doc tβ : String tsβ : List String h_non_emptyβΒΉ : ssβ β [] hββ : Render dββ cβ iβ { fst := sβ , rst := ssβ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβ , rst := ssβ } = Lβ h_non_emptyβ : ssβ β [] hβ : Render dββ cβ iβ { fst := sβ , rst := ssβ } hββ : Render dββ (String.length (List.getLast ssβ h_non_emptyβΒΉ iβ { fst := tβ , rst := tsβ } ihβ : β {Lβ : Layout }, Render dββ (String.length (List.getLast ssβ h_non_emptyβΒΉ iβ Lβ { fst := tβ , rst := tsβ } = Lβ hβ : Render dββ (String.length (List.getLast ssβ h_non_emptyβ iβ { fst := tβ , rst := tsβ } refl.refl
d : Doc c, i : β Lβ : Layout ssβΒΉ : List String slastβΒΉ : String dββ : Doc cβ, iβ : β sβΒΉ : String dββ : Doc tβΒΉ : String tsβΒΉ : List String h_non_emptyβΒΉ : ssβΒΉ β [] h_lastβ : slastβΒΉ = List.getLast ssβΒΉ h_non_emptyβΒΉ hββ : Render dββ cβ iβ { fst := sβΒΉ , rst := ssβΒΉ } hββ : Render dββ (String.length slastβΒΉ iβ { fst := tβΒΉ , rst := tsβΒΉ } ihβ : β {Lβ : Layout }, Render dββ cβ iβ Lβ { fst := sβΒΉ , rst := ssβΒΉ } = Lβ ihβ : β {Lβ : Layout }, Render dββ (String.length slastβΒΉ iβ Lβ { fst := tβΒΉ , rst := tsβΒΉ } = Lβ ssβ : List String slastβ, sβ, tβ : String tsβ : List String h_non_emptyβ : ssβ β [] h_lastβ : slastβ = List.getLast ssβ h_non_emptyβ hβ : Render dββ (String.length slastβ iβ { fst := tβ , rst := tsβ } hβ : Render dββ cβ iβ { fst := sβ , rst := ssβ } rfl
/--
Totality of the rendering relation (Section 3.3)
-/
theorem Render_total ( c i : β ) ( h : Choiceless d ) : β L , Render d c i L := by
dwi { induction d generalizing c i text nl concat nest align choice }
case text s =>
exists β¨ s , [] β©
constructor
case nl =>
exists β¨ "" , [ List.asString ( List.replicate : {Ξ± : Type ?u.11226} β β β Ξ± β List Ξ± i ' ' )]β©
constructor
case concat ihβ ihβ =>
cases h
case concat hβ hβ =>
let β¨β¨ s , ss β©, hβ : Render dββ c i { fst := s , rst := ss } hβ β© := @ ihβ c i hβ
cases ss
case nil =>
let β¨ Lβ , _β© := @ ihβ ( c + s . length ) i hβ
exists β¨ s ++ Lβ . fst , Lβ . rst β©
dwi { constructor hβ Render dββ c i { fst := s , rst := [] } hβ }
case cons hd tl =>
let β¨ Lβ , _β© := @ ihβ ( List.getLast : {Ξ± : Type ?u.17899} β (as : List Ξ± as β [] Ξ± ( hd :: tl ) ( by simp )). length i hβ
exists β¨ s , ( List.dropLast ( hd :: tl )) ++ [ List.getLast : {Ξ± : Type ?u.18191} β (as : List Ξ± as β [] Ξ± ( hd :: tl ) ( by simp ) ++ Lβ . fst ] ++ Lβ . rst β©
dwi { constructor h_last hβ Render dββ c i { fst := s , rst := hd :: tl hβ h_non_empty }
case nest n _ ih =>
cases h
case nest h =>
let β¨ L , _β© := @ ih c ( i + n ) h
exists L
dwi { constructor }
case align ih =>
cases h
case align h =>
let β¨ L , _β© := @ ih c c h
exists L
dwi { constructor }