Aide avec une preuve de coq pour les sous-séquences

Question

J'ai les types inductifs définis:

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

Maintenant, je dois prouver une série de propriétés de ce type inductif, mais je continue à rester coincé.

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.

Quelqu'un peut-il m'aider à avancer.

Answer 1

En fait, il est plus facile de faire une induction sur le jugement du sous-ensemble directement. Cependant, vous devez être aussi général que possible, voici mon conseil:

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.

"inversion" est une tactique qui vérifie un terme inductif et vous donne tout le moyen possible de construire un tel terme !! sans aucune hypothèse d'induction !! Cela ne vous donne que les principes de création constructive.

Vous auriez pu le faire directement par induction sur L1 puis l2, mais vous devriez construire à la main le cas d'inversion correct car votre hypothèse d'induction aurait été vraiment faible.

J'espère que cela aide, V.