(** 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.