Geb.Prototypes.ReadableSExpr — The Geb language

Geb
Prototypes
ReadableSExpr

Imports

/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module

public import Geb.Prototypes.ConcreteSyntax

A readable spelling of the rose syntax

Geb.Csexp.print and Geb.Ast.printViaRose are both [RFC9804] canonical: length-prefixed and whitespace-free, so neither has a readable form. This module spells the same Rose k as parenthesized text, a node's label followed by its children, so that fork (leaf 0) (fork (leaf 1) (leaf 2)) reads as (0 (1 2)).

The fragment lies inside [R7RS] <datum>: a reader conforming to that grammar accepts it without new code, and tools operating on parenthesized text apply to it directly. Labels are decimal numerals, which the [RFC9804] advanced form cannot spell as tokens — § 4.3 requires a token not begin with a digit — where [R7RS] and [EDN] read a digit-initial token as a number.

Main definitions

Rsexp.print — the readable spelling of a Rose k.

Rsexp.parse — the parser matching it, built from Rsexp.parseStep, Rsexp.parseAux and the shared Rose.parseChildren.

Rsexp.skipWs — the whitespace skip the stripping discipline runs.

Rsexp.printViaRose, Rsexp.parseViaRose — the composites with the rose bijection, spelling an Ast k.

Main statements

Rsexp.parse_print, Rsexp.parseViaRose_printViaRose — the retraction law, on Rose and on Ast, with Rsexp.format_idem and Rsexp.print_injective instantiating the generic corollaries.

Implementation notes

The parser strips whitespace on return rather than on entry: parseStep is called on stripped input and returns a stripped remainder. That discipline is what lets Rose.parseChildren be reused verbatim — the loop tests its input's head against ')' immediately, so it must be called on already-stripped input — and what lets parse match some (r, []) syntactically rather than testing a remainder for whitespace.

A childless node prints as a bare numeral, so a printed tree can end in a digit and parseAux_print carries a delimiting side condition on the caller's remainder. Always parenthesizing would remove the obligation and the spelling; Csexp.readDigits_append carries the same condition for the same reason.

References

[R7RS] §§ 4.1.3, 7.1.1, 7.1.2 — the datum grammar this fragment lies inside.

[EDN] — the second readable format the spelling agrees with.

[RFC9804] §§ 4.3, 6, 8 — the token rule that rules out the advanced form, and the conformance of declining it.

[RFC8259] § 2 — the ws production this whitespace class matches.

Whitespace

The whitespace class this syntax admits: space, horizontal tab, carriage return and line feed. It is a subset of the class [R7RS] § 7.1.1 fixes, and admits the same four characters as [RFC8259] § 2's ws.

def isWs (c : Char) : Bool :=
  c = ' ' || c = '\t' || c = '\r' || c = '\n'

Drop a leading run of whitespace. Carried by List.rec rather than by structural recursion, per the recursor rule.

def skipWs : List Char → List Char :=
  List.rec [] fun c cs ih ↦ if isWs c then ih else c :: cs

@[simp] theorem skipWs_nil : skipWs [] = [] := rfl

theorem skipWs_cons (c : Char) (cs : List Char) :
    skipWs (c :: cs) = if isWs c then skipWs cs else c :: cs := rfl

Printer

The readable spelling: a childless node is its label, a node with children is its label and their spellings, parenthesized and each preceded by one space. The uniform space is what makes every element of the child block a cons, which the arity bound and the whitespace skip both use.

def print {k : Nat} : Rose k → List Char :=
  WType.elim (List Char) fun x ↦
    match x with
    | ⟨(i, 0), _⟩ => Csexp.decOf i.val
    | ⟨(i, _ + 1), ch⟩ =>
      '(' :: (Csexp.decOf i.val
        ++ (((List.ofFn ch).map (fun s ↦ ' ' :: s)).flatten ++ [')']))

@[simp] theorem print_zero {k : Nat} (i : Fin k) (f : Fin 0 → Rose k) :
    print (Rose.node i f) = Csexp.decOf i.val := rfl

theorem print_succ {k n : Nat} (i : Fin k) (f : Fin (n + 1) → Rose k) :
    print (Rose.node i f)
      = '(' :: (Csexp.decOf i.val
          ++ (((List.ofFn f).map (fun t ↦ ' ' :: print t)).flatten
              ++ [')'])) := byk:ℕn:ℕi:Fin kf:Fin (n + 1) → Rose k⊢ print (Rose.node i f) = '(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn f)).flatten ++ [')']))
  unfold print Rose.nodek:ℕn:ℕi:Fin kf:Fin (n + 1) → Rose k⊢ WType.elim (List Char)
    (fun x ↦
      match x with
      | ⟨(i, 0), snd⟩ => Csexp.decOf ↑i
      | ⟨(i, n.succ), ch⟩ => '(' :: (Csexp.decOf ↑i ++ ((List.map (fun s ↦ ' ' :: s) (List.ofFn ch)).flatten ++ [')'])))
    (WType.mk (i, n + 1) f) =
  '(' ::
    (Csexp.decOf ↑i ++
      ((List.map
            (fun t ↦
              ' ' ::
                WType.elim (List Char)
                  (fun x ↦
                    match x with
                    | ⟨(i, 0), snd⟩ => Csexp.decOf ↑i
                    | ⟨(i, n.succ), ch⟩ =>
                      '(' :: (Csexp.decOf ↑i ++ ((List.map (fun s ↦ ' ' :: s) (List.ofFn ch)).flatten ++ [')'])))
                  t)
            (List.ofFn f)).flatten ++
        [')']))
  rw [WType.elim_mkk:ℕn:ℕi:Fin kf:Fin (n + 1) → Rose k⊢ (match
    ⟨(i, n + 1), fun b ↦
      WType.elim (List Char)
        (fun x ↦
          match x with
          | ⟨(i, 0), snd⟩ => Csexp.decOf ↑i
          | ⟨(i, n.succ), ch⟩ =>
            '(' :: (Csexp.decOf ↑i ++ ((List.map (fun s ↦ ' ' :: s) (List.ofFn ch)).flatten ++ [')'])))
        (f b)⟩ with
  | ⟨(i, 0), snd⟩ => Csexp.decOf ↑i
  | ⟨(i, n.succ), ch⟩ => '(' :: (Csexp.decOf ↑i ++ ((List.map (fun s ↦ ' ' :: s) (List.ofFn ch)).flatten ++ [')']))) =
  '(' ::
    (Csexp.decOf ↑i ++
      ((List.map
            (fun t ↦
              ' ' ::
                WType.elim (List Char)
                  (fun x ↦
                    match x with
                    | ⟨(i, 0), snd⟩ => Csexp.decOf ↑i
                    | ⟨(i, n.succ), ch⟩ =>
                      '(' :: (Csexp.decOf ↑i ++ ((List.map (fun s ↦ ' ' :: s) (List.ofFn ch)).flatten ++ [')'])))
                  t)
            (List.ofFn f)).flatten ++
        [')']))]k:ℕn:ℕi:Fin kf:Fin (n + 1) → Rose k⊢ (match
    ⟨(i, n + 1), fun b ↦
      WType.elim (List Char)
        (fun x ↦
          match x with
          | ⟨(i, 0), snd⟩ => Csexp.decOf ↑i
          | ⟨(i, n.succ), ch⟩ =>
            '(' :: (Csexp.decOf ↑i ++ ((List.map (fun s ↦ ' ' :: s) (List.ofFn ch)).flatten ++ [')'])))
        (f b)⟩ with
  | ⟨(i, 0), snd⟩ => Csexp.decOf ↑i
  | ⟨(i, n.succ), ch⟩ => '(' :: (Csexp.decOf ↑i ++ ((List.map (fun s ↦ ' ' :: s) (List.ofFn ch)).flatten ++ [')']))) =
  '(' ::
    (Csexp.decOf ↑i ++
      ((List.map
            (fun t ↦
              ' ' ::
                WType.elim (List Char)
                  (fun x ↦
                    match x with
                    | ⟨(i, 0), snd⟩ => Csexp.decOf ↑i
                    | ⟨(i, n.succ), ch⟩ =>
                      '(' :: (Csexp.decOf ↑i ++ ((List.map (fun s ↦ ' ' :: s) (List.ofFn ch)).flatten ++ [')'])))
                  t)
            (List.ofFn f)).flatten ++
        [')']))
  -- reduce the match `WType.elim_mk` exposed, picking the `n.succ` arm
  simp only []k:ℕn:ℕi:Fin kf:Fin (n + 1) → Rose k⊢ '(' ::
    (Csexp.decOf ↑i ++
      ((List.map (fun s ↦ ' ' :: s)
            (List.ofFn fun b ↦
              WType.elim (List Char)
                (fun x ↦
                  match x with
                  | ⟨(i, 0), snd⟩ => Csexp.decOf ↑i
                  | ⟨(i, n.succ), ch⟩ =>
                    '(' :: (Csexp.decOf ↑i ++ ((List.map (fun s ↦ ' ' :: s) (List.ofFn ch)).flatten ++ [')'])))
                (f b))).flatten ++
        [')'])) =
  '(' ::
    (Csexp.decOf ↑i ++
      ((List.map
            (fun t ↦
              ' ' ::
                WType.elim (List Char)
                  (fun x ↦
                    match x with
                    | ⟨(i, 0), snd⟩ => Csexp.decOf ↑i
                    | ⟨(i, n.succ), ch⟩ =>
                      '(' :: (Csexp.decOf ↑i ++ ((List.map (fun s ↦ ' ' :: s) (List.ofFn ch)).flatten ++ [')'])))
                  t)
            (List.ofFn f)).flatten ++
        [')']))
  rw [List.map_ofFn,k:ℕn:ℕi:Fin kf:Fin (n + 1) → Rose k⊢ '(' ::
    (Csexp.decOf ↑i ++
      ((List.ofFn
            ((fun s ↦ ' ' :: s) ∘ fun b ↦
              WType.elim (List Char)
                (fun x ↦
                  match x with
                  | ⟨(i, 0), snd⟩ => Csexp.decOf ↑i
                  | ⟨(i, n.succ), ch⟩ =>
                    '(' :: (Csexp.decOf ↑i ++ ((List.map (fun s ↦ ' ' :: s) (List.ofFn ch)).flatten ++ [')'])))
                (f b))).flatten ++
        [')'])) =
  '(' ::
    (Csexp.decOf ↑i ++
      ((List.map
            (fun t ↦
              ' ' ::
                WType.elim (List Char)
                  (fun x ↦
                    match x with
                    | ⟨(i, 0), snd⟩ => Csexp.decOf ↑i
                    | ⟨(i, n.succ), ch⟩ =>
                      '(' :: (Csexp.decOf ↑i ++ ((List.map (fun s ↦ ' ' :: s) (List.ofFn ch)).flatten ++ [')'])))
                  t)
            (List.ofFn f)).flatten ++
        [')'])) List.map_ofFnk:ℕn:ℕi:Fin kf:Fin (n + 1) → Rose k⊢ '(' ::
    (Csexp.decOf ↑i ++
      ((List.ofFn
            ((fun s ↦ ' ' :: s) ∘ fun b ↦
              WType.elim (List Char)
                (fun x ↦
                  match x with
                  | ⟨(i, 0), snd⟩ => Csexp.decOf ↑i
                  | ⟨(i, n.succ), ch⟩ =>
                    '(' :: (Csexp.decOf ↑i ++ ((List.map (fun s ↦ ' ' :: s) (List.ofFn ch)).flatten ++ [')'])))
                (f b))).flatten ++
        [')'])) =
  '(' ::
    (Csexp.decOf ↑i ++
      ((List.ofFn
            ((fun t ↦
                ' ' ::
                  WType.elim (List Char)
                    (fun x ↦
                      match x with
                      | ⟨(i, 0), snd⟩ => Csexp.decOf ↑i
                      | ⟨(i, n.succ), ch⟩ =>
                        '(' :: (Csexp.decOf ↑i ++ ((List.map (fun s ↦ ' ' :: s) (List.ofFn ch)).flatten ++ [')'])))
                    t) ∘
              f)).flatten ++
        [')']))]k:ℕn:ℕi:Fin kf:Fin (n + 1) → Rose k⊢ '(' ::
    (Csexp.decOf ↑i ++
      ((List.ofFn
            ((fun s ↦ ' ' :: s) ∘ fun b ↦
              WType.elim (List Char)
                (fun x ↦
                  match x with
                  | ⟨(i, 0), snd⟩ => Csexp.decOf ↑i
                  | ⟨(i, n.succ), ch⟩ =>
                    '(' :: (Csexp.decOf ↑i ++ ((List.map (fun s ↦ ' ' :: s) (List.ofFn ch)).flatten ++ [')'])))
                (f b))).flatten ++
        [')'])) =
  '(' ::
    (Csexp.decOf ↑i ++
      ((List.ofFn
            ((fun t ↦
                ' ' ::
                  WType.elim (List Char)
                    (fun x ↦
                      match x with
                      | ⟨(i, 0), snd⟩ => Csexp.decOf ↑i
                      | ⟨(i, n.succ), ch⟩ =>
                        '(' :: (Csexp.decOf ↑i ++ ((List.map (fun s ↦ ' ' :: s) (List.ofFn ch)).flatten ++ [')'])))
                    t) ∘
              f)).flatten ++
        [')']))
  rflAll goals completed! 🐙

Character facts

The two parentheses are distinct characters.

theorem open_ne_close : ('(' : Char) ≠ ')' := by⊢ '(' ≠ ')' decideAll goals completed! 🐙

An opening parenthesis is not whitespace, so the whitespace skip stops at the head of a parenthesized spelling.

theorem open_not_ws : isWs '(' = false := by⊢ isWs '(' = false decideAll goals completed! 🐙

A closing parenthesis is not whitespace, so the whitespace skip stops at a child block's terminator.

theorem close_not_ws : isWs ')' = false := by⊢ isWs ')' = false decideAll goals completed! 🐙

A space is whitespace, so the whitespace skip consumes the separator the printer emits before each child.

theorem space_is_ws : isWs ' ' = true := by⊢ isWs ' ' = true decideAll goals completed! 🐙

The decimal layer

A printed numeral reads back whole, and leaves exactly what followed it. The delimiting hypothesis on the remainder is what a non-parenthesizing spelling of a childless node costs; it is the same condition Csexp.readDigits_append carries.

theorem readNat_append (n : Nat) (rest : List Char)
    (h : ∀ c cs, rest = c :: cs → Csexp.charDigit c = none) :
    Csexp.readNat (Csexp.decOf n ++ rest) = some (n, rest) := byn:ℕrest:List Charh:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none⊢ Csexp.readNat (Csexp.decOf n ++ rest) = some (n, rest)
  unfold Csexp.readNatn:ℕrest:List Charh:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none⊢ (match Csexp.readDigits (Csexp.decOf n ++ rest) with
  | (ds, r) => if ds.isEmpty = true then none else Option.map (fun x ↦ (x, r)) (Csexp.digitsVal ds)) =
  some (n, rest)
  rw [Csexp.readDigits_append _ _ (Csexp.decOf_all_digits n) hn:ℕrest:List Charh:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none⊢ (match (Csexp.decOf n, rest) with
  | (ds, r) => if ds.isEmpty = true then none else Option.map (fun x ↦ (x, r)) (Csexp.digitsVal ds)) =
  some (n, rest)]n:ℕrest:List Charh:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none⊢ (match (Csexp.decOf n, rest) with
  | (ds, r) => if ds.isEmpty = true then none else Option.map (fun x ↦ (x, r)) (Csexp.digitsVal ds)) =
  some (n, rest)
  simp [Csexp.decOf_ne_nil n, Csexp.digitsVal_decOf, List.isEmpty_iff]All goals completed! 🐙

A digit is not whitespace. The conclusion is isWs c = false rather than a disequality because the whitespace class has four members.

theorem digit_not_ws {c : Char} (h : (Csexp.charDigit c).isSome) :
    isWs c = false := byc:Charh:(Csexp.charDigit c).isSome = true⊢ isWs c = false
  unfold isWsc:Charh:(Csexp.charDigit c).isSome = true⊢ (decide (c = ' ') || decide (c = '\t') || decide (c = '\x0d') || decide (c = '\n')) = false
  have h1 : ¬ c = ' ' := byc:Charh:(Csexp.charDigit c).isSome = true⊢ isWs c = false rintro rflh:(Csexp.charDigit ' ').isSome = true⊢ False; exact absurd h (byh:(Csexp.charDigit ' ').isSome = true⊢ ¬(Csexp.charDigit ' ').isSome = true decideAll goals completed! 🐙)c:Charh:(Csexp.charDigit c).isSome = trueh1:¬c = ' '⊢ (decide (c = ' ') || decide (c = '\t') || decide (c = '\x0d') || decide (c = '\n')) = false
  have h2 : ¬ c = '\t' := byc:Charh:(Csexp.charDigit c).isSome = true⊢ isWs c = false rintro rflh:(Csexp.charDigit '\t').isSome = trueh1:¬'\t' = ' '⊢ False; exact absurd h (byh:(Csexp.charDigit '\t').isSome = trueh1:¬'\t' = ' '⊢ ¬(Csexp.charDigit '\t').isSome = true decideAll goals completed! 🐙)c:Charh:(Csexp.charDigit c).isSome = trueh1:¬c = ' 'h2:¬c = '\t'⊢ (decide (c = ' ') || decide (c = '\t') || decide (c = '\x0d') || decide (c = '\n')) = false
  have h3 : ¬ c = '\r' := byc:Charh:(Csexp.charDigit c).isSome = true⊢ isWs c = false rintro rflh:(Csexp.charDigit '\x0d').isSome = trueh1:¬'\x0d' = ' 'h2:¬'\x0d' = '\t'⊢ False; exact absurd h (byh:(Csexp.charDigit '\x0d').isSome = trueh1:¬'\x0d' = ' 'h2:¬'\x0d' = '\t'⊢ ¬(Csexp.charDigit '\x0d').isSome = true decideAll goals completed! 🐙)c:Charh:(Csexp.charDigit c).isSome = trueh1:¬c = ' 'h2:¬c = '\t'h3:¬c = '\x0d'⊢ (decide (c = ' ') || decide (c = '\t') || decide (c = '\x0d') || decide (c = '\n')) = false
  have h4 : ¬ c = '\n' := byc:Charh:(Csexp.charDigit c).isSome = true⊢ isWs c = false rintro rflh:(Csexp.charDigit '\n').isSome = trueh1:¬'\n' = ' 'h2:¬'\n' = '\t'h3:¬'\n' = '\x0d'⊢ False; exact absurd h (byh:(Csexp.charDigit '\n').isSome = trueh1:¬'\n' = ' 'h2:¬'\n' = '\t'h3:¬'\n' = '\x0d'⊢ ¬(Csexp.charDigit '\n').isSome = true decideAll goals completed! 🐙)c:Charh:(Csexp.charDigit c).isSome = trueh1:¬c = ' 'h2:¬c = '\t'h3:¬c = '\x0d'h4:¬c = '\n'⊢ (decide (c = ' ') || decide (c = '\t') || decide (c = '\x0d') || decide (c = '\n')) = false
  simp [h1, h2, h3, h4]All goals completed! 🐙

A digit is not an opening parenthesis.

theorem digit_not_open {c : Char} (h : (Csexp.charDigit c).isSome) :
    c ≠ '(' := byc:Charh:(Csexp.charDigit c).isSome = true⊢ c ≠ '('
  rintro rflh:(Csexp.charDigit '(').isSome = true⊢ False
  exact absurd h (byh:(Csexp.charDigit '(').isSome = true⊢ ¬(Csexp.charDigit '(').isSome = true decideAll goals completed! 🐙)

A digit is not a closing parenthesis.

theorem digit_not_close {c : Char} (h : (Csexp.charDigit c).isSome) :
    c ≠ ')' := byc:Charh:(Csexp.charDigit c).isSome = true⊢ c ≠ ')'
  rintro rflh:(Csexp.charDigit ')').isSome = true⊢ False
  exact absurd h (byh:(Csexp.charDigit ')').isSome = true⊢ ¬(Csexp.charDigit ')').isSome = true decideAll goals completed! 🐙)

Csexp.decOf_ne_nil in the form its consumers use: a shortest-form decimal has a head.

theorem decOf_eq_cons (n : Nat) : ∃ c cs, Csexp.decOf n = c :: cs :=
  List.exists_cons_of_ne_nil (Csexp.decOf_ne_nil n)

The head of a shortest-form decimal is a digit.

theorem decOf_head_digit (n : Nat) :
    ∀ c cs, Csexp.decOf n = c :: cs → (Csexp.charDigit c).isSome := byn:ℕ⊢ ∀ (c : Char) (cs : List Char), Csexp.decOf n = c :: cs → (Csexp.charDigit c).isSome = true
  intro c cs hcn:ℕc:Charcs:List Charhc:Csexp.decOf n = c :: cs⊢ (Csexp.charDigit c).isSome = true
  refine Csexp.decOf_all_digits n c ?_n:ℕc:Charcs:List Charhc:Csexp.decOf n = c :: cs⊢ c ∈ Csexp.decOf n
  rw [hcn:ℕc:Charcs:List Charhc:Csexp.decOf n = c :: cs⊢ c ∈ c :: cs]n:ℕc:Charcs:List Charhc:Csexp.decOf n = c :: cs⊢ c ∈ c :: cs
  simpAll goals completed! 🐙

A numeral is already stripped: the whitespace skip is the identity on a printed decimal and whatever follows it.

theorem skipWs_decOf_append (n : Nat) (rest : List Char) :
    skipWs (Csexp.decOf n ++ rest) = Csexp.decOf n ++ rest := byn:ℕrest:List Char⊢ skipWs (Csexp.decOf n ++ rest) = Csexp.decOf n ++ rest
  obtain ⟨c, cs, hc⟩ := decOf_eq_cons nn:ℕrest:List Charc:Charcs:List Charhc:Csexp.decOf n = c :: cs⊢ skipWs (Csexp.decOf n ++ rest) = Csexp.decOf n ++ rest
  rw [hc,n:ℕrest:List Charc:Charcs:List Charhc:Csexp.decOf n = c :: cs⊢ skipWs (c :: cs ++ rest) = c :: cs ++ rest List.cons_append,n:ℕrest:List Charc:Charcs:List Charhc:Csexp.decOf n = c :: cs⊢ skipWs (c :: (cs ++ rest)) = c :: (cs ++ rest) skipWs_cons,n:ℕrest:List Charc:Charcs:List Charhc:Csexp.decOf n = c :: cs⊢ (if isWs c = true then skipWs (cs ++ rest) else c :: (cs ++ rest)) = c :: (cs ++ rest)
    ite_eq_right (byn:ℕrest:List Charc:Charcs:List Charhc:Csexp.decOf n = c :: cs⊢ ¬isWs c = true simp [digit_not_ws (decOf_head_digit n c cs hc)]All goals completed! 🐙)]All goals completed! 🐙

The head of a spelling

Every spelling begins with an opening parenthesis or with a digit, according to whether the node has children. This is the readable counterpart of Rose.exists_print_eq_cons, which has only the parenthesized case.

theorem print_head {k : Nat} (r : Rose k) :
    ∃ c cs, print r = c :: cs ∧ (c = '(' ∨ (Csexp.charDigit c).isSome) := byk:ℕr:Rose k⊢ ∃ c cs, print r = c :: cs ∧ (c = '(' ∨ (Csexp.charDigit c).isSome = true)
  obtain ⟨⟨i, n⟩, f⟩ := rk:ℕi:Fin kn:ℕf:Rose.Arity (i, n) → WType Rose.Arity⊢ ∃ c cs, print (WType.mk (i, n) f) = c :: cs ∧ (c = '(' ∨ (Csexp.charDigit c).isSome = true)
  cases n with
  | zero =>zerok:ℕi:Fin kf:Rose.Arity (i, 0) → WType Rose.Arity⊢ ∃ c cs, print (WType.mk (i, 0) f) = c :: cs ∧ (c = '(' ∨ (Csexp.charDigit c).isSome = true)
    obtain ⟨c, cs, hc⟩ := decOf_eq_cons i.valzerok:ℕi:Fin kf:Rose.Arity (i, 0) → WType Rose.Arityc:Charcs:List Charhc:Csexp.decOf ↑i = c :: cs⊢ ∃ c cs, print (WType.mk (i, 0) f) = c :: cs ∧ (c = '(' ∨ (Csexp.charDigit c).isSome = true)
    exact ⟨c, cs, (print_zero i f).trans hc, Or.inr (decOf_head_digit i.val c cs hc)⟩All goals completed! 🐙
  | succ n =>succk:ℕi:Fin kn:ℕf:Rose.Arity (i, n + 1) → WType Rose.Arity⊢ ∃ c cs, print (WType.mk (i, n + 1) f) = c :: cs ∧ (c = '(' ∨ (Csexp.charDigit c).isSome = true) exact ⟨'(', _, print_succ i f, Or.inl rfl⟩All goals completed! 🐙

A spelling is already stripped: neither possible head is whitespace, so the skip is the identity on a spelling followed by anything.

theorem skipWs_print_append {k : Nat} (r : Rose k) (rest : List Char) :
    skipWs (print r ++ rest) = print r ++ rest := byk:ℕr:Rose krest:List Char⊢ skipWs (print r ++ rest) = print r ++ rest
  obtain ⟨c, cs, hc, hd⟩ := print_head rk:ℕr:Rose krest:List Charc:Charcs:List Charhc:print r = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = true⊢ skipWs (print r ++ rest) = print r ++ rest
  have hw : isWs c = false := by
    rcases hd with rfl | hdinlk:ℕr:Rose krest:List Charcs:List Charhc:print r = '(' :: cs⊢ isWs '(' = falseinrk:ℕr:Rose krest:List Charc:Charcs:List Charhc:print r = c :: cshd:(Csexp.charDigit c).isSome = true⊢ isWs c = false
    ·inlk:ℕr:Rose krest:List Charcs:List Charhc:print r = '(' :: cs⊢ isWs '(' = false exact open_not_wsAll goals completed! 🐙
    ·inrk:ℕr:Rose krest:List Charc:Charcs:List Charhc:print r = c :: cshd:(Csexp.charDigit c).isSome = true⊢ isWs c = false exact digit_not_ws hdk:ℕr:Rose krest:List Charc:Charcs:List Charhc:print r = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehw:isWs c = false⊢ skipWs (print r ++ rest) = print r ++ rest
  rw [hc,k:ℕr:Rose krest:List Charc:Charcs:List Charhc:print r = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehw:isWs c = false⊢ skipWs (c :: cs ++ rest) = c :: cs ++ rest List.cons_append,k:ℕr:Rose krest:List Charc:Charcs:List Charhc:print r = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehw:isWs c = false⊢ skipWs (c :: (cs ++ rest)) = c :: (cs ++ rest) skipWs_cons,k:ℕr:Rose krest:List Charc:Charcs:List Charhc:print r = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehw:isWs c = false⊢ (if isWs c = true then skipWs (cs ++ rest) else c :: (cs ++ rest)) = c :: (cs ++ rest) ite_eq_right (byk:ℕr:Rose krest:List Charc:Charcs:List Charhc:print r = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehw:isWs c = false⊢ ¬isWs c = true simp [hw]All goals completed! 🐙)]All goals completed! 🐙

The rest = [] instance of skipWs_print_append, which is the form the entry point uses.

theorem skipWs_print {k : Nat} (r : Rose k) : skipWs (print r) = print r := byk:ℕr:Rose k⊢ skipWs (print r) = print r
  have h := skipWs_print_append r []k:ℕr:Rose kh:skipWs (print r ++ []) = print r ++ []⊢ skipWs (print r) = print r
  rwa [List.append_nilk:ℕr:Rose kh:skipWs (print r) = print r⊢ skipWs (print r) = print r]k:ℕr:Rose kh:skipWs (print r) = print r⊢ skipWs (print r) = print r at h

A child block with its terminator never begins with a digit: it begins with the terminator when empty and with a separating space otherwise. Stating it over the terminated block is what makes the empty case true.

theorem block_append_head_not_digit {k : Nat} (ts : List (Rose k))
    (rest : List Char) :
    ∀ c cs, (ts.map (fun t ↦ ' ' :: print t)).flatten ++ ')' :: rest
        = c :: cs → Csexp.charDigit c = none := byk:ℕts:List (Rose k)rest:List Char⊢ ∀ (c : Char) (cs : List Char),
  (List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest = c :: cs → Csexp.charDigit c = none
  intro c cs hk:ℕts:List (Rose k)rest:List Charc:Charcs:List Charh:(List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest = c :: cs⊢ Csexp.charDigit c = none
  cases ts with
  | nil =>nilk:ℕrest:List Charc:Charcs:List Charh:(List.map (fun t ↦ ' ' :: print t) []).flatten ++ ')' :: rest = c :: cs⊢ Csexp.charDigit c = none
    simp only [List.map_nil, List.flatten_nil, List.nil_append] at hnilk:ℕrest:List Charc:Charcs:List Charh:')' :: rest = c :: cs⊢ Csexp.charDigit c = none
    injection h with h1 _nilk:ℕrest:List Charc:Charcs:List Charh1:')' = ctail_eq✝:rest = cs⊢ Csexp.charDigit c = none
    subst h1nilk:ℕrest:List Charcs:List Chartail_eq✝:rest = cs⊢ Csexp.charDigit ')' = none
    decideAll goals completed! 🐙
  | cons t ts =>consk:ℕrest:List Charc:Charcs:List Chart:Rose kts:List (Rose k)h:(List.map (fun t ↦ ' ' :: print t) (t :: ts)).flatten ++ ')' :: rest = c :: cs⊢ Csexp.charDigit c = none
    simp only [List.map_cons, List.flatten_cons, List.cons_append] at hconsk:ℕrest:List Charc:Charcs:List Chart:Rose kts:List (Rose k)h:' ' :: (print t ++ (List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest) = c :: cs⊢ Csexp.charDigit c = none
    injection h with h1 _consk:ℕrest:List Charc:Charcs:List Chart:Rose kts:List (Rose k)h1:' ' = ctail_eq✝:print t ++ (List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest = cs⊢ Csexp.charDigit c = none
    subst h1consk:ℕrest:List Charcs:List Chart:Rose kts:List (Rose k)tail_eq✝:print t ++ (List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest = cs⊢ Csexp.charDigit ' ' = none
    decideAll goals completed! 🐙

Parser

One layer of the recursive descent. A tree is a bare numeral or a parenthesized list, so this branches on the first character. It strips whitespace at four sites: after (, after the label in each branch, and after the child list. The strip after the parenthesized branch's label is the one the grammar makes least obvious: Rose.parseChildren tests its input's head against ')' immediately, so it must be called on stripped input or (0 1 2) fails at its first child. parseStep is called on stripped input and returns a stripped remainder; that invariant is what lets the shared loop be reused.

def parseStep (k : Nat) (childParse : List Char → Option (Rose k × List Char))
    (loopFuel : Nat) : List Char → Option (Rose k × List Char)
  | [] => none
  | c :: cs =>
    if c = '(' then
      match Csexp.readNat (skipWs cs) with
      | some (m, cs1) =>
        if h : m < k then
          (Rose.parseChildren childParse loopFuel (skipWs cs1)).map
            fun p ↦ (Rose.ofList ⟨m, h⟩ p.1, skipWs p.2)
        else none
      | none => none
    else
      match Csexp.readNat (c :: cs) with
      | some (m, cs1) =>
        if h : m < k then some (Rose.node ⟨m, h⟩ Fin.elim0, skipWs cs1)
        else none
      | none => none

Recursive descent over the readable spelling. The Nat bounds the recursion and serves in two roles at each layer: undecremented as the child loop's bound, and decremented as the child parser's fuel.

def parseAux (k : Nat) : Nat → List Char → Option (Rose k × List Char) :=
  Nat.rec (motive := fun _ ↦ List Char → Option (Rose k × List Char))
    (fun _ ↦ none) fun f ih ↦ parseStep k ih (f + 1)

@[simp] theorem parseAux_succ (k f : Nat) :
    parseAux k (f + 1) = parseStep k (parseAux k f) (f + 1) := rfl

The parser of the readable spelling, rejecting trailing input. The leading strip and the stripping invariant together are what let a leading indent and a trailing newline parse.

def parse (k : Nat) (cs : List Char) : Option (Rose k) :=
  match parseAux k cs.length (skipWs cs) with
  | some (r, []) => some r
  | _ => none

theorem parseStep_open (k : Nat)
    (childParse : List Char → Option (Rose k × List Char))
    (loopFuel : Nat) (cs : List Char) :
    parseStep k childParse loopFuel ('(' :: cs)
      = match Csexp.readNat (skipWs cs) with
        | some (m, cs1) =>
          if h : m < k then
            (Rose.parseChildren childParse loopFuel (skipWs cs1)).map
              fun p ↦ (Rose.ofList ⟨m, h⟩ p.1, skipWs p.2)
          else none
        | none => none := rfl

theorem parseStep_other (k : Nat)
    (childParse : List Char → Option (Rose k × List Char))
    (loopFuel : Nat) (c : Char) (cs : List Char) (hc : c ≠ '(') :
    parseStep k childParse loopFuel (c :: cs)
      = match Csexp.readNat (c :: cs) with
        | some (m, cs1) =>
          if h : m < k then some (Rose.node ⟨m, h⟩ Fin.elim0, skipWs cs1)
          else none
        | none => none := ite_eq_right hc

The retraction law

The child loop reads back a printed child sequence, given a child parser that reads back each child from its own spelling and returns the stripped remainder, and one unit of fuel per child plus one for the closing parenthesis. The loop's input is stripped, as every call site's is; the remainder it returns is not, since parseStep strips what it returns.

theorem parseChildren_print {k : Nat}
    (childParse : List Char → Option (Rose k × List Char)) :
    ∀ (ts : List (Rose k)) (fuel : Nat) (rest : List Char),
      (∀ t ∈ ts, ∀ r : List Char,
        (∀ c cs, r = c :: cs → Csexp.charDigit c = none) →
        childParse (print t ++ r) = some (t, skipWs r)) →
      ts.length < fuel →
      Rose.parseChildren childParse fuel
          (skipWs ((ts.map (fun t ↦ ' ' :: print t)).flatten ++ ')' :: rest))
        = some (ts, rest) :=
  List.rec (motive := fun ts ↦ ∀ (fuel : Nat) (rest : List Char),
      (∀ t ∈ ts, ∀ r : List Char,
        (∀ c cs, r = c :: cs → Csexp.charDigit c = none) →
        childParse (print t ++ r) = some (t, skipWs r)) →
      ts.length < fuel →
      Rose.parseChildren childParse fuel
          (skipWs ((ts.map (fun t ↦ ' ' :: print t)).flatten ++ ')' :: rest))
        = some (ts, rest))
    (fun fuel rest _ hfuel ↦ byk:ℕchildParse:List Char → Option (Rose k × List Char)fuel:ℕrest:List Charx✝:∀ t ∈ [],
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t ++ r) = some (t, skipWs r)hfuel:[].length < fuel⊢ Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) []).flatten ++ ')' :: rest)) =
  some ([], rest)
      obtain ⟨g, rfl⟩ : ∃ g, fuel = g + 1 := ⟨fuel - 1, byk:ℕchildParse:List Char → Option (Rose k × List Char)fuel:ℕrest:List Charx✝:∀ t ∈ [],
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t ++ r) = some (t, skipWs r)hfuel:[].length < fuel⊢ fuel = fuel - 1 + 1 omegaAll goals completed! 🐙⟩k:ℕchildParse:List Char → Option (Rose k × List Char)rest:List Charx✝:∀ t ∈ [],
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t ++ r) = some (t, skipWs r)g:ℕhfuel:[].length < g + 1⊢ Rose.parseChildren childParse (g + 1) (skipWs ((List.map (fun t ↦ ' ' :: print t) []).flatten ++ ')' :: rest)) =
  some ([], rest)
      rw [List.map_nil,k:ℕchildParse:List Char → Option (Rose k × List Char)rest:List Charx✝:∀ t ∈ [],
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t ++ r) = some (t, skipWs r)g:ℕhfuel:[].length < g + 1⊢ Rose.parseChildren childParse (g + 1) (skipWs ([].flatten ++ ')' :: rest)) = some ([], rest) List.flatten_nil,k:ℕchildParse:List Char → Option (Rose k × List Char)rest:List Charx✝:∀ t ∈ [],
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t ++ r) = some (t, skipWs r)g:ℕhfuel:[].length < g + 1⊢ Rose.parseChildren childParse (g + 1) (skipWs ([] ++ ')' :: rest)) = some ([], rest) List.nil_append,k:ℕchildParse:List Char → Option (Rose k × List Char)rest:List Charx✝:∀ t ∈ [],
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t ++ r) = some (t, skipWs r)g:ℕhfuel:[].length < g + 1⊢ Rose.parseChildren childParse (g + 1) (skipWs (')' :: rest)) = some ([], rest) skipWs_cons,k:ℕchildParse:List Char → Option (Rose k × List Char)rest:List Charx✝:∀ t ∈ [],
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t ++ r) = some (t, skipWs r)g:ℕhfuel:[].length < g + 1⊢ Rose.parseChildren childParse (g + 1) (if isWs ')' = true then skipWs rest else ')' :: rest) = some ([], rest)
        ite_eq_right (byk:ℕchildParse:List Char → Option (Rose k × List Char)rest:List Charx✝:∀ t ∈ [],
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t ++ r) = some (t, skipWs r)g:ℕhfuel:[].length < g + 1⊢ ¬isWs ')' = true simp [close_not_ws]All goals completed! 🐙), Rose.parseChildren_succ_closek:ℕchildParse:List Char → Option (Rose k × List Char)rest:List Charx✝:∀ t ∈ [],
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t ++ r) = some (t, skipWs r)g:ℕhfuel:[].length < g + 1⊢ some ([], rest) = some ([], rest)]All goals completed! 🐙)
    (fun t ts ih fuel rest hchild hfuel ↦ byk:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)fuel:ℕrest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)hfuel:(t :: ts).length < fuel⊢ Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) (t :: ts)).flatten ++ ')' :: rest)) =
  some (t :: ts, rest)
      obtain ⟨g, rfl⟩ : ∃ g, fuel = g + 1 := ⟨fuel - 1, byk:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)fuel:ℕrest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)hfuel:(t :: ts).length < fuel⊢ fuel = fuel - 1 + 1 omegaAll goals completed! 🐙⟩k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1⊢ Rose.parseChildren childParse (g + 1) (skipWs ((List.map (fun t ↦ ' ' :: print t) (t :: ts)).flatten ++ ')' :: rest)) =
  some (t :: ts, rest)
      obtain ⟨c, cs, hc, hd⟩ := print_head tk:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = true⊢ Rose.parseChildren childParse (g + 1) (skipWs ((List.map (fun t ↦ ' ' :: print t) (t :: ts)).flatten ++ ')' :: rest)) =
  some (t :: ts, rest)
      have hlt : ts.length < g := byk:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)fuel:ℕrest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)hfuel:(t :: ts).length < fuel⊢ Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) (t :: ts)).flatten ++ ')' :: rest)) =
  some (t :: ts, rest) simp at hfuelk:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕc:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehfuel:ts.length < g⊢ ts.length < g; omegak:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < g⊢ Rose.parseChildren childParse (g + 1) (skipWs ((List.map (fun t ↦ ' ' :: print t) (t :: ts)).flatten ++ ')' :: rest)) =
  some (t :: ts, rest)
      have hne : c ≠ ')' := byk:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)fuel:ℕrest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)hfuel:(t :: ts).length < fuel⊢ Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) (t :: ts)).flatten ++ ')' :: rest)) =
  some (t :: ts, rest)
        rcases hd with rfl | hdinlk:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1cs:List Charhlt:ts.length < ghc:print t = '(' :: cs⊢ '(' ≠ ')'inrk:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshlt:ts.length < ghd:(Csexp.charDigit c).isSome = true⊢ c ≠ ')'
        ·inlk:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1cs:List Charhlt:ts.length < ghc:print t = '(' :: cs⊢ '(' ≠ ')' exact open_ne_closeAll goals completed! 🐙
        ·inrk:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshlt:ts.length < ghd:(Csexp.charDigit c).isSome = true⊢ c ≠ ')' exact digit_not_close hdk:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'⊢ Rose.parseChildren childParse (g + 1) (skipWs ((List.map (fun t ↦ ' ' :: print t) (t :: ts)).flatten ++ ')' :: rest)) =
  some (t :: ts, rest)
      have hcons : ∀ u : List Char, print t ++ u = c :: (cs ++ u) := fun u ↦ byk:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'u:List Char⊢ print t ++ u = c :: (cs ++ u)
        rw [hc,k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'u:List Char⊢ c :: cs ++ u = c :: (cs ++ u) List.cons_appendk:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'u:List Char⊢ c :: (cs ++ u) = c :: (cs ++ u)]k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'hcons:∀ (u : List Char), print t ++ u = c :: (cs ++ u)⊢ Rose.parseChildren childParse (g + 1) (skipWs ((List.map (fun t ↦ ' ' :: print t) (t :: ts)).flatten ++ ')' :: rest)) =
  some (t :: ts, rest)
      rw [List.map_cons,k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'hcons:∀ (u : List Char), print t ++ u = c :: (cs ++ u)⊢ Rose.parseChildren childParse (g + 1)
    (skipWs (((' ' :: print t) :: List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
  some (t :: ts, rest) List.flatten_cons,k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'hcons:∀ (u : List Char), print t ++ u = c :: (cs ++ u)⊢ Rose.parseChildren childParse (g + 1)
    (skipWs (' ' :: print t ++ (List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
  some (t :: ts, rest) List.append_assoc,k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'hcons:∀ (u : List Char), print t ++ u = c :: (cs ++ u)⊢ Rose.parseChildren childParse (g + 1)
    (skipWs (' ' :: print t ++ ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest))) =
  some (t :: ts, rest) List.cons_append,k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'hcons:∀ (u : List Char), print t ++ u = c :: (cs ++ u)⊢ Rose.parseChildren childParse (g + 1)
    (skipWs (' ' :: (print t ++ ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)))) =
  some (t :: ts, rest)
        skipWs_cons,k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'hcons:∀ (u : List Char), print t ++ u = c :: (cs ++ u)⊢ Rose.parseChildren childParse (g + 1)
    (if isWs ' ' = true then skipWs (print t ++ ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest))
    else ' ' :: (print t ++ ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest))) =
  some (t :: ts, rest) ite_eq_left (byk:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'hcons:∀ (u : List Char), print t ++ u = c :: (cs ++ u)⊢ isWs ' ' = true simp [space_is_ws]All goals completed! 🐙), skipWs_print_append,k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'hcons:∀ (u : List Char), print t ++ u = c :: (cs ++ u)⊢ Rose.parseChildren childParse (g + 1) (print t ++ ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
  some (t :: ts, rest) hcons,k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'hcons:∀ (u : List Char), print t ++ u = c :: (cs ++ u)⊢ Rose.parseChildren childParse (g + 1) (c :: (cs ++ ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest))) =
  some (t :: ts, rest)
        Rose.parseChildren_succ_cons _ _ _ _ hne,k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'hcons:∀ (u : List Char), print t ++ u = c :: (cs ++ u)⊢ ((childParse (c :: (cs ++ ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)))).bind fun p ↦
    Option.map (fun q ↦ (p.1 :: q.1, q.2)) (Rose.parseChildren childParse g p.2)) =
  some (t :: ts, rest) ← hcons,k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'hcons:∀ (u : List Char), print t ++ u = c :: (cs ++ u)⊢ ((childParse (print t ++ ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest))).bind fun p ↦
    Option.map (fun q ↦ (p.1 :: q.1, q.2)) (Rose.parseChildren childParse g p.2)) =
  some (t :: ts, rest)
        hchild t (byk:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'hcons:∀ (u : List Char), print t ++ u = c :: (cs ++ u)⊢ t ∈ t :: ts simpAll goals completed! 🐙) _ (block_append_head_not_digit ts rest),
        Option.bind_some,k:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'hcons:∀ (u : List Char), print t ++ u = c :: (cs ++ u)⊢ Option.map (fun q ↦ ((t, skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)).1 :: q.1, q.2))
    (Rose.parseChildren childParse g (t, skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)).2) =
  some (t :: ts, rest) ih g rest (fun x hx ↦ hchild x (byk:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'hcons:∀ (u : List Char), print t ++ u = c :: (cs ++ u)x:Rose khx:x ∈ ts⊢ x ∈ t :: ts simp [hx]All goals completed! 🐙)) hlt,
        Option.map_somek:ℕchildParse:List Char → Option (Rose k × List Char)t:Rose kts:List (Rose k)ih:∀ (fuel : ℕ) (rest : List Char),
  (∀ t ∈ ts,
      ∀ (r : List Char),
        (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
          childParse (print t ++ r) = some (t, skipWs r)) →
    ts.length < fuel →
      Rose.parseChildren childParse fuel (skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)) =
        some (ts, rest)rest:List Charhchild:∀ t_1 ∈ t :: ts,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      childParse (print t_1 ++ r) = some (t_1, skipWs r)g:ℕhfuel:(t :: ts).length < g + 1c:Charcs:List Charhc:print t = c :: cshd:c = '(' ∨ (Csexp.charDigit c).isSome = truehlt:ts.length < ghne:c ≠ ')'hcons:∀ (u : List Char), print t ++ u = c :: (cs ++ u)⊢ some ((t, skipWs ((List.map (fun t ↦ ' ' :: print t) ts).flatten ++ ')' :: rest)).1 :: (ts, rest).1, (ts, rest).2) =
  some (t :: ts, rest)]All goals completed! 🐙)

The parser inverts the printer on printed input, given fuel at least the printed length. The remainder returned is the caller's stripped: a childless node's spelling ends in a digit, so the delimiting hypothesis on the remainder is what keeps the label from running on, and the stripping invariant makes what comes back skipWs rest rather than rest.

theorem parseAux_print {k : Nat} (r : Rose k) :
    ∀ (f : Nat) (rest : List Char), (print r).length ≤ f →
      (∀ c cs, rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print r ++ rest) = some (r, skipWs rest) :=
  WType.rec (motive := fun r ↦ ∀ (f : Nat) (rest : List Char),
      (print r).length ≤ f →
      (∀ c cs, rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print r ++ rest) = some (r, skipWs rest))
    (fun s ch ih f rest hf hrest ↦ byk:ℕr:Rose ks:Rose.Shape kch:Rose.Arity s → WType Rose.Arityih:∀ (a : Rose.Arity s) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)f:ℕrest:List Charhf:(print (WType.mk s ch)).length ≤ fhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none⊢ parseAux k f (print (WType.mk s ch) ++ rest) = some (WType.mk s ch, skipWs rest)
      obtain ⟨i, n⟩ := sk:ℕr:Rose kf:ℕrest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kn:ℕch:Rose.Arity (i, n) → WType Rose.Arityih:∀ (a : Rose.Arity (i, n)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)hf:(print (WType.mk (i, n) ch)).length ≤ f⊢ parseAux k f (print (WType.mk (i, n) ch) ++ rest) = some (WType.mk (i, n) ch, skipWs rest)
      change (print (Rose.node i ch)).length ≤ f at hfk:ℕr:Rose kf:ℕrest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kn:ℕch:Rose.Arity (i, n) → WType Rose.Arityih:∀ (a : Rose.Arity (i, n)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)hf:(print (Rose.node i ch)).length ≤ f⊢ parseAux k f (print (WType.mk (i, n) ch) ++ rest) = some (WType.mk (i, n) ch, skipWs rest)
      change parseAux k f (print (Rose.node i ch) ++ rest)
        = some (Rose.node i ch, skipWs rest)k:ℕr:Rose kf:ℕrest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kn:ℕch:Rose.Arity (i, n) → WType Rose.Arityih:∀ (a : Rose.Arity (i, n)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)hf:(print (Rose.node i ch)).length ≤ f⊢ parseAux k f (print (Rose.node i ch) ++ rest) = some (Rose.node i ch, skipWs rest)
      cases n with
      | zero =>zerok:ℕr:Rose kf:ℕrest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)hf:(print (Rose.node i ch)).length ≤ f⊢ parseAux k f (print (Rose.node i ch) ++ rest) = some (Rose.node i ch, skipWs rest)
        rw [print_zerozerok:ℕr:Rose kf:ℕrest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)hf:(Csexp.decOf ↑i).length ≤ f⊢ parseAux k f (Csexp.decOf ↑i ++ rest) = some (Rose.node i ch, skipWs rest)] at hf ⊢zerok:ℕr:Rose kf:ℕrest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)hf:(Csexp.decOf ↑i).length ≤ f⊢ parseAux k f (Csexp.decOf ↑i ++ rest) = some (Rose.node i ch, skipWs rest)
        obtain ⟨c, cs, hc⟩ := decOf_eq_cons i.valzerok:ℕr:Rose kf:ℕrest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)hf:(Csexp.decOf ↑i).length ≤ fc:Charcs:List Charhc:Csexp.decOf ↑i = c :: cs⊢ parseAux k f (Csexp.decOf ↑i ++ rest) = some (Rose.node i ch, skipWs rest)
        obtain ⟨g, rfl⟩ : ∃ g, f = g + 1 :=
          ⟨f - 1, byk:ℕr:Rose kf:ℕrest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)hf:(Csexp.decOf ↑i).length ≤ fc:Charcs:List Charhc:Csexp.decOf ↑i = c :: cs⊢ f = f - 1 + 1 rw [hck:ℕr:Rose kf:ℕrest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)c:Charcs:List Charhf:(c :: cs).length ≤ fhc:Csexp.decOf ↑i = c :: cs⊢ f = f - 1 + 1] at hfk:ℕr:Rose kf:ℕrest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)c:Charcs:List Charhf:(c :: cs).length ≤ fhc:Csexp.decOf ↑i = c :: cs⊢ f = f - 1 + 1; simp only [List.length_cons] at hfk:ℕr:Rose kf:ℕrest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)c:Charcs:List Charhf:cs.length + 1 ≤ fhc:Csexp.decOf ↑i = c :: cs⊢ f = f - 1 + 1; omegaAll goals completed! 🐙⟩zerok:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)c:Charcs:List Charhc:Csexp.decOf ↑i = c :: csg:ℕhf:(Csexp.decOf ↑i).length ≤ g + 1⊢ parseAux k (g + 1) (Csexp.decOf ↑i ++ rest) = some (Rose.node i ch, skipWs rest)
        rw [parseAux_succ,zerok:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)c:Charcs:List Charhc:Csexp.decOf ↑i = c :: csg:ℕhf:(Csexp.decOf ↑i).length ≤ g + 1⊢ parseStep k (parseAux k g) (g + 1) (Csexp.decOf ↑i ++ rest) = some (Rose.node i ch, skipWs rest) hc,zerok:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)c:Charcs:List Charhc:Csexp.decOf ↑i = c :: csg:ℕhf:(Csexp.decOf ↑i).length ≤ g + 1⊢ parseStep k (parseAux k g) (g + 1) (c :: cs ++ rest) = some (Rose.node i ch, skipWs rest) List.cons_append,zerok:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)c:Charcs:List Charhc:Csexp.decOf ↑i = c :: csg:ℕhf:(Csexp.decOf ↑i).length ≤ g + 1⊢ parseStep k (parseAux k g) (g + 1) (c :: (cs ++ rest)) = some (Rose.node i ch, skipWs rest)
          parseStep_other _ _ _ _ _
            (digit_not_open (decOf_head_digit i.val c cs hc)),zerok:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)c:Charcs:List Charhc:Csexp.decOf ↑i = c :: csg:ℕhf:(Csexp.decOf ↑i).length ≤ g + 1⊢ (match Csexp.readNat (c :: (cs ++ rest)) with
  | some (m, cs1) => if h : m < k then some (Rose.node ⟨m, h⟩ Fin.elim0, skipWs cs1) else none
  | none => none) =
  some (Rose.node i ch, skipWs rest)
          ← List.cons_append,zerok:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)c:Charcs:List Charhc:Csexp.decOf ↑i = c :: csg:ℕhf:(Csexp.decOf ↑i).length ≤ g + 1⊢ (match Csexp.readNat (c :: cs ++ rest) with
  | some (m, cs1) => if h : m < k then some (Rose.node ⟨m, h⟩ Fin.elim0, skipWs cs1) else none
  | none => none) =
  some (Rose.node i ch, skipWs rest) ← hc,zerok:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)c:Charcs:List Charhc:Csexp.decOf ↑i = c :: csg:ℕhf:(Csexp.decOf ↑i).length ≤ g + 1⊢ (match Csexp.readNat (Csexp.decOf ↑i ++ rest) with
  | some (m, cs1) => if h : m < k then some (Rose.node ⟨m, h⟩ Fin.elim0, skipWs cs1) else none
  | none => none) =
  some (Rose.node i ch, skipWs rest) readNat_append _ _ hrestzerok:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)c:Charcs:List Charhc:Csexp.decOf ↑i = c :: csg:ℕhf:(Csexp.decOf ↑i).length ≤ g + 1⊢ (match some (↑i, rest) with
  | some (m, cs1) => if h : m < k then some (Rose.node ⟨m, h⟩ Fin.elim0, skipWs cs1) else none
  | none => none) =
  some (Rose.node i ch, skipWs rest)]zerok:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)c:Charcs:List Charhc:Csexp.decOf ↑i = c :: csg:ℕhf:(Csexp.decOf ↑i).length ≤ g + 1⊢ (match some (↑i, rest) with
  | some (m, cs1) => if h : m < k then some (Rose.node ⟨m, h⟩ Fin.elim0, skipWs cs1) else none
  | none => none) =
  some (Rose.node i ch, skipWs rest)
        -- reduce the match on the `some` just produced, exposing the label-bound check
        simp only []zerok:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)c:Charcs:List Charhc:Csexp.decOf ↑i = c :: csg:ℕhf:(Csexp.decOf ↑i).length ≤ g + 1⊢ (if h : ↑i < k then some (Rose.node ⟨↑i, h⟩ Fin.elim0, skipWs rest) else none) = some (Rose.node i ch, skipWs rest)
        rw [dite_eq_left i.isLtzerok:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)c:Charcs:List Charhc:Csexp.decOf ↑i = c :: csg:ℕhf:(Csexp.decOf ↑i).length ≤ g + 1⊢ some (Rose.node ⟨↑i, ⋯⟩ Fin.elim0, skipWs rest) = some (Rose.node i ch, skipWs rest)]zerok:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin kch:Rose.Arity (i, 0) → WType Rose.Arityih:∀ (a : Rose.Arity (i, 0)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)c:Charcs:List Charhc:Csexp.decOf ↑i = c :: csg:ℕhf:(Csexp.decOf ↑i).length ≤ g + 1⊢ some (Rose.node ⟨↑i, ⋯⟩ Fin.elim0, skipWs rest) = some (Rose.node i ch, skipWs rest)
        exact congrArg (fun t ↦ some (t, skipWs rest))
          (congrArg (Rose.node i) (funext fun j ↦ j.elim0))All goals completed! 🐙
      | succ m =>succk:ℕr:Rose kf:ℕrest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)hf:(print (Rose.node i ch)).length ≤ f⊢ parseAux k f (print (Rose.node i ch) ++ rest) = some (Rose.node i ch, skipWs rest)
        rw [print_succsucck:ℕr:Rose kf:ℕrest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)hf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ f⊢ parseAux k f
    ('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')'])) ++ rest) =
  some (Rose.node i ch, skipWs rest)] at hf ⊢succk:ℕr:Rose kf:ℕrest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)hf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ f⊢ parseAux k f
    ('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')'])) ++ rest) =
  some (Rose.node i ch, skipWs rest)
        cases f with
        | zero =>succ.zerok:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)hf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ 0⊢ parseAux k 0
    ('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')'])) ++ rest) =
  some (Rose.node i ch, skipWs rest) simp at hfAll goals completed! 🐙
        | succ g =>succ.succk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1⊢ parseAux k (g + 1)
    ('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')'])) ++ rest) =
  some (Rose.node i ch, skipWs rest)
          have hlen : (Csexp.decOf i.val).length
              + (((List.ofFn ch).map (fun t ↦ ' ' :: print t)).flatten).length
                + 2 ≤ g + 1 := byk:ℕr:Rose ks:Rose.Shape kch:Rose.Arity s → WType Rose.Arityih:∀ (a : Rose.Arity s) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)f:ℕrest:List Charhf:(print (WType.mk s ch)).length ≤ fhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none⊢ parseAux k f (print (WType.mk s ch) ++ rest) = some (WType.mk s ch, skipWs rest)
            simp only [List.length_cons, List.length_append] at hfk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:(Csexp.decOf ↑i).length + ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + ([].length + 1)) + 1 ≤
  g + 1⊢ (Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1
            omegasucc.succk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1⊢ parseAux k (g + 1)
    ('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')'])) ++ rest) =
  some (Rose.node i ch, skipWs rest)
          have hL : (((List.ofFn ch).map (fun t ↦ ' ' :: print t)).flatten).length
              ≤ g := byk:ℕr:Rose ks:Rose.Shape kch:Rose.Arity s → WType Rose.Arityih:∀ (a : Rose.Arity s) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)f:ℕrest:List Charhf:(print (WType.mk s ch)).length ≤ fhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none⊢ parseAux k f (print (WType.mk s ch) ++ rest) = some (WType.mk s ch, skipWs rest) omegasucc.succk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ g⊢ parseAux k (g + 1)
    ('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')'])) ++ rest) =
  some (Rose.node i ch, skipWs rest)
          have hchild : ∀ t ∈ List.ofFn ch, ∀ r : List Char,
              (∀ c cs, r = c :: cs → Csexp.charDigit c = none) →
              parseAux k g (print t ++ r) = some (t, skipWs r) := byk:ℕr:Rose ks:Rose.Shape kch:Rose.Arity s → WType Rose.Arityih:∀ (a : Rose.Arity s) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)f:ℕrest:List Charhf:(print (WType.mk s ch)).length ≤ fhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none⊢ parseAux k f (print (WType.mk s ch) ++ rest) = some (WType.mk s ch, skipWs rest)
            intro t ht r' hr'k:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ gt:WType Rose.Arityht:t ∈ List.ofFn chr':List Charhr':∀ (c : Char) (cs : List Char), r' = c :: cs → Csexp.charDigit c = none⊢ parseAux k g (print t ++ r') = some (t, skipWs r')
            obtain ⟨j, rfl⟩ := List.mem_ofFn.mp htk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ gr':List Charhr':∀ (c : Char) (cs : List Char), r' = c :: cs → Csexp.charDigit c = nonej:Fin (i, m + 1).2ht:ch j ∈ List.ofFn ch⊢ parseAux k g (print (ch j) ++ r') = some (ch j, skipWs r')
            refine ih j g r' ?_ hr'k:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ gr':List Charhr':∀ (c : Char) (cs : List Char), r' = c :: cs → Csexp.charDigit c = nonej:Fin (i, m + 1).2ht:ch j ∈ List.ofFn ch⊢ (print (ch j)).length ≤ g
            have hmem : ' ' :: print (ch j)
                ∈ (List.ofFn ch).map (fun t ↦ ' ' :: print t) :=
              List.mem_map_of_mem (List.mem_ofFn.mpr ⟨j, rfl⟩)k:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ gr':List Charhr':∀ (c : Char) (cs : List Char), r' = c :: cs → Csexp.charDigit c = nonej:Fin (i, m + 1).2ht:ch j ∈ List.ofFn chhmem:' ' :: print (ch j) ∈ List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)⊢ (print (ch j)).length ≤ g
            have hsub : (' ' :: print (ch j)).length
                ≤ (((List.ofFn ch).map (fun t ↦ ' ' :: print t)).flatten).length :=
              (List.sublist_flatten_of_mem hmem).length_lek:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ gr':List Charhr':∀ (c : Char) (cs : List Char), r' = c :: cs → Csexp.charDigit c = nonej:Fin (i, m + 1).2ht:ch j ∈ List.ofFn chhmem:' ' :: print (ch j) ∈ List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)hsub:(' ' :: print (ch j)).length ≤ (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length⊢ (print (ch j)).length ≤ g
            simp only [List.length_cons] at hsubk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ gr':List Charhr':∀ (c : Char) (cs : List Char), r' = c :: cs → Csexp.charDigit c = nonej:Fin (i, m + 1).2ht:ch j ∈ List.ofFn chhmem:' ' :: print (ch j) ∈ List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)hsub:(print (ch j)).length + 1 ≤ (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length⊢ (print (ch j)).length ≤ g
            omegasucc.succk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)⊢ parseAux k (g + 1)
    ('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')'])) ++ rest) =
  some (Rose.node i ch, skipWs rest)
          have hfuel : (List.ofFn ch).length < g + 1 := byk:ℕr:Rose ks:Rose.Shape kch:Rose.Arity s → WType Rose.Arityih:∀ (a : Rose.Arity s) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)f:ℕrest:List Charhf:(print (WType.mk s ch)).length ≤ fhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none⊢ parseAux k f (print (WType.mk s ch) ++ rest) = some (WType.mk s ch, skipWs rest)
            have hpos : ∀ x ∈ ((List.ofFn ch).map (fun t ↦ ' ' :: print t)).map
                List.length, 1 ≤ x := byk:ℕr:Rose ks:Rose.Shape kch:Rose.Arity s → WType Rose.Arityih:∀ (a : Rose.Arity s) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)f:ℕrest:List Charhf:(print (WType.mk s ch)).length ≤ fhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none⊢ parseAux k f (print (WType.mk s ch) ++ rest) = some (WType.mk s ch, skipWs rest)
              intro x hxk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)x:ℕhx:x ∈ List.map List.length (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch))⊢ 1 ≤ x
              obtain ⟨y, hy, rfl⟩ := List.mem_map.mp hxk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)y:List Charhy:y ∈ List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)hx:y.length ∈ List.map List.length (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch))⊢ 1 ≤ y.length
              obtain ⟨t, _, rfl⟩ := List.mem_map.mp hyk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)t:Rose kleft✝:t ∈ List.ofFn chhy:' ' :: print t ∈ List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)hx:(' ' :: print t).length ∈ List.map List.length (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch))⊢ 1 ≤ (' ' :: print t).length
              simpk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hpos:∀ x ∈ List.map List.length (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)), 1 ≤ x⊢ (List.ofFn ch).length < g + 1
            have h := List.length_le_sum_of_one_le _ hposk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hpos:∀ x ∈ List.map List.length (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)), 1 ≤ xh:(List.map List.length (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch))).length ≤
  (List.map List.length (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch))).sum⊢ (List.ofFn ch).length < g + 1
            rw [List.length_map,k:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hpos:∀ x ∈ List.map List.length (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)), 1 ≤ xh:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).length ≤
  (List.map List.length (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch))).sum⊢ (List.ofFn ch).length < g + 1 List.length_map,k:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hpos:∀ x ∈ List.map List.length (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)), 1 ≤ xh:(List.ofFn ch).length ≤ (List.map List.length (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch))).sum⊢ (List.ofFn ch).length < g + 1 ← List.length_flattenk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hpos:∀ x ∈ List.map List.length (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)), 1 ≤ xh:(List.ofFn ch).length ≤ (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length⊢ (List.ofFn ch).length < g + 1] at hk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hpos:∀ x ∈ List.map List.length (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)), 1 ≤ xh:(List.ofFn ch).length ≤ (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length⊢ (List.ofFn ch).length < g + 1
            omegasucc.succk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hfuel:(List.ofFn ch).length < g + 1⊢ parseAux k (g + 1)
    ('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')'])) ++ rest) =
  some (Rose.node i ch, skipWs rest)
          rw [List.cons_append,succ.succk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hfuel:(List.ofFn ch).length < g + 1⊢ parseAux k (g + 1)
    ('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']) ++ rest)) =
  some (Rose.node i ch, skipWs rest) parseAux_succ,succ.succk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hfuel:(List.ofFn ch).length < g + 1⊢ parseStep k (parseAux k g) (g + 1)
    ('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']) ++ rest)) =
  some (Rose.node i ch, skipWs rest) parseStep_opensucc.succk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hfuel:(List.ofFn ch).length < g + 1⊢ (match
    Csexp.readNat
      (skipWs (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']) ++ rest)) with
  | some (m, cs1) =>
    if h : m < k then
      Option.map (fun p ↦ (Rose.ofList ⟨m, h⟩ p.1, skipWs p.2)) (Rose.parseChildren (parseAux k g) (g + 1) (skipWs cs1))
    else none
  | none => none) =
  some (Rose.node i ch, skipWs rest)]succ.succk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hfuel:(List.ofFn ch).length < g + 1⊢ (match
    Csexp.readNat
      (skipWs (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']) ++ rest)) with
  | some (m, cs1) =>
    if h : m < k then
      Option.map (fun p ↦ (Rose.ofList ⟨m, h⟩ p.1, skipWs p.2)) (Rose.parseChildren (parseAux k g) (g + 1) (skipWs cs1))
    else none
  | none => none) =
  some (Rose.node i ch, skipWs rest)
          simp only [List.append_assoc, List.singleton_append]succ.succk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hfuel:(List.ofFn ch).length < g + 1⊢ (match
    Csexp.readNat
      (skipWs (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ ')' :: rest))) with
  | some (m, cs1) =>
    if h : m < k then
      Option.map (fun p ↦ (Rose.ofList ⟨m, h⟩ p.1, skipWs p.2)) (Rose.parseChildren (parseAux k g) (g + 1) (skipWs cs1))
    else none
  | none => none) =
  some (Rose.node i ch, skipWs rest)
          rw [skipWs_decOf_append,succ.succk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hfuel:(List.ofFn ch).length < g + 1⊢ (match
    Csexp.readNat (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ ')' :: rest)) with
  | some (m, cs1) =>
    if h : m < k then
      Option.map (fun p ↦ (Rose.ofList ⟨m, h⟩ p.1, skipWs p.2)) (Rose.parseChildren (parseAux k g) (g + 1) (skipWs cs1))
    else none
  | none => none) =
  some (Rose.node i ch, skipWs rest)
            readNat_append _ _ (block_append_head_not_digit (List.ofFn ch) rest)succ.succk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hfuel:(List.ofFn ch).length < g + 1⊢ (match some (↑i, (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ ')' :: rest) with
  | some (m, cs1) =>
    if h : m < k then
      Option.map (fun p ↦ (Rose.ofList ⟨m, h⟩ p.1, skipWs p.2)) (Rose.parseChildren (parseAux k g) (g + 1) (skipWs cs1))
    else none
  | none => none) =
  some (Rose.node i ch, skipWs rest)]succ.succk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hfuel:(List.ofFn ch).length < g + 1⊢ (match some (↑i, (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ ')' :: rest) with
  | some (m, cs1) =>
    if h : m < k then
      Option.map (fun p ↦ (Rose.ofList ⟨m, h⟩ p.1, skipWs p.2)) (Rose.parseChildren (parseAux k g) (g + 1) (skipWs cs1))
    else none
  | none => none) =
  some (Rose.node i ch, skipWs rest)
          -- reduce the match on the `some` just produced, exposing the label-bound check
          simp only []succ.succk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hfuel:(List.ofFn ch).length < g + 1⊢ (if h : ↑i < k then
    Option.map (fun p ↦ (Rose.ofList ⟨↑i, ⋯⟩ p.1, skipWs p.2))
      (Rose.parseChildren (parseAux k g) (g + 1)
        (skipWs ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ ')' :: rest)))
  else none) =
  some (Rose.node i ch, skipWs rest)
          rw [dite_eq_left i.isLt,succ.succk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hfuel:(List.ofFn ch).length < g + 1⊢ Option.map (fun p ↦ (Rose.ofList ⟨↑i, ⋯⟩ p.1, skipWs p.2))
    (Rose.parseChildren (parseAux k g) (g + 1)
      (skipWs ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ ')' :: rest))) =
  some (Rose.node i ch, skipWs rest)
            parseChildren_print _ (List.ofFn ch) (g + 1) rest hchild hfuel,succ.succk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hfuel:(List.ofFn ch).length < g + 1⊢ Option.map (fun p ↦ (Rose.ofList ⟨↑i, ⋯⟩ p.1, skipWs p.2)) (some (List.ofFn ch, rest)) =
  some (Rose.node i ch, skipWs rest)
            Option.map_some,succ.succk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hfuel:(List.ofFn ch).length < g + 1⊢ some (Rose.ofList ⟨↑i, ⋯⟩ (List.ofFn ch, rest).1, skipWs (List.ofFn ch, rest).2) = some (Rose.node i ch, skipWs rest) Rose.ofList_ofFnsucc.succk:ℕr:Rose krest:List Charhrest:∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = nonei:Fin km:ℕch:Rose.Arity (i, m + 1) → WType Rose.Arityih:∀ (a : Rose.Arity (i, m + 1)) (f : ℕ) (rest : List Char),
  (print (ch a)).length ≤ f →
    (∀ (c : Char) (cs : List Char), rest = c :: cs → Csexp.charDigit c = none) →
      parseAux k f (print (ch a) ++ rest) = some (ch a, skipWs rest)g:ℕhf:('(' :: (Csexp.decOf ↑i ++ ((List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten ++ [')']))).length ≤ g + 1hlen:(Csexp.decOf ↑i).length + (List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length + 2 ≤ g + 1hL:(List.map (fun t ↦ ' ' :: print t) (List.ofFn ch)).flatten.length ≤ ghchild:∀ t ∈ List.ofFn ch,
  ∀ (r : List Char),
    (∀ (c : Char) (cs : List Char), r = c :: cs → Csexp.charDigit c = none) →
      parseAux k g (print t ++ r) = some (t, skipWs r)hfuel:(List.ofFn ch).length < g + 1⊢ some (Rose.node ⟨↑i, ⋯⟩ ch, skipWs (List.ofFn ch, rest).2) = some (Rose.node i ch, skipWs rest)]All goals completed! 🐙) r

The retraction law for the readable spelling: printing a rose tree and parsing the result returns that tree.

theorem parse_print {k : Nat} (r : Rose k) : parse k (print r) = some r := byk:ℕr:Rose k⊢ parse k (print r) = some r
  unfold parsek:ℕr:Rose k⊢ (match parseAux k (print r).length (skipWs (print r)) with
  | some (r, []) => some r
  | x => none) =
  some r
  rw [skipWs_print,k:ℕr:Rose k⊢ (match parseAux k (print r).length (print r) with
  | some (r, []) => some r
  | x => none) =
  some r show print r = print r ++ [] byk:ℕr:Rose k⊢ parse k (print r) = some r simpAll goals completed! 🐙,
    parseAux_print r _ [] (byk:ℕr:Rose k⊢ (print r).length ≤ (print r ++ []).length simpAll goals completed! 🐙) (byk:ℕr:Rose k⊢ ∀ (c : Char) (cs : List Char), [] = c :: cs → Csexp.charDigit c = none simpAll goals completed! 🐙), skipWs_nilk:ℕr:Rose k⊢ (match some (r, []) with
  | some (r, []) => some r
  | x => none) =
  some r]All goals completed! 🐙

The generic corollaries, instantiated here

Geb.Retraction at the readable spelling.

theorem retraction (k : Nat) : Retraction (parse k) (print (k := k)) :=
  parse_print

Geb.format_idem at the readable spelling.

theorem format_idem (k : Nat) (c : List Char) :
    (format (parse k) print c).bind (format (parse k) print)
      = format (parse k) print c :=
  Geb.format_idem _ _ (retraction k) c

Geb.print_injective at the readable spelling.

theorem print_injective (k : Nat) : Function.Injective (print (k := k)) :=
  Geb.print_injective _ _ (retraction k)

The `Ast` composites

The readable spelling of an Ast k, through the rose bijection.

def printViaRose {k : Nat} (a : Ast k) : List Char := print a.toRose

The parser matching printViaRose.

def parseViaRose (k : Nat) (cs : List Char) : Option (Ast k) :=
  (parse k cs).map Ast.ofRose

The retraction law for the Ast composites, transported along the rose retraction by Ast.ofRose_toRose.

theorem parseViaRose_printViaRose {k : Nat} (a : Ast k) :
    parseViaRose k (printViaRose a) = some a := byk:ℕa:Ast k⊢ parseViaRose k (printViaRose a) = some a
  rw [parseViaRose,k:ℕa:Ast k⊢ Option.map Ast.ofRose (parse k (printViaRose a)) = some a printViaRose,k:ℕa:Ast k⊢ Option.map Ast.ofRose (parse k (print a.toRose)) = some a parse_print,k:ℕa:Ast k⊢ Option.map Ast.ofRose (some a.toRose) = some a Option.map_some,k:ℕa:Ast k⊢ some (Ast.ofRose a.toRose) = some a Ast.ofRose_toRosek:ℕa:Ast k⊢ some a = some a]All goals completed! 🐙

end Rsexpend Geb