diff options
Diffstat (limited to 'theories/NArith')
| -rw-r--r-- | theories/NArith/BinNat.v | 223 | ||||
| -rw-r--r-- | theories/NArith/BinNatDef.v | 4 | ||||
| -rw-r--r-- | theories/NArith/Ndigits.v | 99 | ||||
| -rw-r--r-- | theories/NArith/Nnat.v | 61 |
4 files changed, 170 insertions, 217 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 256dce782..a8b086e77 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -8,7 +8,7 @@ Require Export BinNums. Require Import BinPos RelationClasses Morphisms Setoid - Equalities OrdersFacts GenericMinMax Bool NAxioms NProperties. + Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties. Require BinNatDef. (**********************************************************************) @@ -66,6 +66,20 @@ Notation "( p | q )" := (divide p q) (at level 0) : N_scope. Definition Even n := exists m, n = 2*m. Definition Odd n := exists m, n = 2*m+1. +(** Proofs of morphisms, obvious since eq is Leibniz *) + +Local Obligation Tactic := simpl_relation. +Program Definition succ_wd : Proper (eq==>eq) succ := _. +Program Definition pred_wd : Proper (eq==>eq) pred := _. +Program Definition add_wd : Proper (eq==>eq==>eq) add := _. +Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _. +Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _. +Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _. +Program Definition div_wd : Proper (eq==>eq==>eq) div := _. +Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _. +Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _. +Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _. + (** Decidability of equality. *) Definition eq_dec : forall n m : N, { n = m } + { n <> m }. @@ -138,6 +152,50 @@ Proof. apply peano_rect_succ. Qed. +(** Generic induction / recursion *) + +Theorem bi_induction : + forall A : N -> Prop, Proper (Logic.eq==>iff) A -> + A 0 -> (forall n, A n <-> A (succ n)) -> forall n : N, A n. +Proof. +intros A A_wd A0 AS. apply peano_rect. assumption. intros; now apply -> AS. +Qed. + +Definition recursion {A} : A -> (N -> A -> A) -> N -> A := + peano_rect (fun _ => A). + +Instance recursion_wd {A} (Aeq : relation A) : + Proper (Aeq==>(Logic.eq==>Aeq==>Aeq)==>Logic.eq==>Aeq) recursion. +Proof. +intros a a' Ea f f' Ef x x' Ex. subst x'. +induction x using peano_ind. +trivial. +unfold recursion in *. rewrite 2 peano_rect_succ. now apply Ef. +Qed. + +Theorem recursion_0 {A} (a:A) (f:N->A->A) : recursion a f 0 = a. +Proof. reflexivity. Qed. + +Theorem recursion_succ {A} (Aeq : relation A) (a : A) (f : N -> A -> A): + Aeq a a -> Proper (Logic.eq==>Aeq==>Aeq) f -> + forall n : N, Aeq (recursion a f (succ n)) (f n (recursion a f n)). +Proof. +unfold recursion; intros a_wd f_wd n. induction n using peano_ind. +rewrite peano_rect_succ. now apply f_wd. +rewrite !peano_rect_succ in *. now apply f_wd. +Qed. + +(** Specification of constants *) + +Lemma one_succ : 1 = succ 0. +Proof. reflexivity. Qed. + +Lemma two_succ : 2 = succ 1. +Proof. reflexivity. Qed. + +Definition pred_0 : pred 0 = 0. +Proof. reflexivity. Qed. + (** Properties of mixed successor and predecessor. *) Lemma pos_pred_spec p : Pos.pred_N p = pred (pos p). @@ -262,69 +320,30 @@ Qed. Include BoolOrderFacts. -(** We regroup here some results used for proving the correctness - of more advanced functions. These results will also be provided - by the generic functor of properties about natural numbers - instantiated at the end of the file. *) - -Module Import Private_BootStrap. - -Theorem add_0_r n : n + 0 = n. -Proof. -now destruct n. -Qed. - -Theorem add_comm n m : n + m = m + n. -Proof. -destruct n, m; simpl; try reflexivity. simpl. f_equal. apply Pos.add_comm. -Qed. - -Theorem add_assoc n m p : n + (m + p) = n + m + p. -Proof. -destruct n; try reflexivity. -destruct m; try reflexivity. -destruct p; try reflexivity. -simpl. f_equal. apply Pos.add_assoc. -Qed. - -Lemma sub_add n m : n <= m -> m - n + n = m. -Proof. - destruct n as [|p], m as [|q]; simpl; try easy'. intros H. - case Pos.sub_mask_spec; intros; simpl; subst; trivial. - now rewrite Pos.add_comm. - apply Pos.le_nlt in H. elim H. apply Pos.lt_add_r. -Qed. +(** Specification of minimum and maximum *) -Theorem mul_comm n m : n * m = m * n. +Theorem min_l n m : n <= m -> min n m = n. Proof. -destruct n, m; simpl; trivial. f_equal. apply Pos.mul_comm. +unfold min, le. case compare; trivial. now destruct 1. Qed. -Lemma le_0_l n : 0<=n. +Theorem min_r n m : m <= n -> min n m = m. Proof. -now destruct n. +unfold min, le. rewrite compare_antisym. +case compare_spec; trivial. now destruct 2. Qed. -Lemma leb_spec n m : BoolSpec (n<=m) (m<n) (n <=? m). +Theorem max_l n m : m <= n -> max n m = n. Proof. - unfold le, lt, leb. rewrite (compare_antisym n m). - case compare; now constructor. +unfold max, le. rewrite compare_antisym. +case compare_spec; auto. now destruct 2. Qed. -Lemma add_lt_cancel_l n m p : p+n < p+m -> n<m. +Theorem max_r n m : n <= m -> max n m = m. Proof. - intro H. destruct p. simpl; auto. - destruct n; destruct m. - elim (Pos.lt_irrefl _ H). - red; auto. - rewrite add_0_r in H. simpl in H. - red in H. simpl in H. - elim (Pos.lt_not_add_l _ _ H). - now apply (Pos.add_lt_mono_l p). +unfold max, le. case compare; trivial. now destruct 1. Qed. -End Private_BootStrap. - (** Specification of lt and le. *) Lemma lt_succ_r n m : n < succ m <-> n<=m. @@ -334,6 +353,13 @@ split. now destruct p. now destruct 1. apply Pos.lt_succ_r. Qed. +(** 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. + + (** Properties of [double] and [succ_double] *) Lemma double_spec n : double n = 2 * n. @@ -395,30 +421,6 @@ Proof. Qed. -(** Specification of minimum and maximum *) - -Theorem min_l n m : n <= m -> min n m = n. -Proof. -unfold min, le. case compare; trivial. now destruct 1. -Qed. - -Theorem min_r n m : m <= n -> min n m = m. -Proof. -unfold min, le. rewrite compare_antisym. -case compare_spec; trivial. now destruct 2. -Qed. - -Theorem max_l n m : m <= n -> max n m = n. -Proof. -unfold max, le. rewrite compare_antisym. -case compare_spec; auto. now destruct 2. -Qed. - -Theorem max_r n m : n <= m -> max n m = m. -Proof. -unfold max, le. case compare; trivial. now destruct 1. -Qed. - (** 0 is the least natural number *) Theorem compare_0_r n : (n ?= 0) <> Lt. @@ -560,13 +562,13 @@ Proof. (* a~1 *) destruct pos_div_eucl as (q,r); simpl in *. case leb_spec; intros H; simpl; trivial. - apply add_lt_cancel_l with b. rewrite add_comm, sub_add by trivial. + apply add_lt_mono_l with b. rewrite add_comm, sub_add by trivial. destruct b as [|b]; [now destruct Hb| simpl; rewrite Pos.add_diag ]. apply (succ_double_lt _ _ IHa). (* a~0 *) destruct pos_div_eucl as (q,r); simpl in *. case leb_spec; intros H; simpl; trivial. - apply add_lt_cancel_l with b. rewrite add_comm, sub_add by trivial. + apply add_lt_mono_l with b. rewrite add_comm, sub_add by trivial. destruct b as [|b]; [now destruct Hb| simpl; rewrite Pos.add_diag ]. now destruct r. (* 1 *) @@ -754,7 +756,7 @@ Proof. destruct m. now destruct (shiftl a n). rewrite <- (succ_pos_pred p), testbit_succ_r_div2, div2_double by apply le_0_l. apply IHn. - apply add_lt_cancel_l with 1. rewrite 2 (add_succ_l 0). simpl. + apply add_lt_mono_l with 1. rewrite 2 (add_succ_l 0). simpl. now rewrite succ_pos_pred. Qed. @@ -833,69 +835,10 @@ Proof. apply pos_ldiff_spec. Qed. -(** Specification of constants *) - -Lemma one_succ : 1 = succ 0. -Proof. reflexivity. Qed. - -Lemma two_succ : 2 = succ 1. -Proof. reflexivity. Qed. - -Definition pred_0 : pred 0 = 0. -Proof. reflexivity. Qed. - -(** Proofs of morphisms, obvious since eq is Leibniz *) - -Local Obligation Tactic := simpl_relation. -Program Definition succ_wd : Proper (eq==>eq) succ := _. -Program Definition pred_wd : Proper (eq==>eq) pred := _. -Program Definition add_wd : Proper (eq==>eq==>eq) add := _. -Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _. -Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _. -Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _. -Program Definition div_wd : Proper (eq==>eq==>eq) div := _. -Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _. -Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _. -Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _. - -(** Generic induction / recursion *) - -Theorem bi_induction : - forall A : N -> Prop, Proper (Logic.eq==>iff) A -> - A 0 -> (forall n, A n <-> A (succ n)) -> forall n : N, A n. -Proof. -intros A A_wd A0 AS. apply peano_rect. assumption. intros; now apply -> AS. -Qed. - -Definition recursion {A} : A -> (N -> A -> A) -> N -> A := - peano_rect (fun _ => A). - -Instance recursion_wd {A} (Aeq : relation A) : - Proper (Aeq==>(Logic.eq==>Aeq==>Aeq)==>Logic.eq==>Aeq) recursion. -Proof. -intros a a' Ea f f' Ef x x' Ex. subst x'. -induction x using peano_ind. -trivial. -unfold recursion in *. rewrite 2 peano_rect_succ. now apply Ef. -Qed. - -Theorem recursion_0 {A} (a:A) (f:N->A->A) : recursion a f 0 = a. -Proof. reflexivity. Qed. - -Theorem recursion_succ {A} (Aeq : relation A) (a : A) (f : N -> A -> A): - Aeq a a -> Proper (Logic.eq==>Aeq==>Aeq) f -> - forall n : N, Aeq (recursion a f (succ n)) (f n (recursion a f n)). -Proof. -unfold recursion; intros a_wd f_wd n. induction n using peano_ind. -rewrite peano_rect_succ. now apply f_wd. -rewrite !peano_rect_succ in *. now apply f_wd. -Qed. - -(** Instantiation of generic properties of natural numbers *) +(** Instantiation of generic properties of advanced functions + (pow, sqrt, log2, div, gcd, ...) *) -Include NProp - <+ UsualMinMaxLogicalProperties - <+ UsualMinMaxDecProperties. +Include NExtraProp. (** In generic statements, the predicates [lt] and [le] have been favored, whereas [gt] and [ge] don't even exist in the abstract diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 6aeeccaf5..befcf7929 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -325,8 +325,8 @@ Definition lxor n m := (** Shifts *) -Definition shiftl_nat (a:N) := nat_rect _ a (fun _ => double). -Definition shiftr_nat (a:N) := nat_rect _ a (fun _ => div2). +Definition shiftl_nat (a:N)(n:nat) := Nat.iter n double a. +Definition shiftr_nat (a:N)(n:nat) := Nat.iter n div2 a. Definition shiftl a n := match a with diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 662c50abf..b36ea3204 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -6,8 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Bool Morphisms Setoid Bvector BinPos BinNat Wf_nat - Pnat Nnat Compare_dec Lt Minus. +Require Import Bool Morphisms Setoid Bvector BinPos BinNat PeanoNat Pnat Nnat. Local Open Scope N_scope. @@ -111,10 +110,12 @@ Lemma Nshiftl_nat_spec_high : forall a n m, (n<=m)%nat -> N.testbit_nat (N.shiftl_nat a n) m = N.testbit_nat a (m-n). Proof. induction n; intros m H. - now rewrite <- minus_n_O. - destruct m. inversion H. apply le_S_n in H. - simpl. rewrite <- IHn; trivial. - destruct (N.shiftl_nat a n) as [|[p|p|]]; simpl; trivial. + - now rewrite Nat.sub_0_r. + - destruct m. + + inversion H. + + apply le_S_n in H. + simpl. rewrite <- IHn; trivial. + destruct (N.shiftl_nat a n) as [|[p|p|]]; simpl; trivial. Qed. Lemma Nshiftl_nat_spec_low : forall a n m, (m<n)%nat -> @@ -123,9 +124,10 @@ Proof. induction n; intros m H. inversion H. rewrite Nshiftl_nat_S. destruct m. - destruct (N.shiftl_nat a n); trivial. - specialize (IHn m (lt_S_n _ _ H)). - destruct (N.shiftl_nat a n); trivial. + - destruct (N.shiftl_nat a n); trivial. + - apply Lt.lt_S_n in H. + specialize (IHn m H). + destruct (N.shiftl_nat a n); trivial. Qed. (** A left shift for positive numbers (used in BigN) *) @@ -446,49 +448,52 @@ Lemma Nless_trans : Nless a a' = true -> Nless a' a'' = true -> Nless a a'' = true. Proof. induction a as [|a IHa|a IHa] using N.binary_ind; intros a' a'' H H0. - case_eq (Nless N0 a'') ; intros Heqn. trivial. - rewrite (N0_less_2 a'' Heqn), (Nless_z a') in H0. discriminate H0. - induction a' as [|a' _|a' _] using N.binary_ind. - rewrite (Nless_z (N.double a)) in H. discriminate H. - rewrite (Nless_def_1 a a') in H. - induction a'' using N.binary_ind. - rewrite (Nless_z (N.double a')) in H0. discriminate H0. - rewrite (Nless_def_1 a' a'') in H0. rewrite (Nless_def_1 a a''). - exact (IHa _ _ H H0). - apply Nless_def_3. - induction a'' as [|a'' _|a'' _] using N.binary_ind. - rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0. - rewrite (Nless_def_4 a' a'') in H0. discriminate H0. - apply Nless_def_3. - induction a' as [|a' _|a' _] using N.binary_ind. - rewrite (Nless_z (N.succ_double a)) in H. discriminate H. - rewrite (Nless_def_4 a a') in H. discriminate H. + - case_eq (Nless N0 a'') ; intros Heqn. + + trivial. + + rewrite (N0_less_2 a'' Heqn), (Nless_z a') in H0. discriminate H0. + - induction a' as [|a' _|a' _] using N.binary_ind. + + rewrite (Nless_z (N.double a)) in H. discriminate H. + + rewrite (Nless_def_1 a a') in H. induction a'' using N.binary_ind. - rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0. - rewrite (Nless_def_4 a' a'') in H0. discriminate H0. - rewrite (Nless_def_2 a' a'') in H0. rewrite (Nless_def_2 a a') in H. - rewrite (Nless_def_2 a a''). exact (IHa _ _ H H0). + * rewrite (Nless_z (N.double a')) in H0. discriminate H0. + * rewrite (Nless_def_1 a' a'') in H0. rewrite (Nless_def_1 a a''). + exact (IHa _ _ H H0). + * apply Nless_def_3. + + induction a'' as [|a'' _|a'' _] using N.binary_ind. + * rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0. + * rewrite (Nless_def_4 a' a'') in H0. discriminate H0. + * apply Nless_def_3. + - induction a' as [|a' _|a' _] using N.binary_ind. + + rewrite (Nless_z (N.succ_double a)) in H. discriminate H. + + rewrite (Nless_def_4 a a') in H. discriminate H. + + induction a'' using N.binary_ind. + * rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0. + * rewrite (Nless_def_4 a' a'') in H0. discriminate H0. + * rewrite (Nless_def_2 a' a'') in H0. rewrite (Nless_def_2 a a') in H. + rewrite (Nless_def_2 a a''). exact (IHa _ _ H H0). Qed. Lemma Nless_total : forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}. Proof. induction a using N.binary_rec; intro a'. - case_eq (Nless N0 a') ; intros Heqb. left. left. auto. - right. rewrite (N0_less_2 a' Heqb). reflexivity. - induction a' as [|a' _|a' _] using N.binary_rec. - case_eq (Nless N0 (N.double a)) ; intros Heqb. left. right. auto. - right. exact (N0_less_2 _ Heqb). - rewrite 2!Nless_def_1. destruct (IHa a') as [ | ->]. - left. assumption. - right. reflexivity. - left. left. apply Nless_def_3. - induction a' as [|a' _|a' _] using N.binary_rec. - left. right. destruct a; reflexivity. - left. right. apply Nless_def_3. - rewrite 2!Nless_def_2. destruct (IHa a') as [ | ->]. - left. assumption. - right. reflexivity. + - case_eq (Nless N0 a') ; intros Heqb. + + left. left. auto. + + right. rewrite (N0_less_2 a' Heqb). reflexivity. + - induction a' as [|a' _|a' _] using N.binary_rec. + + case_eq (Nless N0 (N.double a)) ; intros Heqb. + * left. right. auto. + * right. exact (N0_less_2 _ Heqb). + + rewrite 2!Nless_def_1. destruct (IHa a') as [ | ->]. + * left. assumption. + * right. reflexivity. + + left. left. apply Nless_def_3. + - induction a' as [|a' _|a' _] using N.binary_rec. + + left. right. destruct a; reflexivity. + + left. right. apply Nless_def_3. + + rewrite 2!Nless_def_2. destruct (IHa a') as [ | ->]. + * left. assumption. + * right. reflexivity. Qed. (** Number of digits in a number *) @@ -622,7 +627,7 @@ induction bv; intros. inversion H. destruct p ; simpl. destruct (Bv2N n bv); destruct h; simpl in *; auto. - specialize IHbv with p (lt_S_n _ _ H). + specialize IHbv with p (Lt.lt_S_n _ _ H). simpl in * ; destruct (Bv2N n bv); destruct h; simpl in *; auto. Qed. @@ -641,7 +646,7 @@ Proof. destruct n as [|n]. inversion H. induction n ; destruct p ; unfold Vector.nth_order in *; simpl in * ; auto. -intros H ; destruct (lt_n_O _ (lt_S_n _ _ H)). +intros H ; destruct (Lt.lt_n_O _ (Lt.lt_S_n _ _ H)). Qed. (** Binary bitwise operations are the same in the two worlds. *) diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index cddc5f4cf..94242394b 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -6,8 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Minus Compare_dec Sumbool Div2 Min Max. -Require Import BinPos BinNat Pnat. +Require Import BinPos BinNat PeanoNat Pnat. (** * Conversions from [N] to [nat] *) @@ -68,52 +67,58 @@ Qed. Lemma inj_sub a a' : N.to_nat (a - a') = N.to_nat a - N.to_nat a'. Proof. - destruct a as [|a], a' as [|a']; simpl; auto with arith. + destruct a as [|a], a' as [|a']; simpl; rewrite ?Nat.sub_0_r; trivial. destruct (Pos.compare_spec a a'). - subst. now rewrite Pos.sub_mask_diag, <- minus_n_n. - rewrite Pos.sub_mask_neg; trivial. apply Pos2Nat.inj_lt in H. - simpl; symmetry; apply not_le_minus_0; auto with arith. - destruct (Pos.sub_mask_pos' _ _ H) as (q & -> & Hq). - simpl. apply plus_minus. now rewrite <- Hq, Pos2Nat.inj_add. + - subst. now rewrite Pos.sub_mask_diag, Nat.sub_diag. + - rewrite Pos.sub_mask_neg; trivial. apply Pos2Nat.inj_lt in H. + simpl; symmetry; apply Nat.sub_0_le. now apply Nat.lt_le_incl. + - destruct (Pos.sub_mask_pos' _ _ H) as (q & -> & Hq). + simpl; symmetry; apply Nat.add_sub_eq_l. now rewrite <- Hq, Pos2Nat.inj_add. Qed. -Lemma inj_pred a : N.to_nat (N.pred a) = pred (N.to_nat a). +Lemma inj_pred a : N.to_nat (N.pred a) = Nat.pred (N.to_nat a). Proof. - intros. rewrite pred_of_minus, N.pred_sub. apply inj_sub. + rewrite <- Nat.sub_1_r, N.pred_sub. apply inj_sub. Qed. -Lemma inj_div2 a : N.to_nat (N.div2 a) = div2 (N.to_nat a). +Lemma inj_div2 a : N.to_nat (N.div2 a) = Nat.div2 (N.to_nat a). Proof. destruct a as [|[p|p| ]]; trivial. - simpl N.to_nat. now rewrite Pos2Nat.inj_xI, div2_double_plus_one. - simpl N.to_nat. now rewrite Pos2Nat.inj_xO, div2_double. + - simpl N.to_nat. now rewrite Pos2Nat.inj_xI, Nat.div2_succ_double. + - simpl N.to_nat. now rewrite Pos2Nat.inj_xO, Nat.div2_double. Qed. Lemma inj_compare a a' : - (a ?= a')%N = nat_compare (N.to_nat a) (N.to_nat a'). + (a ?= a')%N = (N.to_nat a ?= N.to_nat a'). Proof. destruct a, a'; simpl; trivial. - now destruct (Pos2Nat.is_succ p) as (n,->). - now destruct (Pos2Nat.is_succ p) as (n,->). - apply Pos2Nat.inj_compare. + - now destruct (Pos2Nat.is_succ p) as (n,->). + - now destruct (Pos2Nat.is_succ p) as (n,->). + - apply Pos2Nat.inj_compare. Qed. Lemma inj_max a a' : - N.to_nat (N.max a a') = max (N.to_nat a) (N.to_nat a'). + N.to_nat (N.max a a') = Nat.max (N.to_nat a) (N.to_nat a'). Proof. unfold N.max. rewrite inj_compare; symmetry. - case nat_compare_spec; intros H; try rewrite H; auto with arith. + case Nat.compare_spec; intros. + - now apply Nat.max_r, Nat.eq_le_incl. + - now apply Nat.max_r, Nat.lt_le_incl. + - now apply Nat.max_l, Nat.lt_le_incl. Qed. Lemma inj_min a a' : - N.to_nat (N.min a a') = min (N.to_nat a) (N.to_nat a'). + N.to_nat (N.min a a') = Nat.min (N.to_nat a) (N.to_nat a'). Proof. unfold N.min; rewrite inj_compare. symmetry. - case nat_compare_spec; intros H; try rewrite H; auto with arith. + case Nat.compare_spec; intros. + - now apply Nat.min_l, Nat.eq_le_incl. + - now apply Nat.min_l, Nat.lt_le_incl. + - now apply Nat.min_r, Nat.lt_le_incl. Qed. Lemma inj_iter a {A} (f:A->A) (x:A) : - N.iter a f x = nat_rect (fun _ => A) x (fun _ => f) (N.to_nat a). + N.iter a f x = Nat.iter (N.to_nat a) f x. Proof. destruct a as [|a]. trivial. apply Pos2Nat.inj_iter. Qed. @@ -166,7 +171,7 @@ Proof. nat2N. Qed. Lemma inj_succ n : N.of_nat (S n) = N.succ (N.of_nat n). Proof. nat2N. Qed. -Lemma inj_pred n : N.of_nat (pred n) = N.pred (N.of_nat n). +Lemma inj_pred n : N.of_nat (Nat.pred n) = N.pred (N.of_nat n). Proof. nat2N. Qed. Lemma inj_add n n' : N.of_nat (n+n') = (N.of_nat n + N.of_nat n')%N. @@ -178,23 +183,23 @@ Proof. nat2N. Qed. Lemma inj_mul n n' : N.of_nat (n*n') = (N.of_nat n * N.of_nat n')%N. Proof. nat2N. Qed. -Lemma inj_div2 n : N.of_nat (div2 n) = N.div2 (N.of_nat n). +Lemma inj_div2 n : N.of_nat (Nat.div2 n) = N.div2 (N.of_nat n). Proof. nat2N. Qed. Lemma inj_compare n n' : - nat_compare n n' = (N.of_nat n ?= N.of_nat n')%N. + (n ?= n') = (N.of_nat n ?= N.of_nat n')%N. Proof. now rewrite N2Nat.inj_compare, !id. Qed. Lemma inj_min n n' : - N.of_nat (min n n') = N.min (N.of_nat n) (N.of_nat n'). + N.of_nat (Nat.min n n') = N.min (N.of_nat n) (N.of_nat n'). Proof. nat2N. Qed. Lemma inj_max n n' : - N.of_nat (max n n') = N.max (N.of_nat n) (N.of_nat n'). + N.of_nat (Nat.max n n') = N.max (N.of_nat n) (N.of_nat n'). Proof. nat2N. Qed. Lemma inj_iter n {A} (f:A->A) (x:A) : - nat_rect (fun _ => A) x (fun _ => f) n = N.iter (N.of_nat n) f x. + Nat.iter n f x = N.iter (N.of_nat n) f x. Proof. now rewrite N2Nat.inj_iter, !id. Qed. End Nat2N. |