Coincé dans la boucle d'inversion infinie Coq

Question

J'ai une relation inductive comme indiqué ci-dessous intitulé suffixe. J'essaie de prouver le théorème connexe suffix_app. Mon idée générale est d'utiliser ce fait que suffixe xs ys pour montrer que xs est soit égal à ys ou que c'est une série d'éléments contre 'd sur ys.

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. 
    - 

Cependant, quand j'utilise l'inversion, il n'y a aucun moyen de réellement jamais « arriver » à terme est égal à ys. Par conséquent, je suis coincé au point actuellement vu dans le code.

Answer 1

Votre preuve suit simplement par induction sur l'une des structures, par exemple:

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. 

Pour des raisons pratiques, vous voudrez peut-être que tu utiliser une version différente, calcul du suffixe.