diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Arith/Max.v | 2 | ||||
| -rw-r--r-- | theories/FSets/OrderedTypeEx.v | 21 | ||||
| -rw-r--r-- | theories/IntMap/Adalloc.v | 10 | ||||
| -rw-r--r-- | theories/NArith/BinNat.v | 54 | ||||
| -rw-r--r-- | theories/NArith/BinPos.v | 12 | ||||
| -rw-r--r-- | theories/NArith/Ndec.v | 180 | ||||
| -rw-r--r-- | theories/NArith/Nnat.v | 63 | ||||
| -rw-r--r-- | theories/NArith/Pnat.v | 2 |
8 files changed, 246 insertions, 98 deletions
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index a3d658d0c..75e1cdf0c 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require Import Arith. +Require Import Le. Open Local Scope nat_scope. diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v index 8da19706e..0295133a6 100644 --- a/theories/FSets/OrderedTypeEx.v +++ b/theories/FSets/OrderedTypeEx.v @@ -154,16 +154,16 @@ Module N_as_OT <: UsualOrderedType. Definition eq_sym := @sym_eq t. Definition eq_trans := @trans_eq t. - Definition lt p q:= Nle q p = false. + Definition lt p q:= Nleb q p = false. - Definition lt_trans := Nlt_trans. + Definition lt_trans := Nltb_trans. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. Proof. intros; intro. rewrite H0 in H. unfold lt in H. - rewrite Nle_refl in H; discriminate. + rewrite Nleb_refl in H; discriminate. Qed. Definition compare : forall x y : t, Compare lt eq x y. @@ -172,16 +172,15 @@ Module N_as_OT <: UsualOrderedType. case_eq ((x ?= y)%N); intros. apply EQ; apply Ncompare_Eq_eq; auto. apply LT; unfold lt; auto. - generalize (Nle_Ncompare y x). - destruct (Nle y x); auto. - rewrite <- Ncompare_antisym. + generalize (Nleb_Nle y x). + unfold Nle; rewrite <- Ncompare_antisym. destruct (x ?= y)%N; simpl; try discriminate. - intros (H0,_); elim H0; auto. + clear H; intros H. + destruct (Nleb y x); intuition. apply GT; unfold lt. - generalize (Nle_Ncompare x y). - destruct (Nle x y); auto. - destruct (x ?= y)%N; simpl; try discriminate. - intros (H0,_); elim H0; auto. + generalize (Nleb_Nle x y). + unfold Nle; destruct (x ?= y)%N; simpl; try discriminate. + destruct (Nleb x y); intuition. Defined. End N_as_OT. diff --git a/theories/IntMap/Adalloc.v b/theories/IntMap/Adalloc.v index d475bb54d..ef68b1e5c 100644 --- a/theories/IntMap/Adalloc.v +++ b/theories/IntMap/Adalloc.v @@ -64,20 +64,20 @@ Section AdAlloc. Lemma ad_alloc_opt_optimal_1 : forall (m:Map A) (a:ad), - Nle (ad_alloc_opt m) a = false -> {y : A | MapGet A m a = Some y}. + Nleb (ad_alloc_opt m) a = false -> {y : A | MapGet A m a = Some y}. Proof. induction m as [| a y| m0 H m1 H0]. simpl in |- *. unfold Nle in |- *. simpl in |- *. intros. discriminate H. simpl in |- *. intros b H. elim (sumbool_of_bool (Neqb a N0)). intro H0. rewrite H0 in H. - unfold Nle in H. cut (N0 = b). intro. split with y. rewrite <- H1. rewrite H0. reflexivity. + unfold Nleb in H. cut (N0 = b). intro. split with y. rewrite <- H1. rewrite H0. reflexivity. rewrite <- (N_of_nat_of_N b). rewrite <- (le_n_O_eq _ (le_S_n _ _ (leb_complete_conv _ _ H))). reflexivity. intro H0. rewrite H0 in H. discriminate H. intros. simpl in H1. elim (Ndouble_or_double_plus_un a). intro H2. elim H2. intros a0 H3. - rewrite H3 in H1. elim (H _ (Nlt_double_mono_conv _ _ (Nmin_lt_3 _ _ _ H1))). intros y H4. + rewrite H3 in H1. elim (H _ (Nltb_double_mono_conv _ _ (Nmin_lt_3 _ _ _ H1))). intros y H4. split with y. rewrite H3. rewrite MapGet_M2_bit_0_0. rewrite Ndouble_div2. assumption. apply Ndouble_bit0. intro H2. elim H2. intros a0 H3. rewrite H3 in H1. - elim (H0 _ (Nlt_double_plus_one_mono_conv _ _ (Nmin_lt_4 _ _ _ H1))). intros y H4. + elim (H0 _ (Nltb_double_plus_one_mono_conv _ _ (Nmin_lt_4 _ _ _ H1))). intros y H4. split with y. rewrite H3. rewrite MapGet_M2_bit_0_1. rewrite Ndouble_plus_one_div2. assumption. apply Ndouble_plus_one_bit0. @@ -85,7 +85,7 @@ Section AdAlloc. Lemma ad_alloc_opt_optimal : forall (m:Map A) (a:ad), - Nle (ad_alloc_opt m) a = false -> in_dom A a m = true. + Nleb (ad_alloc_opt m) a = false -> in_dom A a m = true. Proof. intros. unfold in_dom in |- *. elim (ad_alloc_opt_optimal_1 m a H). intros y H0. rewrite H0. reflexivity. diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 0f2782bd9..b26a22c9e 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -70,6 +70,21 @@ Definition Nplus n m := Infix "+" := Nplus : N_scope. +(** Substraction *) + +Definition Nminus (x y:N) := + match x, y with + | N0, _ => N0 + | x, N0 => x + | Npos x', Npos y' => + match Pcompare x' y' Eq with + | Lt | Eq => N0 + | Gt => Npos (x' - y') + end + end. + +Infix "-" := Nminus : N_scope. + (** Multiplication *) Definition Nmult n m := @@ -93,6 +108,28 @@ Definition Ncompare n m := Infix "?=" := Ncompare (at level 70, no associativity) : N_scope. +Definition Nlt (x y:N) := (x ?= y) = Lt. +Definition Ngt (x y:N) := (x ?= y) = Gt. +Definition Nle (x y:N) := (x ?= y) <> Gt. +Definition Nge (x y:N) := (x ?= y) <> Lt. + +Infix "<=" := Nle : N_scope. +Infix "<" := Nlt : N_scope. +Infix ">=" := Nge : N_scope. +Infix ">" := Ngt : N_scope. + +(** Min and max *) + +Definition Nmin (n n' : N) := match Ncompare n n' with + | Lt | Eq => n + | Gt => n' + end. + +Definition Nmax (n n' : N) := match Ncompare n n' with + | Lt | Eq => n' + | Gt => n + end. + (** convenient induction principles *) Lemma N_ind_double : @@ -217,6 +254,23 @@ intro n; pattern n in |- *; apply Nind; clear n; simpl in |- *. apply IHn; apply Nsucc_inj; assumption. Qed. +(** Properties of substraction. *) + +Lemma Nle_Nminus_N0 : forall n n':N, n <= n' -> n-n' = N0. +Proof. + destruct n; destruct n'; simpl; intros; auto. + elim H; auto. + red in H; simpl in *. + intros; destruct (Pcompare p p0 Eq); auto. + elim H; auto. +Qed. + +Lemma Nminus_N0_Nle : forall n n':N, n-n' = N0 -> n <= n'. +Proof. + destruct n; destruct n'; red; simpl; intros; try discriminate. + destruct (Pcompare p p0 Eq); discriminate. +Qed. + (** Properties of multiplication *) Theorem Nmult_0_l : forall n:N, N0 * n = N0. diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index c8c94f781..2e3c6a3a5 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -13,7 +13,7 @@ Unset Boxed Definitions. (**********************************************************************) (** Binary positive numbers *) -(** Original development by Pierre Crégut, CNET, Lannion, France *) +(** Original development by Pierre Crégut, CNET, Lannion, France *) Inductive positive : Set := | xI : positive -> positive @@ -220,6 +220,16 @@ Fixpoint Pcompare (x y:positive) (r:comparison) {struct y} : comparison := Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope. +Definition Pmin (p p' : positive) := match Pcompare p p' Eq with + | Lt | Eq => p + | Gt => p' + end. + +Definition Pmax (p p' : positive) := match Pcompare p p' Eq with + | Lt | Eq => p' + | Gt => p + end. + (**********************************************************************) (** Miscellaneous properties of binary positive numbers *) diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v index 29ac72d00..bbab81f4e 100644 --- a/theories/NArith/Ndec.v +++ b/theories/NArith/Ndec.v @@ -37,6 +37,13 @@ Proof. induction p; destruct p'; simpl; intros; try discriminate; auto. Qed. +Lemma Peqb_complete : forall p p', Peqb p p' = true -> p = p'. +Proof. + intros. + apply Pcompare_Eq_eq. + apply Peqb_Pcompare; auto. +Qed. + Lemma Pcompare_Peqb : forall p p', Pcompare p p' Eq = Eq -> Peqb p p' = true. Proof. intros; rewrite <- (Pcompare_Eq_eq _ _ H). @@ -208,205 +215,220 @@ Qed. (** A boolean order on [N] *) -Definition Nle (a b:N) := leb (nat_of_N a) (nat_of_N b). +Definition Nleb (a b:N) := leb (nat_of_N a) (nat_of_N b). -Lemma Nle_Ncompare : forall a b, Nle a b = true <-> Ncompare a b <> Gt. +Lemma Nleb_Nle : forall a b, Nleb a b = true <-> Nle a b. Proof. - intros; rewrite nat_of_Ncompare. - unfold Nle; apply leb_compare. + intros; unfold Nle; rewrite nat_of_Ncompare. + unfold Nleb; apply leb_compare. Qed. -Lemma Nle_refl : forall a, Nle a a = true. +Lemma Nleb_refl : forall a, Nleb a a = true. Proof. - intro. unfold Nle in |- *. apply leb_correct. apply le_n. + intro. unfold Nleb in |- *. apply leb_correct. apply le_n. Qed. -Lemma Nle_antisym : - forall a b, Nle a b = true -> Nle b a = true -> a = b. +Lemma Nleb_antisym : + forall a b, Nleb a b = true -> Nleb b a = true -> a = b. Proof. - unfold Nle in |- *. intros. rewrite <- (N_of_nat_of_N a). rewrite <- (N_of_nat_of_N b). + unfold Nleb in |- *. intros. rewrite <- (N_of_nat_of_N a). rewrite <- (N_of_nat_of_N b). rewrite (le_antisym _ _ (leb_complete _ _ H) (leb_complete _ _ H0)). reflexivity. Qed. -Lemma Nle_trans : - forall a b c, Nle a b = true -> Nle b c = true -> Nle a c = true. +Lemma Nleb_trans : + forall a b c, Nleb a b = true -> Nleb b c = true -> Nleb a c = true. Proof. - unfold Nle in |- *. intros. apply leb_correct. apply le_trans with (m := nat_of_N b). + unfold Nleb in |- *. intros. apply leb_correct. apply le_trans with (m := nat_of_N b). apply leb_complete. assumption. apply leb_complete. assumption. Qed. -Lemma Nle_lt_trans : +Lemma Nleb_ltb_trans : forall a b c, - Nle a b = true -> Nle c b = false -> Nle c a = false. + Nleb a b = true -> Nleb c b = false -> Nleb c a = false. Proof. - unfold Nle in |- *. intros. apply leb_correct_conv. apply le_lt_trans with (m := nat_of_N b). + unfold Nleb in |- *. intros. apply leb_correct_conv. apply le_lt_trans with (m := nat_of_N b). apply leb_complete. assumption. apply leb_complete_conv. assumption. Qed. -Lemma Nlt_le_trans : +Lemma Nltb_leb_trans : forall a b c, - Nle b a = false -> Nle b c = true -> Nle c a = false. + Nleb b a = false -> Nleb b c = true -> Nleb c a = false. Proof. - unfold Nle in |- *. intros. apply leb_correct_conv. apply lt_le_trans with (m := nat_of_N b). + unfold Nleb in |- *. intros. apply leb_correct_conv. apply lt_le_trans with (m := nat_of_N b). apply leb_complete_conv. assumption. apply leb_complete. assumption. Qed. -Lemma Nlt_trans : +Lemma Nltb_trans : forall a b c, - Nle b a = false -> Nle c b = false -> Nle c a = false. + Nleb b a = false -> Nleb c b = false -> Nleb c a = false. Proof. - unfold Nle in |- *. intros. apply leb_correct_conv. apply lt_trans with (m := nat_of_N b). + unfold Nleb in |- *. intros. apply leb_correct_conv. apply lt_trans with (m := nat_of_N b). apply leb_complete_conv. assumption. apply leb_complete_conv. assumption. Qed. -Lemma Nlt_le_weak : forall a b:N, Nle b a = false -> Nle a b = true. +Lemma Nltb_leb_weak : forall a b:N, Nleb b a = false -> Nleb a b = true. Proof. - unfold Nle in |- *. intros. apply leb_correct. apply lt_le_weak. + unfold Nleb in |- *. intros. apply leb_correct. apply lt_le_weak. apply leb_complete_conv. assumption. Qed. -Lemma Nle_double_mono : +Lemma Nleb_double_mono : forall a b, - Nle a b = true -> Nle (Ndouble a) (Ndouble b) = true. + Nleb a b = true -> Nleb (Ndouble a) (Ndouble b) = true. Proof. - unfold Nle in |- *. intros. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. apply leb_correct. + unfold Nleb in |- *. intros. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. apply leb_correct. simpl in |- *. apply plus_le_compat. apply leb_complete. assumption. apply plus_le_compat. apply leb_complete. assumption. apply le_n. Qed. -Lemma Nle_double_plus_one_mono : +Lemma Nleb_double_plus_one_mono : forall a b, - Nle a b = true -> - Nle (Ndouble_plus_one a) (Ndouble_plus_one b) = true. + Nleb a b = true -> + Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = true. Proof. - unfold Nle in |- *. intros. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one. + unfold Nleb in |- *. intros. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one. apply leb_correct. apply le_n_S. simpl in |- *. apply plus_le_compat. apply leb_complete. assumption. apply plus_le_compat. apply leb_complete. assumption. apply le_n. Qed. -Lemma Nle_double_mono_conv : +Lemma Nleb_double_mono_conv : forall a b, - Nle (Ndouble a) (Ndouble b) = true -> Nle a b = true. + Nleb (Ndouble a) (Ndouble b) = true -> Nleb a b = true. Proof. - unfold Nle in |- *. intros a b. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. intro. + unfold Nleb in |- *. intros a b. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. intro. apply leb_correct. apply (mult_S_le_reg_l 1). apply leb_complete. assumption. Qed. -Lemma Nle_double_plus_one_mono_conv : +Lemma Nleb_double_plus_one_mono_conv : forall a b, - Nle (Ndouble_plus_one a) (Ndouble_plus_one b) = true -> - Nle a b = true. + Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = true -> + Nleb a b = true. Proof. - unfold Nle in |- *. intros a b. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one. + unfold Nleb in |- *. intros a b. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one. intro. apply leb_correct. apply (mult_S_le_reg_l 1). apply le_S_n. apply leb_complete. assumption. Qed. -Lemma Nlt_double_mono : +Lemma Nltb_double_mono : forall a b, - Nle a b = false -> Nle (Ndouble a) (Ndouble b) = false. + Nleb a b = false -> Nleb (Ndouble a) (Ndouble b) = false. Proof. - intros. elim (sumbool_of_bool (Nle (Ndouble a) (Ndouble b))). intro H0. - rewrite (Nle_double_mono_conv _ _ H0) in H. discriminate H. + intros. elim (sumbool_of_bool (Nleb (Ndouble a) (Ndouble b))). intro H0. + rewrite (Nleb_double_mono_conv _ _ H0) in H. discriminate H. trivial. Qed. -Lemma Nlt_double_plus_one_mono : +Lemma Nltb_double_plus_one_mono : forall a b, - Nle a b = false -> - Nle (Ndouble_plus_one a) (Ndouble_plus_one b) = false. + Nleb a b = false -> + Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = false. Proof. - intros. elim (sumbool_of_bool (Nle (Ndouble_plus_one a) (Ndouble_plus_one b))). intro H0. - rewrite (Nle_double_plus_one_mono_conv _ _ H0) in H. discriminate H. + intros. elim (sumbool_of_bool (Nleb (Ndouble_plus_one a) (Ndouble_plus_one b))). intro H0. + rewrite (Nleb_double_plus_one_mono_conv _ _ H0) in H. discriminate H. trivial. Qed. -Lemma Nlt_double_mono_conv : +Lemma Nltb_double_mono_conv : forall a b, - Nle (Ndouble a) (Ndouble b) = false -> Nle a b = false. + Nleb (Ndouble a) (Ndouble b) = false -> Nleb a b = false. Proof. - intros. elim (sumbool_of_bool (Nle a b)). intro H0. rewrite (Nle_double_mono _ _ H0) in H. + intros. elim (sumbool_of_bool (Nleb a b)). intro H0. rewrite (Nleb_double_mono _ _ H0) in H. discriminate H. trivial. Qed. -Lemma Nlt_double_plus_one_mono_conv : +Lemma Nltb_double_plus_one_mono_conv : forall a b, - Nle (Ndouble_plus_one a) (Ndouble_plus_one b) = false -> - Nle a b = false. + Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = false -> + Nleb a b = false. Proof. - intros. elim (sumbool_of_bool (Nle a b)). intro H0. - rewrite (Nle_double_plus_one_mono _ _ H0) in H. discriminate H. + intros. elim (sumbool_of_bool (Nleb a b)). intro H0. + rewrite (Nleb_double_plus_one_mono _ _ H0) in H. discriminate H. trivial. Qed. -(* A [min] function over [N] *) +(* An alternate [min] function over [N] *) -Definition Nmin (a b:N) := if Nle a b then a else b. +Definition Nmin' (a b:N) := if Nleb a b then a else b. + +Lemma Nmin_Nmin' : forall a b, Nmin a b = Nmin' a b. +Proof. + unfold Nmin, Nmin', Nleb; intros. + rewrite nat_of_Ncompare. + generalize (leb_compare (nat_of_N a) (nat_of_N b)); + destruct (nat_compare (nat_of_N a) (nat_of_N b)); + destruct (leb (nat_of_N a) (nat_of_N b)); intuition. + lapply H1; intros; discriminate. + lapply H1; intros; discriminate. +Qed. Lemma Nmin_choice : forall a b, {Nmin a b = a} + {Nmin a b = b}. Proof. - unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle a b)). intro H. left. rewrite H. - reflexivity. - intro H. right. rewrite H. reflexivity. + unfold Nmin in *; intros; destruct (Ncompare a b); auto. Qed. -Lemma Nmin_le_1 : forall a b, Nle (Nmin a b) a = true. +Lemma Nmin_le_1 : forall a b, Nleb (Nmin a b) a = true. Proof. - unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle a b)). intro H. rewrite H. - apply Nle_refl. - intro H. rewrite H. apply Nlt_le_weak. assumption. + intros; rewrite Nmin_Nmin'. + unfold Nmin'; elim (sumbool_of_bool (Nleb a b)). intro H. rewrite H. + apply Nleb_refl. + intro H. rewrite H. apply Nltb_leb_weak. assumption. Qed. -Lemma Nmin_le_2 : forall a b, Nle (Nmin a b) b = true. +Lemma Nmin_le_2 : forall a b, Nleb (Nmin a b) b = true. Proof. - unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle a b)). intro H. rewrite H. assumption. - intro H. rewrite H. apply Nle_refl. + intros; rewrite Nmin_Nmin'. + unfold Nmin'; elim (sumbool_of_bool (Nleb a b)). intro H. rewrite H. assumption. + intro H. rewrite H. apply Nleb_refl. Qed. Lemma Nmin_le_3 : - forall a b c, Nle a (Nmin b c) = true -> Nle a b = true. + forall a b c, Nleb a (Nmin b c) = true -> Nleb a b = true. Proof. - unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle b c)). intro H0. rewrite H0 in H. + intros; rewrite Nmin_Nmin' in *. + unfold Nmin' in *; elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H. assumption. - intro H0. rewrite H0 in H. apply Nlt_le_weak. apply Nle_lt_trans with (b := c); assumption. + intro H0. rewrite H0 in H. apply Nltb_leb_weak. apply Nleb_ltb_trans with (b := c); assumption. Qed. Lemma Nmin_le_4 : - forall a b c, Nle a (Nmin b c) = true -> Nle a c = true. + forall a b c, Nleb a (Nmin b c) = true -> Nleb a c = true. Proof. - unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle b c)). intro H0. rewrite H0 in H. - apply Nle_trans with (b := b); assumption. + intros; rewrite Nmin_Nmin' in *. + unfold Nmin' in *; elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H. + apply Nleb_trans with (b := b); assumption. intro H0. rewrite H0 in H. assumption. Qed. Lemma Nmin_le_5 : forall a b c, - Nle a b = true -> Nle a c = true -> Nle a (Nmin b c) = true. + Nleb a b = true -> Nleb a c = true -> Nleb a (Nmin b c) = true. Proof. intros. elim (Nmin_choice b c). intro H1. rewrite H1. assumption. intro H1. rewrite H1. assumption. Qed. Lemma Nmin_lt_3 : - forall a b c, Nle (Nmin b c) a = false -> Nle b a = false. + forall a b c, Nleb (Nmin b c) a = false -> Nleb b a = false. Proof. - unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle b c)). intro H0. rewrite H0 in H. + intros; rewrite Nmin_Nmin' in *. + unfold Nmin' in *. intros. elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H. assumption. - intro H0. rewrite H0 in H. apply Nlt_trans with (b := c); assumption. + intro H0. rewrite H0 in H. apply Nltb_trans with (b := c); assumption. Qed. Lemma Nmin_lt_4 : - forall a b c, Nle (Nmin b c) a = false -> Nle c a = false. + forall a b c, Nleb (Nmin b c) a = false -> Nleb c a = false. Proof. - unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle b c)). intro H0. rewrite H0 in H. - apply Nlt_le_trans with (b := b); assumption. + intros; rewrite Nmin_Nmin' in *. + unfold Nmin' in *. elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H. + apply Nltb_leb_trans with (b := b); assumption. intro H0. rewrite H0 in H. assumption. Qed. diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 5465bc692..e19989aed 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -12,6 +12,8 @@ Require Import Arith_base. Require Import Compare_dec. Require Import Sumbool. Require Import Div2. +Require Import Min. +Require Import Max. Require Import BinPos. Require Import BinNat. Require Import Pnat. @@ -108,6 +110,27 @@ Proof. apply N_of_nat_of_N. Qed. +Lemma nat_of_Nminus : + forall a a', nat_of_N (Nminus a a') = ((nat_of_N a)-(nat_of_N a'))%nat. +Proof. + destruct a; destruct a'; simpl; auto with arith. + case_eq (Pcompare p p0 Eq); simpl; intros. + rewrite (Pcompare_Eq_eq _ _ H); auto with arith. + symmetry; apply not_le_minus_0. + generalize (nat_of_P_lt_Lt_compare_morphism _ _ H); auto with arith. + apply nat_of_P_minus_morphism; auto. +Qed. + +Lemma N_of_minus : + forall n n', N_of_nat (n-n') = Nminus (N_of_nat n) (N_of_nat n'). +Proof. + intros. + pattern n at 1; rewrite <- (nat_of_N_of_nat n). + pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). + rewrite <- nat_of_Nminus. + apply N_of_nat_of_N. +Qed. + Lemma nat_of_Nmult : forall a a', nat_of_N (Nmult a a') = (nat_of_N a)*(nat_of_N a'). Proof. @@ -175,3 +198,43 @@ Proof. pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). symmetry; apply nat_of_Ncompare. Qed. + +Lemma nat_of_Nmin : + forall a a', nat_of_N (Nmin a a') = min (nat_of_N a) (nat_of_N a'). +Proof. + intros; unfold Nmin; rewrite nat_of_Ncompare. + unfold nat_compare. + destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; + simpl; intros; symmetry; auto with arith. + apply min_l; rewrite e; auto with arith. +Qed. + +Lemma N_of_min : + forall n n', N_of_nat (min n n') = Nmin (N_of_nat n) (N_of_nat n'). +Proof. + intros. + pattern n at 1; rewrite <- (nat_of_N_of_nat n). + pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). + rewrite <- nat_of_Nmin. + apply N_of_nat_of_N. +Qed. + +Lemma nat_of_Nmax : + forall a a', nat_of_N (Nmax a a') = max (nat_of_N a) (nat_of_N a'). +Proof. + intros; unfold Nmax; rewrite nat_of_Ncompare. + unfold nat_compare. + destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; + simpl; intros; symmetry; auto with arith. + apply max_r; rewrite e; auto with arith. +Qed. + +Lemma N_of_max : + forall n n', N_of_nat (max n n') = Nmax (N_of_nat n) (N_of_nat n'). +Proof. + intros. + pattern n at 1; rewrite <- (nat_of_N_of_nat n). + pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). + rewrite <- nat_of_Nmax. + apply N_of_nat_of_N. +Qed. diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v index f1c1d72fc..9bec3e994 100644 --- a/theories/NArith/Pnat.v +++ b/theories/NArith/Pnat.v @@ -14,7 +14,7 @@ Require Import BinPos. (** Properties of the injection from binary positive numbers to Peano natural numbers *) -(** Original development by Pierre Crégut, CNET, Lannion, France *) +(** Original development by Pierre Crégut, CNET, Lannion, France *) Require Import Le. Require Import Lt. |