Pomoc z dowodem Coq dla podciągów

Question

Mam zdefiniowane typy indukcyjne:

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). 

teraz muszę udowodnić szereg właściwości tego typu indukcyjnego, ale zachować utknięcie.

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. 

Czy ktoś może mi pomóc awansować.

Answer 1

W rzeczywistości łatwiej jest przeprowadzić indukcję bezpośrednio w wyroku SubSet. Jednak trzeba być tak ogólnie, jak to możliwe, więc tutaj jest moja rada:

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. 

„inwersja” to taktyka, która sprawdza się termin indukcyjną i daje cały możliwy sposób, aby zbudować taki termin !! bez żadnej hipotezy indukcji !! Daje tylko konstruktywne warunki.

Mogłeś zrobić to bezpośrednio przez indukcję na l1, a następnie na l2, ale musiałbyś ręcznie zbudować prawidłowy inwersję, ponieważ twoja hipoteza indukcyjna byłaby naprawdę słaba.

Mam nadzieję, że to pomoże, V.