# Tips for golfing in Lean

Lean is a theorem prover and programming language. It's also as of writing the Language of the Month!

What tips do people have for golfing in Lean? As always, tips should be specific to to Lean (e.g. "Remove comments" is not an answer), and stick to a single tip per answer.

# Introductions

If you've just finished the natural number game you may be familiar with the intro tactic, this can be used to create implications / functions. However this tactic is rarely the golfiest.

If your intro is the first part of your proof then an implicit forall is probably better. Compare:

def q:list ℕ→ℕ:=by{intro x,induction x,exact 0,exact x_hd+x_ih}


with

def q(x:list ℕ):ℕ:=by{induction x,exact 0,exact x_hd+x_ih}


This is frequently always your best option. However if the type of your function can be inferred you have other options.

def f:ℕ→ℕ:=by{intro x,exact x+3}
def f(x:ℕ):ℕ:=by{exact x+3}
def f:=λx,by{exact x+3}
def f(x):=by{exact x+3}


These are ordered by length so implicit forall (the last option is still implicit forall) is the shortest. But the lambda can expression can have the def f:= removed if the function is your submission, making it the shortest in that case.

• Types on a def with parameters can be inferred too: def f(x):=by{exact x+3}, which is shorter in bytes because λ is two bytes. Oct 9 at 1:01
• @AndersKaseorg Nice. The lambda is still shorter if it's your main declaration. Oct 9 at 2:46

## Use by instead of begin ... end

by can be shorter than begin and end.

def foo(m:ℕ):m=m:=begin refl,end


is longer than

def bar(m:ℕ):m=m :=by refl


You can also use it for multiple tactics, though you'll need to encase the tactics in braces, as Wheat Wizard pointed out. For example, by{rw add_assoc,refl} is shorter than begin rw add_assoc,refl end.

• You can use by even when there are multiple tactics, just enclose them in braces, e.g. by{rw add_assoc,refl} Oct 8 at 23:08
• if you use either ; or <|> instead of , (I think ; will usually be the most useful) you don't need braces either Oct 9 at 16:38
• @It'sNotALie. That's really cool, but I don't know how to add that, can you do it? (I made this answer CW so that people could edit it)
– user
Oct 9 at 16:39

## The ; and <|> combinators.

; makes it so that all subgoals created by the last tactic have the next tactic applied; for example, lemma asda (n : ℕ) : n = n := by { induction n; refl } is a valid proof. As a bonus, it also allows you to not use the braces (e.g. def k(n:ℕ):n=n:=by induction n;refl).

The <|> is a bit more niche, but still useful; it allows you to do one tactic, and if it fails, the other instead. It also allows for no braces (although this is longer than ,, so not as useful). For example:

example(x):0+x=x:=by induction x;refl<|>rw nat.zero_add