Доказательство `forall x xs ys, subseq (x :: xs) ys -> subseq xs ys` в Coq

Question

У меня есть следующее определение

Inductive subseq : list nat -> list nat -> Prop :=
| empty_subseq : subseq [] []
| add_right : forall y xs ys, subseq xs ys -> subseq xs (y::ys)
| add_both : forall x y xs ys, subseq xs ys -> subseq (x::xs) (y::ys)
.

Используя это, я хочу доказать следующую лемму

Lemma del_l_preserves_subseq : forall x xs ys, subseq (x :: xs) ys -> subseq xs ys.

Итак, я попытался посмотреть на доказательство subseq (x :: xs) ys, выполнивdestruct H.

Proof.
  intros. induction H.

3 subgoals (ID 209)

  x : nat
  xs : list nat
  ============================
  subseq xs [ ]

subgoal 2 (ID 216) is:
 subseq xs (y :: ys)
subgoal 3 (ID 222) is:
 subseq xs (y :: ys)

Почему первая подзадача просит меня доказать subseq xs []?Разве тактика destruct не должна знать, что доказательство не может иметь форму empty_subseq, поскольку тип содержит x :: xs, а не []?

В общем, как мне доказать, что я лемма?пытаешься доказать?

Answer 1

Ответ Ли-Яо был действительно полезным. Это доказательство леммы.

Lemma del_l_preserves_subseq : forall x xs ys, subseq (x :: xs) ys -> subseq xs ys.
Proof.
  intros x xs ys.
  induction ys as [|y ys'].
  - intros. inversion H. (* Inversion will detect that no constructor matches the type of H *)
  - intros. inversion H. (* Inversion will automatically discharge the first case *)
    + (* When [subseq (x :: xs) ys'] holds *)
      apply IHys' in H2. now apply add_right.
    + (* When [subseq xs ys'] holds *)
      now apply add_right.
Qed

Answer 2

Разве тактика уничтожения не должна знать, что доказательство не может иметь форму empty_subseq, поскольку тип содержит x :: xs, а не []?

На самом деле, destructне так много знает.Он просто заменяет x :: xs и xs на [] и [] в случае empty_subseq.В частности, это часто приводит к потере информации в контексте.Лучшие альтернативы:

• Использование inversion вместо destruct.

• Использование remember для обеспечения обоих типов индексов subseqпеременные до destruct.(remember (x :: xs) as xxs in H.) Это более четкое управление целями также хорошо работает с induction.