# Zulip Chat Archive

## Stream: new members

### Topic: Question in first_proofs.lean

#### Daniel Donnelly (Aug 25 2019 at 21:15):

lemma inf_lt {A : set ℝ} {x : ℝ} (hx : x is_an_inf_of A) :

∀ y, x < y → ∃ a ∈ A, a < y :=

begin

-- Let `y`

be any real number.

intro y,

-- Let's prove the contrapositive

-- ( ... )

end

How does Lean know that `intro y`

means that `y`

is asserted to be a real number? Is that hidden in the prototype somehow?

#### Chris Hughes (Aug 25 2019 at 21:21):

It guesses that it should be a real, because of the inequality `x < y`

and `x`

is real.

#### Patrick Massot (Aug 25 2019 at 21:27):

It is very important to understand that the first and most essential automation that Lean (or any self-respecting proof assistant) will provide is elaboration: filling in missing information. In the statement I could have written `∀ y :ℝ , x < y → ∃ a ∈ A, a < y`

. But Lean figured out the type of `y`

from the following bit `x < y`

.

#### Daniel Donnelly (Aug 25 2019 at 21:30):

Learning Lean is a greater experience than I once thought that it would be. What I mean is that I'm enjoying it and am also impressed with its features.

#### Patrick Massot (Aug 25 2019 at 21:31):

The two main types of elaboration that Lean performs are unification and type class inference. Here you see unification. When Lean meets "∀ y,", where the type of `y`

is not provided, it creates a so-called meta-variable for this missing information, typically denoted by something like `?M_1`

. Then reading `x < y`

and knowing that `x`

has type real creates a constraint `?M_1 = ℝ`

that is straightforward to "unify" by setting `?M_1`

, but there are many cases where Lean has to work much harder (e.g. cleverly unfolding definitions).

#### Patrick Massot (Aug 25 2019 at 21:34):

But then we immediately get a new problem while reading `x < y`

. It also triggers a type class resolution elaboration : we need to find a meaning for `<`

on `ℝ`

, ie an "instance" of `has_lt ℝ`

.

#### Patrick Massot (Aug 25 2019 at 21:41):

You can type

set_option trace.class_instances true example := (by apply_instance : has_lt ℝ)

and look at the bottom of the Lean messages view to see the effort Lean did to find this instance. Where I am it succeeds right away. But looking at something slightly more complicated, like `comm_ring ℝ`

, I see:

[class_instances] class-instance resolution trace [class_instances] (0) ?x_0 : comm_ring ℝ := @Huber_ring.to_comm_ring ?x_1 ?x_2 [class_instances] (0) ?x_0 : comm_ring ℝ := @uniform_space.comm_ring ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 failed is_def_eq [class_instances] (0) ?x_0 : comm_ring ℝ := @uniform_space.completion.comm_ring ?x_6 ?x_7 ?x_8 ?x_9 ?x_10 failed is_def_eq [class_instances] (0) ?x_0 : comm_ring ℝ := @localization.comm_ring ?x_11 ?x_12 ?x_13 ?x_14 failed is_def_eq [class_instances] (0) ?x_0 : comm_ring ℝ := @subalgebra.comm_ring ?x_15 ?x_16 ?x_17 ?x_18 ?x_19 ?x_20 failed is_def_eq [class_instances] (0) ?x_0 : comm_ring ℝ := @algebra.comap.comm_ring ?x_21 ?x_22 ?x_23 ?x_24 ?x_25 ?x_26 ?x_27 ?x_28 failed is_def_eq [class_instances] (0) ?x_0 : comm_ring ℝ := complex.comm_ring failed is_def_eq [class_instances] (0) ?x_0 : comm_ring ℝ := real.comm_ring

Because I'm typing this randomly in the middle of a file about Huber rings (a crucial piece of the definition of perfectoid spaces), Lean first try to find a Huber ring structure on `ℝ`

then see if it's the separated quotient of some uniform space, or the completion of a topological ring (which is not how it's currently defined in mathlib) or a localization etc. until it tries the correct instance.

#### Patrick Massot (Aug 25 2019 at 21:42):

Actually this process is what most experienced Lean users complain about the most frequently in this forum. For instance, I wish Lean would first try to search an instance by name, following the naming convention it uses itself when you don't name an instance. In that case it would find `real.comm_ring`

right away.

#### Patrick Massot (Aug 25 2019 at 21:44):

The above trace is very short because there is no failed attempt that goes on recursively trying to solve other instance resolutions. But sometimes it gets really hairy, and fails after hitting some maximal depth search

#### Patrick Massot (Aug 25 2019 at 21:45):

And now I'll go sleeping. Actual computer science experts will correct what I explained wrong (I'm a mathematician).

#### Daniel Donnelly (Aug 25 2019 at 21:50):

Thank you for the details. I will try out that trace command :)

Last updated: May 10 2021 at 00:31 UTC