Ayuda con una prueba de CoQ para subsecuencias

Question

Tengo los tipos inductivos definidos:

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 sigo siendo 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 sobre el juicio de subconjunto directamente. Sin embargo, debe ser lo más general posible, así que aquí está 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 forma posible de construir un término así! ¡¡¡Sin hipótesis de inducción! Solo te da los premios constructivos.

Podría haberlo hecho directamente por la inducción en L1 luego L2, pero tendría que construir a mano la instancia de inversión correcta porque su hipótesis de inducción habría sido realmente débil.

espero que ayude, V.