하위 시퀀스에 대한 코크 증명을 돕습니다

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.

.

"inversion"은 유도 용어를 확인하고 이러한 용어를 구축하는 모든 방법을 제공하는 전술입니다 !! 유도 가설없이 !! 그것은 단지 당신에게 건설적인 프리미스를 제공합니다.

L1의 L1에서 유도로 직접 해달었을 수 있었지만 유도 가설이 정말로 약 해졌 기 때문에 올바른 반전의 정확한 인스턴스를 손으로 구성해야합니다.

도움이되기를 바랍니다. v.