diff options
Diffstat (limited to 'theories/NArith/Nnat.v')
| -rw-r--r-- | theories/NArith/Nnat.v | 205 |
1 files changed, 204 insertions, 1 deletions
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 94f50bd0..bc3711ee 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -6,15 +6,21 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Nnat.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) +(*i $Id: Nnat.v 10739 2008-04-01 14:45:20Z herbelin $ i*) 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 BinInt. Require Import Pnat. +Require Import Zmax. +Require Import Zmin. +Require Import Znat. (** Translation from [N] to [nat] and back. *) @@ -108,6 +114,30 @@ 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. + rewrite Pminus_mask_diag. simpl. apply minus_n_n. + rewrite Pminus_mask_Lt. pose proof (nat_of_P_lt_Lt_compare_morphism _ _ H). simpl. + symmetry; apply not_le_minus_0. auto with arith. assumption. + pose proof (Pminus_mask_Gt p p0 H) as H1. destruct H1 as [q [H1 _]]. rewrite H1; simpl. + replace q with (Pminus p p0) by (unfold Pminus; now rewrite H1). + 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 +205,176 @@ 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. + +(** Properties concerning [Z_of_N] *) + +Lemma Z_of_nat_of_N : forall n:N, Z_of_nat (nat_of_N n) = Z_of_N n. +Proof. + destruct n; simpl; auto; symmetry; apply Zpos_eq_Z_of_nat_o_nat_of_P. +Qed. + +Lemma Z_of_N_eq : forall n m, n = m -> Z_of_N n = Z_of_N m. +Proof. + intros; f_equal; assumption. +Qed. + +Lemma Z_of_N_eq_rev : forall n m, Z_of_N n = Z_of_N m -> n = m. +Proof. + intros [|n] [|m]; simpl; intros; try discriminate; congruence. +Qed. + +Lemma Z_of_N_eq_iff : forall n m, n = m <-> Z_of_N n = Z_of_N m. +Proof. + split; [apply Z_of_N_eq | apply Z_of_N_eq_rev]. +Qed. + +Lemma Z_of_N_le : forall n m, (n<=m)%N -> (Z_of_N n <= Z_of_N m)%Z. +Proof. + intros [|n] [|m]; simpl; auto. +Qed. + +Lemma Z_of_N_le_rev : forall n m, (Z_of_N n <= Z_of_N m)%Z -> (n<=m)%N. +Proof. + intros [|n] [|m]; simpl; auto. +Qed. + +Lemma Z_of_N_le_iff : forall n m, (n<=m)%N <-> (Z_of_N n <= Z_of_N m)%Z. +Proof. + split; [apply Z_of_N_le | apply Z_of_N_le_rev]. +Qed. + +Lemma Z_of_N_lt : forall n m, (n<m)%N -> (Z_of_N n < Z_of_N m)%Z. +Proof. + intros [|n] [|m]; simpl; auto. +Qed. + +Lemma Z_of_N_lt_rev : forall n m, (Z_of_N n < Z_of_N m)%Z -> (n<m)%N. +Proof. + intros [|n] [|m]; simpl; auto. +Qed. + +Lemma Z_of_N_lt_iff : forall n m, (n<m)%N <-> (Z_of_N n < Z_of_N m)%Z. +Proof. + split; [apply Z_of_N_lt | apply Z_of_N_lt_rev]. +Qed. + +Lemma Z_of_N_ge : forall n m, (n>=m)%N -> (Z_of_N n >= Z_of_N m)%Z. +Proof. + intros [|n] [|m]; simpl; auto. +Qed. + +Lemma Z_of_N_ge_rev : forall n m, (Z_of_N n >= Z_of_N m)%Z -> (n>=m)%N. +Proof. + intros [|n] [|m]; simpl; auto. +Qed. + +Lemma Z_of_N_ge_iff : forall n m, (n>=m)%N <-> (Z_of_N n >= Z_of_N m)%Z. +Proof. + split; [apply Z_of_N_ge | apply Z_of_N_ge_rev]. +Qed. + +Lemma Z_of_N_gt : forall n m, (n>m)%N -> (Z_of_N n > Z_of_N m)%Z. +Proof. + intros [|n] [|m]; simpl; auto. +Qed. + +Lemma Z_of_N_gt_rev : forall n m, (Z_of_N n > Z_of_N m)%Z -> (n>m)%N. +Proof. + intros [|n] [|m]; simpl; auto. +Qed. + +Lemma Z_of_N_gt_iff : forall n m, (n>m)%N <-> (Z_of_N n > Z_of_N m)%Z. +Proof. + split; [apply Z_of_N_gt | apply Z_of_N_gt_rev]. +Qed. + +Lemma Z_of_N_of_nat : forall n:nat, Z_of_N (N_of_nat n) = Z_of_nat n. +Proof. + destruct n; simpl; auto. +Qed. + +Lemma Z_of_N_pos : forall p:positive, Z_of_N (Npos p) = Zpos p. +Proof. + destruct p; simpl; auto. +Qed. + +Lemma Z_of_N_abs : forall z:Z, Z_of_N (Zabs_N z) = Zabs z. +Proof. + destruct z; simpl; auto. +Qed. + +Lemma Z_of_N_le_0 : forall n, (0 <= Z_of_N n)%Z. +Proof. + destruct n; intro; discriminate. +Qed. + +Lemma Z_of_N_plus : forall n m:N, Z_of_N (n+m) = (Z_of_N n + Z_of_N m)%Z. +Proof. + destruct n; destruct m; auto. +Qed. + +Lemma Z_of_N_mult : forall n m:N, Z_of_N (n*m) = (Z_of_N n * Z_of_N m)%Z. +Proof. + destruct n; destruct m; auto. +Qed. + +Lemma Z_of_N_minus : forall n m:N, Z_of_N (n-m) = Zmax 0 (Z_of_N n - Z_of_N m). +Proof. + intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nminus; apply inj_minus. +Qed. + +Lemma Z_of_N_succ : forall n:N, Z_of_N (Nsucc n) = Zsucc (Z_of_N n). +Proof. + intros; do 2 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nsucc; apply inj_S. +Qed. + +Lemma Z_of_N_min : forall n m:N, Z_of_N (Nmin n m) = Zmin (Z_of_N n) (Z_of_N m). +Proof. + intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmin; apply inj_min. +Qed. + +Lemma Z_of_N_max : forall n m:N, Z_of_N (Nmax n m) = Zmax (Z_of_N n) (Z_of_N m). +Proof. + intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmax; apply inj_max. +Qed. + |