Zulip Chat Archive

Stream: general

Topic: filling in an underscore


view this post on Zulip Kevin Buzzard (Mar 29 2018 at 17:11):

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

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 17:12):

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

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 17:13):

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

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 17:13):

or proved it

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 17:13):

or decided it didn't care if it was true

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 17:14):

Note that the result is proved in the definition of gres

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 17:14):

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

view this post on Zulip Chris Hughes (Mar 29 2018 at 17:32):

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

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 17:42):

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

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 16:22):

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

view this post on Zulip Mario Carneiro (Mar 30 2018 at 18:21):

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

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 22:38):

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"

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 22:38):

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

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 22:39):

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.

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 22:40):

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

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 22:41):

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

view this post on Zulip Kenny Lau (Mar 30 2018 at 22:42):

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

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 22:44):

No, just sufficiently advanced technology.

view this post on Zulip Kenny Lau (Mar 30 2018 at 22:44):

which is canonically isomorphic though

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 22:44):

so I heard


Last updated: May 14 2021 at 06:16 UTC