(** 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.
  
  (* definition of the maximum of two natural numbers *)
 (* Fixpoint max (n m:nat) {struct m} : nat :=
    match n, m with
    | O, _ => m
    | S n', O => S n'
    | S n', S m' => S (max n' m')
    end.
    
    (* properties of max *)
    Lemma max_ge: forall n m: nat, n <= max n m.
    Proof.
      intros n.
      induction n as [| n IHn] ; intros m.
      apply le_O_n.
      destruct m as [|m IHm].
      apply le_refl.
      apply le_n_S.
      apply IHn.
    Qed.
    
    Lemma max_sym : forall n m: nat , max n m = max m n.
    Proof.
      induction n as [|n IHn] ; intros m ; destruct m ; 
      try reflexivity.
      simpl.
      rewrite IHn.
      reflexivity.
    Qed.
    
    Lemma max_ge2: forall n m: nat, m <= max n m.
    Proof.
      intros n m.
      rewrite max_sym.
      apply max_ge.
    Qed.
    
    Lemma max_0: forall n: nat, max 0 n = n.
    Proof.
      destruct n as [| n IHn];
      reflexivity.
    Qed.
    
    Lemma max_assoc : forall a b c, max a (max b c) = max (max a b) c.
    Proof.
      induction a as [| a IHa] ;
      intros b c.
      do 2 rewrite max_0.
      reflexivity.
      destruct b as [|b].
      rewrite max_0.
      reflexivity.
      destruct c as [|c].
      reflexivity.
      simpl.
      rewrite IHa.
      reflexivity.
    Qed.
    
    Lemma max_pair : forall n1 n2 m1 m2, n1 <= n2 -> m1 <= m2 -> max n1 m1 <= max n2 m2.
    Proof.
      induction n1 as [|n1 IH] ; intros [|n2] [|m1] [|m2] H1 H2 ; try assumption ; 
      try (apply False_rec, (le_Sn_0 _ H1)) ; try (apply False_rec, (le_Sn_0 _ H2)). 
      apply le_O_n.
      apply (le_trans _ _ _ H2 (max_ge2 (S n2) (S m2))).
      apply (le_trans _ _ _ H1 (max_ge (S n2) (S m2))).
      simpl.
      apply le_n_S.
      apply le_S_n in H1.
      apply le_S_n in H2.
      apply (IH _  _ _ H1 H2).
    Qed.
    
    Lemma max_refl : forall n, max n n = n.
    Proof.
      induction n as [|n IH].
      reflexivity.
      simpl.
      f_equal ; assumption.
    Qed.
    *)
    
    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.