Question in first_proofs.lean

Stream: new members

[Daniel Donnelly]

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]

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

[Patrick Massot]

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]

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]

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]

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]

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]

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]

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]

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

[Daniel Donnelly]

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