Lean golf: List Game Lv2 (is_in_append, is_in_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.

---

The definitions used in Lv1 will be reused here. I've done some improvements:

• Now it starts with import tactic, which means you can freely use powerful mathlib tactics.
• I noticed that I can define the general list notation [a, b, ..., z] without problems.

import tactic
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
notation `[` l:(foldr `, ` (h t, list.cons h t) list.nil `]`) := l

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, here's a new definition we will use from now on: a membership relationship between an element and a list. It is defined recursively using two cases: A value x is in a list l if

• x is the head of l, or
• x is in the tail of l.

inductive is_in : A → list A → Prop
| in_hd {x : A} {l : list A} : is_in x (x :: l)
| in_tl {x y : A} {l : list A} : is_in x l → is_in x (y :: l)
open is_in

Now your task is to prove the following two statements: (think of these as parts of a chapter, sharing a few lemmas)

• is_in_append: x appears in l1 ++ l2 if and only if x appears in l1 or x appears in l2.
• is_in_rev: if x appears in l, x appears in rev l.

theorem is_in_append : ∀ (x : A) (l1 l2 : list A), is_in x (l1 ++ l2) ↔ is_in x l1 \/ is_in x l2 := sorry
theorem is_in_rev : ∀ (x : A) (l : list A), is_in x l → is_in x (rev l) := sorry

You can change the name of each 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, except for tactics).

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.

Tips for beginners

The new beast called "inductive Prop" is a particularly hard concept to grasp. Simply put, a value of is_in x l contains a concrete proof that x appears in l. It is an unknown value, but we can still reason about it:

• Consider all the possible paths is_in x l could have been constructed (i.e. proven). This is done with cases tactic. When used on a hypothesis of is_in x l, it generates two subgoals, one assuming in_hd and the other assuming in_tl.
  • If you use cases on is_in x [], there is no way it could have been constructed (since both possibilities result in a cons), the goal is immediately closed by contradiction.
• Apply induction on the proof. It works just like induction on a nat or a list: to prove a theorem in the form of ∀ (x:A) (l:list A), is_in x l → some_prop, you can prove it by induction on is_in x l and prove the "base case" is_in x (x::l) and "inductive case" (is_in x l → some_prop) → is_in x (y::l) → some_prop.

It takes some practice to see which argument (an inductive data or an inductive prop - in this challenge, list or is_in) works best with induction for a given statement. You can start by proving parts of the main statement separately as lemmas:

lemma is_in_append_l : ∀ (x : A) (l l2 : list A), is_in x l → is_in x (l ++ l2) := sorry
lemma is_in_append_r : ∀ (x : A) (l l2 : list A), is_in x l → is_in x (l2 ++ l) := sorry

(Hint: One works best by induction on l2, and the other works best on is_in x l.)

Answer 1

Lean, 188 bytes

infix`~`:=is_in
def P(x:A)(l m):x~l++m↔x~l\/x~m:=by induction
l;split;repeat{safe[in_hd,in_tl];cases ᾰ<|>cases l_ih.1 ᾰ_ᾰ}def
R(x:A)(l)(i:x~l):x~rev l:=by induction i;safe[P,in_hd]

Try it on Lean Web Editor (warning: very slow 🐌)

Answer 2

Lean, 254 226 221 bytes

infix`~`:=is_in
variables(x y:A)def D(a):x=y\/x~a↔x~y::a:=by
split;rintro(c|d);safe[in_hd,in_tl]def E:¬x~[].
def P(a b):x~a++b↔x~a\/x~b:=by
induction a;safe[<-D,E]def Q(a)(h:x~a):x~rev a:=by
induction h;safe[in_hd,P]

Try it on the Lean Web Editor

P and Q are the desired theorems. I reuse the ~ notation (which is normally for the list.perm relation) to mean the is_in relation, which lets us save a lot of spaces in lemma statements.

I was going for "readable" and fast-to-typecheck (Anders isn't kidding about their solution being slow!). D is a definition lemma for is_in (mathlib calls the reversed version of it list.mem_cons_iff; I had to reverse it to trick Lean into disambiguating :: correctly). The E lemma uses the equation compiler to automatically construct a proof (mathlib calls it list.not_mem_nil).

Some of these tricks can shorten Anders's first solution to 217 bytes:

infix`~`:=is_in
attribute[simp]in_hd in_tl
def P(x:A)(l m):x~l++m↔x~l\/x~m:=by induction l;split;intro;repeat{finish<|>cases
ᾰ<|>cases l_ih.1 ᾰ_ᾰ}def R(x:A)(l)(i:x~l):x~rev l:=by induction i;simp[P];left;tauto

---

I want to mention that is_in might more conventionally be given as a recursive definition:

def is_in (x : A) : Π (l : list A), Prop
| [] := false
| (y::ys) := x = y ∨ is_in ys

Given this, there is a 150 byte solution:

infix`~`:=is_in
def P(x:A)(l m):x~l++m↔x~l\/x~m:=by
induction l;split;simp!;intro;safe
def Q(x:A)(l)(i:x~l):x~rev l:=by induction l;simp![P]at*;safe