diff options
Diffstat (limited to 'theories/NArith')
| -rw-r--r-- | theories/NArith/BinPos.v | 71 | ||||
| -rw-r--r-- | theories/NArith/Nnat.v | 137 |
2 files changed, 208 insertions, 0 deletions
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index 2e3c6a3a5..28c6fdb6d 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -220,6 +220,22 @@ Fixpoint Pcompare (x y:positive) (r:comparison) {struct y} : comparison := Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope. +Definition Plt (x y:positive) := (Pcompare x y Eq) = Lt. +Definition Pgt (x y:positive) := (Pcompare x y Eq) = Gt. +Definition Ple (x y:positive) := (Pcompare x y Eq) <> Gt. +Definition Pge (x y:positive) := (Pcompare x y Eq) <> Lt. + +Infix "<=" := Ple : positive_scope. +Infix "<" := Plt : positive_scope. +Infix ">=" := Pge : positive_scope. +Infix ">" := Pgt : positive_scope. + +Notation "x <= y <= z" := (x <= y /\ y <= z) : positive_scope. +Notation "x <= y < z" := (x <= y /\ y < z) : positive_scope. +Notation "x < y < z" := (x < y /\ y < z) : positive_scope. +Notation "x < y <= z" := (x < y /\ y <= z) : positive_scope. + + Definition Pmin (p p' : positive) := match Pcompare p p' Eq with | Lt | Eq => p | Gt => p' @@ -959,6 +975,11 @@ Qed. (**********************************************************************) (** Properties of subtraction on binary positive numbers *) +Lemma Ppred_minus : forall p, Ppred p = Pminus p xH. +Proof. + destruct p; compute; auto. +Qed. + Lemma double_eq_zero_inversion : forall p:positive_mask, Pdouble_mask p = IsNul -> p = IsNul. Proof. @@ -991,6 +1012,33 @@ Proof. | auto ]. Qed. +Lemma Pminus_mask_carry_diag : forall p, Pminus_mask_carry p p = IsNeg. +Proof. + induction p; simpl; auto; rewrite IHp; auto. +Qed. + +Lemma Pminus_mask_IsNeg : forall p q:positive, + Pminus_mask p q = IsNeg -> Pminus_mask_carry p q = IsNeg. +Proof. + induction p; destruct q; simpl; intros; auto; try discriminate. + + unfold Pdouble_mask in H. + generalize (IHp q). + destruct (Pminus_mask p q); try discriminate. + intro H'; rewrite H'; auto. + + unfold Pdouble_plus_one_mask in H. + destruct (Pminus_mask p q); simpl; auto; try discriminate. + + unfold Pdouble_plus_one_mask in H. + destruct (Pminus_mask_carry p q); simpl; auto; try discriminate. + + unfold Pdouble_mask in H. + generalize (IHp q). + destruct (Pminus_mask p q); try discriminate. + intro H'; rewrite H'; auto. +Qed. + Lemma ZL10 : forall p q:positive, Pminus_mask p q = IsPos xH -> Pminus_mask_carry p q = IsNul. @@ -1099,3 +1147,26 @@ Proof. intros H2 H3; elim H3; intros H4 H5; unfold Pminus in |- *; rewrite H2; exact H4. Qed. + +(* When x<y, the substraction of x by y returns 1 *) + +Lemma Pminus_mask_Lt : forall p q:positive, p<q -> Pminus_mask p q = IsNeg. +Proof. + unfold Plt; induction p; destruct q; simpl; intros; auto; try discriminate. + rewrite IHp; simpl; auto. + rewrite IHp; simpl; auto. + apply Pcompare_Gt_Lt; auto. + destruct (Pcompare_Lt_Lt _ _ H). + rewrite Pminus_mask_IsNeg; simpl; auto. + subst q; rewrite Pminus_mask_carry_diag; auto. + rewrite IHp; simpl; auto. +Qed. + +Lemma Pminus_Lt : forall p q:positive, p<q -> p-q = xH. +Proof. + intros; unfold Plt, Pminus; rewrite Pminus_mask_Lt; auto. +Qed. + + + + 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. + |