Coq ne génère pas l'hypothèse d'induction

Question

m'a donné une solution au théorème suivant comme indiqué ci-dessous:

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. 

je tente de reproduire rapidement sur une autre machine et a tenté ainsi:

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. 

c'est-à-dire sans la clause "as". Cependant, je suis coincé à cause de l'équivalent auto-nommé de "zeq" qui n'est pas généré pour des raisons que je ne peux pas résoudre. Pourquoi l'équivalent (nommé automatiquement) de "zeq" généré par Coq dans le second cas ici?

Answer 1

Comme mentionné dans un commentaire @ejgallego c'est parce que la clause as permet de soi-disant motifs d'introduction (qui est des motifs que vous pouvez utiliser avec la tactique intros, comme mentionné par @AntonTrunov dans un commentaire). Le motif [zs zeq] signifie destruct ... as [zs zeq]. Pour en savoir plus sur les intro-patterns, référez-vous à https://coq.inria.fr/refman/Reference-Manual010.html#hevea_default564