let and rfl in rcases

Stream: general

[Patrick Massot]

@Mario Carneiro is there anything we can do to avoid the error in:

import tactic

example (n : ℕ) : true :=
begin
  let s := {k | k < n},
  rcases set.eq_empty_or_nonempty s with (rfl | hs),

end

[Mario Carneiro]

rcases doesn't actually do the dirty work here, it's all cases and subst doing the heavy lifting. They both fail here; rfl uses subst so you are seeing this:

set_option trace.app_builder true
example (n : ℕ) : true :=
begin
  let s := {k | k < n},
  cases set.eq_empty_or_nonempty s with e hs,
  subst e,
/-
[app_builder] failed to build eq.rec, invalid motive:
let s : set ℕ := {k : ℕ | k < n} in true
-/
end

while cases gives

set_option trace.app_builder true
example (n : ℕ) : true :=
begin
  let s := {k | k < n},
  cases set.eq_empty_or_nonempty s with e hs,
  cases e,
/-
cases tactic failed, unsupported equality between type and constructor indices
(only equalities between constructors and/or variables are supported, try cases on the indices):
(λ (a : ℕ), false) = λ (k : ℕ), k < n

state:
n : ℕ,
s : set ℕ := {k : ℕ | k < n},
e : s = ∅
⊢ ((λ (a : ℕ), false) = λ (k : ℕ), k < n) → e == _ → true
-/
end

[Reid Barton]

What proof state are you hoping for after the rcases?

[Mario Carneiro]

They have a point though; the hypothesis in question says {k : ℕ | k < n} = ∅ and you can't case on that

[Mario Carneiro]

Perhaps this is more to your liking:

example (n : ℕ) : true :=
begin
  generalize e : {k | k < n} = s,
  rcases set.eq_empty_or_nonempty s with rfl | hs,
end

[Patrick Massot]

My example is probably too minimized to make sense. I was looking again at an exercise of LFTCM. The tactic state before casing is:

X : Type u_1,
Y : Type u_2,
f : X → Y,
hf : continuous f,
ε : ℝ,
ε_pos : ε > 0,
K : set (X × X) := {p : X × X | ε ≤ d (f p.fst) (f p.snd)},
K_closed : is_closed K,
K_cpct : is_compact K
⊢ ∃ (δ : ℝ) (H : δ > 0), ∀ {a b : X}, d a b < δ → d (f a) (f b) < ε

And indeed I'd like rfl to bring me to a state where I have an assumption saying {p : X × X | ε ≤ d (f p.fst) (f p.snd)} = ∅

[Reid Barton]

what about not writing rfl but just hK?

[Patrick Massot]

This is what is done in the current proof, but then you need one extra step. It's not a big deal.

[Mario Carneiro]

If you write rfl, you are saying "get rid of this assumption by eliminating the lhs", not "unfold the let variable in this equality". There is no rcases step corresponding to unfold h (something tells me that if we keep going this route rcases patterns are going to turn into ssreflect, which is fine with me but possibly not others), but you can achieve the same effect by a type ascription, that is rcases ... with (hK : {p | _} = _) | hs.

[Patrick Massot]

I was probably trying to over-optimize.

[Patrick Massot]

I'd like to show this proof in a propaganda talk I've been asked to give to students (150 students in 4th and 5th year).

[Patrick Massot]

But I've already simplified the proof enough (compared to what is in the LFTCM repo).

[Reid Barton]

ssrcases