meta-variable war?

Stream: general

[Patrick Massot]

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]

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]

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

[Patrick Massot]

Reid, the goal is a proposition in both cases.

[Patrick Massot]

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]

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]

Hmm

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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