무한 반전 루프 Coq

Question

에 붙어 있습니다. 아래에 표시된 접미어과 같은 유도 관계가 있습니다. 나는 관련 theorem suffix_app을 증명하려고 노력하고 있습니다. 내 일반적인 생각은 xs가 ys와 같거나 몇 가지 일련의 요소임을 나타내는 접미사 xs ys이라는 사실을 사용하는 것입니다. cons '

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 : forall (X: Type) (x:X) (xs ys: list X), 
    suffix xs ys -> 
    exists ws, xs = ws ++ ys. 
Proof. 
    intros. 
    inversion H. 
    - exists []. reflexivity. 
    - 

그러나 내가 반전을 사용할 때 실제로 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]]; [now exists []|]. 
now exists (x :: zs); rewrite zeq. 
Qed. 

당신이 접미사의 다른 전산 버전을 사용할 수 있습니다 thou를 실제 이유 :

Answer 1

귀하의 증거는 단순히 예를 들어, 임의의 구조에 유도에 의해 다음과 같습니다.