Theorem: lexwhile_monotonic (ReckonLean/Parser.lean)

State before:
⊢ ∀ (p : Char → Bool) (inp : List Char), List.length (lexwhile p inp).snd ≤ List.length inp
Tactic:
intro p inp
State after:
p : Char → Bool
inp : List Char
⊢ List.length (lexwhile p inp).snd ≤ List.length inp

State before:
p : Char → Bool
inp : List Char
⊢ List.length (lexwhile p inp).snd ≤ List.length inp
Tactic:
induction inp with
| nil => simp [lexwhile]
| cons c cs ih =>
  simp [lexwhile]
  cases p c <;> simp
  exact Nat.le_succ_of_le ih
State after:
no goals

State before:
case nil
p : Char → Bool
⊢ List.length (lexwhile p []).snd ≤ List.length []
Tactic:
simp [lexwhile]
State after:
no goals

State before:
case cons
p : Char → Bool
c : Char
cs : List Char
ih : List.length (lexwhile p cs).snd ≤ List.length cs
⊢ List.length (lexwhile p (c :: cs)).snd ≤ List.length (c :: cs)
Tactic:
simp [lexwhile]
State after:
case cons
p : Char → Bool
c : Char
cs : List Char
ih : List.length (lexwhile p cs).snd ≤ List.length cs
⊢ List.length
      (if p c = true then (String.append (Char.toString c) (lexwhile p cs).fst, (lexwhile p cs).snd)
        else ("", c :: cs)).snd ≤
    Nat.succ (List.length cs)

State before:
case cons
p : Char → Bool
c : Char
cs : List Char
ih : List.length (lexwhile p cs).snd ≤ List.length cs
⊢ List.length
      (if p c = true then (String.append (Char.toString c) (lexwhile p cs).fst, (lexwhile p cs).snd)
        else ("", c :: cs)).snd ≤
    Nat.succ (List.length cs)
Tactic:
cases p c <;> simp
State after:
case cons.true
p : Char → Bool
c : Char
cs : List Char
ih : List.length (lexwhile p cs).snd ≤ List.length cs
⊢ List.length (lexwhile p cs).snd ≤ Nat.succ (List.length cs)

State before:
case cons.true
p : Char → Bool
c : Char
cs : List Char
ih : List.length (lexwhile p cs).snd ≤ List.length cs
⊢ List.length (lexwhile p cs).snd ≤ Nat.succ (List.length cs)
Tactic:
exact Nat.le_succ_of_le ih
State after:
no goals