Trợ giúp với một bằng chứng Coq cho subsequences

Question

tôi có các loại quy nạp định nghĩa:

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

Bây giờ tôi phải chứng minh một loạt các thuộc tính của kiểu quy nạp, nhưng tôi cứ bị mắc kẹt.

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. 

Một số người có thể giúp tôi thăng tiến.

Answer 1

Thực tế, việc thực hiện cảm ứng trực tiếp trên bản đánh giá SubSet sẽ dễ dàng hơn. Tuy nhiên, bạn cần phải làm tổng càng tốt, vì vậy đây là lời khuyên của tôi:

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. 

"đảo ngược" là một chiến thuật để kiểm tra một thuật ngữ quy nạp và cung cấp cho bạn tất cả các cách có thể để xây dựng một thuật ngữ như vậy !! mà không có bất kỳ giả thuyết cảm ứng nào !! Nó chỉ cung cấp cho bạn các tiền đề xây dựng.

Bạn có thể thực hiện nó trực tiếp bằng cảm ứng trên l1 rồi l2, nhưng bạn sẽ phải xây dựng bằng tay trường hợp đảo ngược chính xác vì giả thuyết cảm ứng của bạn sẽ thực sự yếu.

Hy vọng điều này sẽ giúp ích, V.