COQ 아래와 같이 나는 다음과 같은 정리에 대한 해결책을 받았다 유도 가설

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. 

ie "as"절없이. 그러나, 나는 "zeq"의 자동 - 명명 된 동등 물로 인해 내가 밖으로 운동 할 수없는 이유로 생성되지 않는 붙어있어. 왜 두 번째 경우에 Coq가 생성 한 "zeq"의 (자동으로 명명 된) 동등 물이 아닌가?

as 절은 소위 소개-패턴을 허용하기 때문에이 코멘트에 @ejgallego에서 언급 한 바와 같이

Answer 1

(즉, 코멘트에 @AntonTrunov에서 언급 한 바와 같이 당신은 또한 intros 전술과 함께 사용할 수있는 패턴이다). [zs zeq] 패턴 의미는 destruct ... as [zs zeq]입니다. 소개 패턴에 대한 자세한 내용은 https://coq.inria.fr/refman/Reference-Manual010.html#hevea_default564