I have an inductive relation as shown below titled suffix. I am trying to prove the related theorem suffix_app. My general idea is to use that fact that suffix xs ys to show that xs is either equal to ys or that it is some series of elements cons'd onto 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.
-
However, when I use inversion, there's no way of actually ever "arriving" to the term that is equal to ys. Hence, I am stuck at the point currently seen in the code.
Your proof simply follows by induction on any of the structures, example:
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.
For practical reasons thou you may want to use a different, computational version of suffix.