Как завершить доказательство в Coq?

Question

[RonaldSK]

Я пытаюсь доказать теорему в CoqIDE.

Мне дано определение 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).

и надо написать доказательйство для теоремы Dokaz1

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

Проблема в том что какую бы тактику я не исполжьзовал у меня не получается завершить доказателяство. Как завершить доказательйство или где я допустил ошибку?

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.

Comments

[Михаил Потанин]

Если не секрет, зачем понадобился Coq?

Answer 1

[Михаил Потанин]

Со списками обычно надо по индукции доказывать.
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.