Behavior of cases and cases'

Stream: general

[Sorawee Porncharoenwase]

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]

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

[Mario Carneiro]

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

[Sorawee Porncharoenwase]

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]

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]

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]

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