Lean golf: List Game Lv1 (rev_rev)

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 :: [])


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

• To hopefully encourage more participation from newcomers, I’ll just say for now that my solution is 102 bytes (MD5: c952ab1ce4e4c79aefedff8994db665b). Give it a try! Commented Oct 10, 2021 at 6:59

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.

• @HuỳnhTrầnKhanh As far as I I can't get lean to infer any of the types in the declaration. Commented Oct 10, 2021 at 13:14
• You can't, but I can. def r(s):rev(@rev A s)=s:=by induction s;simp;conv{to_rhs,rw←s_ih};induction rev s_ᾰ_1;simp;simp[ih] Commented Oct 10, 2021 at 13:39
• Avoiding a Unicode character saves 1 more byte. def r(s):rev(@rev A s)=s:=by induction s;simp;conv{to_rhs,rw<-s_ih};induction rev s_ᾰ_1;simp;simp[ih] Commented Oct 10, 2021 at 13:46
• Now, use the equation compiler. We have outgolfed Anders Kaseorg! 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] (101 bytes, UTF-8) Commented Oct 10, 2021 at 14:10

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

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*