rev.lean

variable {T : Type}

inductive list (T : Type) : Type :=
| nil {} : list T
| cons : T → list T → list T
open list

definition append : list T → list T → list T
| nil l := l
| (cons x xs) l := cons x (append xs l)

notation l₁ ++ l₂ := append l₁ l₂

theorem append_nil_right : ∀ (xs : list T), xs ++ nil = xs
| nil := rfl
| (cons x xs) := calc
  cons x xs ++ nil = cons x (xs ++ nil) : rfl
  ... = cons x xs : append_nil_right xs

theorem append_assoc : ∀ (xs ys zs : list T), xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
| nil ys zs := rfl
| (cons x xs) ys zs := calc
  cons x xs ++ (ys ++ zs) = cons x (xs ++ (ys ++ zs)) : rfl
  ... = cons x ((xs ++ ys) ++ zs) : append_assoc
  ... = (cons x xs ++ ys) ++ zs : rfl

definition reverse : list T → list T
| nil := nil
| (cons x xs) := reverse xs ++ cons x nil

theorem rev_append : ∀ (xs ys : list T), reverse (xs ++ ys) = reverse ys ++ reverse xs
| nil nil := rfl
| xs nil := calc
  reverse (xs ++ nil) = reverse xs : append_nil_right xs
| nil ys := calc
  reverse (nil ++ ys) = reverse ys : rfl
  ... = reverse ys ++ reverse nil : append_nil_right
| (cons x xs) ys := calc
  reverse (cons x xs ++ ys) = reverse (cons x (xs ++ ys)) : rfl
  ... = reverse (xs ++ ys) ++ cons x nil : rfl
  ... = (reverse ys ++ reverse xs) ++ cons x nil : rev_append xs ys
  ... = reverse ys ++ (reverse xs ++ cons x nil) : append_assoc
  ... = reverse ys ++ reverse (cons x xs) : rfl

theorem rev_rev_id : ∀ (xs : list T), reverse (reverse xs) = xs
| nil := calc
  reverse (reverse nil) = nil : rfl
| (cons x xs) := calc
  reverse (reverse (cons x xs)) = reverse (reverse xs ++ cons x nil) : rfl
  ... = reverse (cons x nil) ++ reverse (reverse xs) : rev_append
  ... = reverse (cons x nil) ++ xs : rev_rev_id xs
  ... = cons x nil ++ xs : rfl
  ... = cons x xs : rfl