Coq - 應用於每個元素的函數列表上的歸納

Question

我試圖證明將函數f應用於兩個列表中的每個元素的結果類似rel_list列出它們是否是原始相關的。我在列表的元素上有一個rel，並且已經證明了一個引理Lemma1，如果兩個元素都在rel中，它們在rel之後，函數f應用於這兩個元素。我嘗試了列表中的感應和rel_list，但在基本情況解決後，我最終遇到了像xL :: xL0 :: xlL0 = xL0 :: xlL0或進入循環的情況。請有人建議我如何結束證明。 謝謝，

Variable A:Type.  
Variable rel: A -> A -> Prop. 
Variable f: A -> A. 

Lemma lemma1: forall n m n' m', 
rel n m -> 
n' = f n -> 
m' = f m -> 
rel n' m'. 
Proof. 
    ... 
Qed 

Inductive rel_list : list A -> list A -> Prop := 
| rel_list_nil : rel_list nil nil 
| rel_list_cons: forall x y xl yl, 
    rel x y -> 
    rel_list xl yl -> 
    rel_list (x::xl) (y::yl). 

Fixpoint f_list (xl: list A) : list A := 
match xl with 
    | nil => xl 
    | x :: xl' => f x :: (f_list xl') 
end. 

Lemma Lemma2: forall lL lR lL' lR', 
rel_list lL lR -> 
lL' = f_list lL -> 
lR' = f_list lR -> 
rel_list lL' lR'. 
Proof. 
intros ? ? ? ? Hsim HmL HmR. 

Answer 1

這可以很容易地在你的rel_list假設做歸納顯示。這是一個通用版本，它使用標準庫中的函數：

Require Import Coq.Lists.List. 

Section Lists. 

Variables A1 A2 B1 B2 : Type. 
Variables (RA : A1 -> A2 -> Prop) (RB : B1 -> B2 -> Prop). 
Variables (f1 : A1 -> B1) (f2 : A2 -> B2). 

Hypothesis parametric : forall a1 a2, RA a1 a2 -> RB (f1 a1) (f2 a2). 

Lemma l : forall l1 l2, Forall2 RA l1 l2 -> 
         Forall2 RB (map f1 l1) (map f2 l2). 
Proof. 
    intros. 
    induction H as [|a1 a2 l1 l2 HR H IH]; simpl; constructor; eauto. 
Qed. 

End Lists.