Coq not generating inductive hypothesis

Question

I was given a solution to the following theorem as shown below:

Require Import Coq.Lists.List.
Import ListNotations.

Inductive suffix {X : Type} : list X -> list X -> Prop :=
  | suffix_end : forall xs,
          suffix xs xs
  | suffix_step : forall x xs ys,
          suffix xs ys ->
          suffix (x :: xs) ys.

Theorem suffix_app (X: Type) (xs ys: list X) :
  suffix xs ys -> exists ws, xs = ws ++ ys.
Proof.
  induction 1 as [|x xsp ysp hs [zs zeq]]. 
  - exists []. reflexivity.
  - now exists (x :: zs); rewrite zeq.
Qed.

I was trying to quickly replicate it on another machine and attempted it thus:

Theorem suffix_app (X: Type) (xs ys: list X) :
  suffix xs ys -> exists ws, xs = ws ++ ys.
Proof.
  induction 1.
  - exists []. reflexivity.
  - (* Stuck here! *)
Abort.

i.e. without the "as" clause. However, I get stuck due to the auto-named equivalent of "zeq" not being generated for reasons that I can't work out. Why isn't the (automatically named) equivalent of "zeq" generated by Coq in the second case here?

It is there for me, note that in your first example you had a destruct in the pattern. Thus destruct IHsuffix as [zs zeq]. will get you back in game. — ejgallego
I'm shocked I never spotted that but... c'est la vie. Thank, that completely answers my question. Feel free to put it as the answer and I'll accept it. — Sean S
Besides destruction, intros can also do rewrites (->): induction 1 as [|x ? ? ? [zs ->]]; [exists [] | exists (x :: zs)]; trivial. — Anton Trunov

Zimm i48 Zimm i48 · Accepted Answer · 2017-05-22T12:09:21

As mentioned by @ejgallego in a comment this is because the as clause allows for so-called intro-patterns (that is patterns that you can also use with the intros tactic, as mentioned by @AntonTrunov in a comment). The [zs zeq] pattern means destruct ... as [zs zeq]. To learn more about intro-patterns, refer to https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.intros

Coq not generating inductive hypothesis

1 Answers