Stream: general

Topic: Behavior of cases and cases'

Sorawee Porncharoenwase (Jan 18 2021 at 05:03):

Consider:

example {xs : list ℕ} (h : (id xs).length = 1) :
∃ e, (id xs) = [e] :=
begin
sorry,
end


If I cases (id xs), I will get:

case list.nil
xs: list ℕ
h: list.nil.length = 1
⊢ ∃ (e : ℕ), list.nil = [e]
case list.cons
xs: list ℕ
hd: ℕ
tl: list ℕ
h: (hd :: tl).length = 1
⊢ ∃ (e : ℕ), hd :: tl = [e]


So that's great. id xs is replaced uniformly throughout context and goal.

But suppose I cases h' : id xs instead, I will get:

case list.nil
xs: list ℕ
h: (id xs).length = 1
h': id xs = list.nil
⊢ ∃ (e : ℕ), list.nil = [e]
case list.cons
xs: list ℕ
h: (id xs).length = 1
hd: ℕ
tl: list ℕ
h': id xs = hd :: tl
⊢ ∃ (e : ℕ), hd :: tl = [e]


Judging from the documentation, which says:

cases h : e, where e is a variable or an expression, performs cases on e as above, but also adds a hypothesis h : e = ... to each hypothesis, where ... is the constructor instance for that particular case.

I was led to believe that cases h' : id xs should be the same as cases (id xs), except that a hypothesis h': id xs = ... is added. This is clearly not the case. Is it the expected behavior?

(Yes, I can rewrite h' at * afterward, but it's kinda annoying that I need to do that. For now, I write a tactic to perform this additional step, but I hope that I don't need that).

cases' (id xs), on the other hand, doesn't replace id xs in the context at all:

case list.nil
xs: list ℕ
h: (id xs).length = 1
⊢ ∃ (e : ℕ), list.nil = [e]
case list.cons
xs: list ℕ
h: (id xs).length = 1
hd: ℕ
x: list ℕ
⊢ ∃ (e : ℕ), hd :: x = [e]


And cases' h' : (id xs) gives the same result as cases h' : (id xs).

Mario Carneiro (Jan 18 2021 at 05:05):

what's the point of the equality if you are replacing all instances of the variable?

Mario Carneiro (Jan 18 2021 at 05:06):

If you want more control over this you should use generalize_hyp + cases e

Sorawee Porncharoenwase (Jan 18 2021 at 05:24):

what's the point of the equality if you are replacing all instances of the variable?

Yes, there would be no point for a _variable_. But my issue is with an arbitrary _expression_. For expressions, a case analysis without the equality hypothesis could lose information. Consider for example:

def id2 (xs : list ℕ) := xs

example {xs : list ℕ} (h : (id xs).length = 1) :
∃ e, (id2 xs) = [e] :=
begin
sorry,
end


If I split on id xs without generating the equality hypothesis, I would not be able to prove the example.

If you want more control over this you should use generalize_hyp + cases e

Thanks. I suppose that would work, in the same way that cases h' : e; rewrite h' at * would work. I guess I'm not really asking how to solve the problem because I do have a solution already, but just want to ask if the current behavior of cases and cases' is considered a bug.

Mario Carneiro (Jan 18 2021 at 05:39):

The nonreplacement behavior of cases' e sounds like a bug, but I've never used it so I'm not sure what it's trying to address. I don't think that it's necessarily a problem that some actions require a combination of two tactics; adding lots of bells and whistles on one tactic doesn't decrease the complexity budget at all, so if that sequence of tactics has the desired effect then I would say just use that

Yakov Pechersky (Jan 18 2021 at 06:30):

If you need the presence of the hypothesis to solve the goal, it is possible you'll need the hypothesis at a point even after initial global replacement. Consider the tactic proof for docs#parser.bind_eq_done, if the hypothesis on the case of the parser wasn't around, the newly appearing case of the parser after following the relevant bind branch wouldn't be dischargeable.

Jannis Limperg (Jan 18 2021 at 14:56):

The cases' behaviour definitely looks like a bug. I'll check what's going on.

Last updated: May 13 2021 at 18:26 UTC