inversion

Stream: Is there code for X?

[Patrick Thomas]

Suppose I have:

def var := ℕ

inductive term : Type
| var : var → term
| app : term → term → term
-- term.abs y P = λ y . P
| abs : var → term → term


-- sub_is_def M x N means M [ x := N ] is defined
inductive sub_is_def : term → var → term → Prop

-- y [ x := N ] is defined
| var (y : var) (x : var) (N : term) :
  sub_is_def (term.var y) x N

-- P [ x := N ] is defined → Q [ x := N ] is defined → (P Q) [ x := N ] is defined
| app (P : term) (Q : term) (x : var) (N : term) :
  sub_is_def P x N → sub_is_def Q x N → sub_is_def (term.app P Q) x N

-- x = y → ( λ y . P ) [ x := N ] is defined
| abs_same (y : var) (P : term) (x : var) (N : term) :
  x = y → sub_is_def (term.abs y P) x N

-- x ≠ y → x ∉ FV ( λ y . P ) → ( λ y . P ) [ x := N ] is defined
| abs_diff_nel (y : var) (P : term) (x : var) (N : term) :
  x ≠ y → x ∉ FV (term.abs y P) → sub_is_def (term.abs y P) x N

-- x ≠ y → y ∉ FV ( N ) → P [ x := N ] is defined → ( λ y . P ) [ x := N ] is defined
| abs_diff (y : var) (P : term) (x : var) (N : term) :
  x ≠ y → y ∉ FV N → sub_is_def P x N → sub_is_def (term.abs y P) x N

notation M `[` x `:=` N `]` `is_def` := sub_is_def M x N

and H1: (P.app Q)[x:=N]is_defin the context. Is there a tactic to add P [ x := N ] is_def and Q [ x := N ] to the context? I think this might be something like inversion in Coq?

[Alex J. Best]

Check out https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20.60inversion.60.20tactic.3F/near/257345089,, the answer is probably cases H1 but your #mwe doesn't copy paste into lean and work so I can't check

[Patrick Thomas]

Yes, cases H1 worked. Thank you.

[Patrick Thomas]

Is there a way to specify the names of the resulting hypotheses? Adding with doesn't seem to have any effect.

[Eric Wieser]

Try with x y z w

[Eric Wieser]

Sometimes some of the names are ignored

[Eric Wieser]

So just keep adding more!

[Patrick Thomas]

Yes, that does it. I had to use cases H1 with _ _ _ _ _ _ _ H1_P H1_Q. Do you know why?

[Floris van Doorn]

cases replaces the relevant terms by variables (+ equalities that these variables are equal to the terms you had) and then applies induction on that variable. Then the equalities are used to get rid of all impossible cases.
The names for the underscores are probably used for the impossible cases that are removed before you see them. cases is not very smart with the variable names it uses.

[Patrick Thomas]

Thank you.