(*************************************************************)
(*      This file is distributed under the terms of the      *)
(*      GNU Lesser General Public License Version 2.1        *)
(*************************************************************)
(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
(*************************************************************)

(**********************************************************************
     Aux.v                                                                                           
                                                                                                          
     Auxillary functions & Theorems                                              
  **********************************************************************)
Require Export Coq.Lists.List.
Require Export Coq.Arith.Arith.
Require Export Coqprime.Tactic.
Require Import Coq.Wellfounded.Inverse_Image.
Require Import Coq.Arith.Wf_nat.

(************************************** 
   Some properties on list operators: app, map,...
**************************************)
 
Section List.
Variables (A : Set) (B : Set) (C : Set).
Variable f : A ->  B.

(************************************** 
  An induction theorem for list based on length 
**************************************)
 
Theorem list_length_ind:
 forall (P : list A ->  Prop),
 (forall (l1 : list A),
  (forall (l2 : list A), length l2 < length l1 ->  P l2) ->  P l1) ->
 forall (l : list A),  P l.
intros P H l;
 apply well_founded_ind with ( R := fun (x y : list A) => length x < length y );
 auto.
apply wf_inverse_image with ( R := lt ); auto.
apply lt_wf.
Qed.
 
Definition list_length_induction:
 forall (P : list A ->  Set),
 (forall (l1 : list A),
  (forall (l2 : list A), length l2 < length l1 ->  P l2) ->  P l1) ->
 forall (l : list A),  P l.
intros P H l;
 apply well_founded_induction
      with ( R := fun (x y : list A) => length x < length y ); auto.
apply wf_inverse_image with ( R := lt ); auto.
apply lt_wf.
Qed.
 
Theorem in_ex_app:
 forall (a : A) (l : list A),
 In a l ->  (exists l1 : list A , exists l2 : list A , l = l1 ++ (a :: l2)  ).
intros a l; elim l; clear l; simpl; auto.
intros H; case H.
intros a1 l H [H1|H1]; auto.
exists (nil (A:=A)); exists l; simpl; auto.
rewrite H1; auto.
case H; auto; intros l1 [l2 Hl2]; exists (a1 :: l1); exists l2; simpl; auto.
rewrite Hl2; auto.
Qed.

(**************************************
 Properties on app 
**************************************)
 
Theorem length_app:
 forall (l1 l2 : list A),  length (l1 ++ l2) = length l1 + length l2.
intros l1; elim l1; simpl; auto.
Qed.
 
Theorem app_inv_head:
 forall (l1 l2 l3 : list A), l1 ++ l2 = l1 ++ l3 ->  l2 = l3.
intros l1; elim l1; simpl; auto.
intros a l H l2 l3 H0; apply H; injection H0; auto.
Qed.
 
Theorem app_inv_tail:
 forall (l1 l2 l3 : list A), l2 ++ l1 = l3 ++ l1 ->  l2 = l3.
intros l1 l2; generalize l1; elim l2; clear l1 l2; simpl; auto.
intros l1 l3; case l3; auto.
intros b l H; absurd (length ((b :: l) ++ l1) <= length l1).
simpl; rewrite length_app; auto with arith.
rewrite <- H; auto with arith.
intros a l H l1 l3; case l3.
simpl; intros H1; absurd (length (a :: (l ++ l1)) <= length l1).
simpl; rewrite length_app; auto with arith.
rewrite H1; auto with arith.
simpl; intros b l0 H0; injection H0.
intros H1 H2; rewrite H2, (H _ _ H1); auto.
Qed.
 
Theorem app_inv_app:
 forall l1 l2 l3 l4 a,
 l1 ++ l2 = l3 ++ (a :: l4) ->
  (exists l5 : list A , l1 = l3 ++ (a :: l5) ) \/
  (exists l5 , l2 = l5 ++ (a :: l4) ).
intros l1; elim l1; simpl; auto.
intros l2 l3 l4 a H; right; exists l3; auto.
intros a l H l2 l3 l4 a0; case l3; simpl.
intros H0; left; exists l; injection H0; intros; subst; auto.
intros b l0 H0; case (H l2 l0 l4 a0); auto.
injection H0; auto.
intros [l5 H1].
left; exists l5; injection H0; intros; subst; auto.
Qed.
 
Theorem app_inv_app2:
 forall l1 l2 l3 l4 a b,
 l1 ++ l2 = l3 ++ (a :: (b :: l4)) ->
  (exists l5 : list A , l1 = l3 ++ (a :: (b :: l5)) ) \/
  ((exists l5 , l2 = l5 ++ (a :: (b :: l4)) ) \/
   l1 = l3 ++ (a :: nil) /\ l2 = b :: l4).
intros l1; elim l1; simpl; auto.
intros l2 l3 l4 a b H; right; left; exists l3; auto.
intros a l H l2 l3 l4 a0 b; case l3; simpl.
case l; simpl.
intros H0; right; right; injection H0; split; auto.
rewrite H2; auto.
intros b0 l0 H0; left; exists l0; injection H0; intros; subst; auto.
intros b0 l0 H0; case (H l2 l0 l4 a0 b); auto.
injection H0; auto.
intros [l5 HH1]; left; exists l5; injection H0; intros; subst; auto.
intros [H1|[H1 H2]]; auto.
right; right; split; auto; injection H0; intros; subst; auto.
Qed.
 
Theorem same_length_ex:
 forall (a : A) l1 l2 l3,
 length (l1 ++ (a :: l2)) = length l3 ->
  (exists l4 ,
   exists l5 ,
   exists b : B ,
   length l1 = length l4 /\ (length l2 = length l5 /\ l3 = l4 ++ (b :: l5))   ).
intros a l1; elim l1; simpl; auto.
intros l2 l3; case l3; simpl; (try (intros; discriminate)).
intros b l H; exists (nil (A:=B)); exists l; exists b; (repeat (split; auto)).
intros a0 l H l2 l3; case l3; simpl; (try (intros; discriminate)).
intros b l0 H0.
case (H l2 l0); auto.
intros l4 [l5 [b1 [HH1 [HH2 HH3]]]].
exists (b :: l4); exists l5; exists b1; (repeat (simpl; split; auto)).
rewrite HH3; auto.
Qed.

(************************************** 
  Properties on map 
**************************************)
 
Theorem in_map_inv:
 forall (b : B) (l : list A),
 In b (map f l) ->  (exists a : A , In a l /\ b = f a ).
intros b l; elim l; simpl; auto.
intros tmp; case tmp.
intros a0 l0 H [H1|H1]; auto.
exists a0; auto.
case (H H1); intros a1 [H2 H3]; exists a1; auto.
Qed.
 
Theorem in_map_fst_inv:
 forall a (l : list (B * C)),
 In a (map (fst (B:=_)) l) ->  (exists c , In (a, c) l ).
intros a l; elim l; simpl; auto.
intros H; case H.
intros a0 l0 H [H0|H0]; auto.
exists (snd a0); left; rewrite <- H0; case a0; simpl; auto.
case H; auto; intros l1 Hl1; exists l1; auto.
Qed.
 
Theorem length_map: forall l,  length (map f l) = length l.
intros l; elim l; simpl; auto.
Qed.
 
Theorem map_app: forall l1 l2,  map f (l1 ++ l2) = map f l1 ++ map f l2.
intros l; elim l; simpl; auto.
intros a l0 H l2; rewrite H; auto.
Qed.
 
Theorem map_length_decompose:
 forall l1 l2 l3 l4,
 length l1 = length l2 ->
 map f (app l1 l3) = app l2 l4 ->  map f l1 = l2 /\ map f l3 = l4.
intros l1; elim l1; simpl; auto; clear l1.
intros l2; case l2; simpl; auto.
intros; discriminate.
intros a l1 Rec l2; case l2; simpl; clear l2; auto.
intros; discriminate.
intros b l2 l3 l4 H1 H2.
injection H2; clear H2; intros H2 H3.
case (Rec l2 l3 l4); auto.
intros H4 H5; split; auto.
subst; auto.
Qed.

(************************************** 
  Properties of flat_map 
**************************************)
 
Theorem in_flat_map:
 forall (l : list B) (f : B ->  list C) a b,
 In a (f b) -> In b l ->  In a (flat_map f l).
intros l g; elim l; simpl; auto.
intros a l0 H a0 b H0 [H1|H1]; apply in_or_app; auto.
left; rewrite H1; auto.
right; apply H with ( b := b ); auto.
Qed.
 
Theorem in_flat_map_ex:
 forall (l : list B) (f : B ->  list C) a,
 In a (flat_map f l) ->  (exists b , In b l /\ In a (f b) ).
intros l g; elim l; simpl; auto.
intros a H; case H.
intros a l0 H a0 H0; case in_app_or with ( 1 := H0 ); simpl; auto.
intros H1; exists a; auto.
intros H1; case H with ( 1 := H1 ).
intros b [H2 H3]; exists b; simpl; auto.
Qed.

(************************************** 
  Properties of fold_left 
**************************************)

Theorem fold_left_invol: 
  forall (f: A -> B -> A) (P: A -> Prop) l a,
  P a ->  (forall x y, P x -> P (f x y)) -> P (fold_left f l a).
intros f1 P l; elim l; simpl; auto.
Qed. 

Theorem fold_left_invol_in: 
  forall (f: A -> B -> A) (P: A -> Prop) l a b,
  In b l -> (forall x, P (f x b)) -> (forall x y, P x -> P (f x y)) ->
  P (fold_left f l a).
intros f1 P l; elim l; simpl; auto.
intros a1 b HH; case HH.
intros a1 l1 Rec a2 b [V|V] V1 V2; subst; auto.
apply fold_left_invol; auto.
apply Rec with (b := b); auto.
Qed.

End List.


(************************************** 
  Propertie of list_prod
**************************************)
 
Theorem length_list_prod:
 forall (A : Set) (l1 l2 : list A),
  length (list_prod l1 l2) = length l1 * length l2.
intros A l1 l2; elim l1; simpl; auto.
intros a l H; rewrite length_app; rewrite length_map; rewrite H; auto.
Qed.
 
Theorem in_list_prod_inv:
 forall (A B : Set) a l1 l2,
 In a (list_prod l1 l2) ->
  (exists b : A , exists c : B , a = (b, c) /\ (In b l1 /\ In c l2)  ).
intros A B a l1 l2; elim l1; simpl; auto; clear l1.
intros H; case H.
intros a1 l1 H1 H2.
case in_app_or with ( 1 := H2 ); intros H3; auto.
case in_map_inv with ( 1 := H3 ); intros b1 [Hb1 Hb2]; auto.
exists a1; exists b1; split; auto.
case H1; auto; intros b1 [c1 [Hb1 [Hb2 Hb3]]].
exists b1; exists c1; split; auto.
Qed.