Lean 4: simple experiments with List

SimpleList.lean

import Mathlib.Data.List.Basic

section
-- BEGIN

-- https://lean-lang.org/blog/2024-1-11-recursive-definitions-in-lean/


-- TODO make tail-recursive?

def my_reverse {α : Type u} (xs : List α) : List α :=
  match xs with
  | []  => []
  | x :: rest => my_reverse rest ++ [x]

def reverse_spec {α : Type u} (xs : List α) : Prop :=
  my_reverse xs = xs.reverse

theorem my_reverse_satisfies_spec : reverse_spec xs := by
  induction xs with
  | nil => simp [my_reverse, reverse_spec]
  | cons y ys ih => 
    rw [reverse_spec]
    rw [my_reverse]
    rw [List.reverse_cons]
    rw [ih]

def reverse_length_spec {α : Type u} (xs : List α) : Prop :=
  xs.length = (my_reverse xs).length

example : reverse_length_spec xs := by
  induction xs with
  | nil => exact List.length_nil
  | cons y ys ih => 
    rw [reverse_length_spec]
    rw [my_reverse]
    rw [List.length_append]
    rw [List.length_cons]
    rw [ih]
    rw [List.length_cons]
    rw [List.length_nil]


#check my_reverse
#check reverse_spec
#check my_reverse_satisfies_spec
#check reverse_length_spec

#eval my_reverse [1, 2, 3]
#eval my_reverse ["hello", "world"]

#check (my_reverse [List, Array]).length

-- END
end