Aiuto con una prova Coq per sottosequenze

Question

Ho i tipi induttivi definiti:

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

Ora devo dimostrare una serie di proprietà di tale tipo induttivo, ma continuo a rimanere bloccati.

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. 

Qualcuno può aiutarmi ad avanzare.

Answer 1

In effetti, è più facile eseguire un'induzione direttamente sul giudizio SubSet. Tuttavia, è necessario essere più generale possibile, ecco il mio consiglio:

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. 

"inversione" è una tattica che controlla un termine di induttiva e ti dà tutto il senso possibile costruire un tale termine !! senza ipotesi di induzione !! Ti dà solo i presupposti costruttivi.

Si potrebbe averlo fatto direttamente per induzione su l1 poi su l2, ma bisognerebbe costruire manualmente l'istanza di inversione corretta perché l'ipotesi di induzione sarebbe stata veramente debole.

Speranza che aiuta, V.