幫助與勒柯克證明了亞

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

實際上，直接對SubSet判斷進行歸納比較容易。 但是，你需要儘可能通用，所以這裏是我的建議：

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.