diff options
Diffstat (limited to 'theories/ZArith/ZOdiv_def.v')
| -rw-r--r-- | theories/ZArith/ZOdiv_def.v | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/theories/ZArith/ZOdiv_def.v b/theories/ZArith/ZOdiv_def.v index 2c84765e..88d573bb 100644 --- a/theories/ZArith/ZOdiv_def.v +++ b/theories/ZArith/ZOdiv_def.v @@ -17,9 +17,9 @@ Definition NPgeb (a:N)(b:positive) := | Npos na => match Pcompare na b Eq with Lt => false | _ => true end end. -Fixpoint Pdiv_eucl (a b:positive) {struct a} : N * N := +Fixpoint Pdiv_eucl (a b:positive) : N * N := match a with - | xH => + | xH => match b with xH => (1, 0)%N | _ => (0, 1)%N end | xO a' => let (q, r) := Pdiv_eucl a' b in @@ -33,21 +33,21 @@ Fixpoint Pdiv_eucl (a b:positive) {struct a} : N * N := else (2 * q, r')%N end. -Definition ZOdiv_eucl (a b:Z) : Z * Z := +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 + | 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 + | 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 + | 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 + | Zneg na, Zneg nb => + let (nq, nr) := Pdiv_eucl na nb in (Z_of_N nq, Zopp (Z_of_N nr)) end. @@ -55,7 +55,7 @@ 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 := +Definition Ndiv_eucl (a b:N) : N * N := match a, b with | N0, _ => (N0, N0) | _, N0 => (N0, a) @@ -68,13 +68,13 @@ Definition Nmod a b := snd (Ndiv_eucl a b). (* Proofs of specifications for these euclidean divisions. *) -Theorem NPgeb_correct: forall (a:N)(b:positive), +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. + rewrite H0; auto. now rewrite Pminus_mask_diag. destruct (Pminus_mask_Gt p b H) as [d [H2 [H3 _]]]. rewrite H2. rewrite <- H3. @@ -82,11 +82,11 @@ Proof. 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. + 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 + 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. |