リストを2回逆順にすると元に戻る in Lean

rev_rev_id.lean

open list (hiding reverse)

#check 1
#reduce head [0, 1, 2, 3]


variable {T : Type}

def snoc : list T → T → list T
| []        y := [y]
| (x :: xs) y := x :: snoc xs y
#reduce snoc [0, 1, 2, 3] 5

def reverse : list T → list T
| []        := nil
| (x :: xs) := snoc (reverse xs) x
#reduce reverse [0, 1, 2, 3]

lemma l1 : ∀ (xs : list T) (y : T), reverse (snoc xs y) = y :: (reverse xs)
| []        _ := rfl
| (x :: xs) y := calc
  reverse (snoc (x :: xs) y) = reverse (x :: snoc xs y) : rfl
  ... = snoc (reverse (snoc xs y)) x                    : rfl
  ... = snoc (y :: (reverse xs)) x       : congr_arg (λ t, snoc t x) (l1 xs y)

theorem rev_rev_id : ∀ (xs : list T), reverse (reverse xs) = xs
| []        := rfl
| (x :: xs) := calc
  reverse (reverse (x :: xs)) = reverse (snoc (reverse xs) x) : rfl
  ... = x :: (reverse (reverse xs))                : by rw l1 (reverse xs) x
  ... = x :: xs                                    : by rw rev_rev_id