加工のためのCOQ証明を助ける

Question

私は定義された誘導型を持っています：

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

.

今私はその誘導型の一連の特性を証明する必要がありますが、私は立ち往生し続けています。

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.

.

何らかの先に助けてくれることがあります。

Answer 1

実際には、サブセット判定の誘導を直接行う方が簡単です。 しかし、あなたはできるだけ一般的になる必要があるので、ここに私のアドバイスです：

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.

.

「反転」は、誘導用語をチェックし、そのような用語を構築するためのすべての可能な方法をあなたに与える戦術です!!誘導仮説なしで！ それはあなたに建設的なプレミスを与えるだけです。

あなたはL1からL2の誘導によって直接それを完成させることができましたが、あなたの誘導仮説は本当に弱いだろうからあなたは反転の正しいインスタンスを手で構築する必要があります。

それが役立つことを願っています v。