コックは、以下に示すように、私は次の定理に解決策を与えた誘導仮説

Question

を生成しない：

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. 

が、私はすぐに別のマシン上でそれを再現しようとしていたので、それを実行しようとしました：

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. 

つまり、 "as"句を使用しないでください。しかし、私は "zeq"という名前の自動的な名前が生成されないために動かなくなってしまいました。なぜ、ここで2番目のケースでCoqによって生成される "zeq"の（自動的に名前が付けられた）同等物ではないのですか？

Answer 1

コメントに@ejgallegoで述べたようにas句は、いわゆるイントロパターン（つまり、コメントに@AntonTrunovで述べたように、あなたも、intros戦術で使用できるパターンです）することができますので、これはです。 [zs zeq]パターンの意味はdestruct ... as [zs zeq]です。 イントロパターンの詳細については、https://coq.inria.fr/refman/Reference-Manual010.html#hevea_default564