How to complete a proof in Coq?

Question

Programming languages

I am trying to prove a theorem in CoqIDE.

I was given the definition of PRIFIKS

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

and you need to write a proof for the Dokaz1 theorem

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

The problem is that no matter what tactics I use, I can't complete the proof. How to complete the proof or where did I make a mistake?

Theorem Dokaz1: forall A l1 l2, @PRIFIKS A l1 l2 -> exists l3, l2 = l1 ++ l3.
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.

Answer 1

With lists, you usually need to prove by induction.
Theorem Dokaz1: forall A l1 l2, @PRIFIKS A l1 l2 -> exists l3, l2 = l1 ++ l3.
proof.
intros.
induction H.
- exists l.
reflexivity.
-destruct IHPRIFIKS.
exists x0.
simpl.
rewrite H0.
reflexivity.
Qed.