@RonaldSK

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

Я пытаюсь доказать теорему в 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.
  • Вопрос задан
  • 102 просмотра
Пригласить эксперта
Ответы на вопрос 1
@potan
Функциональный программист
Со списками обычно надо по индукции доказывать.
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.
Ответ написан
Комментировать
Ваш ответ на вопрос

Войдите, чтобы написать ответ

Войти через центр авторизации
Похожие вопросы