inductive rule inversion

Stream: general

[Ariel Davis]

Hi :wave: I'm trying to use Lean to prove stuff about a simple expression language e ::= zero | succ(e) | true | false. The language has types, so e.g. e: nat => succ(e): nat. I'm trying to prove the inversion of one of the inductive rules, so succ(e): nat => e: nat like the following, but I'm not sure how to say that 'only one of the rules in the inductive definition can possibly apply'. Sorry if this is a super basic question :bow:

inductive exp: Type
| zero: exp
| succ: exp -> exp
| true_: exp
| false_: exp

inductive typ: Type
| nat: typ
| bool: typ

inductive has_typ: exp -> typ -> Prop
| zero: has_typ exp.zero typ.nat
| succ (e: exp): has_typ e typ.nat -> has_typ (exp.succ e) typ.nat
| true_: has_typ exp.true_ typ.bool
| false_: has_typ exp.true_ typ.bool

theorem inversion_succ (e: exp) (typing: has_typ (exp.succ e) typ.nat): has_typ e typ.nat :=
begin
  induction typing,
  case has_typ.zero { sorry },
  case has_typ.succ { exact typing_ih },
  case has_typ.true_ { sorry },
  case has_typ.false_ { sorry },
end

[Mario Carneiro]

try cases typing

[Mario Carneiro]

Incidentally, your inversion theorem can be strengthened to has_typ (exp.succ e) A -> A = typ.nat /\ has_typ e typ.nat

[Mario Carneiro]

also, true is not a keyword, so you don't have to use true_

[Ariel Davis]

great, thanks :D