Ayuda con una prueba de Coq de subsecuencias

Question

tengo los tipos definidos inductivas:

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

Ahora tengo que demostrar una serie de propiedades de ese tipo inductivo, pero no dejo de quedarse atascado.

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. 

Puede alguien ayudarme a avanzar.

Answer 1

De hecho, es más fácil hacer una inducción en la sentencia SubSet directamente. Sin embargo, tiene que ser lo más general posible, por lo que aquí es mi consejo:

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. 

"inversión" es una táctica que comprueba un término inductivo y le da toda la posible manera de construir un término tan !! sin ninguna hipótesis de inducción !! Solo te da las premisas constructivas.

Podrías haberlo hecho directamente por inducción en l1 y luego en l2, pero tendrías que construir a mano la instancia correcta de inversión porque tu hipótesis de inducción habría sido muy débil.

creo que sirve, V.