Zulip Chat Archive

Stream: new members

Topic: Question in first_proofs.lean


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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 ℝ.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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