(** Tools.v Version 1.0 January 2012 *)
(** runs under V8.3, tested with 8.3pl2 *)

(** Celia Picard with contributions by Ralph Matthes, 
    I.R.I.T.,  University of Toulouse and CNRS*)

(**  provides the implementation of some basic tools
     relating to arithmetic, lists, and so on *)

Require Export Arith.
Require Import Utf8.
Require Import Setoid.
Require Import Morphisms.
Require Import List.
Require Import Basics.
Require Import MinMax. 

Set Implicit Arguments.

Section Tools_lists.

  Lemma eq_nth (T: Set)(l1 l2 : list T)(d: T) : 
    length l1 = length l2 -> 
    (forall n, nth n l1 d = nth n l2 d) -> l1 = l2.
  Proof.
    revert l2.
    induction l1 as [|t1 l1 IH] ; intros l2 H1 H2 ;destruct l2 as [|t2 l2].
    reflexivity.
    inversion H1.
    inversion H1.
    f_equal.
    apply (H2 0).
    apply IH.
    apply eq_add_S, H1.
    intros n.
    apply (H2 (S n)).
  Qed.
  
  
  Lemma eq_nth_cor (T: Set)(l1 l2 : list T): 
    length l1 = length l2 -> 
    (forall n d, nth n l1 d = nth n l2 d) -> l1 = l2.
  Proof.
    intros H1 H2.
    destruct l1 as [|t1 l1] ;destruct l2 as [|t2 l2].
    reflexivity.
    inversion H1.
    inversion H1.
    apply (eq_nth _ _ t1).
    assumption.
    intros n.
    apply (H2 n t1).
  Qed.
  
  Lemma nth_default (T: Set)(l: list T)(n: nat)(d: T) : length l <= n -> nth n l d = d.
  Proof.
    revert l ; induction n as [|n IH] ; destruct l as [|t l] ; intros H.
    reflexivity.
    inversion H.
    reflexivity.
    simpl.
    apply IH.
    apply le_S_n.
    assumption.
  Qed.
  
  Lemma eq_nth_cor' (T: Set)(l1 l2 : list T): 
    length l1 = length l2 -> 
    (forall n d,  n < length l1 -> nth n l1 d = nth n l2 d) -> l1 = l2.
  Proof.
    intros h1 h2.
    apply eq_nth_cor ; try assumption.
    intros n d.
    elim (le_lt_dec (length l1) n); intros a.
    rewrite nth_default, nth_default ; try assumption.
    reflexivity.
    rewrite <- h1 ; assumption.
    apply h2.
    assumption.
  Qed.
  
  Section MaxListNat.
  
    Fixpoint max_list_nat_aux (m: nat)(l: list nat){struct l}: nat :=
      match l with 
      | nil => m 
      | t :: h => (max_list_nat_aux (max m t) h)
      end.
      
      (* definition of the maximum of a list of natural numbers *)
      Definition max_list_nat (l: list nat) : nat := max_list_nat_aux 0 l.
      
      Fixpoint max_list_nat' (l: list nat): nat := 
        fold_left max l 0.
        
      Lemma max_list_nat_max_list_nat': forall (l: list nat), max_list_nat l = max_list_nat' l.
      Proof.
        destruct l as [|t q].
        reflexivity.
        revert t ; induction q as [|t' q' IH]; intros t.
        reflexivity.
        apply IH.
      Qed.
      
      (* properties on max_list_nat *)
      Lemma max_list_nat_aux_max: forall (n m: nat)(l: list nat), 
        max_list_nat_aux (max n m) l = max n (max_list_nat_aux m l).
      Proof.
        intros n m l.
        revert n m ; 
        induction l as [|t l IHl] ; intros n m.
        reflexivity.
        simpl.
        do 2 rewrite IHl.
        rewrite max_assoc.
        reflexivity.
      Qed.

      Lemma max_list_cons: forall (t: nat)(l: list nat),
        max_list_nat (t:: l) = max t (max_list_nat l).
      Proof.
        intros t l.
        destruct l as [| h l].
        destruct t as [|t] ;
        reflexivity.
        destruct t as [|t].
        reflexivity.
        apply max_list_nat_aux_max.
      Qed.
      

      Lemma max_list_nat_nil: max_list_nat nil = 0.
      Proof.
        reflexivity.
      Qed.
      
      Lemma max_list_max (l: list nat) : 
        forall (x: nat), In x l -> x <= max_list_nat l.
      Proof.
        induction l as [|h t] ;
        intros x H.
        inversion H.
        rewrite max_list_cons.
        destruct H as [e | H].
        rewrite <- e.
        apply le_max_l.
        assert (H1: max_list_nat t <= max h (max_list_nat t)).
        apply le_max_r.
        apply (le_trans _ _ _ (IHt x H) H1).
      Qed.
      
      Lemma exists_max_list_nat: forall l: list nat, 
        exists m, forall n, In n l -> n <= m.
      Proof.
        intros l.
        exists (max_list_nat l).
        apply max_list_max.
      Qed.
  
  End MaxListNat.
  
   
End Tools_lists.

Section Tools_arith.

  Lemma lt_m_n_Sm_n: forall m n: nat, m < n -> (n - (S m)) < n.
  Proof.
    intros m n h.
    apply lt_minus.
    apply (lt_le_S m n h).
    apply lt_O_Sn.
  Qed.

  Lemma Sn_Sm_eq_n_m: forall (n m: nat), (S n) - (S m) = n - m.
  Proof.
    reflexivity.
  Qed.

  Lemma minus_to_minus: forall (n m p: nat), n - m = p -> n - m - p = 0. 
  Proof.
    intros n m p h.
    rewrite h.
    apply minus_diag.
  Qed.

  Lemma minus_reg_l: forall (n m: nat)(h: m <= n), n - m = n -> m = 0.
  Proof.
    intros n m h H.
    elim (lt_eq_lt_dec m 0); intros a.
    inversion_clear a as [H0|e].
    inversion H0.
    assumption.
    apply False_rec.
    assert (n-m < n).
    apply (lt_minus _ _ h a).
    rewrite H in H0.
    apply (lt_irrefl _ H0).
  Qed.

  Lemma lt_plus_S : forall n m, n < n + (S m).
  Proof.
    intros n m.
    rewrite <- plus_n_Sm , <- plus_Sn_m.
    apply lt_plus_trans, lt_n_Sn.
  Qed.

  Lemma minus_n_m_0 (n m: nat) : m <= n -> n - m = 0 -> n = m.
  Proof.
    revert m ; induction n as [|n IH] ; intros m h1 h2.
    symmetry.
    apply (minus_reg_l h1 h2).
    destruct m as [|m].
    inversion h2.
    apply eq_S.
    apply IH.
    apply le_S_n, h1.
    rewrite <- Sn_Sm_eq_n_m; assumption.
  Qed.

  Lemma lt_minus_S: forall m n: nat, m < n -> (n - (S m)) < n.
  Proof.
    intros m n h.
    apply lt_minus.
    apply (lt_le_S m n h).
    apply lt_O_Sn.
  Qed.

  Lemma lt_n_m_0: forall m n: nat, m < n -> 0 < n.
  Proof.
    intros m n h.
    rewrite (S_pred n m h).
    apply (gt_Sn_O (pred n)).
  Qed. 

  Lemma pred_inf_n: forall m n: nat, m < n -> pred n < n. 
  Proof. 
    intros m n h.
    apply (lt_pred_n_n n (lt_n_m_0 h)).
  Qed.



End Tools_arith.

Section Tools_option.

  Definition RelOp (T: Set)(RelT: relation T): relation (option T).
  Proof.
    intros [t1|] [t2|].
    exact (RelT t1 t2).
    exact False.
    exact False.
    exact True.
  Defined.

  Lemma RelOp_refl (T: Set)(RelT: relation T)(Req: Reflexive RelT)(ot: option T): 
    RelOp RelT ot ot.
  Proof.
    destruct ot as [t|] ; simpl ; reflexivity.
  Qed.
  
  Lemma RelOp_sym (T: Set)(RelT: relation T)(Req: Symmetric RelT)(ot1 ot2: option T): 
    RelOp RelT ot1 ot2 -> RelOp RelT ot2 ot1.
  Proof.
    intros H ; destruct ot1 as [t1|] ; destruct ot2 as [t2|] ; simpl ; try inversion H.
    simpl in H ; symmetry ; assumption.
    reflexivity.
  Qed.
  
  Lemma RelOp_trans (T: Set)(RelT: relation T)(Req: Transitive RelT)(ot1 ot2 ot3: option T): 
    RelOp RelT ot1 ot2 -> RelOp RelT ot2 ot3 -> RelOp RelT ot1 ot3.
  Proof.
    intros H1 H2 ; destruct ot1 as [t1|] ; destruct ot2 as [t2|] ; destruct ot3 as [t3|] ; 
    simpl ; try inversion H1 ; try inversion H2.
    simpl in H1, H2 ; transitivity t2 ; assumption.
    reflexivity.
  Qed.
  
  Add Parametric Relation (T: Set)(RelT: relation T)(Req: Equivalence RelT): 
    (option T) (RelOp RelT)
    reflexivity proved by (RelOp_refl _)
    symmetry proved by (RelOp_sym _)
    transitivity proved by (RelOp_trans _)
  as RelOpRel.
End Tools_option.

Section Bijective.

   Definition Bijective (T U:Type) (f:T->U)(g: U -> T):Prop:=
     (forall t, g (f t) = t) /\ (forall u, f (g u) = u).

   Lemma Bij_sym (T U:Type)(f:T->U)(g: U -> T): 
     Bijective f g -> Bijective g f.
   Proof.
     intros [h1 h2].
     split ; assumption.
   Qed.

   Lemma Bij_trans (T U V: Set)(f1: T -> U)(g1 : U -> T)(f2 : U -> V)(g2 : V -> U) :
     Bijective f1 g1 -> Bijective f2 g2 -> Bijective (fun x => f2 (f1 x)) (fun x => g1 (g2 x)).
   Proof.
     intros [h1 h2] [h3 h4].
     split.
     intros t.
     rewrite h3.
     apply h1.
     intros u.
     rewrite h2.
     apply h4.
   Qed.

  Lemma bij_inj (A B: Set)(f : A -> B)(g : B -> A): 
    Bijective f g -> forall a1 a2, f a1 = f a2 -> a1 = a2.
  Proof.
    intros [H1 _] a1 a2 H3.
    rewrite <- (H1 a1), <- (H1 a2).
    rewrite H3.
    reflexivity.
  Qed.

End Bijective.