division and numerals

Stream: general

[Kevin Buzzard]

-- example : 2 ∣ 4 := ⟨2, rfl⟩ -- fails
/-
invalid constructor ⟨...⟩, 'has_dvd.dvd' is not an inductive type
-/
--example : (2 : ℕ) ∣ 4 := ⟨2,rfl⟩ -- fails
--example : 2 ∣ (4 : ℕ) := ⟨2,rfl⟩ -- fails
example : (2 : ℕ) ∣ (4 : ℕ) := ⟨2,rfl⟩ -- works
--example (a : ℕ) : a ∣ a * 2 := ⟨2,rfl⟩ -- fails
example (a : ℕ) : a ∣ (a * 2 : ℕ) := ⟨2,rfl⟩ -- works
example (a : ℕ) : a ∣ a * (2 : ℕ) := ⟨2,rfl⟩ -- works

Why do so many of these fail? In particular the fourth one: why does Lean need to be told that a * 2 is a nat when it knows a is a nat? The type of has_dvd.dvd (the notation) is α → α → Prop and it is looking straight at two nats when it decides how to deal with what alpha is.

[Gabriel Ebner]

Now you know why by exact is so popular. :smile:

[Gabriel Ebner]

The reason is that while Lean does know at some point that | is the divisibility relation on a commutative semiring defined by ∃ x, ...; Lean only figures this out too late, after ⟨2, rfl⟩ is elaborated. It looks like a bug that could be fixed by synthesizing instances before elaborating anonymous constructors.

[Gabriel Ebner]

In this example, you can also force instances to be synthesized before elaborating the proof by using lemma instead of example.

[Gabriel Ebner]

(Oh, and by exact foo also changes the order in which things are elaborated. Tactics are called last; this has the effect of elaborating foo later than the rest of the term, when typeclass instances, etc. will have hopefully been figured out.)

[Kevin Buzzard]

I now feel like I've asked this question several times. I think it's about time I understood the answer properly. My current understanding of the answer, which I guess I already had when I posted, is "it's all to do with when elaboration occurs". I hadn't realised this one was in the "lemma / example makes a difference" category and I know I've asked at least one of these before.