Coq - induction on lists with a function applied to each element

Question

Am trying to prove that applying a function f to every element of two lists results similar rel_list lists if they were originaly related. I have a rel on the elements of the list and have proved a lemma Lemma1 that if two elements are in rel, they are in rel after function f is applied to both elements. I tried induction on list and rel_list but after base case is solved, I end up with case like xL :: xL0 :: xlL0 = xL0 :: xlL0 or enter looping. Please some one suggest me how to close the proof. Thanks,

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

This can be shown easily by doing induction on your rel_list hypothesis. Here's a generalized version of this that uses functions in the standard library:

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.