(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU Lesser General Public License for more details.                *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)

Auxiliary functions and theorems


From Coq Require Export List Arith.
From Coq Require Import Inverse_Image Wf_nat Sorting.Permutation.
Export ListNotations.

Set Default Proof Using "Type".

Theorem le_minus : a b : , a - b a.
Proof.
intros a; elim a; simpl in |- *; auto.
intros n H b; case b; simpl in |- *; auto.
Qed.


#[export] Hint Resolve le_minus: arith.

Properties of the fold operator
Section Fold.

Variables (A : Type) (B : Type).
Variable f : A B A.
Variable g : B A A.
Variable h : A A.

Theorem fold_left_eta :
  l a f1,
 ( a b, In b l f a b = a b) fold_left f l a = fold_left l a.
Proof.
intros l; elim l; simpl in |- *; auto.
intros a H .
rewrite ; auto.
Qed.


Theorem fold_left_map :
  (C : Type) a l (k : C B),
 fold_left f (map k l) a = fold_left (fun a b f a (k b)) l a.
Proof.
intros C a l k; generalize a; elim l; simpl in |- *; auto.
Qed.


Theorem fold_left_init :
 ( (a : A) (b : B), h (f a b) = f (h a) b)
  (a : A) (l : list B), fold_left f l (h a) = h (fold_left f l a).
Proof.
intros H a l; generalize a; elim l; clear l a; simpl in |- *; auto.
intros a l .
rewrite H; auto.
Qed.


End Fold.

Some properties of list operators: app, map, ...
Section List.

Variables (A : Type) (B : Type) (C : Type).
Variable f : A B.

An induction theorem for list based on length
Theorem list_length_ind :
  P : list A Prop,
 ( l1 : list A,
  ( l2 : list A, length < length P ) P )
  l : list A, P l.
Proof.
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.


Program Definition list_length_induction (P : list A Type)
 (rec: l1 : list A, ( l2 : list A, length < length P ) P )
 (l : list A) : P l
@well_founded_induction_type _
 (fun x y : list A length x < length y)
  ((fun _ _ _ @wf_inverse_image _ _ lt _ _) P rec l) P rec l.

Theorem in_ex_app :
  (a : A) (l : list A),
 In a l l1 : list A, ( l2 : list A, l = a ).
Proof.
intros a l; elim l; clear l; simpl in |- *; auto.
intros H; case H.
intros l H [| ]; auto.
exists []; exists l; simpl in |- *; auto.
apply f_equal2 with (f cons (AA)); auto.
case H; auto; intros (, ); exists ( ); exists ;
 simpl in |- *; auto.
apply f_equal2 with (f cons (AA)); auto.
Qed.


Theorem app_inv_app :
  l1 l2 l3 l4 a,
  = a
 ( l5 : list A, = a )
 ( l5, = a ).
Proof.
intros ; elim ; simpl in |- *; auto.
intros a H; right; exists ; auto.
intros a l H ; case ; simpl in |- *.
intros ; left; exists l; apply f_equal2 with (f cons (AA));
 injection ; auto.
intros b ; case (H ); auto.
injection ; auto.
intros (, ).
left; exists ; apply f_equal2 with (f cons (AA)); injection ; auto.
Qed.


Theorem app_inv_app2 :
  l1 l2 l3 l4 a b,
  = a b
 ( l5 : list A, = a b )
 ( l5, = a b )
  = a [] = b .
Proof.
intros ; elim ; simpl in |- *; auto.
intros a b H; right; left; exists ; auto.
intros a l H b; case ; simpl in |- *.
case l; simpl in |- *.
intros ; right; right; injection ; split; auto.
apply f_equal2 with (f cons (AA)); auto.
intros ; left; exists ; injection ; intros;
 repeat apply f_equal2 with (f cons (AA)); auto.
intros ; case (H b); auto.
injection ; auto.
intros (, ); left; exists ; apply f_equal2 with (f cons (AA));
 auto; injection ; auto.
intros [| (, )]; auto.
right; right; split; auto; apply f_equal2 with (f cons (AA)); auto;
 injection ; auto.
Qed.


Theorem same_length_ex :
  (a : A) l1 l2 l3,
 length ( a ) = length
  l4,
   ( l5,
      ( b : B,
         length = length length = length = b )).
Proof.
intros a ; elim ; simpl in |- *; auto.
intros ; case ; simpl in |- *; try (intros; discriminate).
intros b l H; exists []; exists l; exists b; repeat (split; auto).
intros l H ; case ; simpl in |- *; try (intros; discriminate).
intros b .
case (H ); auto.
intros (, (, (, (, )))).
exists (b ); exists ; exists ; repeat (simpl in |- *; split; auto).
apply f_equal2 with (f cons (AB)); auto.
Qed.


Properties of map
Theorem in_map_inv :
  (b : B) (l : list A),
 In b (map f l) a : A, In a l b = f a.
Proof.
intros b l; elim l; simpl in |- *; auto.
intros tmp; case tmp.
intros H [| ]; auto.
exists ; auto.
case (H ); intros (, ); exists ; auto.
Qed.


Theorem in_map_fst_inv :
  a (l : list (B C)),
 In a (map (fst (B_)) l) c, In (a, c) l.
Proof.
intros a l; elim l; simpl in |- *; auto.
intros H; case H.
intros H [| ]; auto.
exists (snd ); left; rewrite ; case ; simpl in |- *; auto.
case H; auto; intros ; exists ; auto.
Qed.


Properties of flat_map
Theorem in_flat_map_in :
  (l : list B) (f : B list C) a b,
 In a (f b) In b l In a (flat_map f l).
Proof.
intros; apply in_flat_map; exists b; split; auto.
Qed.


Theorem in_flat_map_ex :
  (l : list B) (f : B list C) a,
 In a (flat_map f l) b, In b l In a (f b).
Proof.
intros; apply in_flat_map; auto.
Qed.


Theorem NoDup_app :
  l1 l2,
 NoDup
 NoDup ( a : A, In a In a ) NoDup ( ).
Proof.
intros ; elim ; simpl in |- *; auto.
intros a l H ; apply NoDup_cons; simpl in |- *; auto.
red in |- *; intros ; case in_app_or with (1 ); auto; intros .
inversion ; auto.
apply with a; auto.
apply H; auto.
apply NoDup_cons_iff with (1 ); auto.
intros ; apply ( ); auto.
Qed.


Theorem NoDup_app_inv :
  l1 l2 (a : A), NoDup ( ) In a In a .
Proof.
intros ; elim ; simpl in |- *; auto.
intros a l H [| ] .
inversion ; auto.
case ; rewrite ; auto with datatypes.
apply (H ); auto.
apply NoDup_cons_iff with (1 ); auto.
Qed.


Theorem NoDup_app_inv_l :
  (l1 l2 : list A), NoDup ( ) NoDup .
Proof.
intros ; elim ; simpl in |- *; auto using NoDup_nil.
intros a l H ; inversion ; apply NoDup_cons; auto.
contradict ; auto with datatypes.
apply H with ; auto.
Qed.


Theorem NoDup_app_inv_r : l1 l2 : list A, NoDup ( ) NoDup .
Proof.
intros ; elim ; simpl in |- *; auto.
intros a l H ; inversion ; auto.
Qed.


End List.

Definition of map2
Section map2.
Variables (A : Type) (B : Type) (C : Type).
Variable f : A B C.

Fixpoint (l1 : list A) : list B list C
  fun l2
  match with
  | [] []
  | a
      match with
      | [] []
      | b f a b
      end
  end.

Theorem map2_app :
  l1 l2 l3 l4,
 length = length
  ( ) ( ) = .
Proof.
intros ; elim ; auto.
intros ; case ; simpl in |- *; auto; intros; discriminate.
intros a l H ; case .
simpl in |- *; intros; discriminate.
intros b .
apply trans_equal with (f a b (l ) ( )).
simpl in |- *; auto.
rewrite H; auto.
Qed.


End map2.
Arguments [A B C].

Properties of the firstn and skipn functions
Section First.
Variable A : Type.

Properties of firstn
Theorem firstn_le_app1 :
  (n : ) (l1 l2 : list A),
 length n firstn n ( ) = firstn (n - length ) .
Proof.
intros n; elim n; simpl in |- *; auto.
intros ; case ; simpl in |- *; auto.
intros b l H; contradict H; auto with arith.
intros H ; case ; simpl in |- *; auto with arith.
intros b l ; rewrite H; auto with arith.
Qed.


Theorem firstn_le_app2 :
  (n : ) (l1 l2 : list A),
 n length firstn n ( ) = firstn n .
Proof.
intros n; elim n; simpl in |- *; auto.
intros H ; case ; simpl in |- *.
intros ; contradict ; auto with arith.
intros a l ; (apply f_equal2 with (f cons (AA)); auto).
apply H; apply le_S_n; auto.
Qed.


Theorem firstn_le_length_eq :
  (n : ) (l1 : list A), n length length (firstn n ) = n.
Proof.
intros n ; generalize n; elim ; clear n ; simpl in |- *; auto.
intros n; case n; simpl in |- *; auto.
intros ; contradict ; auto with arith.
intros a l H n; case n; simpl in |- *; auto with arith.
Qed.


Theorem skipn_le_app1 :
  (n : ) (l1 l2 : list A),
 length n skipn n ( ) = skipn (n - length ) .
Proof.
intros n; elim n; simpl in |- *; auto.
intros ; case ; simpl in |- *; auto.
intros b l H; contradict H; auto with arith.
intros H ; case ; simpl in |- *; auto with arith.
Qed.


Theorem skipn_le_app2 :
  (n : ) (l1 l2 : list A),
 n length skipn n ( ) = skipn n .
Proof.
intros n; elim n; simpl in |- *; auto.
intros H ; case ; simpl in |- *; auto with arith.
intros ; contradict ; auto with arith.
Qed.


End First.

Existence of a first max
Section FirstMax.

Theorem exist_first_max :
  l : list ,
 l []
  a : ,
   ( l1 : list ,
      ( l2 : list ,
         l = a
         ( n1, In < a) ( n1, In a))).
Proof.
intros l; elim l; simpl in |- *; auto.
intros H; case H; auto.
intros a ; case .
intros H ; exists a; exists []; exists [];
 repeat (split; simpl in |- *; auto with datatypes).
intros ; case .
intros ; case .
intros n H ; case H; clear H; auto.
red in |- *; intros ; discriminate; auto.
intros (, (, (, (, )))).
case (Nat.le_gt_cases a); intros ; auto.
exists a; exists []; exists (n );
 repeat (split; auto with datatypes).
intros ; case .
rewrite .
intros ; apply Nat.le_trans with (2 ); case in_app_or with (1 );
 auto with arith.
intros ; apply Nat.lt_le_incl; auto.
simpl in |- *; intros [| ]; [ rewrite | idtac ]; auto.
exists ; exists (a ); exists ;
 repeat (split; simpl in |- *; auto with datatypes).
apply f_equal2 with (f cons (A)); auto.
intros [| ]; [ rewrite | idtac ]; auto.
Qed.


End FirstMax.

Find the minimum and the maximun in a list
Section FindMin.
Variable A : Type.
Variable f : A .

Search in the list for the min with respect to a valuation function f
Fixpoint find_min (l : list A) : option ( A)
  match l with
  | [] None
  | a
      match find_min with
      | None Some (f a, a)
      | Some (, b)
          let n2 f a in
          match le_lt_dec with
          | left _ Some (, b)
          | right _ Some (, a)
          end
      end
  end.

Theorem find_min_correct :
  l : list A,
 match find_min l with
 | None l = []
 | Some (a, b) (In b l a = f b) ( c : A, In c l f b f c)
 end.
Proof.
intros l; elim l; simpl in |- *; auto.
intros a ; case (find_min ); simpl in |- *.
intros p; case p; simpl in |- *.
intros n b ((, ), ); case (le_lt_dec n (f a)); simpl in |- *.
intros ; split; auto.
intros c [| ]; auto.
rewrite ; rewrite ; auto.
intros ; split; auto.
intros c [| ]; auto.
rewrite ; auto.
apply Nat.le_trans with (f b); auto.
rewrite ; auto with arith.
intros H; rewrite H; split; simpl in |- *; auto.
intros c [| ]; rewrite || case ; auto.
Qed.


Search in the list for the max with respect to a valuation function f
Fixpoint find_max (l : list A) : option ( A)
  match l with
  | [] None
  | a
      match find_max with
      | None Some (f a, a)
      | Some (, b)
          let n2 f a in
          match le_lt_dec with
          | right _ Some (, b)
          | left _ Some (, a)
          end
      end
  end.

Theorem find_max_correct :
  l : list A,
 match find_max l with
 | None l = []
 | Some (a, b) (In b l a = f b) ( c : A, In c l f c f b)
 end.
Proof.
intros l; elim l; simpl in |- *; auto.
intros a ; case (find_max ); simpl in |- *.
intros p; case p; simpl in |- *.
intros n b ((, ), ); case (le_lt_dec n (f a)); simpl in |- *.
intros ; split; auto.
intros c [| ]; auto.
rewrite ; auto.
apply Nat.le_trans with (f b); auto.
rewrite ; auto with arith.
intros ; split; auto.
intros c [| ]; auto.
rewrite ; auto.
apply Nat.le_trans with (f b); auto.
rewrite ; auto with arith.
intros H; rewrite H; split; simpl in |- *; auto.
intros c [| ]; rewrite || case ; auto.
Qed.


End FindMin.

Arguments find_min [A].
Arguments find_max [A].

Permutation is compatible with fold_left
Theorem fold_left_permutation :
  (A B : Type) (f : A B A),
 ( (a : A) (b1 b2 : B), f (f a ) = f (f a ) )
  (a : A) (l1 l2 : list B),
 Permutation fold_left f a = fold_left f a.
Proof.
intros A B f Hf a H; generalize a; elim H; clear H a ;
 simpl in |- *; auto.
intros a b l ; rewrite Hf; auto.
intros H a; apply trans_equal with (1 a); auto.
Qed.


Section Permutation.
Variable A : Type.

Local Hint Constructors Permutation : core.
Local Hint Resolve Permutation_refl : core.
Local Hint Resolve Permutation_app : core.
Local Hint Resolve Permutation_app_swap : core.

Take a list and return the list of all pairs of an element of the list and the remaining list
Fixpoint split_one (l : list A) : list (A list A)
  match l with
  | [] []
  | a
     (a, ) map (fun p : A list A (fst p, a snd p)) (split_one )
  end.

The pairs of the list are a permutation
Theorem split_one_permutation :
  (a : A) (l1 l2 : list A),
 In (a, ) (split_one ) Permutation (a ) .
Proof.
intros a ; generalize a ; elim ; clear a ; simpl in |- *; auto.
intros a ; case .
intros a l H [| ].
injection ; intros ; rewrite ; rewrite ; auto.
generalize H ; elim (split_one l); simpl in |- *; auto.
intros ; case .
intros [| ]; auto.
injection ; intros ; (rewrite ; rewrite ).
apply Permutation_trans with (a fst snd ); auto.
apply perm_skip.
apply ; auto.
case ; simpl in |- *; auto.
Qed.


All elements of the list are there
Theorem split_one_in_ex :
  (a : A) (l1 : list A),
 In a l2 : list A, In (a, ) (split_one ).
Proof.
intros a ; elim ; simpl in |- *; auto.
intros H; case H.
intros l H [| ]; auto.
exists l; left; apply f_equal2 with (f pair (AA) (Blist A)); auto.
case H; auto.
intros x ; exists ( x); right; auto.
apply
 (in_map (fun p : A list A (fst p, snd p)) (split_one l) (a, x));
 auto.
Qed.


An auxillary function to generate all permutations
Fixpoint all_permutations_aux (l : list A) (n : ) {struct n} :
 list (list A)
  match n with
  | O [] []
  | S
      flat_map
        (fun p : A list A
         map (cons (fst p)) (all_permutations_aux (snd p) ))
        (split_one l)
  end.

Generate all the permutations
Definition all_permutations (l : list A)
 all_permutations_aux l (length l).

Lemma all_permutations_aux_permutation :
   (n : ) (l1 l2 : list A),
  n = length In (all_permutations_aux n) Permutation .
Proof.
intros n; elim n; simpl in |- *; auto.
intros ; case .
simpl in |- *; intros [| ].
rewrite ; auto.
case .
simpl in |- *; intros; discriminate.
intros H .
case in_flat_map_ex with (1 ).
clear ; intros x; case x; clear x; intros (, ).
case in_map_inv with (1 ).
simpl in |- *; intros y (, ).
rewrite ; auto.
apply Permutation_trans with ( ); auto.
apply perm_skip; auto.
apply H with (2 ).
apply eq_add_S.
apply trans_equal with (1 ).
change (length = length ( )) in |- *.
apply Permutation_length; auto.
apply Permutation_sym; apply split_one_permutation; auto.
apply split_one_permutation; auto.
Qed.


All the elements of the list are permutations
Theorem all_permutations_permutation :
  l1 l2 : list A, In (all_permutations ) Permutation .
Proof.
intros H; apply all_permutations_aux_permutation with (n length );
 auto.
Qed.


Lemma permutation_all_permutations_aux :
   (n : ) (l1 l2 : list A),
  n = length Permutation In (all_permutations_aux n).
Proof.
intros n; elim n; simpl in |- *; auto.
intros ; case .
intros H ; apply Permutation_sym in ; rewrite Permutation_nil with (1 ); auto with datatypes.
simpl in |- *; intros; discriminate.
intros H ; case .
intros ;
 rewrite Permutation_nil with (1 ) in ;
 discriminate.
clear ; intros .
case (split_one_in_ex ); auto.
apply Permutation_in with (1 ); auto with datatypes.
intros x .
apply in_flat_map_in with (b (, x)); auto.
apply in_map; simpl in |- *.
apply H; auto.
apply eq_add_S.
apply trans_equal with (1 ).
change (length = length ( x)) in |- *.
apply Permutation_length; auto.
apply Permutation_sym; apply split_one_permutation; auto.
apply Permutation_cons_inv with (a ).
apply Permutation_trans with (1 ).
apply Permutation_sym; apply split_one_permutation; auto.
Qed.


A permutation is in the list
Theorem permutation_all_permutations :
  l1 l2 : list A, Permutation In (all_permutations ).
Proof.
intros H; unfold all_permutations in |- *;
 apply permutation_all_permutations_aux; auto.
Qed.


Permutation is decidable
Definition Permutation_dec :
  ( a b : A, {a = b} + {a b})
   l1 l2 : list A, {Permutation } + { Permutation }.
Proof.
intros H .
case (In_dec (list_eq_dec H) (all_permutations )).
intros i; left; apply all_permutations_permutation; auto.
intros i; right; contradict i; apply permutation_all_permutations; auto.
Defined.


Theorem Permutation_transposition :
  (a b : A) l1 l2,
 Permutation (a b ) (b a ).
Proof.
intros a b .
assert (H_eq: b a = (b ) a ) by reflexivity.
rewrite H_eq.
apply Permutation_cons_app.
apply Permutation_sym.
apply Permutation_cons_app; auto.
Qed.


End Permutation.

Arguments split_one [A].
Arguments all_permutations [A].
Arguments Permutation_dec [A].