Zulip Chat Archive

Stream: new members

Topic: cases with doesn't rename


Horatiu Cheval (Mar 13 2021 at 10:48):

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 (Mar 13 2021 at 11:47):

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 (Mar 13 2021 at 11:48):

cases h with x p σ t u ht hu works

Mario Carneiro (Mar 14 2021 at 05:31):

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


Last updated: Dec 20 2023 at 11:08 UTC