Zulip Chat Archive

Stream: general

Topic: leaky option


Kevin Buzzard (May 31 2019 at 19:39):

@Amelia Livingston asked why this doesn't work:

import data.real.basic order.bounded_lattice

open option
def tropical := with_bot 
notation ` 𝕋 ` := tropical

noncomputable instance : has_add 𝕋 :=
⟨λ x y, option.cases_on x y $ λ x', option.cases_on y (some x') (λ y', some $ max x' y')

-- doesn't compile
lemma none_add (x : 𝕋) : (none : 𝕋) + x = x := sorry
/-
failed to synthesize type class instance for
x : 𝕋
⊢ has_add (option ℝ)
-/

lemma none_add' (x : 𝕋) : (none + x : 𝕋) = x := sorry -- works fine

The first attempt at none_add fails and I don't understand why. Explicitly telling Lean that (none : 𝕋) should surely force a typeclass search for has_add 𝕋, but somehow option leaks out.

Johan Commelin (May 31 2019 at 19:42):

shouldn't you use bot instead of none?

Mario Carneiro (May 31 2019 at 19:42):

it's because you used none

Kevin Buzzard (May 31 2019 at 19:42):

Patrick, Johan and I had troubles with option leaking out like this when we were using with_zero. We even considered writing our own with_zero which wasn't just a copy of option -- Patrick pointed out that we might not really be using any of the constructions which had been made for option anyway. In Edinburgh Patrick even suggested just writing our own class for totally ordered groups with a zero, and I am very much coming round to his way of thinking.

Johan Commelin (May 31 2019 at 19:42):

I don't know if that helps... but tropical is defined as with_bot ...

Mario Carneiro (May 31 2019 at 19:42):

(none : 𝕋) doesn't say "none, of type T", it says "none" and checks that this has type defeq to T

Kevin Buzzard (May 31 2019 at 19:43):

Oh!

Mario Carneiro (May 31 2019 at 19:43):

show 𝕋, from none has type T

Mario Carneiro (May 31 2019 at 19:43):

or @id 𝕋 none

Mario Carneiro (May 31 2019 at 19:43):

but these options leave a trace in the term

Kevin Buzzard (May 31 2019 at 19:44):

Oh this is a subtlety of which I was not at all aware, but am finally perhaps in a position to understand.

Mario Carneiro (May 31 2019 at 19:44):

I think ((+) : 𝕋 -> 𝕋 -> 𝕋) none x might work

Mario Carneiro (May 31 2019 at 19:45):

or (none + x : 𝕋)

Kevin Buzzard (May 31 2019 at 19:45):

So when Lean is trying to figure out what is going on with (none : \bbT) + x it decides that none has type option ?m, tries to unify option ?m with \bbT, decides that ?m is real, but then leaves none as type option real?

Kevin Buzzard (May 31 2019 at 19:45):

or (none + x : 𝕋)

Yes, that one works and was in my original post. Kenny pointed it out to us.

Mario Carneiro (May 31 2019 at 19:46):

right

Mario Carneiro (May 31 2019 at 19:47):

more importantly, the option ?m is the type that it's going to search for a + instance

Kevin Buzzard (May 31 2019 at 19:47):

right

But then why would bot make things any better? We'd just get bot of type with_zero real and this is not syntactically equal to \bbT

Mario Carneiro (May 31 2019 at 19:47):

You are right, it will find the + on with_bot in that case

Mario Carneiro (May 31 2019 at 19:48):

or if there is no such thing it will also fail

Mario Carneiro (May 31 2019 at 19:49):

But because has_bot is a typeclass you can give an instance of has_bot 𝕋 and then it will work

Mario Carneiro (May 31 2019 at 19:49):

more precisely, it won't be able to figure out the type at all looking at the + or bot, so it will find the x and get the type there

Mario Carneiro (May 31 2019 at 19:50):

aha, actually that will happen regardless... so you won't find the bot of with_bot real

Kevin Buzzard (May 31 2019 at 19:58):

import data.real.basic order.bounded_lattice

def tropical := with_bot 
notation ` 𝕋 ` := tropical

open lattice

instance with_bot.has_bot' : has_bot 𝕋 := by unfold tropical; apply_instance

noncomputable instance : has_add 𝕋 :=
⟨λ x y, option.cases_on x y $ λ x', option.cases_on y (some x') (λ y', some $ max x' y')

lemma bot_add (x : 𝕋) : ( : 𝕋) + x = x := sorry

This does compile

Kevin Buzzard (May 31 2019 at 19:58):

Aah, of course it compiles.

Kevin Buzzard (May 31 2019 at 19:59):

I had no idea that the elaborator did not read (x : t) as "this term must have type t" -- my understanding now is that it says "this term has some type which Lean can prove is definitionally equal to t but the elaborator reserves the right to insist that it has another type when trying to figure out some other types of other things later on in its elaboration journey"

Mario Carneiro (May 31 2019 at 20:03):

Note that the elaborator does get some information from (x : t), because it produces the goal "(expected type of x) =?= t" which may cause metavariables to be instantiated

Mario Carneiro (May 31 2019 at 20:03):

and then after that it continues with checking "x :? expected type"

Kevin Buzzard (May 31 2019 at 20:07):

Note that the elaborator does get some information from (x : t), because it produces the goal "(expected type of x) =?= t" which may cause metavariables to be instantiated

Just not the metavariable in @has_add.add ?m_1 ...

Mario Carneiro (May 31 2019 at 20:08):

ah, you are right, that description has the order wrong

Mario Carneiro (May 31 2019 at 20:08):

it first uses the expected type to elaborate x, then does "(expected type of x) =?= t"

Kevin Buzzard (May 31 2019 at 20:10):

Is there no way I can work out exactly what the elaborator is doing, short of reading the C++ (which I am not capable of doing, of course) or asking here?

Kevin Buzzard (May 31 2019 at 20:11):

Maybe there is some weird meta hack

Mario Carneiro (May 31 2019 at 20:36):

you can infer the behavior from various real and toy examples; that's what I do

Patrick Massot (Jun 01 2019 at 09:11):

Patrick, Johan and I had troubles with option leaking out like this when we were using with_zero. We even considered writing our own with_zero which wasn't just a copy of option -- Patrick pointed out that we might not really be using any of the constructions which had been made for option anyway. In Edinburgh Patrick even suggested just writing our own class for totally ordered groups with a zero, and I am very much coming round to his way of thinking.

For the record, let me point out that we had leaks only because we were incompetent. After some initial messing up we started to see leaking and, instead of fixing things properly, we started adding lemmas, or even simp lemmas, mixing leaked and non leaked version, making everything worse. I'm almost done refactoring all this.


Last updated: Dec 20 2023 at 11:08 UTC