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
1 answer
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