cases unfolding stuff

Stream: general

[Reid Barton]

Is there any way to get cases to not do this kind of unfolding?

inductive P : set ℕ → Prop
| z : P {0}

example (s : set ℕ) (h : P s) : true :=
begin
  cases h,
/-
h : P (λ (b : ℕ), b = 0)
⊢ true
-/
end

[Reid Barton]

I guess I could apply the recursor directly

[Reid Barton]

I suppose another question is whether this is a bug or a feature

[Reid Barton]

aha, is it unfolding in order to check if the case might be impossible somehow?

[Reid Barton]

In any case, applying the recursor by hand was easy enough :checkbox:

[Jannis Limperg]

Reid Barton said:

aha, is it unfolding in order to check if the case might be impossible somehow?

Yeah exactly. cases could be more careful to preserve the original expression when it does this.

[Reid Barton]

Would that be difficult? I'm not familiar with the implementation of cases

[Floris van Doorn]

If you just want to apply the recursor, use induction instead.

cases will do more than just applying the recursor when working with inductive families. For example:

• cases v where v : dvector \a 0 will change v to nil (dvector is the type of vectors as an inductive family)
• cases h where h : succ n = succ m will change h to rfl (or at least remove the applications of succ.

[Floris van Doorn]

(that said, maybe we can improve cases so that it reverts any unfolding if it didn't make (enough) progress).

[Reid Barton]

Thanks, induction is much nicer!