6
\$\begingroup\$

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.

\$\endgroup\$
5
\$\begingroup\$

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.

\$\endgroup\$
2
  • 2
    \$\begingroup\$ 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. \$\endgroup\$ Oct 9 at 1:01
  • \$\begingroup\$ @AndersKaseorg Nice. The lambda is still shorter if it's your main declaration. \$\endgroup\$
    – Wheat Witch
    Oct 9 at 2:46
4
\$\begingroup\$

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.

\$\endgroup\$
3
  • 4
    \$\begingroup\$ You can use by even when there are multiple tactics, just enclose them in braces, e.g. by{rw add_assoc,refl} \$\endgroup\$
    – Wheat Witch
    Oct 8 at 23:08
  • 1
    \$\begingroup\$ if you use either ; or <|> instead of , (I think ; will usually be the most useful) you don't need braces either \$\endgroup\$ Oct 9 at 16:38
  • \$\begingroup\$ @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) \$\endgroup\$
    – user
    Oct 9 at 16:39
3
\$\begingroup\$

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
\$\endgroup\$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.