3

我试图证明将函数 f 应用于两个列表的每个元素会产生相似的rel_list列表，如果它们最初是相关的。我rel在列表的元素上有 a 并且已经证明了一个引理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.
4

1 回答 1

2

这可以通过对您的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.
于 2013-12-19T02:29:01.807 回答