I'm a beginner, and I'm confused as to a feature of the `induction`

tactic. In some cases, it will automatically derive more hypotheses then expected, with seemingly no way to name them. For example, consider this (rather silly) MWE:

```
Inductive NonEmpty {X: Type}: list X -> Prop := NE x l: NonEmpty (x :: l).
Theorem ne_thm : forall {X: Type} {l: list X}, (NonEmpty l) -> True.
Proof.
intros X l H.
destruct l as [| h t].
- apply I.
- inversion H as [h' t' Eh].
(* Hypotheses H0: t' = t *)
Abort.
```

The `inversion H`

command generates the hypotheses `H0: t' = t`

(on top of the expected `h'`

, `t'`

, and `Eh`

). My questions are

- How can I give this hypothesis an explicit name?
- Under what circumstances does
`inversion`

do this?

Probably should've searched this before asking... this comment answers my first question (`inversion H as [h' t' [Eh Et]].`

), but I don't understand why the conjunction notation works.

my policy is "if I need to use the names that come out of inversion then it's not the right tactic"

Note that one reasonable thing to do to clean-up the equalities introduced by `inversion`

is `subst`

, which is usually sufficient.

Last updated: Jun 13 2024 at 21:01 UTC