Stream: Coq users

Topic: Automatically generated names from `induction` tactic.


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip 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