cases with doesn't rename

Stream: new members

[Horatiu Cheval]

I encountered situations when cases h with h1 h2 ... doesn't rename the introduced hypotheses as I would expect. For example:

inductive type
| zero : type
| arrow : type → type → type

infixr `↣` : 50 := type.arrow

inductive preterm
| var : ℕ → preterm
| app : preterm → preterm → preterm

inductive wt  : preterm → type → Prop
| var : ∀ (x : ℕ), wt (preterm.var x) type.zero
| app : ∀ (ρ σ : type) (t u : preterm), wt t (ρ ↣ σ) → wt u ρ → wt (t.app u) σ

example (t : preterm) (τ : type) : wt t τ → false  :=
begin
  intros h,
  induction t,
  case app: u v ihu ihv
  { cases h, /-breaks h in h_ρ h_ᾰ_1 h_ᾰ-/ }
end

I thought cases h with σ h1 h2 would rename the three introduced hypotheses, in this order, but it actually only replaces h_ρ with h1 (so the first one with second one), leaving the rest unchanged. What's happening here? How can I give names to the hypotheses?

[Eric Wieser]

Not your question, but something your example raises - it looks like the lean server puts the error message on the case when it should probably put it on the }. Is this easy to fix?

[Eric Wieser]

cases h with x p σ t u ht hu works

[Mario Carneiro]

Eric Wieser said:

Not your question, but something your example raises - it looks like the lean server puts the error message on the case when it should probably put it on the }. Is this easy to fix?

Not really. It is the case tactic that fails, and } is part of the syntax of case, not a separate tactic like with { tacs .. } where braces represent a separate syntax form that can be treated specially