# How to complete the proof in Coq?

I'm trying to prove the theorem in CoqIDE.

To me this definition PRIFIKS

``````Inductive PRIFIKS {A:Type}: list A -> list A -> Prop :=
| pri_nul : forall (l : list A), nil PRIFIKS l
| pri_g : forall x:A, forall (l1 l2 : list A), PRIFIKS l1 l2 -> PRIFIKS (x::l1) (x::l2).``````

and need to write dokazateljstvo for theorem Dokaz1

``Theorem Dokaz1: forall A l1 l2, @PRIFIKS A l1 l2 -> exists l3, l2 = l3 ++ l1.``

The problem is that whatever tactics I didn't isparitel I can't complete dokazateljstvo. How to complete dokazateljstvo or where I made a mistake?

``````Theorem Dokaz1: forall A l1 l2, @PRIFIKS A l1 l2 -> exists l3, l2 = l3 ++ l1.
Proof.
intros.
destruct l1.
- exists l2.
reflexivity.
- exists [].
assert (H2: (a::l1) = [] -> PRIFIKS [] l2).
* intros.
apply pri_nul.
* assert (H3: PRIFIKS [] l2).
apply pri_nul.``````
April 8th 20 at 02:36
April 8th 20 at 02:38
Lists usually need induction to prove it.
Theorem Dokaz1: forall A l1 l2, @PRIFIKS A l1 l2 -> exists l3, l2 = l3 ++ l1.
Proof.
intros.
induction H.
- l exists.
reflexivity.
- destruct IHPRIFIKS.
exists x0.
simpl.
rewrite H0.
reflexivity.
Qed.

Find more questions by tags Programming languages