diff options
Diffstat (limited to 'theories/ZArith/ZOdiv_def.v')
| -rw-r--r-- | theories/ZArith/ZOdiv_def.v | 136 |
1 files changed, 0 insertions, 136 deletions
diff --git a/theories/ZArith/ZOdiv_def.v b/theories/ZArith/ZOdiv_def.v deleted file mode 100644 index 71d6cad4..00000000 --- a/theories/ZArith/ZOdiv_def.v +++ /dev/null @@ -1,136 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - - -Require Import BinPos BinNat Nnat ZArith_base. - -Open Scope Z_scope. - -Definition NPgeb (a:N)(b:positive) := - match a with - | N0 => false - | Npos na => match Pcompare na b Eq with Lt => false | _ => true end - end. - -Fixpoint Pdiv_eucl (a b:positive) : N * N := - match a with - | xH => - match b with xH => (1, 0)%N | _ => (0, 1)%N end - | xO a' => - let (q, r) := Pdiv_eucl a' b in - let r' := (2 * r)%N in - if (NPgeb r' b) then (2 * q + 1, (Nminus r' (Npos b)))%N - else (2 * q, r')%N - | xI a' => - let (q, r) := Pdiv_eucl a' b in - let r' := (2 * r + 1)%N in - if (NPgeb r' b) then (2 * q + 1, (Nminus r' (Npos b)))%N - else (2 * q, r')%N - end. - -Definition ZOdiv_eucl (a b:Z) : Z * Z := - match a, b with - | Z0, _ => (Z0, Z0) - | _, Z0 => (Z0, a) - | Zpos na, Zpos nb => - let (nq, nr) := Pdiv_eucl na nb in - (Z_of_N nq, Z_of_N nr) - | Zneg na, Zpos nb => - let (nq, nr) := Pdiv_eucl na nb in - (Zopp (Z_of_N nq), Zopp (Z_of_N nr)) - | Zpos na, Zneg nb => - let (nq, nr) := Pdiv_eucl na nb in - (Zopp (Z_of_N nq), Z_of_N nr) - | Zneg na, Zneg nb => - let (nq, nr) := Pdiv_eucl na nb in - (Z_of_N nq, Zopp (Z_of_N nr)) - end. - -Definition ZOdiv a b := fst (ZOdiv_eucl a b). -Definition ZOmod a b := snd (ZOdiv_eucl a b). - - -Definition Ndiv_eucl (a b:N) : N * N := - match a, b with - | N0, _ => (N0, N0) - | _, N0 => (N0, a) - | Npos na, Npos nb => Pdiv_eucl na nb - end. - -Definition Ndiv a b := fst (Ndiv_eucl a b). -Definition Nmod a b := snd (Ndiv_eucl a b). - - -(* Proofs of specifications for these euclidean divisions. *) - -Theorem NPgeb_correct: forall (a:N)(b:positive), - if NPgeb a b then a = (Nminus a (Npos b) + Npos b)%N else True. -Proof. - destruct a; intros; simpl; auto. - generalize (Pcompare_Eq_eq p b). - case_eq (Pcompare p b Eq); intros; auto. - rewrite H0; auto. - now rewrite Pminus_mask_diag. - destruct (Pminus_mask_Gt p b H) as [d [H2 [H3 _]]]. - rewrite H2. rewrite <- H3. - simpl; f_equal; apply Pplus_comm. -Qed. - -Hint Rewrite Z_of_N_plus Z_of_N_mult Z_of_N_minus Zmult_1_l Zmult_assoc - Zmult_plus_distr_l Zmult_plus_distr_r : zdiv. -Hint Rewrite <- Zplus_assoc : zdiv. - -Theorem Pdiv_eucl_correct: forall a b, - let (q,r) := Pdiv_eucl a b in - Zpos a = Z_of_N q * Zpos b + Z_of_N r. -Proof. - induction a; cbv beta iota delta [Pdiv_eucl]; fold Pdiv_eucl; cbv zeta. - intros b; generalize (IHa b); case Pdiv_eucl. - intros q1 r1 Hq1. - generalize (NPgeb_correct (2 * r1 + 1) b); case NPgeb; intros H. - set (u := Nminus (2 * r1 + 1) (Npos b)) in * |- *. - assert (HH: Z_of_N u = (Z_of_N (2 * r1 + 1) - Zpos b)%Z). - rewrite H; autorewrite with zdiv; simpl. - rewrite Zplus_comm, Zminus_plus; trivial. - rewrite HH; autorewrite with zdiv; simpl Z_of_N. - rewrite Zpos_xI, Hq1. - autorewrite with zdiv; f_equal; rewrite Zplus_minus; trivial. - rewrite Zpos_xI, Hq1; autorewrite with zdiv; auto. - intros b; generalize (IHa b); case Pdiv_eucl. - intros q1 r1 Hq1. - generalize (NPgeb_correct (2 * r1) b); case NPgeb; intros H. - set (u := Nminus (2 * r1) (Npos b)) in * |- *. - assert (HH: Z_of_N u = (Z_of_N (2 * r1) - Zpos b)%Z). - rewrite H; autorewrite with zdiv; simpl. - rewrite Zplus_comm, Zminus_plus; trivial. - rewrite HH; autorewrite with zdiv; simpl Z_of_N. - rewrite Zpos_xO, Hq1. - autorewrite with zdiv; f_equal; rewrite Zplus_minus; trivial. - rewrite Zpos_xO, Hq1; autorewrite with zdiv; auto. - destruct b; auto. -Qed. - -Theorem ZOdiv_eucl_correct: forall a b, - let (q,r) := ZOdiv_eucl a b in a = q * b + r. -Proof. - destruct a; destruct b; simpl; auto; - generalize (Pdiv_eucl_correct p p0); case Pdiv_eucl; auto; intros; - try change (Zneg p) with (Zopp (Zpos p)); rewrite H. - destruct n; auto. - repeat (rewrite Zopp_plus_distr || rewrite Zopp_mult_distr_l); trivial. - repeat (rewrite Zopp_plus_distr || rewrite Zopp_mult_distr_r); trivial. -Qed. - -Theorem Ndiv_eucl_correct: forall a b, - let (q,r) := Ndiv_eucl a b in a = (q * b + r)%N. -Proof. - destruct a; destruct b; simpl; auto; - generalize (Pdiv_eucl_correct p p0); case Pdiv_eucl; auto; intros; - destruct n; destruct n0; simpl; simpl in H; try discriminate; - injection H; intros; subst; trivial. -Qed. |