differences in elaboration

Stream: general

[Gihan Marasingha]

If I copy out the definition of nat.no_confusion and call it nat.no_confusion', as below, Lean has no problems with the line nat.no_confusion' h in the proof of one_ne_two. But if I use nat.no_confusion itself, I need to write @nat.no_confusion _ _ _ h instead.

Two questions:

1. Why is there this difference in behaviour? That is, how does nat.no_confusion differ from nat.no_confusion'?
2. Why does @nat.no_confusion _ _ _ hwork when nat.no_confusion hdoesn't? The former expression seems to provide no more information than the latter.

universe l

@[reducible]
protected def nat.no_confusion' : Π {P : Sort l} {v1 v2 : ℕ}, v1 = v2 → nat.no_confusion_type P v1 v2 :=
λ {P : Sort l} {v1 v2 : ℕ} (h12 : v1 = v2),
  @eq.rec ℕ v1 (λ (a : ℕ), v1 = a → nat.no_confusion_type P v1 a)
    (λ (h11 : v1 = v1),
       @nat.cases_on (λ {v1 : ℕ}, nat.no_confusion_type P v1 v1) v1 (λ (a : P), a)
         (λ (n : ℕ) (a : n = n → P), a (@eq.refl ℕ n))) v2 h12 h12

open nat

lemma zero_ne_one : 0 ≠ 1 := λ h, nat.no_confusion' h

lemma one_ne_two : succ 0 ≠ succ (succ 0) :=
λ (h : succ 0 = succ(succ 0)),
have h₂ : (0 = succ 0 → false) → false, from
  nat.no_confusion' h,
h₂ zero_ne_one

[Eric Wieser]

The difference is that nat.no_confusion has @[elab_as_eliminator]

[Eric Rodriguez]

Is there any easy way to see what attributes there is? Maybe a #print attribute?

[Mario Carneiro]

regular #print will show you all the attributes on a definition

[Alex J. Best]

The elaborator works differently for "official" no_confusion applications https://github.com/leanprover-community/lean/blob/65ad4ffdb3abac75be748554e3cbe990fb1c6500/src/frontends/lean/elaborator.cpp#L1814 as you've made a new declaration by hand it doesnt satisfy is_no_confusion and so is not treated specially by the elaborator.

[Eric Wieser]

(id @nat.no_confusion) works too in place of nat.no_confusion'

[Mario Carneiro]

note that in the error message, the type that it thinks nat.no_confusion h ought to have:

nat.no_confusion_type ((0 = 1 → false) → false) 1 1.succ

unfolds to

(0 = 1 → (0 = 1 → false) → false) → (0 = 1 → false) → false

[Mario Carneiro]

that is, it is using the entire goal as the major premise, rather than just the right hand side of the implication

[Mario Carneiro]

this is the proof it was expecting you to write:

lemma one_ne_two : succ 0 ≠ succ (succ 0) :=
λ (h : succ 0 = succ(succ 0)),
  nat.no_confusion h $ λ h, nat.no_confusion h

[Gihan Marasingha]

Thanks all. It seems (unless I'm wildly mistaken [EDIT: I am wildly mistaken!]) that @Eric Wieser's answer is related to the answers to the question I asked yesterday about the use of id in generated proofs.

I don't yet understand enough about elaboration / type-checking to see why id helps the kernel in inferring the correct type. Does its use here prevent the special elaboration of no_confusion function applications mentioned by @Alex J. Best ?

[Mario Carneiro]

no, id is helping the kernel, after elaboration is complete. This no_confusion stuff is about how elaboration works, before we know all details of the given expression and are trying to fill metavariables

[Mario Carneiro]

the reason having id helps the kernel is because checking id B (id C e) : A entails proving that A is defeq to B and B is defeq to C and the type of e is defeq to C, while checking e : A means checking that the type of e is defeq to C

[Gihan Marasingha]

Thanks @Mario Carneiro. So would it be fair to say that I was wildly mistaken in my previous comment?

[Mario Carneiro]

obviously the first thing implies the second if you assume defeq is transitive, but it's not, and more to the point, there can be a large runtime cost difference between checking the former and the latter, even if the kernel can ultimately find its way to the end

[Mario Carneiro]

it's the same idea as giving a proof in small steps vs giving no hints and letting the reader come up with their own proof

[Mario Carneiro]

That said, most uses of id in tactics are superfluous. The reason they show up so often is because the primitive that does change inserts that identity term, in order to avoid the rare pathologies where dropping the id causes problems

[Yakov Pechersky]

Specifically, this part: image.png

[Gihan Marasingha]

I think I understand now. Just to make sure I'm not being an idiot, @Mario Carneiro, are those meant to be @ids in your example? If so, I see that the use of @id provides type information.

I also see that the answers to many of the questions I ask are found in your thesis, so I really should get round to reading it!

[Mario Carneiro]

yes those are @id

[Mario Carneiro]

by the way, show T, from e is syntactic sugar for @id T e

[Eric Wieser]

Can that be turned off in the pretty-printer?