## Stream: general

### Topic: let and rfl in rcases

#### Patrick Massot (Aug 27 2020 at 09:46):

@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 (Aug 27 2020 at 09:51):

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 (Aug 27 2020 at 09:52):

What proof state are you hoping for after the rcases?

#### Mario Carneiro (Aug 27 2020 at 09:52):

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

#### Mario Carneiro (Aug 27 2020 at 09:54):

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 (Aug 27 2020 at 10:54):

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 (Aug 27 2020 at 10:56):

what about not writing rfl but just hK?

#### Patrick Massot (Aug 27 2020 at 10:56):

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

#### Mario Carneiro (Aug 27 2020 at 19:42):

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 (Aug 27 2020 at 19:43):

I was probably trying to over-optimize.

#### Patrick Massot (Aug 27 2020 at 19:44):

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 (Aug 27 2020 at 19:45):

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

#### Reid Barton (Aug 27 2020 at 19:45):

ssrcases

Last updated: May 11 2021 at 22:14 UTC