Lean golf: List Game Lv1 (rev_rev)

Question

The title is an homage of the Natural Number Game, which is a nice interactive tutorial into proving certain properties of natural numbers in Lean.

Given that the previous two were slightly too involved (either mathematically or technically) for newcomers to Lean (i.e. the vast majority of CGCC community), I decided to pose some simpler theorems.

---

Let's start with the classic definition of a linked list. You can ignore most of the theoretical fluff; the point is that list A is a linked list containing values of type A, and defined as either an empty list [] (aka list.nil) or a pair (cons) of a value and a tail h :: t (aka list.cons).

Our definitions of list and functions on it live in the namespace mylist in order to avoid clash with the existing definitions.

universe u
variables {A : Type u}
namespace mylist

inductive list (T : Type u) : Type u
| nil : list
| cons : T → list → list

infixr ` :: `:67 := list.cons
notation `[]` := list.nil

We then define append and rev (reverse) on lists. Note that has_append instance is necessary in order to use ++ notation, and unfolding lemmas are needed to use the definitional equations of append on ++. Also, rev is defined using the simplest possible definition via ++.

def append : list A → list A → list A
| [] t := t
| (h :: s) t := h :: (append s t)
instance : has_append (list A) := ⟨@append A⟩

@[simp] lemma nil_append (s : list A) : [] ++ s = s := rfl
@[simp] lemma cons_append (x : A) (s t : list A) : (x :: s) ++ t = x :: (s ++ t) := rfl

@[simp] def rev : list A → list A
| [] := []
| (h :: t) := rev t ++ (h :: [])

Now your task is to prove the following statement:

theorem rev_rev (s : list A) : rev (rev s) = s := sorry

You can change the name of this statement and golf its definition, as long as its type is correct. Any kind of sidestepping is not allowed. Due to the nature of this challenge, adding imports is also not allowed (i.e. no mathlib).

The entire boilerplate is provided here. Your score is the length of the code between the two dashed lines, measured in bytes. The shortest code wins.

For beginners, proving the following lemmas in order will help you solve the challenge:

lemma append_nil (s : list A) : s ++ [] = s := sorry
lemma append_assoc (s t u : list A) : s ++ t ++ u = s ++ (t ++ u) := sorry
lemma rev_append (s t : list A) : rev (s ++ t) = rev t ++ rev s := sorry

Answer 1

Lean, 101 bytes

def r:∀s,rev(@rev A s)=s|[]:=rfl|(x::t):=by
conv{to_rhs,rw<-r t};simp;induction rev t;simp;simp[ih]

Try it online!

I'm pretty happy with this.

Thanks to Huỳnh Trần Khanh for their help.

Answer 2

Lean, 102 93 bytes

def R:∀s,rev(@rev A s)=s:=by let:(∀s(h:A),rev(s++h::[])=h::rev s);intro;induction s;simp*

Try it on Lean Web Editor

The 102 byte solution I advertised earlier had suboptimal type annotations:

def R:∀s:list A,rev(rev s)=s:=by let:(∀(s:list A)h,rev(s++h::[])=h::rev s);intro;induction s;simp*