## Stream: Coq users

### Topic: Automatically generated names from `induction` tactic.

#### Quinn Flavel (Nov 28 2023 at 06:10):

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?

#### Quinn Flavel (Nov 28 2023 at 06:14):

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.

#### Gaëtan Gilbert (Nov 28 2023 at 09:57):

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

#### Meven Lennon-Bertrand (Nov 28 2023 at 09:58):

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