Tips for golfing in Lean

Question

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.

Answer 1

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.

Answer 2

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.

Answer 3

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