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?

Answer 1

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