une preuve Coq pour

Question

Je sousséquences 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. 

Peut-on m'aider à avancer.

Answer 1

En fait, il est plus facile de faire une induction sur le jugement SubSet directement. Cependant, vous devez être aussi générale que possible, voici donc 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 chemin possible de construire un tel terme !! sans aucune hypothèse d'induction !! Il ne vous donne que les prémisses constructives.

Vous auriez pu le faire directement par induction sur l1 puis l2, mais vous auriez à construire manuellement l'instance correcte d'inversion car votre hypothèse d'induction aurait été vraiment faible.

Hope it helps, V.