卡在无限的反转环coq中

Question

我有一个感应关系，如下所示，标题为"后缀" 。我正在尝试证明相关定理 suffix_app 。我的总体想法是使用这个事实，即后缀xs ys 表明XS要么等于ys，要么是ys上的一系列元素 cons 'd。

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的术语。因此，我被困在当前在代码中看到的点。

Answer 1

您的证明只需归纳任何结构，例如：

：

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.

出于实际原因，您可能需要使用其他的，计算版本的后缀。