In lean, how do I expand a definition without knowing what it is?

Question

Suppose I have a goal of proving

$a \lt b$

But I don't how < is defined. Maybe it's defined as $\exists c \in \mathbb{N}. a + c + 1 = b$ or maybe it's defined inductively as an example $0 \lt 1$ and a rule $a < b \implies (a + 1 < b + 1) \land (a < b + 1)$.

Ultimately need to know which definition is present in order to make a valid proof. But finding the definition by searching documentation can be quite involved. I'd much rather be able to say, for example expand and have a < b be replaced by its definition.

Anyways, is there such a command? In general, is there a way to view definitions or find names of definitions from within the editor?

Note that I'm not looking for a tactic that solves the problem, I'm purely looking for something that tells me what the problem is. I'm looking for the equivalent of python's help() function, which prints an object's __doc__ attribute.

Answer 1

The TL;DR is probably to try set_option pp.all true, but here is a more comprehensive answer. (Some of this advice is for VS Code and the online editor. I don't know about Emacs, but I assume it is similar to VS Code.)

A definition in the code (no notation)

Let's first consider the case where there is no notation involved and the thing you are interested is a definition in the code. For example, let's say you encounter a theorem like

open nat
theorem foo : (gcd 1 1) = 1 := by simp [gcd]

and you want to know more about gcd.

First, here is how you get the full name and type signature: nat.gcd : ℕ → ℕ → ℕ

• In VS Code, you can hover over gcd and it will give you the full name and type signature.
• In the online editor you can click on the definition and on the left it will show you the full name and signature.

You have many options to drill down more into the definition:

• In VS Code, you can ctrl-click on Windows (cmd-click on a Mac) to teleport to the file where this definition comes from. Note, this can sometimes cause problems in Lean if the definition is really far back in the history. If Lean becomes slow, close the definition file and restart the Lean server (or close and re-open VS Code).

  def gcd : nat → nat → nat
  | 0        y := y
  | (succ x) y := have y % succ x < succ x, from mod_lt _ $ succ_pos _,
                gcd (y % succ x) (succ x)
  

• If the definition is part of core Lean, or mathlib, you can find it in the mathlib docs. For example, nat.gcd. There is also a link to the source code on Github.
• You can print the definition with #print. This will show you how Lean sees the definition internally. Sometimes you also have the print the inner definitions (and it can get ugly).

  #print nat.gcd
  -- def nat.gcd : ℕ → ℕ → ℕ :=
  -- gcd._main
  #print nat.gcd._main
  -- def nat.gcd._main : ℕ → ℕ → ℕ :=
  -- λ (ᾰ ᾰ_1 : ℕ), gcd._main._pack ⟨ᾰ, ᾰ_1⟩
  #print nat.gcd._main._pack
  -- def nat.gcd._main._pack : Π (_x : Σ' (ᾰ :
  -- λ (_x : Σ' (ᾰ : ℕ), ℕ),
  --   has_well_founded.wf.fix
  --     (λ (_x : Σ' (ᾰ : ℕ), ℕ),
  --        _x.cases_on
  --          (λ (fst snd : ℕ),
  --             fst.cases_on
  --               (id_rhs ((Π (_y : Σ' (ᾰ : ℕ), ℕ),
  --                  (λ (_F : Π (_y : Σ' (ᾰ : ℕ), ℕ
  --               (λ (fst : ℕ),
  --                  id_rhs ((Π (_y : Σ' (ᾰ : ℕ), ℕ),
  --                    (λ (_F : Π (_y : Σ' (ᾰ : ℕ), ℕ
  --                       have this : snd % fst.succ < fst.succ, from _
  --                       _F ⟨snd % fst.succ, fst.succ⟩ _))))
  --     _x
  

Notation in the code

Now, as for your case, you are interested in the notation <. Maybe you find this in the code:

theorem bar (n : nat) : n < n + 1 := sorry

If you see this in the code, in VS Code you can hover over < (in the online editor click on <) it will tell you that < stands for

has_lt.lt : Π {α : Type} [self : has_lt α], α → α → Prop

This is somewhat helpful, but all it really tells you is that < is notation for the type class has_lt.lt. It doesn't tell you what instance of has_lt is filling in that particular occurrence of <. To get that information, there are four methods I know about:

• Go to the mathlib documentation of has_lt and you can see all the instances. Since you know in this case you are working with natural numbers, the instance is likely nat.has_lt, which is a wrapper around nat.lt which is based on nat.less_than_or_equal.
• Add set_option pp.all true to the code and use #check to look at your term without any pretty printing. By turning the pretty printer off, you can see the details of what is going on:

  set_option pp.all true
  #check λ n : nat, n < n + 1
  -- λ (n : nat), @has_lt.lt.{0} nat nat.has_lt n (@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one)) : nat → Prop
  

  We see here that < is @has_lt.lt.{0} nat nat.has_lt, so again we are using the instance nat.has_lt to define < in this case.
• Again, use set_option pp.all true but just use the goal view. So in our goal:

  set_option pp.all true
  theorem bar (n : nat) : n < n + 1 := begin
  -- Goal:
  -- n: nat
  -- ⊢ @has_lt.lt.{0} nat nat.has_lt n (@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one))
  end
  

• If in VS Code, use the interactive widgets view of the goal (which should be on by default). In the right panel click on the n < n + 1 in the goal and you should see has_lt.lt ℕ nat.has_lt n n + 1. This again tells you that n < n + 1 is notation for has_lt.lt ℕ nat.has_lt n (n + 1).

Definition or notation inside a goal

If you encounter something unfamiliar in a goal, you can

• paste part of the goal into a #check statement in order to be able to hover on it or cntl-click,
• turn on set_option pp.all true before the theorem to see the goal without the pretty printing, or
• use the interactive widget interface in VS Code to learn more about the goal.

Note about set_option pp.all true

This is the nuclear option where we turn off everything. There are a number of other pretty printer (pp) options which you can toggle. Use #help options to find them and play with them.