diff options
Diffstat (limited to 'theories/Arith')
| -rw-r--r-- | theories/Arith/Arith_base.v | 2 | ||||
| -rw-r--r-- | theories/Arith/Compare_dec.v | 228 | ||||
| -rw-r--r-- | theories/Arith/Div2.v | 165 | ||||
| -rw-r--r-- | theories/Arith/EqNat.v | 98 | ||||
| -rw-r--r-- | theories/Arith/Even.v | 297 | ||||
| -rw-r--r-- | theories/Arith/Factorial.v | 27 | ||||
| -rw-r--r-- | theories/Arith/Gt.v | 131 | ||||
| -rw-r--r-- | theories/Arith/Le.v | 120 | ||||
| -rw-r--r-- | theories/Arith/Lt.v | 170 | ||||
| -rw-r--r-- | theories/Arith/Max.v | 6 | ||||
| -rw-r--r-- | theories/Arith/Min.v | 6 | ||||
| -rw-r--r-- | theories/Arith/Minus.v | 137 | ||||
| -rw-r--r-- | theories/Arith/Mult.v | 199 | ||||
| -rw-r--r-- | theories/Arith/PeanoNat.v | 755 | ||||
| -rw-r--r-- | theories/Arith/Peano_dec.v | 64 | ||||
| -rw-r--r-- | theories/Arith/Plus.v | 191 | ||||
| -rw-r--r-- | theories/Arith/Wf_nat.v | 87 | ||||
| -rw-r--r-- | theories/Arith/vo.itarget | 1 |
18 files changed, 1507 insertions, 1177 deletions
diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v index 9f0f05db4..290ce548a 100644 --- a/theories/Arith/Arith_base.v +++ b/theories/Arith/Arith_base.v @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +Require Export PeanoNat. + Require Export Le. Require Export Lt. Require Export Plus. diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 76132aed0..bcf409e66 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -6,10 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Le. -Require Import Lt. -Require Import Gt. -Require Import Decidable. +Require Import Le Lt Gt Decidable PeanoNat. Local Open Scope nat_scope. @@ -29,31 +26,31 @@ Defined. Definition gt_eq_gt_dec n m : {m > n} + {n = m} + {n > m}. Proof. - intros; apply lt_eq_lt_dec; assumption. + now apply lt_eq_lt_dec. Defined. Definition le_lt_dec n m : {n <= m} + {m < n}. Proof. induction n in m |- *. - auto with arith. - destruct m. - auto with arith. - elim (IHn m); auto with arith. + - left; auto with arith. + - destruct m. + + right; auto with arith. + + elim (IHn m); [left|right]; auto with arith. Defined. Definition le_le_S_dec n m : {n <= m} + {S m <= n}. Proof. - intros; exact (le_lt_dec n m). + exact (le_lt_dec n m). Defined. Definition le_ge_dec n m : {n <= m} + {n >= m}. Proof. - intros; elim (le_lt_dec n m); auto with arith. + elim (le_lt_dec n m); auto with arith. Defined. Definition le_gt_dec n m : {n <= m} + {n > m}. Proof. - intros; exact (le_lt_dec n m). + exact (le_lt_dec n m). Defined. Definition le_lt_eq_dec n m : n <= m -> {n < m} + {n = m}. @@ -62,162 +59,121 @@ Proof. intros; absurd (m < n); auto with arith. Defined. -Theorem le_dec : forall n m, {n <= m} + {~ n <= m}. +Theorem le_dec n m : {n <= m} + {~ n <= m}. Proof. - intros n m. destruct (le_gt_dec n m). - auto with arith. - right. apply gt_not_le. assumption. + destruct (le_gt_dec n m). + - now left. + - right. now apply gt_not_le. Defined. -Theorem lt_dec : forall n m, {n < m} + {~ n < m}. +Theorem lt_dec n m : {n < m} + {~ n < m}. Proof. - intros; apply le_dec. + apply le_dec. Defined. -Theorem gt_dec : forall n m, {n > m} + {~ n > m}. +Theorem gt_dec n m : {n > m} + {~ n > m}. Proof. - intros; apply lt_dec. + apply lt_dec. Defined. -Theorem ge_dec : forall n m, {n >= m} + {~ n >= m}. +Theorem ge_dec n m : {n >= m} + {~ n >= m}. Proof. - intros; apply le_dec. + apply le_dec. Defined. (** Proofs of decidability *) -Theorem dec_le : forall n m, decidable (n <= m). +Theorem dec_le n m : decidable (n <= m). Proof. - intros n m; destruct (le_dec n m); unfold decidable; auto. + apply Nat.le_decidable. Qed. -Theorem dec_lt : forall n m, decidable (n < m). +Theorem dec_lt n m : decidable (n < m). Proof. - intros; apply dec_le. + apply Nat.lt_decidable. Qed. -Theorem dec_gt : forall n m, decidable (n > m). +Theorem dec_gt n m : decidable (n > m). Proof. - intros; apply dec_lt. + apply Nat.lt_decidable. Qed. -Theorem dec_ge : forall n m, decidable (n >= m). +Theorem dec_ge n m : decidable (n >= m). Proof. - intros; apply dec_le. + apply Nat.le_decidable. Qed. -Theorem not_eq : forall n m, n <> m -> n < m \/ m < n. +Theorem not_eq n m : n <> m -> n < m \/ m < n. Proof. - intros x y H; elim (lt_eq_lt_dec x y); - [ intros H1; elim H1; - [ auto with arith | intros H2; absurd (x = y); assumption ] - | auto with arith ]. + apply Nat.lt_gt_cases. Qed. - -Theorem not_le : forall n m, ~ n <= m -> n > m. +Theorem not_le n m : ~ n <= m -> n > m. Proof. - intros x y H; elim (le_gt_dec x y); - [ intros H1; absurd (x <= y); assumption | trivial with arith ]. + apply Nat.nle_gt. Qed. -Theorem not_gt : forall n m, ~ n > m -> n <= m. +Theorem not_gt n m : ~ n > m -> n <= m. Proof. - intros x y H; elim (le_gt_dec x y); - [ trivial with arith | intros H1; absurd (x > y); assumption ]. + apply Nat.nlt_ge. Qed. -Theorem not_ge : forall n m, ~ n >= m -> n < m. +Theorem not_ge n m : ~ n >= m -> n < m. Proof. - intros x y H; exact (not_le y x H). + apply Nat.nle_gt. Qed. -Theorem not_lt : forall n m, ~ n < m -> n >= m. +Theorem not_lt n m : ~ n < m -> n >= m. Proof. - intros x y H; exact (not_gt y x H). + apply Nat.nlt_ge. Qed. -(** A ternary comparison function in the spirit of [Z.compare]. *) +(** A ternary comparison function in the spirit of [Z.compare]. + See now [Nat.compare] and its properties. + In scope [nat_scope], the notation for [Nat.compare] is "?=" *) -Fixpoint nat_compare n m := - match n, m with - | O, O => Eq - | O, S _ => Lt - | S _, O => Gt - | S n', S m' => nat_compare n' m' - end. +Notation nat_compare := Nat.compare (compat "8.4"). -Lemma nat_compare_S : forall n m, nat_compare (S n) (S m) = nat_compare n m. -Proof. - reflexivity. -Qed. +Notation nat_compare_spec := Nat.compare_spec (compat "8.4"). +Notation nat_compare_eq_iff := Nat.compare_eq_iff (compat "8.4"). +Notation nat_compare_S := Nat.compare_succ (compat "8.4"). -Lemma nat_compare_eq_iff : forall n m, nat_compare n m = Eq <-> n = m. +Lemma nat_compare_lt n m : n<m <-> (n ?= m) = Lt. Proof. - induction n; destruct m; simpl; split; auto; try discriminate; - destruct (IHn m); auto. + symmetry. apply Nat.compare_lt_iff. Qed. -Lemma nat_compare_eq : forall n m, nat_compare n m = Eq -> n = m. +Lemma nat_compare_gt n m : n>m <-> (n ?= m) = Gt. Proof. - intros; apply -> nat_compare_eq_iff; auto. + symmetry. apply Nat.compare_gt_iff. Qed. -Lemma nat_compare_lt : forall n m, n<m <-> nat_compare n m = Lt. +Lemma nat_compare_le n m : n<=m <-> (n ?= m) <> Gt. Proof. - induction n; destruct m; simpl; split; auto with arith; - try solve [inversion 1]. - destruct (IHn m); auto with arith. - destruct (IHn m); auto with arith. + symmetry. apply Nat.compare_le_iff. Qed. -Lemma nat_compare_gt : forall n m, n>m <-> nat_compare n m = Gt. +Lemma nat_compare_ge n m : n>=m <-> (n ?= m) <> Lt. Proof. - induction n; destruct m; simpl; split; auto with arith; - try solve [inversion 1]. - destruct (IHn m); auto with arith. - destruct (IHn m); auto with arith. + symmetry. apply Nat.compare_ge_iff. Qed. -Lemma nat_compare_le : forall n m, n<=m <-> nat_compare n m <> Gt. -Proof. - split. - intros LE; contradict LE. - apply lt_not_le. apply <- nat_compare_gt; auto. - intros NGT. apply not_lt. contradict NGT. - apply -> nat_compare_gt; auto. -Qed. - -Lemma nat_compare_ge : forall n m, n>=m <-> nat_compare n m <> Lt. -Proof. - split. - intros GE; contradict GE. - apply lt_not_le. apply <- nat_compare_lt; auto. - intros NLT. apply not_lt. contradict NLT. - apply -> nat_compare_lt; auto. -Qed. +(** Some projections of the above equivalences. *) -Lemma nat_compare_spec : - forall x y, CompareSpec (x=y) (x<y) (y<x) (nat_compare x y). +Lemma nat_compare_eq n m : (n ?= m) = Eq -> n = m. Proof. - intros. - destruct (nat_compare x y) eqn:?; constructor. - apply nat_compare_eq; auto. - apply <- nat_compare_lt; auto. - apply <- nat_compare_gt; auto. + apply Nat.compare_eq_iff. Qed. -(** Some projections of the above equivalences. *) - -Lemma nat_compare_Lt_lt : forall n m, nat_compare n m = Lt -> n<m. +Lemma nat_compare_Lt_lt n m : (n ?= m) = Lt -> n<m. Proof. - intros; apply <- nat_compare_lt; auto. + apply Nat.compare_lt_iff. Qed. -Lemma nat_compare_Gt_gt : forall n m, nat_compare n m = Gt -> n>m. +Lemma nat_compare_Gt_gt n m : (n ?= m) = Gt -> n>m. Proof. - intros; apply <- nat_compare_gt; auto. + apply Nat.compare_gt_iff. Qed. (** A previous definition of [nat_compare] in terms of [lt_eq_lt_dec]. @@ -230,70 +186,48 @@ Definition nat_compare_alt (n m:nat) := | inright _ => Gt end. -Lemma nat_compare_equiv: forall n m, - nat_compare n m = nat_compare_alt n m. +Lemma nat_compare_equiv n m : (n ?= m) = nat_compare_alt n m. Proof. - intros; unfold nat_compare_alt; destruct lt_eq_lt_dec as [[LT|EQ]|GT]. - apply -> nat_compare_lt; auto. - apply <- nat_compare_eq_iff; auto. - apply -> nat_compare_gt; auto. + unfold nat_compare_alt; destruct lt_eq_lt_dec as [[|]|]. + - now apply Nat.compare_lt_iff. + - now apply Nat.compare_eq_iff. + - now apply Nat.compare_gt_iff. Qed. +(** A boolean version of [le] over [nat]. + See now [Nat.leb] and its properties. + In scope [nat_scope], the notation for [Nat.leb] is "<=?" *) -(** A boolean version of [le] over [nat]. *) - -Fixpoint leb (m:nat) : nat -> bool := - match m with - | O => fun _:nat => true - | S m' => - fun n:nat => match n with - | O => false - | S n' => leb m' n' - end - end. +Notation leb := Nat.leb (compat "8.4"). -Lemma leb_correct : forall m n, m <= n -> leb m n = true. -Proof. - induction m as [| m IHm]. trivial. - destruct n. intro H. elim (le_Sn_O _ H). - intros. simpl. apply IHm. apply le_S_n. assumption. -Qed. +Notation leb_iff := Nat.leb_le (compat "8.4"). -Lemma leb_complete : forall m n, leb m n = true -> m <= n. +Lemma leb_iff_conv m n : (n <=? m) = false <-> m < n. Proof. - induction m. trivial with arith. - destruct n. intro H. discriminate H. - auto with arith. + rewrite Nat.leb_nle. apply Nat.nle_gt. Qed. -Lemma leb_iff : forall m n, leb m n = true <-> m <= n. +Lemma leb_correct m n : m <= n -> (m <=? n) = true. Proof. - split; auto using leb_correct, leb_complete. + apply Nat.leb_le. Qed. -Lemma leb_correct_conv : forall m n, m < n -> leb n m = false. +Lemma leb_complete m n : (m <=? n) = true -> m <= n. Proof. - intros. - generalize (leb_complete n m). - destruct (leb n m); auto. - intros; elim (lt_not_le m n); auto. + apply Nat.leb_le. Qed. -Lemma leb_complete_conv : forall m n, leb n m = false -> m < n. +Lemma leb_correct_conv m n : m < n -> (n <=? m) = false. Proof. - intros m n EQ. apply not_le. - intro LE. apply leb_correct in LE. rewrite LE in EQ; discriminate. + apply leb_iff_conv. Qed. -Lemma leb_iff_conv : forall m n, leb n m = false <-> m < n. +Lemma leb_complete_conv m n : (n <=? m) = false -> m < n. Proof. - split; auto using leb_complete_conv, leb_correct_conv. + apply leb_iff_conv. Qed. -Lemma leb_compare : forall n m, leb n m = true <-> nat_compare n m <> Gt. +Lemma leb_compare n m : (n <=? m) = true <-> (n ?= m) <> Gt. Proof. - split; intros. - apply -> nat_compare_le. auto using leb_complete. - apply leb_correct. apply <- nat_compare_le; auto. + rewrite Nat.compare_le_iff. apply Nat.leb_le. Qed. - diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 56115c7f0..8cef48b69 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -6,10 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Lt. -Require Import Plus. -Require Import Compare_dec. -Require Import Even. +(** Nota : this file is OBSOLETE, and left only for compatibility. + Please consider using [Nat.div2] directly, and results about it + (see file PeanoNat). *) + +Require Import PeanoNat Even. Local Open Scope nat_scope. @@ -17,12 +18,7 @@ Implicit Type n : nat. (** Here we define [n/2] and prove some of its properties *) -Fixpoint div2 n : nat := - match n with - | O => 0 - | S O => 0 - | S (S n') => S (div2 n') - end. +Notation div2 := Nat.div2 (compat "8.4"). (** Since [div2] is recursively defined on [0], [1] and [(S (S n))], it is useful to prove the corresponding induction principle *) @@ -31,53 +27,48 @@ Lemma ind_0_1_SS : forall P:nat -> Prop, P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n. Proof. - intros P H0 H1 Hn. - cut (forall n, P n /\ P (S n)). - intros H'n n. elim (H'n n). auto with arith. - - induction n. auto with arith. - intros. elim IHn; auto with arith. + intros P H0 H1 H2. + fix 1. + destruct n as [|[|n]]. + - exact H0. + - exact H1. + - apply H2, ind_0_1_SS. Qed. (** [0 <n => n/2 < n] *) -Lemma lt_div2 : forall n, 0 < n -> div2 n < n. -Proof. - intro n. pattern n. apply ind_0_1_SS. - (* n = 0 *) - inversion 1. - (* n=1 *) - simpl; trivial. - (* n=S S n' *) - intro n'; case (zerop n'). - intro n'_eq_0. rewrite n'_eq_0. auto with arith. - auto with arith. -Qed. +Lemma lt_div2 n : 0 < n -> div2 n < n. +Proof. apply Nat.lt_div2. Qed. Hint Resolve lt_div2: arith. (** Properties related to the parity *) -Lemma even_div2 : forall n, even n -> div2 n = div2 (S n) -with odd_div2 : forall n, odd n -> S (div2 n) = div2 (S n). +Lemma even_div2 n : even n -> div2 n = div2 (S n). Proof. - destruct n; intro H. - (* 0 *) trivial. - (* S n *) inversion_clear H. apply odd_div2 in H0 as <-. trivial. - destruct n; intro. - (* 0 *) inversion H. - (* S n *) inversion_clear H. apply even_div2 in H0 as <-. trivial. + rewrite Even.even_equiv. intros (p,->). + rewrite Nat.div2_succ_double. apply Nat.div2_double. Qed. -Lemma div2_even n : div2 n = div2 (S n) -> even n -with div2_odd n : S (div2 n) = div2 (S n) -> odd n. +Lemma odd_div2 n : odd n -> S (div2 n) = div2 (S n). Proof. -{ destruct n; intro H. - - constructor. - - constructor. apply div2_odd. rewrite H. trivial. } -{ destruct n; intro H. - - discriminate. - - constructor. apply div2_even. injection H as <-. trivial. } + rewrite Even.odd_equiv. intros (p,->). + rewrite Nat.add_1_r, Nat.div2_succ_double. + simpl. f_equal. symmetry. apply Nat.div2_double. +Qed. + +Lemma div2_even n : div2 n = div2 (S n) -> even n. +Proof. + destruct (even_or_odd n) as [Ev|Od]; trivial. + apply odd_div2 in Od. rewrite <- Od. intro Od'. + elim (n_Sn _ Od'). +Qed. + +Lemma div2_odd n : S (div2 n) = div2 (S n) -> odd n. +Proof. + destruct (even_or_odd n) as [Ev|Od]; trivial. + apply even_div2 in Ev. rewrite <- Ev. intro Ev'. + symmetry in Ev'. elim (n_Sn _ Ev'). Qed. Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith. @@ -93,58 +84,52 @@ Qed. (** Properties related to the double ([2n]) *) -Definition double n := n + n. +Notation double := Nat.double (compat "8.4"). -Hint Unfold double: arith. +Hint Unfold double Nat.double: arith. -Lemma double_S : forall n, double (S n) = S (S (double n)). +Lemma double_S n : double (S n) = S (S (double n)). Proof. - intro. unfold double. simpl. auto with arith. + apply Nat.add_succ_r. Qed. -Lemma double_plus : forall n (m:nat), double (n + m) = double n + double m. +Lemma double_plus n m : double (n + m) = double n + double m. Proof. - intros m n. unfold double. - do 2 rewrite plus_assoc_reverse. rewrite (plus_permute n). - reflexivity. + apply Nat.add_shuffle1. Qed. Hint Resolve double_S: arith. -Lemma even_odd_double : - forall n, - (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))). +Lemma even_odd_double n : + (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))). Proof. - intro n. pattern n. apply ind_0_1_SS. - (* n = 0 *) - split; split; auto with arith. - intro H. inversion H. - (* n = 1 *) - split; split; auto with arith. - intro H. inversion H. inversion H1. - (* n = (S (S n')) *) - intros. destruct H as ((IH1,IH2),(IH3,IH4)). - split; split. - intro H. inversion H. inversion H1. - simpl. rewrite (double_S (div2 n0)). auto with arith. - simpl. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith. - intro H. inversion H. inversion H1. - simpl. rewrite (double_S (div2 n0)). auto with arith. - simpl. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith. + revert n. fix 1. destruct n as [|[|n]]. + - (* n = 0 *) + split; split; auto with arith. inversion 1. + - (* n = 1 *) + split; split; auto with arith. inversion_clear 1. inversion H0. + - (* n = (S (S n')) *) + destruct (even_odd_double n) as ((Ev,Ev'),(Od,Od')). + split; split; simpl; rewrite ?double_S. + + inversion_clear 1. inversion_clear H0. auto. + + injection 1. auto with arith. + + inversion_clear 1. inversion_clear H0. auto. + + injection 1. auto with arith. Qed. + (** Specializations *) -Lemma even_double : forall n, even n -> n = double (div2 n). -Proof fun n => proj1 (proj1 (even_odd_double n)). +Lemma even_double n : even n -> n = double (div2 n). +Proof proj1 (proj1 (even_odd_double n)). -Lemma double_even : forall n, n = double (div2 n) -> even n. -Proof fun n => proj2 (proj1 (even_odd_double n)). +Lemma double_even n : n = double (div2 n) -> even n. +Proof proj2 (proj1 (even_odd_double n)). -Lemma odd_double : forall n, odd n -> n = S (double (div2 n)). -Proof fun n => proj1 (proj2 (even_odd_double n)). +Lemma odd_double n : odd n -> n = S (double (div2 n)). +Proof proj1 (proj2 (even_odd_double n)). -Lemma double_odd : forall n, n = S (double (div2 n)) -> odd n. -Proof fun n => proj2 (proj2 (even_odd_double n)). +Lemma double_odd n : n = S (double (div2 n)) -> odd n. +Proof proj2 (proj2 (even_odd_double n)). Hint Resolve even_double double_even odd_double double_odd: arith. @@ -166,22 +151,8 @@ Defined. (** Doubling before dividing by two brings back to the initial number. *) -Lemma div2_double : forall n:nat, div2 (2*n) = n. -Proof. - induction n. - simpl; auto. - simpl. - replace (n+S(n+0)) with (S (2*n)). - f_equal; auto. - simpl; auto with arith. -Qed. +Lemma div2_double n : div2 (2*n) = n. +Proof. apply Nat.div2_double. Qed. -Lemma div2_double_plus_one : forall n:nat, div2 (S (2*n)) = n. -Proof. - induction n. - simpl; auto. - simpl. - replace (n+S(n+0)) with (S (2*n)). - f_equal; auto. - simpl; auto with arith. -Qed. +Lemma div2_double_plus_one n : div2 (S (2*n)) = n. +Proof. apply Nat.div2_succ_double. Qed. diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index ce8eb4785..699ac281e 100644 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -6,11 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Equality on natural numbers *) - +Require Import PeanoNat. Local Open Scope nat_scope. -Implicit Types m n x y : nat. +(** Equality on natural numbers *) (** * Propositional equality *) @@ -22,28 +21,33 @@ Fixpoint eq_nat n m : Prop := | S n1, S m1 => eq_nat n1 m1 end. -Theorem eq_nat_refl : forall n, eq_nat n n. +Theorem eq_nat_refl n : eq_nat n n. +Proof. induction n; simpl; auto. Qed. Hint Resolve eq_nat_refl: arith v62. (** [eq] restricted to [nat] and [eq_nat] are equivalent *) -Lemma eq_eq_nat : forall n m, n = m -> eq_nat n m. - induction 1; trivial with arith. +Theorem eq_nat_is_eq n m : eq_nat n m <-> n = m. +Proof. + split. + - revert m; induction n; destruct m; simpl; contradiction || auto. + - intros <-; apply eq_nat_refl. Qed. -Hint Immediate eq_eq_nat: arith v62. -Lemma eq_nat_eq : forall n m, eq_nat n m -> n = m. - induction n; induction m; simpl; contradiction || auto with arith. +Lemma eq_eq_nat n m : n = m -> eq_nat n m. +Proof. + apply eq_nat_is_eq. Qed. -Hint Immediate eq_nat_eq: arith v62. -Theorem eq_nat_is_eq : forall n m, eq_nat n m <-> n = m. +Lemma eq_nat_eq n m : eq_nat n m -> n = m. Proof. - split; auto with arith. + apply eq_nat_is_eq. Qed. +Hint Immediate eq_eq_nat eq_nat_eq: arith v62. + Theorem eq_nat_elim : forall n (P:nat -> Prop), P n -> forall m, eq_nat n m -> P m. Proof. @@ -52,63 +56,47 @@ Qed. Theorem eq_nat_decide : forall n m, {eq_nat n m} + {~ eq_nat n m}. Proof. - induction n. - destruct m as [| n]. - auto with arith. - intros; right; red; trivial with arith. - destruct m as [| n0]. - right; red; auto with arith. - intros. - simpl. - apply IHn. + induction n; destruct m; simpl. + - left; trivial. + - right; intro; trivial. + - right; intro; trivial. + - apply IHn. Defined. -(** * Boolean equality on [nat] *) +(** * Boolean equality on [nat]. -Fixpoint beq_nat n m : bool := - match n, m with - | O, O => true - | O, S _ => false - | S _, O => false - | S n1, S m1 => beq_nat n1 m1 - end. + We reuse the one already defined in module [Nat]. + In scope [nat_scope], the notation "=?" can be used. *) -Lemma beq_nat_refl : forall n, true = beq_nat n n. -Proof. - intro x; induction x; simpl; auto. -Qed. +Notation beq_nat := Nat.eqb (compat "8.4"). -Definition beq_nat_eq : forall x y, true = beq_nat x y -> x = y. -Proof. - double induction x y; simpl. - reflexivity. - intros n H1 H2. discriminate H2. - intros n H1 H2. discriminate H2. - intros n H1 z H2 H3. case (H2 _ H3). reflexivity. -Defined. +Notation beq_nat_true_iff := Nat.eqb_eq (compat "8.4"). +Notation beq_nat_false_iff := Nat.eqb_neq (compat "8.4"). -Lemma beq_nat_true : forall x y, beq_nat x y = true -> x=y. +Lemma beq_nat_refl n : true = (n =? n). Proof. - induction x; destruct y; simpl; auto; intros; discriminate. + symmetry. apply Nat.eqb_refl. Qed. -Lemma beq_nat_false : forall x y, beq_nat x y = false -> x<>y. +Lemma beq_nat_true n m : (n =? m) = true -> n=m. Proof. - induction x; destruct y; simpl; auto; intros; discriminate. + apply Nat.eqb_eq. Qed. -Lemma beq_nat_true_iff : forall x y, beq_nat x y = true <-> x=y. +Lemma beq_nat_false n m : (n =? m) = false -> n<>m. Proof. - split. apply beq_nat_true. - intros; subst; symmetry; apply beq_nat_refl. + apply Nat.eqb_neq. Qed. -Lemma beq_nat_false_iff : forall x y, beq_nat x y = false <-> x<>y. +(** TODO: is it really useful here to have a Defined ? + Otherwise we could use Nat.eqb_eq *) + +Definition beq_nat_eq : forall n m, true = (n =? m) -> n = m. Proof. - intros x y. - split. apply beq_nat_false. - generalize (beq_nat_true_iff x y). - destruct beq_nat; auto. - intros IFF NEQ. elim NEQ. apply IFF; auto. -Qed. + induction n; destruct m; simpl. + - reflexivity. + - discriminate. + - discriminate. + - intros H. case (IHn _ H). reflexivity. +Defined. diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index 4f679fe2b..050b45ed9 100644 --- a/theories/Arith/Even.v +++ b/theories/Arith/Even.v @@ -6,16 +6,22 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Nota : this file is OBSOLETE, and left only for compatibility. + Please consider instead predicates [Nat.Even] and [Nat.Odd] + and Boolean functions [Nat.even] and [Nat.odd]. *) + (** Here we define the predicates [even] and [odd] by mutual induction and we prove the decidability and the exclusion of those predicates. The main results about parity are proved in the module Div2. *) +Require Import PeanoNat. + Local Open Scope nat_scope. Implicit Types m n : nat. -(** * Definition of [even] and [odd], and basic facts *) +(** * Inductive definition of [even] and [odd] *) Inductive even : nat -> Prop := | even_O : even 0 @@ -26,225 +32,150 @@ with odd : nat -> Prop := Hint Constructors even: arith. Hint Constructors odd: arith. -Lemma even_or_odd : forall n, even n \/ odd n. +(** * Equivalence with predicates [Nat.Even] and [Nat.odd] *) + +Lemma even_equiv : forall n, even n <-> Nat.Even n. +Proof. + fix 1. + destruct n as [|[|n]]; simpl. + - split; [now exists 0 | constructor]. + - split. + + inversion_clear 1. inversion_clear H0. + + now rewrite <- Nat.even_spec. + - rewrite Nat.Even_succ_succ, <- even_equiv. + split. + + inversion_clear 1. now inversion_clear H0. + + now do 2 constructor. +Qed. + +Lemma odd_equiv : forall n, odd n <-> Nat.Odd n. +Proof. + fix 1. + destruct n as [|[|n]]; simpl. + - split. + + inversion_clear 1. + + now rewrite <- Nat.odd_spec. + - split; [ now exists 0 | do 2 constructor ]. + - rewrite Nat.Odd_succ_succ, <- odd_equiv. + split. + + inversion_clear 1. now inversion_clear H0. + + now do 2 constructor. +Qed. + +(** Basic facts *) + +Lemma even_or_odd n : even n \/ odd n. Proof. induction n. - auto with arith. - elim IHn; auto with arith. + - auto with arith. + - elim IHn; auto with arith. Qed. -Lemma even_odd_dec : forall n, {even n} + {odd n}. +Lemma even_odd_dec n : {even n} + {odd n}. Proof. induction n. - auto with arith. - elim IHn; auto with arith. + - auto with arith. + - elim IHn; auto with arith. Defined. -Lemma not_even_and_odd : forall n, even n -> odd n -> False. +Lemma not_even_and_odd n : even n -> odd n -> False. Proof. induction n. - intros even_0 odd_0. inversion odd_0. - intros even_Sn odd_Sn. inversion even_Sn. inversion odd_Sn. auto with arith. + - intros Ev Od. inversion Od. + - intros Ev Od. inversion Ev. inversion Od. auto with arith. Qed. (** * Facts about [even] & [odd] wrt. [plus] *) -Lemma even_plus_split : forall n m, - (even (n + m) -> even n /\ even m \/ odd n /\ odd m) -with odd_plus_split : forall n m, +Ltac parity2bool := + rewrite ?even_equiv, ?odd_equiv, <- ?Nat.even_spec, <- ?Nat.odd_spec. + +Ltac parity_binop_spec := + rewrite ?Nat.even_add, ?Nat.odd_add, ?Nat.even_mul, ?Nat.odd_mul. + +Ltac parity_binop := + parity2bool; parity_binop_spec; unfold Nat.odd; + do 2 destruct Nat.even; simpl; tauto. + + +Lemma even_plus_split n m : + even (n + m) -> even n /\ even m \/ odd n /\ odd m. +Proof. parity_binop. Qed. + +Lemma odd_plus_split n m : odd (n + m) -> odd n /\ even m \/ even n /\ odd m. -Proof. -intros. clear even_plus_split. destruct n; simpl in *. - auto with arith. - inversion_clear H; - apply odd_plus_split in H0 as [(H0,?)|(H0,?)]; auto with arith. -intros. clear odd_plus_split. destruct n; simpl in *. - auto with arith. - inversion_clear H; - apply even_plus_split in H0 as [(H0,?)|(H0,?)]; auto with arith. -Qed. +Proof. parity_binop. Qed. -Lemma even_even_plus : forall n m, even n -> even m -> even (n + m) -with odd_plus_l : forall n m, odd n -> even m -> odd (n + m). -Proof. -intros n m [|] ?. trivial. apply even_S, odd_plus_l; trivial. -intros n m [] ?. apply odd_S, even_even_plus; trivial. -Qed. +Lemma even_even_plus n m : even n -> even m -> even (n + m). +Proof. parity_binop. Qed. -Lemma odd_plus_r : forall n m, even n -> odd m -> odd (n + m) -with odd_even_plus : forall n m, odd n -> odd m -> even (n + m). -Proof. -intros n m [|] ?. trivial. apply odd_S, odd_even_plus; trivial. -intros n m [] ?. apply even_S, odd_plus_r; trivial. -Qed. +Lemma odd_plus_l n m : odd n -> even m -> odd (n + m). +Proof. parity_binop. Qed. + +Lemma odd_plus_r n m : even n -> odd m -> odd (n + m). +Proof. parity_binop. Qed. -Lemma even_plus_aux : forall n m, +Lemma odd_even_plus n m : odd n -> odd m -> even (n + m). +Proof. parity_binop. Qed. + +Lemma even_plus_aux n m : (odd (n + m) <-> odd n /\ even m \/ even n /\ odd m) /\ (even (n + m) <-> even n /\ even m \/ odd n /\ odd m). -Proof. -split; split; auto using odd_plus_split, even_plus_split. -intros [[]|[]]; auto using odd_plus_r, odd_plus_l. -intros [[]|[]]; auto using even_even_plus, odd_even_plus. -Qed. +Proof. parity_binop. Qed. -Lemma even_plus_even_inv_r : forall n m, even (n + m) -> even n -> even m. -Proof. - intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto. - intro; destruct (not_even_and_odd n); auto. -Qed. +Lemma even_plus_even_inv_r n m : even (n + m) -> even n -> even m. +Proof. parity_binop. Qed. -Lemma even_plus_even_inv_l : forall n m, even (n + m) -> even m -> even n. -Proof. - intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto. - intro; destruct (not_even_and_odd m); auto. -Qed. +Lemma even_plus_even_inv_l n m : even (n + m) -> even m -> even n. +Proof. parity_binop. Qed. -Lemma even_plus_odd_inv_r : forall n m, even (n + m) -> odd n -> odd m. -Proof. - intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto. - intro; destruct (not_even_and_odd n); auto. -Qed. +Lemma even_plus_odd_inv_r n m : even (n + m) -> odd n -> odd m. +Proof. parity_binop. Qed. -Lemma even_plus_odd_inv_l : forall n m, even (n + m) -> odd m -> odd n. -Proof. - intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto. - intro; destruct (not_even_and_odd m); auto. -Qed. -Hint Resolve even_even_plus odd_even_plus: arith. +Lemma even_plus_odd_inv_l n m : even (n + m) -> odd m -> odd n. +Proof. parity_binop. Qed. -Lemma odd_plus_even_inv_l : forall n m, odd (n + m) -> odd m -> even n. -Proof. - intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto. - intro; destruct (not_even_and_odd m); auto. -Qed. +Lemma odd_plus_even_inv_l n m : odd (n + m) -> odd m -> even n. +Proof. parity_binop. Qed. -Lemma odd_plus_even_inv_r : forall n m, odd (n + m) -> odd n -> even m. -Proof. - intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto. - intro; destruct (not_even_and_odd n); auto. -Qed. +Lemma odd_plus_even_inv_r n m : odd (n + m) -> odd n -> even m. +Proof. parity_binop. Qed. -Lemma odd_plus_odd_inv_l : forall n m, odd (n + m) -> even m -> odd n. -Proof. - intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto. - intro; destruct (not_even_and_odd m); auto. -Qed. +Lemma odd_plus_odd_inv_l n m : odd (n + m) -> even m -> odd n. +Proof. parity_binop. Qed. -Lemma odd_plus_odd_inv_r : forall n m, odd (n + m) -> even n -> odd m. -Proof. - intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto. - intro; destruct (not_even_and_odd n); auto. -Qed. -Hint Resolve odd_plus_l odd_plus_r: arith. +Lemma odd_plus_odd_inv_r n m : odd (n + m) -> even n -> odd m. +Proof. parity_binop. Qed. (** * Facts about [even] and [odd] wrt. [mult] *) -Lemma even_mult_aux : - forall n m, - (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m). -Proof. - intros n; elim n; simpl; auto with arith. - intros m; split; split; auto with arith. - intros H'; inversion H'. - intros H'; elim H'; auto. - intros n0 H' m; split; split; auto with arith. - intros H'0. - elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'3; intros H'1 H'2; - case H'1; auto. - intros H'5; elim H'5; intros H'6 H'7; auto with arith. - split; auto with arith. - case (H' m). - intros H'8 H'9; case H'9. - intros H'10; case H'10; auto with arith. - intros H'11 H'12; case (not_even_and_odd m); auto with arith. - intros H'5; elim H'5; intros H'6 H'7; case (not_even_and_odd (n0 * m)); auto. - case (H' m). - intros H'8 H'9; case H'9; auto. - intros H'0; elim H'0; intros H'1 H'2; clear H'0. - elim (even_plus_aux m (n0 * m)); auto. - intros H'0 H'3. - elim H'0. - intros H'4 H'5; apply H'5; auto. - left; split; auto with arith. - case (H' m). - intros H'6 H'7; elim H'7. - intros H'8 H'9; apply H'9. - left. - inversion H'1; auto. - intros H'0. - elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'4. - intros H'1 H'2. - elim H'1; auto. - intros H; case H; auto. - intros H'5; elim H'5; intros H'6 H'7; auto with arith. - left. - case (H' m). - intros H'8; elim H'8. - intros H'9; elim H'9; auto with arith. - intros H'0; elim H'0; intros H'1. - case (even_or_odd m); intros H'2. - apply even_even_plus; auto. - case (H' m). - intros H H0; case H0; auto. - apply odd_even_plus; auto. - inversion H'1; case (H' m); auto. - intros H1; case H1; auto. - apply even_even_plus; auto. - case (H' m). - intros H H0; case H0; auto. -Qed. +Lemma even_mult_aux n m : + (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m). +Proof. parity_binop. Qed. -Lemma even_mult_l : forall n m, even n -> even (n * m). -Proof. - intros n m; case (even_mult_aux n m); auto. - intros H H0; case H0; auto. -Qed. +Lemma even_mult_l n m : even n -> even (n * m). +Proof. parity_binop. Qed. -Lemma even_mult_r : forall n m, even m -> even (n * m). -Proof. - intros n m; case (even_mult_aux n m); auto. - intros H H0; case H0; auto. -Qed. -Hint Resolve even_mult_l even_mult_r: arith. +Lemma even_mult_r n m : even m -> even (n * m). +Proof. parity_binop. Qed. -Lemma even_mult_inv_r : forall n m, even (n * m) -> odd n -> even m. -Proof. - intros n m H' H'0. - case (even_mult_aux n m). - intros H'1 H'2; elim H'2. - intros H'3; elim H'3; auto. - intros H; case (not_even_and_odd n); auto. -Qed. +Lemma even_mult_inv_r n m : even (n * m) -> odd n -> even m. +Proof. parity_binop. Qed. -Lemma even_mult_inv_l : forall n m, even (n * m) -> odd m -> even n. -Proof. - intros n m H' H'0. - case (even_mult_aux n m). - intros H'1 H'2; elim H'2. - intros H'3; elim H'3; auto. - intros H; case (not_even_and_odd m); auto. -Qed. +Lemma even_mult_inv_l n m : even (n * m) -> odd m -> even n. +Proof. parity_binop. Qed. -Lemma odd_mult : forall n m, odd n -> odd m -> odd (n * m). -Proof. - intros n m; case (even_mult_aux n m); intros H; case H; auto. -Qed. -Hint Resolve even_mult_l even_mult_r odd_mult: arith. +Lemma odd_mult n m : odd n -> odd m -> odd (n * m). +Proof. parity_binop. Qed. -Lemma odd_mult_inv_l : forall n m, odd (n * m) -> odd n. -Proof. - intros n m H'. - case (even_mult_aux n m). - intros H'1 H'2; elim H'1. - intros H'3; elim H'3; auto. -Qed. +Lemma odd_mult_inv_l n m : odd (n * m) -> odd n. +Proof. parity_binop. Qed. -Lemma odd_mult_inv_r : forall n m, odd (n * m) -> odd m. -Proof. - intros n m H'. - case (even_mult_aux n m). - intros H'1 H'2; elim H'1. - intros H'3; elim H'3; auto. -Qed. +Lemma odd_mult_inv_r n m : odd (n * m) -> odd m. +Proof. parity_binop. Qed. + +Hint Resolve + even_even_plus odd_even_plus odd_plus_l odd_plus_r + even_mult_l even_mult_r even_mult_l even_mult_r odd_mult : arith. diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index 37aa1b2c5..d560b4af9 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -6,9 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Plus. -Require Import Mult. -Require Import Lt. +Require Import PeanoNat Plus Mult Lt. Local Open Scope nat_scope. (** Factorial *) @@ -21,28 +19,19 @@ Fixpoint fact (n:nat) : nat := Arguments fact n%nat. -Lemma lt_O_fact : forall n:nat, 0 < fact n. +Lemma lt_O_fact n : 0 < fact n. Proof. - simple induction n; unfold lt; simpl; auto with arith. + induction n; simpl; auto with arith. Qed. -Lemma fact_neq_0 : forall n:nat, fact n <> 0. +Lemma fact_neq_0 n : fact n <> 0. Proof. - intro. - apply not_eq_sym. - apply lt_O_neq. - apply lt_O_fact. + apply Nat.neq_0_lt_0, lt_O_fact. Qed. -Lemma fact_le : forall n m:nat, n <= m -> fact n <= fact m. +Lemma fact_le n m : n <= m -> fact n <= fact m. Proof. induction 1. - apply le_n. - assert (1 * fact n <= S m * fact m). - apply mult_le_compat. - apply lt_le_S; apply lt_O_Sn. - assumption. - simpl (1 * fact n) in H0. - rewrite <- plus_n_O in H0. - assumption. + - apply le_n. + - simpl. transitivity (fact m). trivial. apply Nat.le_add_r. Qed. diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v index 31b155071..d142f3105 100644 --- a/theories/Arith/Gt.v +++ b/theories/Arith/Gt.v @@ -6,149 +6,140 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Theorems about [gt] in [nat]. [gt] is defined in [Init/Peano.v] as: +(** Theorems about [gt] in [nat]. + + This file is DEPRECATED now, see module [PeanoNat.Nat] instead, + which favor [lt] over [gt]. + + [gt] is defined in [Init/Peano.v] as: << Definition gt (n m:nat) := m < n. >> *) -Require Import Le. -Require Import Lt. -Require Import Plus. +Require Import PeanoNat Le Lt Plus. Local Open Scope nat_scope. -Implicit Types m n p : nat. - (** * Order and successor *) -Theorem gt_Sn_O : forall n, S n > 0. -Proof. - auto with arith. -Qed. -Hint Resolve gt_Sn_O: arith v62. +Theorem gt_Sn_O n : S n > 0. +Proof Nat.lt_0_succ _. -Theorem gt_Sn_n : forall n, S n > n. -Proof. - auto with arith. -Qed. -Hint Resolve gt_Sn_n: arith v62. +Theorem gt_Sn_n n : S n > n. +Proof Nat.lt_succ_diag_r _. -Theorem gt_n_S : forall n m, n > m -> S n > S m. +Theorem gt_n_S n m : n > m -> S n > S m. Proof. - auto with arith. + apply Nat.succ_lt_mono. Qed. -Hint Resolve gt_n_S: arith v62. -Lemma gt_S_n : forall n m, S m > S n -> m > n. +Lemma gt_S_n n m : S m > S n -> m > n. Proof. - auto with arith. + apply Nat.succ_lt_mono. Qed. -Hint Immediate gt_S_n: arith v62. -Theorem gt_S : forall n m, S n > m -> n > m \/ m = n. +Theorem gt_S n m : S n > m -> n > m \/ m = n. Proof. - intros n m H; unfold gt; apply le_lt_or_eq; auto with arith. + intro. now apply Nat.lt_eq_cases, Nat.succ_le_mono. Qed. -Lemma gt_pred : forall n m, m > S n -> pred m > n. +Lemma gt_pred n m : m > S n -> pred m > n. Proof. - auto with arith. + apply Nat.lt_succ_lt_pred. Qed. -Hint Immediate gt_pred: arith v62. (** * Irreflexivity *) -Lemma gt_irrefl : forall n, ~ n > n. -Proof lt_irrefl. -Hint Resolve gt_irrefl: arith v62. +Lemma gt_irrefl n : ~ n > n. +Proof Nat.lt_irrefl _. (** * Asymmetry *) -Lemma gt_asym : forall n m, n > m -> ~ m > n. -Proof fun n m => lt_asym m n. - -Hint Resolve gt_asym: arith v62. +Lemma gt_asym n m : n > m -> ~ m > n. +Proof Nat.lt_asymm _ _. (** * Relating strict and large orders *) -Lemma le_not_gt : forall n m, n <= m -> ~ n > m. -Proof le_not_lt. -Hint Resolve le_not_gt: arith v62. - -Lemma gt_not_le : forall n m, n > m -> ~ n <= m. +Lemma le_not_gt n m : n <= m -> ~ n > m. Proof. -auto with arith. + apply Nat.le_ngt. Qed. -Hint Resolve gt_not_le: arith v62. +Lemma gt_not_le n m : n > m -> ~ n <= m. +Proof. + apply Nat.lt_nge. +Qed. -Theorem le_S_gt : forall n m, S n <= m -> m > n. +Theorem le_S_gt n m : S n <= m -> m > n. Proof. - auto with arith. + apply Nat.le_succ_l. Qed. -Hint Immediate le_S_gt: arith v62. -Lemma gt_S_le : forall n m, S m > n -> n <= m. +Lemma gt_S_le n m : S m > n -> n <= m. Proof. - intros n p; exact (lt_n_Sm_le n p). + apply Nat.succ_le_mono. Qed. -Hint Immediate gt_S_le: arith v62. -Lemma gt_le_S : forall n m, m > n -> S n <= m. +Lemma gt_le_S n m : m > n -> S n <= m. Proof. - auto with arith. + apply Nat.le_succ_l. Qed. -Hint Resolve gt_le_S: arith v62. -Lemma le_gt_S : forall n m, n <= m -> S m > n. +Lemma le_gt_S n m : n <= m -> S m > n. Proof. - auto with arith. + apply Nat.succ_le_mono. Qed. -Hint Resolve le_gt_S: arith v62. (** * Transitivity *) -Theorem le_gt_trans : forall n m p, m <= n -> m > p -> n > p. +Theorem le_gt_trans n m p : m <= n -> m > p -> n > p. Proof. - red; intros; apply lt_le_trans with m; auto with arith. + intros. now apply Nat.lt_le_trans with m. Qed. -Theorem gt_le_trans : forall n m p, n > m -> p <= m -> n > p. +Theorem gt_le_trans n m p : n > m -> p <= m -> n > p. Proof. - red; intros; apply le_lt_trans with m; auto with arith. + intros. now apply Nat.le_lt_trans with m. Qed. -Lemma gt_trans : forall n m p, n > m -> m > p -> n > p. +Lemma gt_trans n m p : n > m -> m > p -> n > p. Proof. - red; intros n m p H1 H2. - apply lt_trans with m; auto with arith. + intros. now apply Nat.lt_trans with m. Qed. -Theorem gt_trans_S : forall n m p, S n > m -> m > p -> n > p. +Theorem gt_trans_S n m p : S n > m -> m > p -> n > p. Proof. - red; intros; apply lt_le_trans with m; auto with arith. + intros. apply Nat.lt_le_trans with m; trivial. now apply Nat.succ_le_mono. Qed. -Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62. - (** * Comparison to 0 *) -Theorem gt_0_eq : forall n, n > 0 \/ 0 = n. +Theorem gt_0_eq n : n > 0 \/ 0 = n. Proof. - intro n; apply gt_S; auto with arith. + destruct n; [now right | left; apply Nat.lt_0_succ]. Qed. (** * Simplification and compatibility *) -Lemma plus_gt_reg_l : forall n m p, p + n > p + m -> n > m. +Lemma plus_gt_reg_l n m p : p + n > p + m -> n > m. Proof. - red; intros n m p H; apply plus_lt_reg_l with p; auto with arith. + apply Nat.add_lt_mono_l. Qed. -Lemma plus_gt_compat_l : forall n m p, n > m -> p + n > p + m. +Lemma plus_gt_compat_l n m p : n > m -> p + n > p + m. Proof. - auto with arith. + apply Nat.add_lt_mono_l. Qed. + +(** * Hints *) + +Hint Resolve gt_Sn_O gt_Sn_n gt_n_S : arith v62. +Hint Immediate gt_S_n gt_pred : arith v62. +Hint Resolve gt_irrefl gt_asym : arith v62. +Hint Resolve le_not_gt gt_not_le : arith v62. +Hint Immediate le_S_gt gt_S_le : arith v62. +Hint Resolve gt_le_S le_gt_S : arith v62. +Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62. Hint Resolve plus_gt_compat_l: arith v62. (* begin hide *) diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index c3386787d..53bb5cde2 100644 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -6,7 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Order on natural numbers. [le] is defined in [Init/Peano.v] as: +(** Order on natural numbers. + + This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead. + + [le] is defined in [Init/Peano.v] as: << Inductive le (n:nat) : nat -> Prop := | le_n : n <= n @@ -14,110 +18,58 @@ Inductive le (n:nat) : nat -> Prop := where "n <= m" := (le n m) : nat_scope. >> - *) +*) -Local Open Scope nat_scope. +Require Import PeanoNat. -Implicit Types m n p : nat. +Local Open Scope nat_scope. -(** * [le] is a pre-order *) +(** * [le] is an order on [nat] *) -(** Reflexivity *) -Theorem le_refl : forall n, n <= n. -Proof. - exact le_n. -Qed. +Notation le_refl := Nat.le_refl (compat "8.4"). +Notation le_trans := Nat.le_trans (compat "8.4"). +Notation le_antisym := Nat.le_antisymm (compat "8.4"). -(** Transitivity *) -Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p. -Proof. - induction 2; auto. -Qed. Hint Resolve le_trans: arith v62. +Hint Immediate le_antisym: arith v62. -(** * Properties of [le] w.r.t. successor, predecessor and 0 *) - -(** Comparison to 0 *) - -Theorem le_0_n : forall n, 0 <= n. -Proof. - induction n; auto. -Qed. - -Theorem le_Sn_0 : forall n, ~ S n <= 0. -Proof. - red; intros n H. - change (IsSucc 0); elim H; simpl; auto with arith. -Qed. +(** * Properties of [le] w.r.t 0 *) -Hint Resolve le_0_n le_Sn_0: arith v62. +Notation le_0_n := Nat.le_0_l (compat "8.4"). (* 0 <= n *) +Notation le_Sn_0 := Nat.nle_succ_0 (compat "8.4"). (* ~ S n <= 0 *) -Theorem le_n_0_eq : forall n, n <= 0 -> 0 = n. +Lemma le_n_0_eq n : n <= 0 -> 0 = n. Proof. - induction n. auto with arith. idtac. auto with arith. - intro; contradiction le_Sn_0 with n. + intros. symmetry. now apply Nat.le_0_r. Qed. -Hint Immediate le_n_0_eq: arith v62. +(** * Properties of [le] w.r.t successor *) -(** [le] and successor *) +(** See also [Nat.succ_le_mono]. *) Theorem le_n_S : forall n m, n <= m -> S n <= S m. -Proof. - induction 1; auto. -Qed. +Proof Peano.le_n_S. -Theorem le_n_Sn : forall n, n <= S n. -Proof. - auto. -Qed. +Theorem le_S_n : forall n m, S n <= S m -> n <= m. +Proof Peano.le_S_n. -Hint Resolve le_n_S le_n_Sn : arith v62. +Notation le_n_Sn := Nat.le_succ_diag_r (compat "8.4"). (* n <= S n *) +Notation le_Sn_n := Nat.nle_succ_diag_l (compat "8.4"). (* ~ S n <= n *) Theorem le_Sn_le : forall n m, S n <= m -> n <= m. -Proof. - intros n m H; apply le_trans with (S n); auto with arith. -Qed. -Hint Immediate le_Sn_le: arith v62. +Proof Nat.lt_le_incl. -Theorem le_S_n : forall n m, S n <= S m -> n <= m. -Proof. - exact Peano.le_S_n. -Qed. -Hint Immediate le_S_n: arith v62. +Hint Resolve le_0_n le_Sn_0: arith v62. +Hint Resolve le_n_S le_n_Sn le_Sn_n : arith v62. +Hint Immediate le_n_0_eq le_Sn_le le_S_n : arith v62. -Theorem le_Sn_n : forall n, ~ S n <= n. -Proof. - induction n; auto with arith. -Qed. -Hint Resolve le_Sn_n: arith v62. +(** * Properties of [le] w.r.t predecessor *) -(** [le] and predecessor *) +Notation le_pred_n := Nat.le_pred_l (compat "8.4"). (* pred n <= n *) +Notation le_pred := Nat.pred_le_mono (compat "8.4"). (* n<=m -> pred n <= pred m *) -Theorem le_pred_n : forall n, pred n <= n. -Proof. - induction n; auto with arith. -Qed. Hint Resolve le_pred_n: arith v62. -Theorem le_pred : forall n m, n <= m -> pred n <= pred m. -Proof. - exact Peano.le_pred. -Qed. - -(** * [le] is a order on [nat] *) -(** Antisymmetry *) - -Theorem le_antisym : forall n m, n <= m -> m <= n -> n = m. -Proof. - intros n m H; destruct H as [|m' H]; auto with arith. - intros H1. - absurd (S m' <= m'); auto with arith. - apply le_trans with n; auto with arith. -Qed. -Hint Immediate le_antisym: arith v62. - - (** * A different elimination principle for the order on natural numbers *) Lemma le_elim_rel : @@ -126,10 +78,10 @@ Lemma le_elim_rel : (forall p (q:nat), p <= q -> P p q -> P (S p) (S q)) -> forall n m, n <= m -> P n m. Proof. - induction n; auto with arith. - intros m Le. - elim Le; auto with arith. -Qed. + intros P H0 HS. + induction n; trivial. + intros m Le. elim Le; auto with arith. + Qed. (* begin hide *) Notation le_O_n := le_0_n (only parsing). diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index 8559b782b..5a793ffdd 100644 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -6,185 +6,149 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Theorems about [lt] in nat. [lt] is defined in library [Init/Peano.v] as: +(** Strict order on natural numbers. + + This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead. + + [lt] is defined in library [Init/Peano.v] as: << Definition lt (n m:nat) := S n <= m. Infix "<" := lt : nat_scope. >> *) -Require Import Le. -Local Open Scope nat_scope. +Require Import PeanoNat. -Implicit Types m n p : nat. +Local Open Scope nat_scope. (** * Irreflexivity *) -Theorem lt_irrefl : forall n, ~ n < n. -Proof le_Sn_n. +Notation lt_irrefl := Nat.lt_irrefl (compat "8.4"). (* ~ x < x *) + Hint Resolve lt_irrefl: arith v62. (** * Relationship between [le] and [lt] *) -Theorem lt_le_S : forall n m, n < m -> S n <= m. +Theorem lt_le_S n m : n < m -> S n <= m. Proof. - auto with arith. + apply Nat.le_succ_l. Qed. -Hint Immediate lt_le_S: arith v62. -Theorem lt_n_Sm_le : forall n m, n < S m -> n <= m. +Theorem lt_n_Sm_le n m : n < S m -> n <= m. Proof. - auto with arith. + apply Nat.lt_succ_r. Qed. -Hint Immediate lt_n_Sm_le: arith v62. -Theorem le_lt_n_Sm : forall n m, n <= m -> n < S m. +Theorem le_lt_n_Sm n m : n <= m -> n < S m. Proof. - auto with arith. + apply Nat.lt_succ_r. Qed. + +Hint Immediate lt_le_S: arith v62. +Hint Immediate lt_n_Sm_le: arith v62. Hint Immediate le_lt_n_Sm: arith v62. -Theorem le_not_lt : forall n m, n <= m -> ~ m < n. +Theorem le_not_lt n m : n <= m -> ~ m < n. Proof. - induction 1; auto with arith. + apply Nat.le_ngt. Qed. -Theorem lt_not_le : forall n m, n < m -> ~ m <= n. +Theorem lt_not_le n m : n < m -> ~ m <= n. Proof. - red; intros n m Lt Le; exact (le_not_lt m n Le Lt). + apply Nat.lt_nge. Qed. + Hint Immediate le_not_lt lt_not_le: arith v62. (** * Asymmetry *) -Theorem lt_asym : forall n m, n < m -> ~ m < n. -Proof. - induction 1; auto with arith. -Qed. +Notation lt_asym := Nat.lt_asymm (compat "8.4"). (* n<m -> ~m<n *) -(** * Order and successor *) +(** * Order and 0 *) -Theorem lt_n_Sn : forall n, n < S n. -Proof. - auto with arith. -Qed. -Hint Resolve lt_n_Sn: arith v62. +Notation lt_0_Sn := Nat.lt_0_succ (compat "8.4"). (* 0 < S n *) +Notation lt_n_0 := Nat.nlt_0_r (compat "8.4"). (* ~ n < 0 *) -Theorem lt_S : forall n m, n < m -> n < S m. +Theorem neq_0_lt n : 0 <> n -> 0 < n. Proof. - auto with arith. + intros. now apply Nat.neq_0_lt_0, Nat.neq_sym. Qed. -Hint Resolve lt_S: arith v62. -Theorem lt_n_S : forall n m, n < m -> S n < S m. +Theorem lt_0_neq n : 0 < n -> 0 <> n. Proof. - auto with arith. + intros. now apply Nat.neq_sym, Nat.neq_0_lt_0. Qed. -Hint Resolve lt_n_S: arith v62. -Theorem lt_S_n : forall n m, S n < S m -> n < m. +Hint Resolve lt_0_Sn lt_n_0 : arith v62. +Hint Immediate neq_0_lt lt_0_neq: arith v62. + +(** * Order and successor *) + +Notation lt_n_Sn := Nat.lt_succ_diag_r (compat "8.4"). (* n < S n *) +Notation lt_S := Nat.lt_lt_succ_r (compat "8.4"). (* n < m -> n < S m *) + +Theorem lt_n_S n m : n < m -> S n < S m. Proof. - auto with arith. + apply Nat.succ_lt_mono. Qed. -Hint Immediate lt_S_n: arith v62. -Theorem lt_0_Sn : forall n, 0 < S n. +Theorem lt_S_n n m : S n < S m -> n < m. Proof. - auto with arith. + apply Nat.succ_lt_mono. Qed. -Hint Resolve lt_0_Sn: arith v62. -Theorem lt_n_0 : forall n, ~ n < 0. -Proof le_Sn_0. -Hint Resolve lt_n_0: arith v62. +Hint Resolve lt_n_Sn lt_S lt_n_S : arith v62. +Hint Immediate lt_S_n : arith v62. (** * Predecessor *) -Lemma S_pred : forall n m, m < n -> n = S (pred n). +Lemma S_pred n m : m < n -> n = S (pred n). Proof. -induction 1; auto with arith. + intros. symmetry. now apply Nat.lt_succ_pred with m. Qed. -Lemma lt_pred : forall n m, S n < m -> n < pred m. +Lemma lt_pred n m : S n < m -> n < pred m. Proof. -induction 1; simpl; auto with arith. + apply Nat.lt_succ_lt_pred. Qed. -Hint Immediate lt_pred: arith v62. -Lemma lt_pred_n_n : forall n, 0 < n -> pred n < n. -destruct 1; simpl; auto with arith. +Lemma lt_pred_n_n n : 0 < n -> pred n < n. +Proof. + intros. now apply Nat.lt_pred_l, Nat.neq_0_lt_0. Qed. + +Hint Immediate lt_pred: arith v62. Hint Resolve lt_pred_n_n: arith v62. (** * Transitivity properties *) -Theorem lt_trans : forall n m p, n < m -> m < p -> n < p. -Proof. - induction 2; auto with arith. -Qed. - -Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p. -Proof. - induction 2; auto with arith. -Qed. - -Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p. -Proof. - induction 2; auto with arith. -Qed. +Notation lt_trans := Nat.lt_trans (compat "8.4"). +Notation lt_le_trans := Nat.lt_le_trans (compat "8.4"). +Notation le_lt_trans := Nat.le_lt_trans (compat "8.4"). Hint Resolve lt_trans lt_le_trans le_lt_trans: arith v62. (** * Large = strict or equal *) -Theorem le_lt_or_eq : forall n m, n <= m -> n < m \/ n = m. -Proof. - induction 1; auto with arith. -Qed. +Notation le_lt_or_eq_iff := Nat.lt_eq_cases (compat "8.4"). -Theorem le_lt_or_eq_iff : forall n m, n <= m <-> n < m \/ n = m. +Theorem le_lt_or_eq n m : n <= m -> n < m \/ n = m. Proof. - split. - intros; apply le_lt_or_eq; auto. - destruct 1; subst; auto with arith. + apply Nat.lt_eq_cases. Qed. -Theorem lt_le_weak : forall n m, n < m -> n <= m. -Proof. - auto with arith. -Qed. +Notation lt_le_weak := Nat.lt_le_incl (compat "8.4"). + Hint Immediate lt_le_weak: arith v62. (** * Dichotomy *) -Theorem le_or_lt : forall n m, n <= m \/ m < n. -Proof. - intros n m; pattern n, m; apply nat_double_ind; auto with arith. - induction 1; auto with arith. -Qed. - -Theorem nat_total_order : forall n m, n <> m -> n < m \/ m < n. -Proof. - intros m n diff. - elim (le_or_lt n m); [ intro H'0 | auto with arith ]. - elim (le_lt_or_eq n m); auto with arith. - intro H'; elim diff; auto with arith. -Qed. - -(** * Comparison to 0 *) +Notation le_or_lt := Nat.le_gt_cases (compat "8.4"). (* n <= m \/ m < n *) -Theorem neq_0_lt : forall n, 0 <> n -> 0 < n. +Theorem nat_total_order n m : n <> m -> n < m \/ m < n. Proof. - induction n; auto with arith. - intros; absurd (0 = 0); trivial with arith. + apply Nat.lt_gt_cases. Qed. -Hint Immediate neq_0_lt: arith v62. - -Theorem lt_0_neq : forall n, 0 < n -> 0 <> n. -Proof. - induction 1; auto with arith. -Qed. -Hint Immediate lt_0_neq: arith v62. (* begin hide *) Notation lt_O_Sn := lt_0_Sn (only parsing). @@ -192,3 +156,7 @@ Notation neq_O_lt := neq_0_lt (only parsing). Notation lt_O_neq := lt_0_neq (only parsing). Notation lt_n_O := lt_n_0 (only parsing). (* end hide *) + +(** For compatibility, we "Require" the same files as before *) + +Require Import Le. diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index 5623564a2..d38ed7e4e 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -6,14 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *) +(** THIS FILE IS DEPRECATED. Use [PeanoNat.Nat] instead. *) -Require Import NPeano. +Require Import PeanoNat. Local Open Scope nat_scope. Implicit Types m n p : nat. -Notation max := Peano.max (only parsing). +Notation max := Nat.max (only parsing). Definition max_0_l := Nat.max_0_l. Definition max_0_r := Nat.max_0_r. diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index a2a7930df..115901792 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -6,14 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *) +(** THIS FILE IS DEPRECATED. Use [PeanoNat.Nat] instead. *) -Require Import NPeano. +Require Import PeanoNat. Local Open Scope nat_scope. Implicit Types m n p : nat. -Notation min := Peano.min (only parsing). +Notation min := Nat.min (only parsing). Definition min_0_l := Nat.min_0_l. Definition min_0_r := Nat.min_0_r. diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index 480243311..cb6cc646f 100644 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -6,151 +6,114 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as: +(** Properties of subtraction between natural numbers. + + This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead. + + [minus] is now an alias for [Nat.sub], which is defined in [Init/Nat.v] as: << -Fixpoint minus (n m:nat) : nat := +Fixpoint sub (n m:nat) : nat := match n, m with - | O, _ => n - | S k, O => S k | S k, S l => k - l + | _, _ => n end -where "n - m" := (minus n m) : nat_scope. +where "n - m" := (sub n m) : nat_scope. >> *) -Require Import Lt. -Require Import Le. +Require Import PeanoNat Lt Le. Local Open Scope nat_scope. -Implicit Types m n p : nat. - (** * 0 is right neutral *) -Lemma minus_n_O : forall n, n = n - 0. +Lemma minus_n_O n : n = n - 0. Proof. - induction n; simpl; auto with arith. + symmetry. apply Nat.sub_0_r. Qed. -Hint Resolve minus_n_O: arith v62. (** * Permutation with successor *) -Lemma minus_Sn_m : forall n m, m <= n -> S (n - m) = S n - m. +Lemma minus_Sn_m n m : m <= n -> S (n - m) = S n - m. Proof. - intros n m Le; pattern m, n; apply le_elim_rel; simpl; - auto with arith. + intros. symmetry. now apply Nat.sub_succ_l. Qed. -Hint Resolve minus_Sn_m: arith v62. -Theorem pred_of_minus : forall n, pred n = n - 1. +Theorem pred_of_minus n : pred n = n - 1. Proof. - intro x; induction x; simpl; auto with arith. + symmetry. apply Nat.sub_1_r. Qed. (** * Diagonal *) -Lemma minus_diag : forall n, n - n = 0. -Proof. - induction n; simpl; auto with arith. -Qed. +Notation minus_diag := Nat.sub_diag (compat "8.4"). (* n - n = 0 *) -Lemma minus_diag_reverse : forall n, 0 = n - n. +Lemma minus_diag_reverse n : 0 = n - n. Proof. - auto using minus_diag. + symmetry. apply Nat.sub_diag. Qed. -Hint Resolve minus_diag_reverse: arith v62. Notation minus_n_n := minus_diag_reverse. (** * Simplification *) -Lemma minus_plus_simpl_l_reverse : forall n m p, n - m = p + n - (p + m). +Lemma minus_plus_simpl_l_reverse n m p : n - m = p + n - (p + m). Proof. - induction p; simpl; auto with arith. + now rewrite Nat.sub_add_distr, Nat.add_comm, Nat.add_sub. Qed. -Hint Resolve minus_plus_simpl_l_reverse: arith v62. (** * Relation with plus *) -Lemma plus_minus : forall n m p, n = m + p -> p = n - m. +Lemma plus_minus n m p : n = m + p -> p = n - m. Proof. - intros n m p; pattern m, n; apply nat_double_ind; simpl; - intros. - replace (n0 - 0) with n0; auto with arith. - absurd (0 = S (n0 + p)); auto with arith. - auto with arith. + symmetry. now apply Nat.add_sub_eq_l. Qed. -Hint Immediate plus_minus: arith v62. -Lemma minus_plus : forall n m, n + m - n = m. - symmetry ; auto with arith. +Lemma minus_plus n m : n + m - n = m. +Proof. + rewrite Nat.add_comm. apply Nat.add_sub. Qed. -Hint Resolve minus_plus: arith v62. -Lemma le_plus_minus : forall n m, n <= m -> m = n + (m - n). +Lemma le_plus_minus_r n m : n <= m -> n + (m - n) = m. Proof. - intros n m Le; pattern n, m; apply le_elim_rel; simpl; - auto with arith. + rewrite Nat.add_comm. apply Nat.sub_add. Qed. -Hint Resolve le_plus_minus: arith v62. -Lemma le_plus_minus_r : forall n m, n <= m -> n + (m - n) = m. +Lemma le_plus_minus n m : n <= m -> m = n + (m - n). Proof. - symmetry ; auto with arith. + intros. symmetry. rewrite Nat.add_comm. now apply Nat.sub_add. Qed. -Hint Resolve le_plus_minus_r: arith v62. (** * Relation with order *) -Theorem minus_le_compat_r : forall n m p : nat, n <= m -> n - p <= m - p. -Proof. - intros n m p; generalize n m; clear n m; induction p as [|p HI]. - intros n m; rewrite <- (minus_n_O n); rewrite <- (minus_n_O m); trivial. - - intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); auto with arith. - intros q r H _. simpl. auto using HI. -Qed. - -Theorem minus_le_compat_l : forall n m p : nat, n <= m -> p - m <= p - n. -Proof. - intros n m p; generalize n m; clear n m; induction p as [|p HI]. - trivial. +Notation minus_le_compat_r := + Nat.sub_le_mono_r (compat "8.4"). (* n <= m -> n - p <= m - p. *) - intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); trivial. - intros q; destruct q; auto with arith. - simpl. - apply le_trans with (m := p - 0); [apply HI | rewrite <- minus_n_O]; - auto with arith. +Notation minus_le_compat_l := + Nat.sub_le_mono_l (compat "8.4"). (* n <= m -> p - m <= p - n. *) - intros q r Hqr _. simpl. auto using HI. -Qed. +Notation le_minus := Nat.le_sub_l (compat "8.4"). (* n - m <= n *) +Notation lt_minus := Nat.sub_lt (compat "8.4"). (* m <= n -> 0 < m -> n-m < n *) -Corollary le_minus : forall n m, n - m <= n. +Lemma lt_O_minus_lt n m : 0 < n - m -> m < n. Proof. - intros n m; rewrite minus_n_O; auto using minus_le_compat_l with arith. + apply Nat.lt_add_lt_sub_r. Qed. -Lemma lt_minus : forall n m, m <= n -> 0 < m -> n - m < n. +Theorem not_le_minus_0 n m : ~ m <= n -> n - m = 0. Proof. - intros n m Le; pattern m, n; apply le_elim_rel; simpl; - auto using le_minus with arith. - intros; absurd (0 < 0); auto with arith. + intros. now apply Nat.sub_0_le, Nat.lt_le_incl, Nat.lt_nge. Qed. -Hint Resolve lt_minus: arith v62. -Lemma lt_O_minus_lt : forall n m, 0 < n - m -> m < n. -Proof. - intros n m; pattern n, m; apply nat_double_ind; simpl; - auto with arith. - intros; absurd (0 < 0); trivial with arith. -Qed. -Hint Immediate lt_O_minus_lt: arith v62. +(** * Hints *) -Theorem not_le_minus_0 : forall n m, ~ m <= n -> n - m = 0. -Proof. - intros y x; pattern y, x; apply nat_double_ind; - [ simpl; trivial with arith - | intros n H; absurd (0 <= S n); [ assumption | apply le_O_n ] - | simpl; intros n m H1 H2; apply H1; unfold not; intros H3; - apply H2; apply le_n_S; assumption ]. -Qed. +Hint Resolve minus_n_O: arith v62. +Hint Resolve minus_Sn_m: arith v62. +Hint Resolve minus_diag_reverse: arith v62. +Hint Resolve minus_plus_simpl_l_reverse: arith v62. +Hint Immediate plus_minus: arith v62. +Hint Resolve minus_plus: arith v62. +Hint Resolve le_plus_minus: arith v62. +Hint Resolve le_plus_minus_r: arith v62. +Hint Resolve lt_minus: arith v62. +Hint Immediate lt_O_minus_lt: arith v62. diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index cbb9b376b..d53a1646a 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -6,215 +6,139 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Export Plus. -Require Export Minus. -Require Export Lt. -Require Export Le. +(** * Properties of multiplication. -Local Open Scope nat_scope. + This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead. + + [Nat.mul] is defined in [Init/Nat.v]. +*) -Implicit Types m n p : nat. +Require Import PeanoNat. +(** For Compatibility: *) +Require Export Plus Minus Le Lt. -(** Theorems about multiplication in [nat]. [mult] is defined in module [Init/Peano.v]. *) +Local Open Scope nat_scope. (** * [nat] is a semi-ring *) (** ** Zero property *) -Lemma mult_0_r : forall n, n * 0 = 0. -Proof. - intro; symmetry ; apply mult_n_O. -Qed. - -Lemma mult_0_l : forall n, 0 * n = 0. -Proof. - reflexivity. -Qed. +Notation mult_0_l := Nat.mul_0_l (compat "8.4"). (* 0 * n = 0 *) +Notation mult_0_r := Nat.mul_0_r (compat "8.4"). (* n * 0 = 0 *) (** ** 1 is neutral *) -Lemma mult_1_l : forall n, 1 * n = n. -Proof. - simpl; auto with arith. -Qed. -Hint Resolve mult_1_l: arith v62. +Notation mult_1_l := Nat.mul_1_l (compat "8.4"). (* 1 * n = n *) +Notation mult_1_r := Nat.mul_1_r (compat "8.4"). (* n * 1 = n *) -Lemma mult_1_r : forall n, n * 1 = n. -Proof. - induction n; [ trivial | - simpl; rewrite IHn; reflexivity]. -Qed. -Hint Resolve mult_1_r: arith v62. +Hint Resolve mult_1_l mult_1_r: arith v62. (** ** Commutativity *) -Lemma mult_comm : forall n m, n * m = m * n. -Proof. -intros; induction n; simpl; auto with arith. -rewrite <- mult_n_Sm. -rewrite IHn; apply plus_comm. -Qed. +Notation mult_comm := Nat.mul_comm (compat "8.4"). (* n * m = m * n *) + Hint Resolve mult_comm: arith v62. (** ** Distributivity *) -Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p. -Proof. - intros; induction n; simpl; auto with arith. - rewrite <- plus_assoc, IHn; auto with arith. -Qed. -Hint Resolve mult_plus_distr_r: arith v62. +Notation mult_plus_distr_r := + Nat.mul_add_distr_r (compat "8.4"). (* (n+m)*p = n*p + m*p *) -Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p. -Proof. - induction n. trivial. - intros. simpl. rewrite IHn. symmetry. apply plus_permute_2_in_4. -Qed. +Notation mult_plus_distr_l := + Nat.mul_add_distr_l (compat "8.4"). (* n*(m+p) = n*m + n*p *) -Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p. -Proof. - intros; induction n, m using nat_double_ind; simpl; auto with arith. - rewrite <- minus_plus_simpl_l_reverse; auto with arith. -Qed. -Hint Resolve mult_minus_distr_r: arith v62. +Notation mult_minus_distr_r := + Nat.mul_sub_distr_r (compat "8.4"). (* (n-m)*p = n*p - m*p *) -Lemma mult_minus_distr_l : forall n m p, n * (m - p) = n * m - n * p. -Proof. - intros n m p. - rewrite mult_comm, mult_minus_distr_r, (mult_comm m n), (mult_comm p n); reflexivity. -Qed. +Notation mult_minus_distr_l := + Nat.mul_sub_distr_l (compat "8.4"). (* n*(m-p) = n*m - n*p *) + +Hint Resolve mult_plus_distr_r: arith v62. +Hint Resolve mult_minus_distr_r: arith v62. Hint Resolve mult_minus_distr_l: arith v62. (** ** Associativity *) -Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p). -Proof. - intros; induction n; simpl; auto with arith. - rewrite mult_plus_distr_r. - induction IHn; auto with arith. -Qed. -Hint Resolve mult_assoc_reverse: arith v62. +Notation mult_assoc := Nat.mul_assoc (compat "8.4"). (* n*(m*p)=n*m*p *) -Lemma mult_assoc : forall n m p, n * (m * p) = n * m * p. +Lemma mult_assoc_reverse n m p : n * m * p = n * (m * p). Proof. - auto with arith. + symmetry. apply Nat.mul_assoc. Qed. + +Hint Resolve mult_assoc_reverse: arith v62. Hint Resolve mult_assoc: arith v62. (** ** Inversion lemmas *) -Lemma mult_is_O : forall n m, n * m = 0 -> n = 0 \/ m = 0. +Lemma mult_is_O n m : n * m = 0 -> n = 0 \/ m = 0. Proof. - destruct n as [| n]; simpl; intros m H. - left; trivial. - right; apply plus_is_O in H; destruct H; trivial. + apply Nat.eq_mul_0. Qed. -Lemma mult_is_one : forall n m, n * m = 1 -> n = 1 /\ m = 1. +Lemma mult_is_one n m : n * m = 1 -> n = 1 /\ m = 1. Proof. - destruct n as [|n]; simpl; intros m H. - edestruct O_S; eauto. - destruct plus_is_one with (1:=H) as [[-> Hnm] | [-> Hnm]]. - simpl in H; rewrite mult_0_r in H; elim (O_S _ H). - rewrite mult_1_r in Hnm; auto. + apply Nat.eq_mul_1. Qed. (** ** Multiplication and successor *) -Lemma mult_succ_l : forall n m:nat, S n * m = n * m + m. -Proof. - intros; simpl. rewrite plus_comm. reflexivity. -Qed. - -Lemma mult_succ_r : forall n m:nat, n * S m = n * m + n. -Proof. - induction n as [| p H]; intro m; simpl. - reflexivity. - rewrite H, <- plus_n_Sm; apply f_equal; rewrite plus_assoc; reflexivity. -Qed. +Notation mult_succ_l := Nat.mul_succ_l (compat "8.4"). (* S n * m = n * m + m *) +Notation mult_succ_r := Nat.mul_succ_r (compat "8.4"). (* n * S m = n * m + n *) (** * Compatibility with orders *) -Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n. +Lemma mult_O_le n m : m = 0 \/ n <= m * n. Proof. - induction m; simpl; auto with arith. + destruct m; [left|right]; simpl; trivial using Nat.le_add_r. Qed. Hint Resolve mult_O_le: arith v62. -Lemma mult_le_compat_l : forall n m p, n <= m -> p * n <= p * m. +Lemma mult_le_compat_l n m p : n <= m -> p * n <= p * m. Proof. - induction p as [| p IHp]; intros; simpl. - apply le_n. - auto using plus_le_compat. + apply Nat.mul_le_mono_nonneg_l, Nat.le_0_l. (* TODO : get rid of 0<=n hyp *) Qed. Hint Resolve mult_le_compat_l: arith. - -Lemma mult_le_compat_r : forall n m p, n <= m -> n * p <= m * p. +Lemma mult_le_compat_r n m p : n <= m -> n * p <= m * p. Proof. - intros m n p H; rewrite mult_comm, (mult_comm n); auto with arith. + apply Nat.mul_le_mono_nonneg_r, Nat.le_0_l. Qed. -Lemma mult_le_compat : - forall n m p (q:nat), n <= m -> p <= q -> n * p <= m * q. +Lemma mult_le_compat n m p q : n <= m -> p <= q -> n * p <= m * q. Proof. - intros m n p q Hmn Hpq; induction Hmn. - induction Hpq. - (* m*p<=m*p *) - apply le_n. - (* m*p<=m*m0 -> m*p<=m*(S m0) *) - rewrite <- mult_n_Sm; apply le_trans with (m * m0). - assumption. - apply le_plus_l. - (* m*p<=m0*q -> m*p<=(S m0)*q *) - simpl; apply le_trans with (m0 * q). - assumption. - apply le_plus_r. + intros. apply Nat.mul_le_mono_nonneg; trivial; apply Nat.le_0_l. Qed. -Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p. +Lemma mult_S_lt_compat_l n m p : m < p -> S n * m < S n * p. Proof. - induction n; intros; simpl in *. - rewrite <- 2 plus_n_O; assumption. - auto using plus_lt_compat. + apply Nat.mul_lt_mono_pos_l, Nat.lt_0_succ. Qed. Hint Resolve mult_S_lt_compat_l: arith. -Lemma mult_lt_compat_l : forall n m p, n < m -> 0 < p -> p * n < p * m. +Lemma mult_lt_compat_l n m p : n < m -> 0 < p -> p * n < p * m. Proof. - intros m n p H Hp. destruct p. elim (lt_irrefl _ Hp). - now apply mult_S_lt_compat_l. + intros. now apply Nat.mul_lt_mono_pos_l. Qed. -Lemma mult_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p. +Lemma mult_lt_compat_r n m p : n < m -> 0 < p -> n * p < m * p. Proof. - intros m n p H Hp. destruct p. elim (lt_irrefl _ Hp). - rewrite (mult_comm m), (mult_comm n). now apply mult_S_lt_compat_l. + intros. now apply Nat.mul_lt_mono_pos_r. Qed. -Lemma mult_S_le_reg_l : forall n m p, S n * m <= S n * p -> m <= p. +Lemma mult_S_le_reg_l n m p : S n * m <= S n * p -> m <= p. Proof. - intros m n p H; destruct (le_or_lt n p). trivial. - assert (H1:S m * n < S m * n). - apply le_lt_trans with (m := S m * p). assumption. - apply mult_S_lt_compat_l. assumption. - elim (lt_irrefl _ H1). + apply Nat.mul_le_mono_pos_l, Nat.lt_0_succ. Qed. (** * n|->2*n and n|->2n+1 have disjoint image *) -Theorem odd_even_lem : forall p q, 2 * p + 1 <> 2 * q. +Theorem odd_even_lem p q : 2 * p + 1 <> 2 * q. Proof. - induction p; destruct q. - discriminate. - simpl; rewrite plus_comm. discriminate. - discriminate. - intro H0; destruct (IHp q). - replace (2 * q) with (2 * S q - 2). - rewrite <- H0; simpl. - repeat rewrite (fun x y => plus_comm x (S y)); simpl; auto. - simpl; rewrite (fun y => plus_comm q (S y)); destruct q; simpl; auto. + intro. apply (Nat.Even_Odd_False (2*q)). + - now exists q. + - now exists p. Qed. @@ -232,10 +156,9 @@ Fixpoint mult_acc (s:nat) m n : nat := Lemma mult_acc_aux : forall n m p, m + n * p = mult_acc m p n. Proof. - induction n as [| p IHp]; simpl; auto. - intros s m; rewrite <- plus_tail_plus; rewrite <- IHp. - rewrite <- plus_assoc_reverse; apply f_equal2; auto. - rewrite plus_comm; auto. + induction n as [| n IHn]; simpl; auto. + intros. rewrite Nat.add_assoc, IHn. f_equal. + rewrite Nat.add_comm. apply plus_tail_plus. Qed. Definition tail_mult n m := mult_acc 0 m n. diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v new file mode 100644 index 000000000..3657d9544 --- /dev/null +++ b/theories/Arith/PeanoNat.v @@ -0,0 +1,755 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +Require Import NAxioms NProperties OrdersFacts. + +(** Implementation of [NAxiomsSig] by [nat] *) + +Module Nat + <: NAxiomsSig + <: UsualDecidableTypeFull + <: OrderedTypeFull + <: TotalOrder. + +(** Operations over [nat] are defined in a separate module *) + +Include Coq.Init.Nat. + +(** When including property functors, inline t eq zero one two lt le succ *) + +Set Inline Level 50. + +(** All operations are well-defined (trivial here since eq is Leibniz) *) + +Definition eq_equiv : Equivalence (@eq nat) := eq_equivalence. +Local Obligation Tactic := simpl_relation. +Program Instance succ_wd : Proper (eq==>eq) S. +Program Instance pred_wd : Proper (eq==>eq) pred. +Program Instance add_wd : Proper (eq==>eq==>eq) plus. +Program Instance sub_wd : Proper (eq==>eq==>eq) minus. +Program Instance mul_wd : Proper (eq==>eq==>eq) mult. +Program Instance pow_wd : Proper (eq==>eq==>eq) pow. +Program Instance div_wd : Proper (eq==>eq==>eq) div. +Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. +Program Instance lt_wd : Proper (eq==>eq==>iff) lt. +Program Instance testbit_wd : Proper (eq==>eq==>eq) testbit. + +(** Bi-directional induction. *) + +Theorem bi_induction : + forall A : nat -> Prop, Proper (eq==>iff) A -> + A 0 -> (forall n : nat, A n <-> A (S n)) -> forall n : nat, A n. +Proof. +intros A A_wd A0 AS. apply nat_ind. assumption. intros; now apply -> AS. +Qed. + +(** Recursion fonction *) + +Definition recursion {A} : A -> (nat -> A -> A) -> nat -> A := + nat_rect (fun _ => A). + +Instance recursion_wd {A} (Aeq : relation A) : + Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) recursion. +Proof. +intros a a' Ha f f' Hf n n' Hn. subst n'. +induction n; simpl; auto. apply Hf; auto. +Qed. + +Theorem recursion_0 : + forall {A} (a : A) (f : nat -> A -> A), recursion a f 0 = a. +Proof. +reflexivity. +Qed. + +Theorem recursion_succ : + forall {A} (Aeq : relation A) (a : A) (f : nat -> A -> A), + Aeq a a -> Proper (eq==>Aeq==>Aeq) f -> + forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)). +Proof. +unfold Proper, respectful in *; induction n; simpl; auto. +Qed. + +(** ** Remaining constants not defined in Coq.Init.Nat *) + +(** NB: Aliasing [le] is mandatory, since only a Definition can implement + an interface Parameter... *) + +Definition eq := @Logic.eq nat. +Definition le := Peano.le. +Definition lt := Peano.lt. + +(** ** Basic specifications : pred add sub mul *) + +Lemma pred_succ n : pred (S n) = n. +Proof. +reflexivity. +Qed. + +Lemma pred_0 : pred 0 = 0. +Proof. +reflexivity. +Qed. + +Lemma one_succ : 1 = S 0. +Proof. +reflexivity. +Qed. + +Lemma two_succ : 2 = S 1. +Proof. +reflexivity. +Qed. + +Lemma add_0_l n : 0 + n = n. +Proof. +reflexivity. +Qed. + +Lemma add_succ_l n m : (S n) + m = S (n + m). +Proof. +reflexivity. +Qed. + +Lemma sub_0_r n : n - 0 = n. +Proof. +now destruct n. +Qed. + +Lemma sub_succ_r n m : n - (S m) = pred (n - m). +Proof. +revert m. induction n; destruct m; simpl; auto. apply sub_0_r. +Qed. + +Lemma mul_0_l n : 0 * n = 0. +Proof. +reflexivity. +Qed. + +Lemma mul_succ_l n m : S n * m = n * m + m. +Proof. +assert (succ_r : forall x y, x+S y = S(x+y)) by now induction x. +assert (comm : forall x y, x+y = y+x). +{ induction x; simpl; auto. intros; rewrite succ_r; now f_equal. } +now rewrite comm. +Qed. + +Lemma lt_succ_r n m : n < S m <-> n <= m. +Proof. +split. apply Peano.le_S_n. induction 1; auto. +Qed. + +(** ** Boolean comparisons *) + +Lemma eqb_eq n m : eqb n m = true <-> n = m. +Proof. + revert m. + induction n; destruct m; simpl; rewrite ?IHn; split; try easy. + - now intros ->. + - now injection 1. +Qed. + +Lemma leb_le n m : (n <=? m) = true <-> n <= m. +Proof. + revert m. + induction n; destruct m; simpl. + - now split. + - split; trivial. intros; apply Peano.le_0_n. + - now split. + - rewrite IHn; split. + + apply Peano.le_n_S. + + apply Peano.le_S_n. +Qed. + +Lemma ltb_lt n m : (n <? m) = true <-> n < m. +Proof. + apply leb_le. +Qed. + +(** ** Decidability of equality over [nat]. *) + +Lemma eq_dec : forall n m : nat, {n = m} + {n <> m}. +Proof. + induction n; destruct m. + - now left. + - now right. + - now right. + - destruct (IHn m); [left|right]; auto. +Defined. + +(** ** Ternary comparison *) + +(** With [nat], it would be easier to prove first [compare_spec], + then the properties below. But then we wouldn't be able to + benefit from functor [BoolOrderFacts] *) + +Lemma compare_eq_iff n m : (n ?= m) = Eq <-> n = m. +Proof. + revert m; induction n; destruct m; simpl; rewrite ?IHn; split; auto; easy. +Qed. + +Lemma compare_lt_iff n m : (n ?= m) = Lt <-> n < m. +Proof. + revert m; induction n; destruct m; simpl; rewrite ?IHn; split; try easy. + - intros _. apply Peano.le_n_S, Peano.le_0_n. + - apply Peano.le_n_S. + - apply Peano.le_S_n. +Qed. + +Lemma compare_le_iff n m : (n ?= m) <> Gt <-> n <= m. +Proof. + revert m; induction n; destruct m; simpl; rewrite ?IHn. + - now split. + - split; intros. apply Peano.le_0_n. easy. + - split. now destruct 1. inversion 1. + - split; intros. now apply Peano.le_n_S. now apply Peano.le_S_n. +Qed. + +Lemma compare_antisym n m : (m ?= n) = CompOpp (n ?= m). +Proof. + revert m; induction n; destruct m; simpl; trivial. +Qed. + +Lemma compare_succ n m : (S n ?= S m) = (n ?= m). +Proof. + reflexivity. +Qed. + + +(* BUG: Ajout d'un cas * après preuve finie (deuxième niveau +++*** ) : + * ---> Anomaly: Uncaught exception Proofview.IndexOutOfRange(_). Please report. *) + +(** ** Minimum, maximum *) + +Lemma max_l : forall n m, m <= n -> max n m = n. +Proof. + exact Peano.max_l. +Qed. + +Lemma max_r : forall n m, n <= m -> max n m = m. +Proof. + exact Peano.max_r. +Qed. + +Lemma min_l : forall n m, n <= m -> min n m = n. +Proof. + exact Peano.min_l. +Qed. + +Lemma min_r : forall n m, m <= n -> min n m = m. +Proof. + exact Peano.min_r. +Qed. + +(** Some more advanced properties of comparison and orders, + including [compare_spec] and [lt_irrefl] and [lt_eq_cases]. *) + +Include BoolOrderFacts. + +(** We can now derive all properties of basic functions and orders, + and use these properties for proving the specs of more advanced + functions. *) + +Include NBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. + +(** ** Power *) + +Lemma pow_neg_r a b : b<0 -> a^b = 0. inversion 1. Qed. + +Lemma pow_0_r a : a^0 = 1. +Proof. reflexivity. Qed. + +Lemma pow_succ_r a b : 0<=b -> a^(S b) = a * a^b. +Proof. reflexivity. Qed. + +(** ** Square *) + +Lemma square_spec n : square n = n * n. +Proof. reflexivity. Qed. + +(** ** Parity *) + +Definition Even n := exists m, n = 2*m. +Definition Odd n := exists m, n = 2*m+1. + +Module Private_Parity. + +Lemma Even_1 : ~ Even 1. +Proof. + intros ([|], H); try discriminate. + simpl in H. now rewrite <- plus_n_Sm in H. +Qed. + +Lemma Even_2 n : Even n <-> Even (S (S n)). +Proof. + split; intros (m,H). + - exists (S m). rewrite H. simpl. now rewrite plus_n_Sm. + - destruct m; try discriminate. + exists m. simpl in H. rewrite <- plus_n_Sm in H. now inversion H. +Qed. + +Lemma Odd_0 : ~ Odd 0. +Proof. + now intros ([|], H). +Qed. + +Lemma Odd_2 n : Odd n <-> Odd (S (S n)). +Proof. + split; intros (m,H). + - exists (S m). rewrite H. simpl. now rewrite <- (plus_n_Sm m). + - destruct m; try discriminate. + exists m. simpl in H. rewrite <- plus_n_Sm in H. inversion H. + simpl. now rewrite <- !plus_n_Sm, <- !plus_n_O. +Qed. + +End Private_Parity. +Import Private_Parity. + +Lemma even_spec : forall n, even n = true <-> Even n. +Proof. + fix 1. + destruct n as [|[|n]]; simpl. + - split; [ now exists 0 | trivial ]. + - split; [ discriminate | intro H; elim (Even_1 H) ]. + - rewrite even_spec. apply Even_2. +Qed. + +Lemma odd_spec : forall n, odd n = true <-> Odd n. +Proof. + unfold odd. + fix 1. + destruct n as [|[|n]]; simpl. + - split; [ discriminate | intro H; elim (Odd_0 H) ]. + - split; [ now exists 0 | trivial ]. + - rewrite odd_spec. apply Odd_2. +Qed. + +(** ** Division *) + +Lemma divmod_spec : forall x y q u, u <= y -> + let (q',u') := divmod x y q u in + x + (S y)*q + (y-u) = (S y)*q' + (y-u') /\ u' <= y. +Proof. + induction x. + - simpl; intuition. + - intros y q u H. destruct u; simpl divmod. + + generalize (IHx y (S q) y (le_n y)). destruct divmod as (q',u'). + intros (EQ,LE); split; trivial. + rewrite <- EQ, sub_0_r, sub_diag, add_0_r. + now rewrite !add_succ_l, <- add_succ_r, <- add_assoc, mul_succ_r. + + assert (H' : u <= y). + { apply le_trans with (S u); trivial. do 2 constructor. } + generalize (IHx y q u H'). destruct divmod as (q',u'). + intros (EQ,LE); split; trivial. + rewrite <- EQ. + rewrite !add_succ_l, <- add_succ_r. f_equal. now rewrite <- sub_succ_l. +Qed. + +Lemma div_mod x y : y<>0 -> x = y*(x/y) + x mod y. +Proof. + intros Hy. + destruct y; [ now elim Hy | clear Hy ]. + unfold div, modulo. + generalize (divmod_spec x y 0 y (le_n y)). + destruct divmod as (q,u). + intros (U,V). + simpl in *. + now rewrite mul_0_r, sub_diag, !add_0_r in U. +Qed. + +Lemma mod_bound_pos x y : 0<=x -> 0<y -> 0 <= x mod y < y. +Proof. + intros Hx Hy. split. apply le_0_l. + destruct y; [ now elim Hy | clear Hy ]. + unfold modulo. + apply lt_succ_r, le_sub_l. +Qed. + +(** ** Square root *) + +Lemma sqrt_iter_spec : forall k p q r, + q = p+p -> r<=q -> + let s := sqrt_iter k p q r in + s*s <= k + p*p + (q - r) < (S s)*(S s). +Proof. + induction k. + - (* k = 0 *) + simpl; intros p q r Hq Hr. + split. + + apply le_add_r. + + apply lt_succ_r. + rewrite mul_succ_r. + rewrite add_assoc, (add_comm p), <- add_assoc. + apply add_le_mono_l. + rewrite <- Hq. apply le_sub_l. + - (* k = S k' *) + destruct r. + + (* r = 0 *) + intros Hq _. + replace (S k + p*p + (q-0)) with (k + (S p)*(S p) + (S (S q) - S (S q))). + * apply IHk. + simpl. now rewrite add_succ_r, Hq. apply le_n. + * rewrite sub_diag, sub_0_r, add_0_r. simpl. + rewrite add_succ_r; f_equal. rewrite <- add_assoc; f_equal. + rewrite mul_succ_r, (add_comm p), <- add_assoc. now f_equal. + + (* r = S r' *) + intros Hq Hr. + replace (S k + p*p + (q-S r)) with (k + p*p + (q - r)). + * apply IHk; trivial. apply le_trans with (S r); trivial. do 2 constructor. + * simpl. rewrite <- add_succ_r. f_equal. rewrite <- sub_succ_l; trivial. +Qed. + +Lemma sqrt_specif n : (sqrt n)*(sqrt n) <= n < S (sqrt n) * S (sqrt n). +Proof. + set (s:=sqrt n). + replace n with (n + 0*0 + (0-0)). + apply sqrt_iter_spec; auto. + simpl. now rewrite !add_0_r. +Qed. + +Definition sqrt_spec a (Ha:0<=a) := sqrt_specif a. + +Lemma sqrt_neg a : a<0 -> sqrt a = 0. +Proof. inversion 1. Qed. + +(** ** Logarithm *) + +Lemma log2_iter_spec : forall k p q r, + 2^(S p) = q + S r -> r < 2^p -> + let s := log2_iter k p q r in + 2^s <= k + q < 2^(S s). +Proof. + induction k. + - (* k = 0 *) + intros p q r EQ LT. simpl log2_iter. cbv zeta. + split. + + rewrite add_0_l. + rewrite (add_le_mono_l _ _ (2^p)). + simpl pow in EQ. rewrite add_0_r in EQ. rewrite EQ. + rewrite add_comm. apply add_le_mono_r. apply LT. + + rewrite EQ, add_comm. apply add_lt_mono_l. + apply lt_succ_r, le_0_l. + - (* k = S k' *) + intros p q r EQ LT. destruct r. + + (* r = 0 *) + rewrite add_succ_r, add_0_r in EQ. + rewrite add_succ_l, <- add_succ_r. apply IHk. + * rewrite <- EQ. remember (S p) as p'; simpl. now rewrite add_0_r. + * rewrite EQ. constructor. + + (* r = S r' *) + rewrite add_succ_l, <- add_succ_r. apply IHk. + * now rewrite add_succ_l, <- add_succ_r. + * apply le_lt_trans with (S r); trivial. do 2 constructor. +Qed. + +Lemma log2_spec n : 0<n -> + 2^(log2 n) <= n < 2^(S (log2 n)). +Proof. + intros. + set (s:=log2 n). + replace n with (pred n + 1). + apply log2_iter_spec; auto. + rewrite add_1_r. + apply succ_pred. now apply neq_sym, lt_neq. +Qed. + +Lemma log2_nonpos n : n<=0 -> log2 n = 0. +Proof. + inversion 1; now subst. +Qed. + +(** ** Gcd *) + +Definition divide x y := exists z, y=z*x. +Notation "( x | y )" := (divide x y) (at level 0) : nat_scope. + +Lemma gcd_divide : forall a b, (gcd a b | a) /\ (gcd a b | b). +Proof. + fix 1. + intros [|a] b; simpl. + split. + now exists 0. + exists 1. simpl. now rewrite <- plus_n_O. + fold (b mod (S a)). + destruct (gcd_divide (b mod (S a)) (S a)) as (H,H'). + set (a':=S a) in *. + split; auto. + rewrite (div_mod b a') at 2 by discriminate. + destruct H as (u,Hu), H' as (v,Hv). + rewrite mul_comm. + exists ((b/a')*v + u). + rewrite mul_add_distr_r. + now rewrite <- mul_assoc, <- Hv, <- Hu. +Qed. + +Lemma gcd_divide_l : forall a b, (gcd a b | a). +Proof. + intros. apply gcd_divide. +Qed. + +Lemma gcd_divide_r : forall a b, (gcd a b | b). +Proof. + intros. apply gcd_divide. +Qed. + +Lemma gcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|gcd a b). +Proof. + fix 1. + intros [|a] b; simpl; auto. + fold (b mod (S a)). + intros c H H'. apply gcd_greatest; auto. + set (a':=S a) in *. + rewrite (div_mod b a') in H' by discriminate. + destruct H as (u,Hu), H' as (v,Hv). + exists (v - (b/a')*u). + rewrite mul_comm in Hv. + rewrite mul_sub_distr_r, <- Hv, <- mul_assoc, <-Hu. + now rewrite add_comm, add_sub. +Qed. + +Lemma gcd_nonneg a b : 0<=gcd a b. +Proof. apply le_0_l. Qed. + + +(** ** Bitwise operations *) + +Lemma div2_double n : div2 (2*n) = n. +Proof. + induction n; trivial. + simpl mul. rewrite add_succ_r. simpl. now f_equal. +Qed. + +Lemma div2_succ_double n : div2 (S (2*n)) = n. +Proof. + induction n; trivial. + simpl. f_equal. now rewrite add_succ_r. +Qed. + +Lemma le_div2 n : div2 (S n) <= n. +Proof. + revert n. + fix 1. + destruct n; simpl; trivial. apply lt_succ_r. + destruct n; [simpl|]; trivial. now constructor. +Qed. + +Lemma lt_div2 n : 0 < n -> div2 n < n. +Proof. + destruct n. + - inversion 1. + - intros _. apply lt_succ_r, le_div2. +Qed. + +Lemma div2_decr a n : a <= S n -> div2 a <= n. +Proof. + destruct a; intros H. + - simpl. apply le_0_l. + - apply succ_le_mono in H. + apply le_trans with a; [ apply le_div2 | trivial ]. +Qed. + +Lemma double_twice : forall n, double n = 2*n. +Proof. + simpl; intros. now rewrite add_0_r. +Qed. + +Lemma testbit_0_l : forall n, testbit 0 n = false. +Proof. + now induction n. +Qed. + +Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true. +Proof. + unfold testbit. rewrite odd_spec. now exists a. +Qed. + +Lemma testbit_even_0 a : testbit (2*a) 0 = false. +Proof. + unfold testbit, odd. rewrite (proj2 (even_spec _)); trivial. + now exists a. +Qed. + +Lemma testbit_odd_succ' a n : testbit (2*a+1) (S n) = testbit a n. +Proof. + unfold testbit; fold testbit. + rewrite add_1_r. f_equal. + apply div2_succ_double. +Qed. + +Lemma testbit_even_succ' a n : testbit (2*a) (S n) = testbit a n. +Proof. + unfold testbit; fold testbit. f_equal. apply div2_double. +Qed. + +Lemma shiftr_specif : forall a n m, + testbit (shiftr a n) m = testbit a (m+n). +Proof. + induction n; intros m. trivial. + now rewrite add_0_r. + now rewrite add_succ_r, <- add_succ_l, <- IHn. +Qed. + +Lemma shiftl_specif_high : forall a n m, n<=m -> + testbit (shiftl a n) m = testbit a (m-n). +Proof. + induction n; intros m H. trivial. + now rewrite sub_0_r. + destruct m. inversion H. + simpl. apply succ_le_mono in H. + change (shiftl a (S n)) with (double (shiftl a n)). + rewrite double_twice, div2_double. now apply IHn. +Qed. + +Lemma shiftl_spec_low : forall a n m, m<n -> + testbit (shiftl a n) m = false. +Proof. + induction n; intros m H. inversion H. + change (shiftl a (S n)) with (double (shiftl a n)). + destruct m; simpl. + unfold odd. apply negb_false_iff. + apply even_spec. exists (shiftl a n). apply double_twice. + rewrite double_twice, div2_double. apply IHn. + now apply succ_le_mono. +Qed. + +Lemma div2_bitwise : forall op n a b, + div2 (bitwise op (S n) a b) = bitwise op n (div2 a) (div2 b). +Proof. + intros. unfold bitwise; fold bitwise. + destruct (op (odd a) (odd b)). + now rewrite div2_succ_double. + now rewrite add_0_l, div2_double. +Qed. + +Lemma odd_bitwise : forall op n a b, + odd (bitwise op (S n) a b) = op (odd a) (odd b). +Proof. + intros. unfold bitwise; fold bitwise. + destruct (op (odd a) (odd b)). + apply odd_spec. rewrite add_comm. eexists; eauto. + unfold odd. apply negb_false_iff. apply even_spec. + rewrite add_0_l; eexists; eauto. +Qed. + +Lemma testbit_bitwise_1 : forall op, (forall b, op false b = false) -> + forall n m a b, a<=n -> + testbit (bitwise op n a b) m = op (testbit a m) (testbit b m). +Proof. + intros op Hop. + induction n; intros m a b Ha. + simpl. inversion Ha; subst. now rewrite testbit_0_l. + destruct m. + apply odd_bitwise. + unfold testbit; fold testbit. rewrite div2_bitwise. + apply IHn. now apply div2_decr. +Qed. + +Lemma testbit_bitwise_2 : forall op, op false false = false -> + forall n m a b, a<=n -> b<=n -> + testbit (bitwise op n a b) m = op (testbit a m) (testbit b m). +Proof. + intros op Hop. + induction n; intros m a b Ha Hb. + simpl. inversion Ha; inversion Hb; subst. now rewrite testbit_0_l. + destruct m. + apply odd_bitwise. + unfold testbit; fold testbit. rewrite div2_bitwise. + apply IHn; now apply div2_decr. +Qed. + +Lemma land_spec a b n : + testbit (land a b) n = testbit a n && testbit b n. +Proof. + unfold land. apply testbit_bitwise_1; trivial. +Qed. + +Lemma ldiff_spec a b n : + testbit (ldiff a b) n = testbit a n && negb (testbit b n). +Proof. + unfold ldiff. apply testbit_bitwise_1; trivial. +Qed. + +Lemma lor_spec a b n : + testbit (lor a b) n = testbit a n || testbit b n. +Proof. + unfold lor. apply testbit_bitwise_2. + - trivial. + - destruct (compare_spec a b). + + rewrite max_l; subst; trivial. + + apply lt_le_incl in H. now rewrite max_r. + + apply lt_le_incl in H. now rewrite max_l. + - destruct (compare_spec a b). + + rewrite max_r; subst; trivial. + + apply lt_le_incl in H. now rewrite max_r. + + apply lt_le_incl in H. now rewrite max_l. +Qed. + +Lemma lxor_spec a b n : + testbit (lxor a b) n = xorb (testbit a n) (testbit b n). +Proof. + unfold lxor. apply testbit_bitwise_2. + - trivial. + - destruct (compare_spec a b). + + rewrite max_l; subst; trivial. + + apply lt_le_incl in H. now rewrite max_r. + + apply lt_le_incl in H. now rewrite max_l. + - destruct (compare_spec a b). + + rewrite max_r; subst; trivial. + + apply lt_le_incl in H. now rewrite max_r. + + apply lt_le_incl in H. now rewrite max_l. +Qed. + +Lemma div2_spec a : div2 a = shiftr a 1. +Proof. + reflexivity. +Qed. + +(** Aliases with extra dummy hypothesis, to fulfil the interface *) + +Definition testbit_odd_succ a n (_:0<=n) := testbit_odd_succ' a n. +Definition testbit_even_succ a n (_:0<=n) := testbit_even_succ' a n. +Lemma testbit_neg_r a n (H:n<0) : testbit a n = false. +Proof. inversion H. Qed. + +Definition shiftl_spec_high a n m (_:0<=m) := shiftl_specif_high a n m. +Definition shiftr_spec a n m (_:0<=m) := shiftr_specif a n m. + +(** Properties of advanced functions (pow, sqrt, log2, ...) *) + +Include NExtraProp. + +End Nat. + +(** Re-export notations that should be available even when + the [Nat] module is not imported. *) + +Bind Scope nat_scope with Nat.t nat. + +Infix "^" := Nat.pow : nat_scope. +Infix "=?" := Nat.eqb (at level 70) : nat_scope. +Infix "<=?" := Nat.leb (at level 70) : nat_scope. +Infix "<?" := Nat.ltb (at level 70) : nat_scope. +Infix "?=" := Nat.compare (at level 70) : nat_scope. +Infix "/" := Nat.div : nat_scope. +Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope. + +Hint Unfold Nat.le : core. +Hint Unfold Nat.lt : core. + +(** [Nat] contains an [order] tactic for natural numbers *) + +(** Note that [Nat.order] is domain-agnostic: it will not prove + [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *) + +Section TestOrder. + Let test : forall x y, x<=y -> y<=x -> x=y. + Proof. + Nat.order. + Qed. +End TestOrder. diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 9b8ebfe55..72edc6eef 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -6,47 +6,61 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Decidable. +Require Import Decidable PeanoNat. Require Eqdep_dec. -Require Import Le Lt. Local Open Scope nat_scope. Implicit Types m n x y : nat. -Theorem O_or_S : forall n, {m : nat | S m = n} + {0 = n}. +Theorem O_or_S n : {m : nat | S m = n} + {0 = n}. Proof. induction n. - auto. - left; exists n; auto. + - now right. + - left; exists n; auto. Defined. -Theorem eq_nat_dec : forall n m, {n = m} + {n <> m}. -Proof. - induction n; destruct m; auto. - elim (IHn m); auto. -Defined. +Notation eq_nat_dec := Nat.eq_dec (compat "8.4"). Hint Resolve O_or_S eq_nat_dec: arith. -Theorem dec_eq_nat : forall n m, decidable (n = m). - intros x y; unfold decidable; elim (eq_nat_dec x y); auto with arith. +Theorem dec_eq_nat n m : decidable (n = m). +Proof. + elim (Nat.eq_dec n m); [left|right]; trivial. Defined. -Definition UIP_nat:= Eqdep_dec.UIP_dec eq_nat_dec. +Definition UIP_nat:= Eqdep_dec.UIP_dec Nat.eq_dec. + +Import EqNotations. Lemma le_unique: forall m n (h1 h2: m <= n), h1 = h2. Proof. fix 3. -refine (fun m _ h1 => match h1 as h' in _ <= k return forall hh: m <= k, h' = hh - with le_n _ => _ |le_S _ i H => _ end). -refine (fun hh => match hh as h' in _ <= k return forall eq: m = k, - le_n m = match eq in _ = p return m <= p -> m <= m with |eq_refl => fun bli => bli end h' with - |le_n _ => fun eq => _ |le_S _ j H' => fun eq => _ end eq_refl). -rewrite (UIP_nat _ _ eq eq_refl). reflexivity. -subst m. destruct (Lt.lt_irrefl j H'). -refine (fun hh => match hh as h' in _ <= k return match k as k' return m <= k' -> Prop - with |0 => fun _ => True |S i' => fun h'' => forall H':m <= i', le_S m i' H' = h'' end h' - with |le_n _ => _ |le_S _ j H2 => fun H' => _ end H). -destruct m. exact I. intros; destruct (Lt.lt_irrefl m H'). -f_equal. apply le_unique. +destruct h1 as [ | i h1 ]; intros h2. +- set (Return k (le:m<=k) := + forall (eq:m=k), + le_n m = (rew eq in fun (le':m<=m) => le') le). + refine + (match h2 as h2' return (Return _ h2') with + | le_n _ => fun eq => _ + | le_S _ j h2 => fun eq => _ + end eq_refl). + + rewrite (UIP_nat _ _ eq eq_refl). simpl. reflexivity. + + exfalso. revert h2. rewrite eq. apply Nat.lt_irrefl. +- set (Return k (le:m<=k) := + match k as k' return (m <= k' -> Prop) with + | 0 => fun _ => True + | S i' => fun (le':m<=S i') => forall (H':m<=i'), le_S _ _ H' = le' + end le). + refine + (match h2 as h2' return (Return _ h2') with + | le_n _ => _ + | le_S _ j h2 => fun h1' => _ + end h1). + + unfold Return; clear. destruct m; simpl. + * exact I. + * intros h1'. destruct (Nat.lt_irrefl _ h1'). + + f_equal. apply le_unique. Qed. + +(** For compatibility *) +Require Import Le Lt. diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index 5428ada32..3b823da6f 100644 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -6,176 +6,139 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Properties of addition. [add] is defined in [Init/Peano.v] as: +(** Properties of addition. + + This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead. + + [Nat.add] is defined in [Init/Nat.v] as: << -Fixpoint plus (n m:nat) : nat := +Fixpoint add (n m:nat) : nat := match n with | O => m | S p => S (p + m) end -where "n + m" := (plus n m) : nat_scope. +where "n + m" := (add n m) : nat_scope. >> - *) +*) -Require Import Le. -Require Import Lt. +Require Import PeanoNat. Local Open Scope nat_scope. -Implicit Types m n p q : nat. - -(** * Zero is neutral -Deprecated : Already in Init/Peano.v *) -Notation plus_0_l := plus_O_n (only parsing). -Definition plus_0_r n := eq_sym (plus_n_O n). - -(** * Commutativity *) - -Lemma plus_comm : forall n m, n + m = m + n. -Proof. - intros n m; elim n; simpl; auto with arith. - intros y H; elim (plus_n_Sm m y); auto with arith. -Qed. -Hint Immediate plus_comm: arith v62. - -(** * Associativity *) +(** * Neutrality of 0, commutativity, associativity *) -Definition plus_Snm_nSm : forall n m, S n + m = n + S m:= - plus_n_Sm. +Notation plus_0_l := Nat.add_0_l (compat "8.4"). +Notation plus_0_r := Nat.add_0_r (compat "8.4"). +Notation plus_comm := Nat.add_comm (compat "8.4"). +Notation plus_assoc := Nat.add_assoc (compat "8.4"). -Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p. -Proof. - intros n m p; elim n; simpl; auto with arith. -Qed. -Hint Resolve plus_assoc: arith v62. +Notation plus_permute := Nat.add_shuffle3 (compat "8.4"). -Lemma plus_permute : forall n m p, n + (m + p) = m + (n + p). -Proof. - intros; rewrite (plus_assoc m n p); rewrite (plus_comm m n); auto with arith. -Qed. +Definition plus_Snm_nSm : forall n m, S n + m = n + S m := + Peano.plus_n_Sm. -Lemma plus_assoc_reverse : forall n m p, n + m + p = n + (m + p). +Lemma plus_assoc_reverse n m p : n + m + p = n + (m + p). Proof. - auto with arith. + symmetry. apply Nat.add_assoc. Qed. -Hint Resolve plus_assoc_reverse: arith v62. (** * Simplification *) -Lemma plus_reg_l : forall n m p, p + n = p + m -> n = m. +Lemma plus_reg_l n m p : p + n = p + m -> n = m. Proof. - intros m p n; induction n; simpl; auto with arith. + apply Nat.add_cancel_l. Qed. -Lemma plus_le_reg_l : forall n m p, p + n <= p + m -> n <= m. +Lemma plus_le_reg_l n m p : p + n <= p + m -> n <= m. Proof. - induction p; simpl; auto with arith. + apply Nat.add_le_mono_l. Qed. -Lemma plus_lt_reg_l : forall n m p, p + n < p + m -> n < m. +Lemma plus_lt_reg_l n m p : p + n < p + m -> n < m. Proof. - induction p; simpl; auto with arith. + apply Nat.add_lt_mono_l. Qed. (** * Compatibility with order *) -Lemma plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m. +Lemma plus_le_compat_l n m p : n <= m -> p + n <= p + m. Proof. - induction p; simpl; auto with arith. + apply Nat.add_le_mono_l. Qed. -Hint Resolve plus_le_compat_l: arith v62. -Lemma plus_le_compat_r : forall n m p, n <= m -> n + p <= m + p. +Lemma plus_le_compat_r n m p : n <= m -> n + p <= m + p. Proof. - induction 1; simpl; auto with arith. + apply Nat.add_le_mono_r. Qed. -Hint Resolve plus_le_compat_r: arith v62. -Lemma le_plus_l : forall n m, n <= n + m. +Lemma plus_lt_compat_l n m p : n < m -> p + n < p + m. Proof. - induction n; simpl; auto with arith. + apply Nat.add_lt_mono_l. Qed. -Hint Resolve le_plus_l: arith v62. -Lemma le_plus_r : forall n m, m <= n + m. +Lemma plus_lt_compat_r n m p : n < m -> n + p < m + p. Proof. - intros n m; elim n; simpl; auto with arith. + apply Nat.add_lt_mono_r. Qed. -Hint Resolve le_plus_r: arith v62. -Theorem le_plus_trans : forall n m p, n <= m -> n <= m + p. +Lemma plus_le_compat n m p q : n <= m -> p <= q -> n + p <= m + q. Proof. - intros; apply le_trans with (m := m); auto with arith. + apply Nat.add_le_mono. Qed. -Hint Resolve le_plus_trans: arith v62. -Theorem lt_plus_trans : forall n m p, n < m -> n < m + p. +Lemma plus_le_lt_compat n m p q : n <= m -> p < q -> n + p < m + q. Proof. - intros; apply lt_le_trans with (m := m); auto with arith. + apply Nat.add_le_lt_mono. Qed. -Hint Immediate lt_plus_trans: arith v62. -Lemma plus_lt_compat_l : forall n m p, n < m -> p + n < p + m. +Lemma plus_lt_le_compat n m p q : n < m -> p <= q -> n + p < m + q. Proof. - induction p; simpl; auto with arith. + apply Nat.add_lt_le_mono. Qed. -Hint Resolve plus_lt_compat_l: arith v62. -Lemma plus_lt_compat_r : forall n m p, n < m -> n + p < m + p. +Lemma plus_lt_compat n m p q : n < m -> p < q -> n + p < m + q. Proof. - intros n m p H; rewrite (plus_comm n p); rewrite (plus_comm m p). - elim p; auto with arith. + apply Nat.add_lt_mono. Qed. -Hint Resolve plus_lt_compat_r: arith v62. -Lemma plus_le_compat : forall n m p q, n <= m -> p <= q -> n + p <= m + q. +Lemma le_plus_l n m : n <= n + m. Proof. - intros n m p q H H0. - elim H; simpl; auto with arith. + apply Nat.le_add_r. Qed. -Lemma plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q. +Lemma le_plus_r n m : m <= n + m. Proof. - unfold lt. intros. change (S n + p <= m + q). rewrite plus_Snm_nSm. - apply plus_le_compat; assumption. + rewrite Nat.add_comm. apply Nat.le_add_r. Qed. -Lemma plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q. +Theorem le_plus_trans n m p : n <= m -> n <= m + p. Proof. - unfold lt. intros. change (S n + p <= m + q). apply plus_le_compat; assumption. + intros. now rewrite <- Nat.le_add_r. Qed. -Lemma plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q. +Theorem lt_plus_trans n m p : n < m -> n < m + p. Proof. - intros. apply plus_lt_le_compat. assumption. - apply lt_le_weak. assumption. + intros. apply Nat.lt_le_trans with m. trivial. apply Nat.le_add_r. Qed. (** * Inversion lemmas *) -Lemma plus_is_O : forall n m, n + m = 0 -> n = 0 /\ m = 0. +Lemma plus_is_O n m : n + m = 0 -> n = 0 /\ m = 0. Proof. - intro m; destruct m as [| n]; auto. - intros. discriminate H. + destruct n; now split. Qed. -Definition plus_is_one : - forall m n, m + n = 1 -> {m = 0 /\ n = 1} + {m = 1 /\ n = 0}. +Definition plus_is_one m n : + m + n = 1 -> {m = 0 /\ n = 1} + {m = 1 /\ n = 0}. Proof. - intro m; destruct m as [| n]; auto. - destruct n; auto. - intros. - simpl in H. discriminate H. + destruct m as [| m]; auto. + destruct m; auto. + discriminate. Defined. (** * Derived properties *) -Lemma plus_permute_2_in_4 : forall n m p q, n + m + (p + q) = n + p + (m + q). -Proof. - intros m n p q. - rewrite <- (plus_assoc m n (p + q)). rewrite (plus_assoc n p q). - rewrite (plus_comm n p). rewrite <- (plus_assoc p n q). apply plus_assoc. -Qed. +Notation plus_permute_2_in_4 := Nat.add_shuffle1 (compat "8.4"). (** * Tail-recursive plus *) @@ -190,31 +153,37 @@ Fixpoint tail_plus n m : nat := end. Lemma plus_tail_plus : forall n m, n + m = tail_plus n m. +Proof. induction n as [| n IHn]; simpl; auto. intro m; rewrite <- IHn; simpl; auto. Qed. (** * Discrimination *) -Lemma succ_plus_discr : forall n m, n <> S (plus m n). +Lemma succ_plus_discr n m : n <> S (m+n). Proof. - intros n m; induction n as [|n IHn]. - discriminate. - intro H; apply IHn; apply eq_add_S; rewrite H; rewrite <- plus_n_Sm; - reflexivity. + apply Nat.succ_add_discr. Qed. -Lemma n_SSn : forall n, n <> S (S n). -Proof. - intro n; exact (succ_plus_discr n 1). -Qed. +Lemma n_SSn n : n <> S (S n). +Proof (succ_plus_discr n 1). -Lemma n_SSSn : forall n, n <> S (S (S n)). -Proof. - intro n; exact (succ_plus_discr n 2). -Qed. +Lemma n_SSSn n : n <> S (S (S n)). +Proof (succ_plus_discr n 2). -Lemma n_SSSSn : forall n, n <> S (S (S (S n))). -Proof. - intro n; exact (succ_plus_discr n 3). -Qed. +Lemma n_SSSSn n : n <> S (S (S (S n))). +Proof (succ_plus_discr n 3). + + +(** * Compatibility Hints *) + +Hint Immediate plus_comm : arith v62. +Hint Resolve plus_assoc plus_assoc_reverse : arith v62. +Hint Resolve plus_le_compat_l plus_le_compat_r : arith v62. +Hint Resolve le_plus_l le_plus_r le_plus_trans : arith v62. +Hint Immediate lt_plus_trans : arith v62. +Hint Resolve plus_lt_compat_l plus_lt_compat_r : arith v62. + +(** For compatibility, we "Require" the same files as before *) + +Require Import Le Lt. diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 05be5e1a3..2cb7c3c09 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -8,7 +8,7 @@ (** Well-founded relations and natural numbers *) -Require Import Lt. +Require Import PeanoNat Lt. Local Open Scope nat_scope. @@ -24,16 +24,12 @@ Definition gtof (a b:A) := f b > f a. Theorem well_founded_ltof : well_founded ltof. Proof. - red. - cut (forall n (a:A), f a < n -> Acc ltof a). - intros H a; apply (H (S (f a))); auto with arith. - induction n. - intros; absurd (f a < 0); auto with arith. - intros a ltSma. - apply Acc_intro. - unfold ltof; intros b ltfafb. - apply IHn. - apply lt_le_trans with (f a); auto with arith. + assert (H : forall n (a:A), f a < n -> Acc ltof a). + { induction n. + - intros; absurd (f a < 0); auto with arith. + - intros a Ha. apply Acc_intro. unfold ltof at 1. intros b Hb. + apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. } + intros a. apply (H (S (f a))). auto with arith. Defined. Theorem well_founded_gtof : well_founded gtof. @@ -67,15 +63,13 @@ Theorem induction_ltof1 : forall P:A -> Set, (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a. Proof. - intros P F; cut (forall n (a:A), f a < n -> P a). - intros H a; apply (H (S (f a))); auto with arith. - induction n. - intros; absurd (f a < 0); auto with arith. - intros a ltSma. - apply F. - unfold ltof; intros b ltfafb. - apply IHn. - apply lt_le_trans with (f a); auto with arith. + intros P F. + assert (H : forall n (a:A), f a < n -> P a). + { induction n. + - intros; absurd (f a < 0); auto with arith. + - intros a Ha. apply F. unfold ltof. intros b Hb. + apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. } + intros a. apply (H (S (f a))). auto with arith. Defined. Theorem induction_gtof1 : @@ -108,16 +102,12 @@ Hypothesis H_compat : forall x y:A, R x y -> f x < f y. Theorem well_founded_lt_compat : well_founded R. Proof. - red. - cut (forall n (a:A), f a < n -> Acc R a). - intros H a; apply (H (S (f a))); auto with arith. - induction n. - intros; absurd (f a < 0); auto with arith. - intros a ltSma. - apply Acc_intro. - intros b ltfafb. - apply IHn. - apply lt_le_trans with (f a); auto with arith. + assert (H : forall n (a:A), f a < n -> Acc R a). + { induction n. + - intros; absurd (f a < 0); auto with arith. + - intros a Ha. apply Acc_intro. intros b Hb. + apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. } + intros a. apply (H (S (f a))). auto with arith. Defined. End Well_founded_Nat. @@ -208,6 +198,7 @@ End LT_WF_REL. Lemma well_founded_inv_rel_inv_lt_rel : forall (A:Set) (F:A -> nat -> Prop), well_founded (inv_lt_rel A F). +Proof. intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial. Qed. @@ -230,30 +221,18 @@ Proof. intros P Pdec (n0,HPn0). assert (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'') - \/(forall n', P n' -> n<=n')). - induction n. - right. - intros n' Hn'. - apply le_O_n. - destruct IHn. - left; destruct H as (n', (Hlt', HPn')). - exists n'; split. - apply lt_S; assumption. - assumption. - destruct (Pdec n). - left; exists n; split. - apply lt_n_Sn. - split; assumption. - right. - intros n' Hltn'. - destruct (le_lt_eq_dec n n') as [Hltn|Heqn]. - apply H; assumption. - assumption. - destruct H0. - rewrite Heqn; assumption. - destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0]; - repeat split; - assumption || intros n' (HPn',Hminn'); apply le_antisym; auto. + \/ (forall n', P n' -> n<=n')). + { induction n. + - right. intros. apply Nat.le_0_l. + - destruct IHn as [(n' & IH1 & IH2)|IH]. + + left. exists n'; auto with arith. + + destruct (Pdec n) as [HP|HP]. + * left. exists n; auto with arith. + * right. intros n' Hn'. + apply Nat.le_neq; split; auto. intros <-. auto. } + destruct (H n0) as [(n & H1 & H2 & H3)|H0]; [exists n | exists n0]; + repeat split; trivial; + intros n' (HPn',Hn'); apply Nat.le_antisymm; auto. Qed. Unset Implicit Arguments. diff --git a/theories/Arith/vo.itarget b/theories/Arith/vo.itarget index 0b6564e15..0b3d31e98 100644 --- a/theories/Arith/vo.itarget +++ b/theories/Arith/vo.itarget @@ -1,3 +1,4 @@ +PeanoNat.vo Arith_base.vo Arith.vo Between.vo |