Theorem: LoVe.Palindrome_reverse (LoVe/Lectures/LoVe06_InductivePredicates_Demo.lean)

State before:
α : Type
xs : List α
hxs : Palindrome xs
⊢ Palindrome (reverse xs)
Tactic:
induction hxs with
| nil                  => exact Palindrome.nil
| single x             => exact Palindrome.single x
| sandwich x xs hxs ih =>
  { simp [reverse, reverse_append]
    exact Palindrome.sandwich _ _ ih }
State after:
no goals

State before:
case nil
α : Type
xs : List α
⊢ Palindrome (reverse [])
Tactic:
exact Palindrome.nil
State after:
no goals

State before:
case single
α : Type
xs : List α
x : α
⊢ Palindrome (reverse [x])
Tactic:
exact Palindrome.single x
State after:
no goals

State before:
case sandwich
α : Type
xs✝ : List α
x : α
xs : List α
hxs : Palindrome xs
ih : Palindrome (reverse xs)
⊢ Palindrome (reverse ([x] ++ xs ++ [x]))
Tactic:
simp [reverse, reverse_append]
State after:
case sandwich
α : Type
xs✝ : List α
x : α
xs : List α
hxs : Palindrome xs
ih : Palindrome (reverse xs)
⊢ Palindrome (x :: (reverse xs ++ [x]))

State before:
case sandwich
α : Type
xs✝ : List α
x : α
xs : List α
hxs : Palindrome xs
ih : Palindrome (reverse xs)
⊢ Palindrome (x :: (reverse xs ++ [x]))
Tactic:
exact Palindrome.sandwich _ _ ih
State after:
no goals