leaky option

Stream: general

[Kevin Buzzard]

@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]

shouldn't you use bot instead of none?

[Mario Carneiro]

it's because you used none

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

Oh!

[Mario Carneiro]

show 𝕋, from none has type T

[Mario Carneiro]

or @id 𝕋 none

[Mario Carneiro]

but these options leave a trace in the term

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

or (none + x : 𝕋)

[Kevin Buzzard]

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]

or (none + x : 𝕋)

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

[Mario Carneiro]

right

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

or if there is no such thing it will also fail

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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]

Aah, of course it compiles.

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

Maybe there is some weird meta hack

[Mario Carneiro]

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

[Patrick Massot]

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.