# Zulip Chat Archive

## 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