Помощь с доказательством Coq для подпоследовательностей - PullRequest
Новая
       7

Помощь с доказательством Coq для подпоследовательностей

5 голосов
/ 10 июля 2010

У меня есть определенные индуктивные типы: 

Inductive InL (A:Type) (y:A) : list A -> Prop := 
  | InHead : forall xs:list A, InL y (cons y xs) 
  | InTail : forall (x:A) (xs:list A), InL y xs -> InL y (cons x xs).

Inductive SubSeq (A:Type) : list A -> list A -> Prop :=
 | SubNil : forall l:list A, SubSeq nil l
 | SubCons1 : forall (x:A) (l1 l2:list A), SubSeq l1 l2 -> SubSeq l1 (x::l2)
 | SubCons2 : forall (x:A) (l1 l2:list A), SubSeq l1 l2 -> SubSeq (x::l1) (x::l2).

Теперь я должен доказать ряд свойств этого индуктивного типа, но я продолжаю зацикливаться. 

Lemma proof1: forall (A:Type) (x:A) (l1 l2:list A), SubSeq l1 l2 -> InL x l1 -> InL x l2.
Proof.
 intros.
 induction l1.
 induction l2.
 exact H0.

Qed.

Может некоторыепомогите мне продвинуться.

1 Ответ

8 голосов
/ 11 июля 2010

На самом деле, проще непосредственно подсказать суждение о подсети.Тем не менее, вы должны быть максимально общими, поэтому вот мой совет: 

Lemma proof1: forall (A:Type) (x:A) (l1 l2:list A), 
  SubSeq l1 l2 -> InL x l1 -> InL x l2.
(* first introduce your hypothesis, but put back x and In foo
   inside the goal, so that your induction hypothesis are correct*)
intros. 
revert x H0. induction H; intros.
(* x In [] is not possible, so inversion will kill the subgoal *)
inversion H0.

(* here it is straitforward: just combine the correct hypothesis *)
apply InTail; apply IHSubSeq; trivial.

(* x0 in x::l1 has to possible sources: x0 == x or x0 in l1 *)
inversion H0; subst; clear H0.
apply InHead.
apply InTail; apply IHSubSeq; trivial.
Qed.

«инверсия» - это тактика, которая проверяет индуктивный термин и дает вам все возможные способы построения такого термина!без всякой индукционной гипотезы !!Это дает вам только конструктивные предпосылки.

Вы могли бы сделать это напрямую, индуцируя по l1, затем по l2, но вам пришлось бы вручную построить правильный пример инверсии, потому что ваша гипотеза индукции была бы действительно слабой.

Надеюсь, это поможет, V.

...