Coq nicht zu erzeugen induktive Hypothese

Question

ich eine Lösung für den folgenden Satz gegeben wurde, wie unten dargestellt:

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. 

Ich habe versucht, es auf einem anderen Rechner zu schnell zu replizieren und versucht es so:

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. 

dh ohne die "as" -Klausel. Allerdings bleibe ich stecken, weil das automatisch benannte Äquivalent von "zeq" aus Gründen, die ich nicht herausfinden kann, nicht erzeugt wird. Warum wird hier im zweiten Fall nicht das (automatisch benannte) Äquivalent von "zeq" von Coq erzeugt?

Answer 1

Wie in einem Kommentar von @ejgallego erwähnt ist dies, weil die as Klausel für sogenanntes Intro-Muster erlaubt (dh Muster, die Sie auch mit der intros Taktik verwenden können, wie @AntonTrunov in einem Kommentar erwähnt). Das [zs zeq] Muster bedeutet destruct ... as [zs zeq]. Um mehr über Intro-Muster zu erfahren, beziehen Sie sich auf https://coq.inria.fr/refman/Reference-Manual010.html#hevea_default564