filling in an underscore

Stream: general

[Kevin Buzzard]

import data.fintype
import algebra

universes u v
-- Chris multiset example

theorem meh {i : ℕ} {n : ℕ} : i < n → i < nat.succ n := λ H, lt.trans H $ nat.lt_succ_self _

theorem miracle (f : ℕ → ℕ)
(d : ℕ)
(Hd :
  ∀ (g : fin d → ℕ),
    (∀ (i : fin d), f (i.val) = g i) →
      finset.sum (finset.range d) f = finset.sum finset.univ g)
(g : fin (nat.succ d) → ℕ)
(h : ∀ (i : fin (nat.succ d)), f (i.val) = g i)
: finset.sum (finset.range d) f = finset.sum finset.univ (λ (i : fin d), g ⟨i.val, meh i.is_lt⟩)
:=
let gres : fin d → ℕ := λ (i : fin d), g ⟨i.val, meh i.is_lt⟩ in
begin
rw Hd gres (λ i, h ⟨i.val,_⟩)
end

[Kevin Buzzard]

Lean magically filled in the underscore in the last but one line

[Kevin Buzzard]

It either guessed that i<n -> i<succ n

[Kevin Buzzard]

or proved it

[Kevin Buzzard]

or decided it didn't care if it was true

[Kevin Buzzard]

Note that the result is proved in the definition of gres

[Kevin Buzzard]

(gres is the restriction of g : fin (d+1) -> nat, to fin d)

[Chris Hughes]

I think it proved it. Looking at the proof term, it used lt_succ_of_lt. I didn't know lean could do that.

[Kevin Buzzard]

What triggered that? Is it the rw ? I tried to minimise this but didn't get far.

[Kevin Buzzard]

@Mario Carneiro can you clarify what is going on here?

[Mario Carneiro]

The rw is a confounder here. You could equally well use exact Hd gres (λ i, h ⟨i.val, _⟩) to close the goal. Here are some intermediate data points:

Hd gres (λ i, _) -- -> looking for proof of ⊢ f (i.val) = gres i

Hd gres (λ i, h _)
type mismatch at application
  Hd gres (λ (i : fin d), h ?m_1[i])
term
  λ (i : fin d), h ?m_1[i]
has type
  ∀ (i : fin d), f (?m_1[i].val) = g ?m_1[i]
but is expected to have type
  ∀ (i : fin d), f (i.val) = gres i

Hd gres (λ i, h ⟨_, _⟩) -- works

Lean isn't magically guessing the proof, it's unfolding gres and unifying with the enclosed proof

[Kevin Buzzard]

Oh I see. The moment I saw rw I thought "I don't understand that tactic properly, maybe it's doing something under the hood, so I give in"

[Kevin Buzzard]

But now you tell me exact works I can just debug it myself with pp.proofs true.

[Kevin Buzzard]

I used to think of stuff like type class inference and proofs being magicked around was just all part of some magic, it's only now I begin to realise that everything that happens, happens for a really precise reason.

[Kevin Buzzard]

In some sense I still draw the line at reading tactic.interactive (partly because I know it will be incomprehensible).

[Kevin Buzzard]

but really it's because I feel like "end users" shouldn't have to know anything about a tactic other than what is documented.

[Kenny Lau]

I used to think of stuff like type class inference and proofs being magicked around was just all part of some magic, it's only now I begin to realise that everything that happens, happens for a really precise reason.

there is no magic in lean

[Kevin Buzzard]

No, just sufficiently advanced technology.

[Kenny Lau]

which is canonically isomorphic though

[Kevin Buzzard]

so I heard