diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-13 19:31:29 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-13 19:31:29 +0000 |
commit | b99396f1ee52d285f4dca9cecc6e89b06105448f (patch) | |
tree | 41b8e04da10102c807746347ed7dbcf3888f8906 /theories/ZArith/Znumtheory.v | |
parent | b9f6c5b7641115a18e7b9832da435c32aaa27014 (diff) |
un Zgcd calculant dans coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8813 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Znumtheory.v')
-rw-r--r-- | theories/ZArith/Znumtheory.v | 541 |
1 files changed, 393 insertions, 148 deletions
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index c336cf262..b6ade8fd3 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -367,11 +367,392 @@ rewrite H6; rewrite H7; ring. ring. Qed. +Lemma Zis_gcd_0_abs : forall b, + Zis_gcd 0 b (Zabs b) /\ Zabs b >= 0 /\ 0 = Zabs b * 0 /\ b = Zabs b * Zsgn b. +Proof. +intro b. +elim (Z_le_lt_eq_dec _ _ (Zabs_pos b)). +intros H0; split. +apply Zabs_ind. +intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto. +intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto. +repeat split; auto with zarith. +symmetry; apply Zabs_Zsgn. + +intros H0; rewrite <- H0. +rewrite <- (Zabs_Zsgn b); rewrite <- H0; simpl in |- *. +split; [ apply Zis_gcd_0 | idtac ]; auto with zarith. +Qed. + + (** We could obtain a [Zgcd] function via [euclid]. But we propose - here a more direct version of a [Zgcd], with better extraction - (no bezout coeffs). *) + here a more direct version of a [Zgcd], that can compute within Coq. + For that, we use an explicit measure in [nat], and we proved later + that using [2(d+1)] is enough, where [d] is the number of binary digits + of the first argument. *) + +Fixpoint Zgcdn (n:nat) : Z -> Z -> Z := fun a b => + match n with + | O => 1 (* arbitrary, since n should be big enough *) + | S n => match a with + | Z0 => Zabs b + | Zpos _ => Zgcdn n (Zmod b a) a + | Zneg a => Zgcdn n (Zmod b (Zpos a)) (Zpos a) + end + end. + +(* For technical reason, we don't use [Ndigit.Psize] but this + ad-hoc version: [Psize p = S (Psiz p)]. *) + +Fixpoint Psiz (p:positive) : nat := + match p with + | xH => O + | xI p => S (Psiz p) + | xO p => S (Psiz p) + end. + +Definition Zgcd_bound (a:Z) := match a with + | Z0 => S O + | Zpos p => let n := Psiz p in S (S (n+n)) + | Zneg p => let n := Psiz p in S (S (n+n)) +end. + +Definition Zgcd a b := Zgcdn (Zgcd_bound a) a b. + +(** A first obvious fact : [Zgcd a b] is positive. *) + +Lemma Zgcdn_pos : forall n a b, + 0 <= Zgcdn n a b. +Proof. +induction n. +simpl; auto with zarith. +destruct a; simpl; intros; auto with zarith; auto. +Qed. -Definition Zgcd_pos : +Lemma Zgcd_pos : forall a b, 0 <= Zgcd a b. +Proof. +intros; unfold Zgcd; apply Zgcdn_pos; auto. +Qed. + +(** We now prove that Zgcd is indeed a gcd. *) + +(** 1) We prove a weaker & easier bound. *) + +Lemma Zgcdn_linear_bound : forall n a b, + Zabs a < Z_of_nat n -> Zis_gcd a b (Zgcdn n a b). +Proof. +induction n. +simpl; intros. +elimtype False; generalize (Zabs_pos a); omega. +destruct a; intros; simpl; + [ generalize (Zis_gcd_0_abs b); intuition | | ]; + unfold Zmod; + generalize (Z_div_mod b (Zpos p) (refl_equal Gt)); + destruct (Zdiv_eucl b (Zpos p)) as (q,r); + intros (H0,H1); + rewrite inj_S in H; simpl Zabs in H; + (assert (H2: Zabs r < Z_of_nat n) by + rewrite Zabs_eq; auto with zarith); + assert (IH:=IHn r (Zpos p) H2); clear IHn; + simpl in IH |- *; + rewrite H0. + apply Zis_gcd_for_euclid2; auto. + apply Zis_gcd_minus; apply Zis_gcd_sym. + apply Zis_gcd_for_euclid2; auto. +Qed. + +(** 2) For Euclid's algorithm, the worst-case situation corresponds + to Fibonacci numbers. Let's define them: *) + +Fixpoint fibonacci (n:nat) : Z := + match n with + | O => 1 + | S O => 1 + | S (S n as p) => fibonacci p + fibonacci n + end. + +Lemma fibonacci_pos : forall n, 0 <= fibonacci n. +Proof. +cut (forall N n, (n<N)%nat -> 0<=fibonacci n). +eauto. +induction N. +inversion 1. +intros. +destruct n. +simpl; auto with zarith. +destruct n. +simpl; auto with zarith. +change (0 <= fibonacci (S n) + fibonacci n). +generalize (IHN n) (IHN (S n)); omega. +Qed. + +Lemma fibonacci_incr : + forall n m, (n<=m)%nat -> fibonacci n <= fibonacci m. +Proof. +induction 1. +auto with zarith. +apply Zle_trans with (fibonacci m); auto. +clear. +destruct m. +simpl; auto with zarith. +change (fibonacci (S m) <= fibonacci (S m)+fibonacci m). +generalize (fibonacci_pos m); omega. +Qed. + +(** 3) We prove that fibonacci numbers are indeed worst-case: + for a given number [n], if we reach a conclusion about [gcd(a,b)] in + exactly [n+1] loops, then [fibonacci (n+1)<=a /\ fibonacci(n+2)<=b] *) + +Lemma Zgcdn_worst_is_fibonacci : forall n a b, + 0 < a < b -> + Zis_gcd a b (Zgcdn (S n) a b) -> + Zgcdn n a b <> Zgcdn (S n) a b -> + fibonacci (S n) <= a /\ + fibonacci (S (S n)) <= b. +Proof. +induction n. +simpl; intros. +destruct a; omega. +intros. +destruct a; [simpl in *; omega| | destruct H; discriminate]. +revert H1; revert H0. +set (m:=S n) in *; (assert (m=S n) by auto); clearbody m. +pattern m at 2; rewrite H0. +simpl Zgcdn. +unfold Zmod; generalize (Z_div_mod b (Zpos p) (refl_equal Gt)). +destruct (Zdiv_eucl b (Zpos p)) as (q,r). +intros (H1,H2). +destruct H2. +destruct (Zle_lt_or_eq _ _ H2). +generalize (IHn _ _ (conj H4 H3)). +intros H5 H6 H7. +replace (fibonacci (S (S m))) with (fibonacci (S m) + fibonacci m) by auto. +assert (r = Zpos p * (-q) + b) by rewrite H1; ring. +destruct H5; auto. +pattern r at 1; rewrite H8. +apply Zis_gcd_sym. +apply Zis_gcd_for_euclid2; auto. +apply Zis_gcd_sym; auto. +split; auto. +rewrite H1. +apply Zplus_le_compat; auto. +apply Zle_trans with (Zpos p * 1); auto. +ring (Zpos p * 1); auto. +apply Zmult_le_compat_l. +destruct q. +omega. +assert (0 < Zpos p0) by compute; auto. +omega. +assert (Zpos p * Zneg p0 < 0) by compute; auto. +omega. +compute; intros; discriminate. +(* r=0 *) +subst r. +simpl; rewrite H0. +intros. +simpl in H4. +simpl in H5. +destruct n. +simpl in H5. +simpl. +omega. +simpl in H5. +elim H5; auto. +Qed. + +(** 3b) We reformulate the previous result in a more positive way. *) + +Lemma Zgcdn_ok_before_fibonacci : forall n a b, + 0 < a < b -> a < fibonacci (S n) -> + Zis_gcd a b (Zgcdn n a b). +Proof. +destruct a; [ destruct 1; elimtype False; omega | | destruct 1; discriminate]. +cut (forall k n b, + k = (S (nat_of_P p) - n)%nat -> + 0 < Zpos p < b -> Zpos p < fibonacci (S n) -> + Zis_gcd (Zpos p) b (Zgcdn n (Zpos p) b)). +destruct 2; eauto. +clear n; induction k. +intros. +assert (nat_of_P p < n)%nat by omega. +apply Zgcdn_linear_bound. +simpl. +generalize (inj_le _ _ H2). +rewrite inj_S. +rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto. +omega. +intros. +generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros. +assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)). + apply IHk; auto. + omega. + replace (fibonacci (S (S n))) with (fibonacci (S n)+fibonacci n) by auto. + generalize (fibonacci_pos n); omega. +replace (Zgcdn n (Zpos p) b) with (Zgcdn (S n) (Zpos p) b); auto. +generalize (H2 H3); clear H2 H3; omega. +Qed. + +(** 4) The proposed bound leads to a fibonacci number that is big enough. *) + +Lemma Zgcd_bound_fibonacci : + forall a, 0 < a -> a < fibonacci (Zgcd_bound a). +Proof. +destruct a; [omega| | intro H; discriminate]. +intros _. +induction p. +simpl Zgcd_bound in *. +rewrite Zpos_xI. +rewrite plus_comm; simpl plus. +set (n:=S (Psiz p+Psiz p)) in *. +change (2*Zpos p+1 < + fibonacci (S n) + fibonacci n + fibonacci (S n)). +generalize (fibonacci_pos n). +omega. +simpl Zgcd_bound in *. +rewrite Zpos_xO. +rewrite plus_comm; simpl plus. +set (n:= S (Psiz p +Psiz p)) in *. +change (2*Zpos p < + fibonacci (S n) + fibonacci n + fibonacci (S n)). +generalize (fibonacci_pos n). +omega. +simpl; auto with zarith. +Qed. + +(* 5) the end: we glue everything together and take care of + situations not corresponding to [0<a<b]. *) + +Lemma Zgcd_is_gcd : + forall a b, Zis_gcd a b (Zgcd a b). +Proof. +unfold Zgcd; destruct a; intros. +simpl; generalize (Zis_gcd_0_abs b); intuition. +(*Zpos*) +generalize (Zgcd_bound_fibonacci (Zpos p)). +simpl Zgcd_bound. +set (n:=S (Psiz p+Psiz p)); (assert (n=S (Psiz p+Psiz p)) by auto); clearbody n. +simpl Zgcdn. +unfold Zmod. +generalize (Z_div_mod b (Zpos p) (refl_equal Gt)). +destruct (Zdiv_eucl b (Zpos p)) as (q,r). +intros (H1,H2) H3. +rewrite H1. +apply Zis_gcd_for_euclid2. +destruct H2. +destruct (Zle_lt_or_eq _ _ H0). +apply Zgcdn_ok_before_fibonacci; auto; omega. +subst r n; simpl. +apply Zis_gcd_sym; apply Zis_gcd_0. +(*Zneg*) +generalize (Zgcd_bound_fibonacci (Zpos p)). +simpl Zgcd_bound. +set (n:=S (Psiz p+Psiz p)); (assert (n=S (Psiz p+Psiz p)) by auto); clearbody n. +simpl Zgcdn. +unfold Zmod. +generalize (Z_div_mod b (Zpos p) (refl_equal Gt)). +destruct (Zdiv_eucl b (Zpos p)) as (q,r). +intros (H1,H2) H3. +rewrite H1. +apply Zis_gcd_minus. +apply Zis_gcd_sym. +apply Zis_gcd_for_euclid2. +destruct H2. +destruct (Zle_lt_or_eq _ _ H0). +apply Zgcdn_ok_before_fibonacci; auto; omega. +subst r n; simpl. +apply Zis_gcd_sym; apply Zis_gcd_0. +Qed. + +(** A generalized gcd: it additionnally keeps track of the divisors. *) + +Fixpoint Zggcdn (n:nat) : Z -> Z -> (Z*(Z*Z)) := fun a b => + match n with + | O => (1,(a,b)) (*(Zabs b,(0,Zsgn b))*) + | S n => match a with + | Z0 => (Zabs b,(0,Zsgn b)) + | Zpos _ => + let (q,r) := Zdiv_eucl b a in (* b = q*a+r *) + let (g,p) := Zggcdn n r a in + let (rr,aa) := p in (* r = g *rr /\ a = g * aa *) + (g,(aa,q*aa+rr)) + | Zneg a => + let (q,r) := Zdiv_eucl b (Zpos a) in (* b = q*(-a)+r *) + let (g,p) := Zggcdn n r (Zpos a) in + let (rr,aa) := p in (* r = g*rr /\ (-a) = g * aa *) + (g,(-aa,q*aa+rr)) + end + end. + +Definition Zggcd a b : Z * (Z * Z) := Zggcdn (Zgcd_bound a) a b. + +(** The first component of [Zggcd] is [Zgcd] *) + +Lemma Zggcdn_gcdn : forall n a b, + fst (Zggcdn n a b) = Zgcdn n a b. +Proof. +induction n; simpl; auto. +destruct a; unfold Zmod; simpl; intros; auto; + destruct (Zdiv_eucl b (Zpos p)) as (q,r); + rewrite <- IHn; + destruct (Zggcdn n r (Zpos p)) as (g,(rr,aa)); simpl; auto. +Qed. + +Lemma Zggcd_gcdn : forall a b, fst (Zggcd a b) = Zgcd a b. +Proof. +intros; unfold Zggcd, Zgcd; apply Zggcdn_gcdn; auto. +Qed. + +(** [Zggcd] always returns divisors that are coherent with its + first output. *) + +Lemma Zggcdn_correct_divisors : forall n a b, + let (g,p) := Zggcdn n a b in + let (aa,bb):=p in + a=g*aa /\ b=g*bb. +Proof. +induction n. +simpl. +split; [destruct a|destruct b]; auto. +intros. +simpl. +destruct a. +rewrite Zmult_comm; simpl. +split; auto. +symmetry; apply Zabs_Zsgn. +generalize (Z_div_mod b (Zpos p)); +destruct (Zdiv_eucl b (Zpos p)) as (q,r). +generalize (IHn r (Zpos p)); +destruct (Zggcdn n r (Zpos p)) as (g,(rr,aa)). +intuition. +destruct H0. +compute; auto. +rewrite H; rewrite H1; rewrite H2; ring. +generalize (Z_div_mod b (Zpos p)); +destruct (Zdiv_eucl b (Zpos p)) as (q,r). +destruct 1. +compute; auto. +generalize (IHn r (Zpos p)); +destruct (Zggcdn n r (Zpos p)) as (g,(rr,aa)). +intuition. +destruct H0. +replace (Zneg p) with (-Zpos p) by compute; auto. +rewrite H4; ring. +rewrite H; rewrite H4; rewrite H0; ring. +Qed. + +Lemma Zggcd_correct_divisors : forall a b, + let (g,p) := Zggcd a b in + let (aa,bb):=p in + a=g*aa /\ b=g*bb. +Proof. +unfold Zggcd; intros; apply Zggcdn_correct_divisors; auto. +Qed. + +(** Due to the use of an explicit measure, the extraction of [Zgcd] + isn't optimal. We propose here another version [Zgcd_spec] that + doesn't suffer from this problem (but doesn't compute in Coq). *) + +Definition Zgcd_spec_pos : forall a:Z, 0 <= a -> forall b:Z, {g : Z | 0 <= a -> Zis_gcd a b g /\ g >= 0}. Proof. @@ -382,16 +763,7 @@ apply try assumption. intro x; case x. intros _ _ b; exists (Zabs b). - elim (Z_le_lt_eq_dec _ _ (Zabs_pos b)). - intros H0; split. - apply Zabs_ind. - intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto. - intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto. - auto with zarith. - - intros H0; rewrite <- H0. - rewrite <- (Zabs_Zsgn b); rewrite <- H0; simpl in |- *. - split; [ apply Zis_gcd_0 | idtac ]; auto with zarith. +generalize (Zis_gcd_0_abs b); intuition. intros p Hrec _ b. generalize (Z_div_mod b (Zpos p)). @@ -414,25 +786,15 @@ Proof. intros a; case (Z_gt_le_dec 0 a). intros; assert (0 <= - a). omega. -elim (Zgcd_pos (- a) H b); intros g Hgkl. +elim (Zgcd_spec_pos (- a) H b); intros g Hgkl. exists g. intuition. -intros Ha b; elim (Zgcd_pos a Ha b); intros g; exists g; intuition. +intros Ha b; elim (Zgcd_spec_pos a Ha b); intros g; exists g; intuition. Defined. -Definition Zgcd (a b:Z) := let (g, _) := Zgcd_spec a b in g. - -Lemma Zgcd_is_pos : forall a b:Z, Zgcd a b >= 0. -intros a b; unfold Zgcd in |- *; case (Zgcd_spec a b); tauto. -Qed. - -Lemma Zgcd_is_gcd : forall a b:Z, Zis_gcd a b (Zgcd a b). -intros a b; unfold Zgcd in |- *; case (Zgcd_spec a b); tauto. -Qed. +(** A last version aimed at extraction that also returns the divisors. *) -(** A version of gcd that stores coefficients (used for fraction reduction) *) - -Definition Zgcd_gen_pos : +Definition Zggcd_spec_pos : forall a:Z, 0 <= a -> forall b:Z, {p : Z*(Z*Z) | let (g,p):=p in let (aa,bb):=p in 0 <= a -> Zis_gcd a b g /\ g >= 0 /\ a=g*aa /\ b=g*bb}. @@ -441,17 +803,7 @@ intros a Ha. pattern a; apply Zlt_0_rec; try assumption. intro x; case x. intros _ _ b; exists (Zabs b,(0,Zsgn b)). - elim (Z_le_lt_eq_dec _ _ (Zabs_pos b)). - intros H0; split. - apply Zabs_ind. - intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto. - intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto. - repeat split; auto with zarith. - symmetry; apply Zabs_Zsgn. - - intros H0; rewrite <- H0. - rewrite <- (Zabs_Zsgn b); rewrite <- H0; simpl in |- *. - split; [ apply Zis_gcd_0 | idtac ]; auto with zarith. +intros _; apply Zis_gcd_0_abs. intros p Hrec _ b. generalize (Z_div_mod b (Zpos p)). @@ -471,129 +823,22 @@ intros p _ H b. elim H; auto. Defined. -Definition Zgcd_gen_spec : +Definition Zggcd_spec : forall a b:Z, {p : Z*(Z*Z) | let (g,p):=p in let (aa,bb):=p in Zis_gcd a b g /\ g >= 0 /\ a=g*aa /\ b=g*bb}. Proof. intros a; case (Z_gt_le_dec 0 a). intros; assert (0 <= - a). omega. -destruct (Zgcd_gen_pos (- a) H b) as ((g,(aa,bb)),Hgkl). +destruct (Zggcd_spec_pos (- a) H b) as ((g,(aa,bb)),Hgkl). exists (g,(-aa,bb)). intuition. rewrite <- Zopp_mult_distr_r. rewrite <- H2; auto with zarith. -intros Ha b; elim (Zgcd_gen_pos a Ha b); intros p; exists p. +intros Ha b; elim (Zggcd_spec_pos a Ha b); intros p; exists p. repeat destruct p; intuition. Defined. -Definition Zgcd_gen (a b:Z) := let (p, _) := Zgcd_gen_spec a b in p. - -(** a last version of [Zgcd] that can compute within Coq. - We use an explicit measure in [nat], that should at least be - bigger than the absolute value of the first argument. - (in fact, bigger than the log of the first argument should be enough - ...TO CHECK) -*) - -Fixpoint Zgcd_gen' (n:nat) : Z -> Z -> (Z*(Z*Z)) := fun a b => - match n with - | O => (Zabs b,(0,Zsgn b)) - | S n => match a with - | Z0 => (Zabs b,(0,Zsgn b)) - | Zpos _ => - let (q,r) := Zdiv_eucl b a in (* b = q*a+r *) - let (g,p) := Zgcd_gen' n r a in - let (rr,aa) := p in (* r = g *rr /\ a = g * aa *) - (g,(aa,q*aa+rr)) - | Zneg a => - let (q,r) := Zdiv_eucl b (Zpos a) in (* b = q*(-a)+r *) - let (g,p) := Zgcd_gen' n r (Zpos a) in - let (rr,aa) := p in (* r = g*rr /\ (-a) = g * aa *) - (g,(-aa,q*aa+rr)) - end - end. - -Lemma Zgcd_gen'_correct : forall n a b, - Zabs a <= Z_of_nat n -> - let (g,p) := Zgcd_gen' n a b in - let (aa,bb):=p in - Zis_gcd a b g /\ g >= 0 /\ a=g*aa /\ b=g*bb. -Proof. -induction n. -simpl; intros. -destruct a; simpl in *; [|elim H|elim H]; auto. - elim (Z_le_lt_eq_dec _ _ (Zabs_pos b)). - intros H0; split. - apply Zabs_ind. - intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto. - intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto. - repeat split; auto with zarith. - symmetry; apply Zabs_Zsgn. - - intros H0; rewrite <- H0. - rewrite <- (Zabs_Zsgn b); rewrite <- H0; simpl in |- *. - split; [ apply Zis_gcd_0 | idtac ]; auto with zarith. -destruct a. -clear IHn; intros b _; simpl. - elim (Z_le_lt_eq_dec _ _ (Zabs_pos b)). - intros H0; split. - apply Zabs_ind. - intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto. - intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto. - repeat split; auto with zarith. - symmetry; apply Zabs_Zsgn. - - intros H0; rewrite <- H0. - rewrite <- (Zabs_Zsgn b); rewrite <- H0; simpl in |- *. - split; [ apply Zis_gcd_0 | idtac ]; auto with zarith. -intros; simpl. - generalize (Z_div_mod b (Zpos p)). - destruct (Zdiv_eucl b (Zpos p)) as (q,r). - destruct 1; auto with zarith. - rewrite inj_S in H; simpl Zabs in H. - assert (Zabs r <= Z_of_nat n) by - rewrite Zabs_eq; auto with zarith. - generalize (IHn r (Zpos p) H2). - destruct (Zgcd_gen' n r (Zpos p)) as (g,(rr,aa)). - intros (H3,(H4,(H5,H6))). - split. - rewrite H0. - apply Zis_gcd_for_euclid2; auto. - repeat split; auto. - rewrite H0; rewrite H6; rewrite H5; ring. -intros; simpl. - generalize (Z_div_mod b (Zpos p)). - destruct (Zdiv_eucl b (Zpos p)) as (q,r). - destruct 1; auto with zarith. - rewrite inj_S in H; simpl Zabs in H. - assert (Zabs r <= Z_of_nat n) by - rewrite Zabs_eq; auto with zarith. - generalize (IHn r (Zpos p) H2). - destruct (Zgcd_gen' n r (Zpos p)) as (g,(rr,aa)). - intros (H3,(H4,(H5,H6))). - split. - rewrite H0. - apply Zis_gcd_minus. - apply Zis_gcd_sym; simpl Zopp. - apply Zis_gcd_for_euclid2; auto. - repeat split; auto. - replace (Zneg p) with (- Zpos p) by auto. - rewrite H6; ring. - rewrite H0; rewrite H6; rewrite H5; ring. -Qed. - -(** To speedup things, one way is to factor first the binary 0 digits - TO BE USED. *) - -Fixpoint Pfactor_twos (p p':positive) {struct p} : (positive*(positive*positive)) := - match p, p' with - | xO p, xO p' => let (g,p) := Pfactor_twos p p' in - let (a,b) := p in - (xO g,(a,b)) - | _, _ => (xH,(p,p')) - end. - (** * Relative primality *) Definition rel_prime (a b:Z) : Prop := Zis_gcd a b 1. |