Zulip Chat Archive

Stream: general

Topic: meta-variable war?


Patrick Massot (Apr 13 2020 at 15:47):

The following proof works:

example (n : ) (h :  k, n  2*k) : ¬  k, n = 2*k :=
begin
  intros h_exist,
  cases h_exist with k hk,
  apply h,
  exact hk,
end

But if you switch lines 2 and 3 then it no longer works. It seems cases somehow messes up the meta-variables created by apply. Does anyone understand what happens here? (by the way, the above is a MWE, no import required).

Rob Lewis (Apr 13 2020 at 16:00):

Maybe this is one of those situations where term mode is clearer than tactic mode!

example (n : ) (h :  k, n  2*k) : ¬  k, n = 2*k :=
λ h_exist, h _ (exists.elim h_exist (λ k hk, hk))

This is the term you're trying to construct in your failing proof. What goes in the placeholder after h?

Reid Barton (Apr 13 2020 at 16:01):

As a general principle, it's better to use cases on this ∃ while your goal is a proposition

Patrick Massot (Apr 13 2020 at 16:04):

Reid, the goal is a proposition in both cases.

Patrick Massot (Apr 13 2020 at 16:07):

Rob, if I start the proof with refine λ h_exist, h _ (exists.elim h_exist (λ k hk, hk)), then Lean doesn't give me a chance to fill the hole.

Rob Lewis (Apr 13 2020 at 16:10):

Because that's not a good proof. Nothing can fill that hole. h needs a k and a proof of something that depends on k. But you've constructed that proof first, for a k that's out of scope at the moment you apply h.

Patrick Massot (Apr 13 2020 at 16:16):

Hmm

Kevin Buzzard (Apr 13 2020 at 16:19):

Whenever I see those [_] brackets in the goal I know I'm doomed. You can get them by applying delta too many times as well.

Rob Lewis (Apr 13 2020 at 16:19):

Note that you can do this if you "destruct" the existential using classical.some.

example (n : ) (h :  k, n  2*k) : ¬  k, n = 2*k :=
λ h_exist, h (classical.some h_exist) (classical.some_spec h_exist)

Rob Lewis (Apr 13 2020 at 16:20):

Because now the witness is classical.some h_exist which is in scope when you apply h.

Kevin Buzzard (Apr 13 2020 at 16:24):

Tactic mode illustration of the problem:

import tactic

example (n : ) (h :  k, n  2*k) : ¬  k, n = 2*k :=
begin
  intros h_exist,
  apply h,
  cases h_exist with k hk,
  swap,
  -- use k, -- there is no k!
  -- cases h_exist, -- recursor can only eliminate into prop
  use classical.some h_exist,
  convert hk,
  -- now h_exist has gone!
  sorry
end

Last updated: Dec 20 2023 at 11:08 UTC