Implementation of exact

Stream: lean4

[Filippo A. E. Nuccio]

Until stumbling upon this unexpected behaviour

example (h : 0 < -1) : False := by
exact (Int.negSucc_not_nonneg (0 + 0).succ).mp h -- fails
exact (Int.negSucc_not_nonneg (0 + 0).succ).mp (by exact h) -- is OK

I was convinced that exact was really not doing much. Then I tried to look inside its definition in docs#Lean.Elab.Tactic.evalExact and I cannot understand what, in that definition, is responsible for the behaviour in the example above.

[Damiano Testa]

Could it be the EnsuringType kicking in?

[Filippo A. E. Nuccio]

On line 76, you mean?

[Damiano Testa]

Indeed (I'm on mobile, sorry for being cryptic).

[Damiano Testa]

I think that there you pass extra information to Lean.

[Mario Carneiro]

also by delays elaboration

[Filippo A. E. Nuccio]

(deleted)

[Filippo A. E. Nuccio]

Damiano Testa said:

Indeed (I'm on mobile, sorry for being cryptic).

But then why does it succeed in the second call? After

apply (Int.negSucc_not_nonneg (0 + 0).succ).mp

is expects a term of the same type.

[Filippo A. E. Nuccio]

Mario Carneiro said:

also by delays elaboration

Can you expand a bit on this?

[Damiano Testa]

I think that there are a few things at play that end up having similar effects. I hope that if I say something wrong, someone will correct me!

When you write a proof (especially in tactic mode), you often leave work to lean to do to figure out what lots of implicit terms are. The two mechanism for addressing incomplete information that are at play here are

• using information from the goal to squeeze out some more information,
• wait out until some other missing terms have been figured out and use that information to fill in more blanks.

The former is what exact does (possibly with the EnsuringType).

The latter is probably what Mario is referring to: when Lean sees by it decides to try harder to figure out the rest, before coming back to this specific hole.

apply creates a new metavariable. In this context it probably means that it decides to delay figuring out what the hole is until you give it more information after apply is done.

Often, information is redundant enough that these three methods work interchangeably. Sometimes, the information is involved enough that some of these methods work, while others do not.

[Damiano Testa]

I honestly do not know the details of what is going on here, but I'm guessing that some combination of the above plays a role! :smile:

[Filippo A. E. Nuccio]

Thanks! What you say agrees (about exact and apply, I had no idea that by really do have some effect) with my rough picture. But if someone is willing to fill in more details I'd be happy to read them! :nerd:

[Mario Carneiro]

I believe the issue here is the expression (0 + 0).succ. Lean doesn't know what function .succ is referring to, because it doesn't know the type of 0 + 0, because it's waiting for the type of 0 to be resolved. It will be default-resolved to Nat, but this is supposed to happen "last", and in particular it tries to resolve the application involving h before type defaulting. But because the whole expression (0+0).succ is stuck, all it knows is that the type of (Int.negSucc_not_nonneg ?).mp is 0 ≤ Int.negSucc ? → False so applying that to h means solving 0 < -1 =?= 0 ≤ Int.negSucc ?, which is wrong on a few levels.

[Mario Carneiro]

note that even the version that works is pretty sus, you have h : 0 < -1 and the function is expecting a proof of 0 <= -2

[Filippo A. E. Nuccio]

Mario Carneiro said:

I believe the issue here is the expression (0 + 0).succ. Lean doesn't know what function .succ is referring to, because it doesn't know the type of 0 + 0, because it's waiting for the type of 0 to be resolved. It will be default-resolved to Nat, but this is supposed to happen "last", and in particular it tries to resolve the application involving h before type defaulting. But because the whole expression (0+0).succ is stuck, all it knows is that the type of (Int.negSucc_not_nonneg ?).mp is 0 ≤ Int.negSucc ? → False so applying that to h means solving 0 < -1 =?= 0 ≤ Int.negSucc ?, which is wrong on a few levels.

Oh, I see. You mean that at the point Int.negSucc_not_nonneg it is just waiting for a Nat, and there might be a function .succ from some type T to Nat that maps ((0 : T) + (0 : T)).succ to some Nat, and Lean is waiting to undestand what T is?

[Mario Carneiro]

exactly

[Mario Carneiro]

I think if you did (.succ (0 + 0)) instead it would work since the type deduction goes the other way

[Filippo A. E. Nuccio]

Oh, nice. But then why all this disappears in the second call? When you say that by delays elaboration, do you mean that after the by Lean creates a metavariable precisely there T should land?

[Mario Carneiro]

because by comes after the default types are resolved

[Mario Carneiro]

by has even lower priority than default types

[Mario Carneiro]

(everyone wants to come last)

[Filippo A. E. Nuccio]

Mario Carneiro said:

I think if you did (.succ (0 + 0)) instead it would work since the type deduction goes the other way

Indeed, it works as (you) expected!

[Matthew Ballard]

Related https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Heavy.20rfl/near/469781815

[Filippo A. E. Nuccio]

Mario Carneiro said:

because by comes after the default types are resolved

But is it " coming" somewhere? Or do you mean that every term constructed with a by comes last?

[Mario Carneiro]

every by block is delayed until every other elaboration problem and available trick is used

[Mario Carneiro]

that way the goal state doesn't have confusing metavariables in it which are already resolved later in the term

[Filippo A. E. Nuccio]

Oh, so this really have little to do with exact in the end, it is really the priority ofby.

[Filippo A. E. Nuccio]

Wow.

[Mario Carneiro]

one of the design criteria of tactic mode is that elaboration should be predictable and in-order top down

[Filippo A. E. Nuccio]

And just to be sure: the (.succ (0+0)) trick works because Lean parses right to left and first sees the 0, it defaults it to 0 : Nat, so .succ must be Nat.succ and everything goes smoothly?

[Mario Carneiro]

but term mode is a crazy dance of priorities and out of order execution

[Mario Carneiro]

It's not because of parsing order, it's because (.succ ...) elaborates to T.succ where T is the expected type, while (...).succ elaborates to T.succ where T is the type of (...)

[Mario Carneiro]

we know the expected type is Nat, we don't know the type of 0 + 0

[Kyle Miller]

This works too:

example (h : 0 < -1) : False :=
  (Int.negSucc_not_nonneg (0 + 0 : Nat).succ).mp h

[Filippo A. E. Nuccio]

Mario Carneiro said:

It's not because of parsing order, it's because (.succ ...) elaborates to T.succ where T is the expected type, while (...).succ elaborates to T.succ where T is the type of (...)

Crystal clear, thanks! :crystal: (although dotted identifier notation is still somewhat arcane to me in its implementation details).

[Mario Carneiro]

don't worry, it's arcane even to the people that wrote it