無限反転ループCoq

Question

私は以下に示す接尾辞のような誘導関係を持っています。私は関連する定理を証明しようとしています 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. 

サフィックスの異なる、計算バージョンを使用したい場合があり汝実用上の理由：

Answer 1

あなたの証明は、単に例として、構造のいずれかに誘導することにより、以下の。