Aiuto con una prova di coq per le successive

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 quel tipo induttivo, ma continuo a rimanere bloccato.

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 fare un'induzione sul giudizio del sottoinsieme direttamente. Tuttavia, è necessario essere il più generale possibile, quindi 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 induttivo e ti dà tutto il modo possibile di costruire un tale termine !! senza alcuna ipotesi di induzione !! Ti dà solo le preme costruttive.

Avresti potuto farlo direttamente per induzione su L1 poi L2, ma dovresti costruire a mano l'istanza corretta di inversione perché la tua ipotesi di induzione sarebbe stata davvero debole.

Spero che aiuti, V.