Zulip Chat Archive

Stream: general

Topic: let and rfl in rcases


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 27 2020 at 09:52):

What proof state are you hoping for after the rcases?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)} = ∅

view this post on Zulip Reid Barton (Aug 27 2020 at 10:56):

what about not writing rfl but just hK?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Aug 27 2020 at 19:43):

I was probably trying to over-optimize.

view this post on Zulip 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).

view this post on Zulip Patrick Massot (Aug 27 2020 at 19:45):

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

view this post on Zulip Reid Barton (Aug 27 2020 at 19:45):

ssrcases


Last updated: May 11 2021 at 22:14 UTC