diff options
Diffstat (limited to 'theories/NArith/Nnat.v')
| -rw-r--r-- | theories/NArith/Nnat.v | 137 |
1 files changed, 137 insertions, 0 deletions
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index e19989aed..76a3d616c 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -16,7 +16,11 @@ 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. *) @@ -238,3 +242,136 @@ Proof. 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. +intros; repeat rewrite <- Z_of_nat_of_N; rewrite nat_of_Nplus; apply inj_plus. +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. +intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmult; apply inj_mult. +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. + |