diff options
Diffstat (limited to 'plugins/setoid_ring/Field_theory.v')
-rw-r--r-- | plugins/setoid_ring/Field_theory.v | 132 |
1 files changed, 46 insertions, 86 deletions
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index ccdec656..40138526 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -96,7 +96,7 @@ Hint Resolve (ARadd_0_l ARth) (ARadd_comm ARth) (ARadd_assoc ARth) (ARsub_def ARth) . (* Power coefficients *) - Variable Cpow : Set. + Variable Cpow : Type. Variable Cp_phi : N -> Cpow. Variable rpow : R -> Cpow -> R. Variable pow_th : power_theory rI rmul req Cp_phi rpow. @@ -390,52 +390,16 @@ Qed. ***************************************************************************) -Fixpoint positive_eq (p1 p2 : positive) {struct p1} : bool := - match p1, p2 with - xH, xH => true - | xO p3, xO p4 => positive_eq p3 p4 - | xI p3, xI p4 => positive_eq p3 p4 - | _, _ => false - end. - -Theorem positive_eq_correct: - forall p1 p2, if positive_eq p1 p2 then p1 = p2 else p1 <> p2. -intros p1; elim p1; - (try (intros p2; case p2; simpl; auto; intros; discriminate)). -intros p3 rec p2; case p2; simpl; auto; (try (intros; discriminate)); intros p4. -generalize (rec p4); case (positive_eq p3 p4); auto. -intros H1; apply f_equal with ( f := xI ); auto. -intros H1 H2; case H1; injection H2; auto. -intros p3 rec p2; case p2; simpl; auto; (try (intros; discriminate)); intros p4. -generalize (rec p4); case (positive_eq p3 p4); auto. -intros H1; apply f_equal with ( f := xO ); auto. -intros H1 H2; case H1; injection H2; auto. -Qed. - -Definition N_eq n1 n2 := - match n1, n2 with - | N0, N0 => true - | Npos p1, Npos p2 => positive_eq p1 p2 - | _, _ => false - end. - -Lemma N_eq_correct : forall n1 n2, if N_eq n1 n2 then n1 = n2 else n1 <> n2. -Proof. - intros [ |p1] [ |p2];simpl;trivial;try(intro H;discriminate H;fail). - assert (H:=positive_eq_correct p1 p2);destruct (positive_eq p1 p2); - [rewrite H;trivial | intro H1;injection H1;subst;apply H;trivial]. -Qed. - (* equality test *) Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool := match e1, e2 with PEc c1, PEc c2 => ceqb c1 c2 - | PEX p1, PEX p2 => positive_eq p1 p2 + | PEX p1, PEX p2 => Pos.eqb p1 p2 | PEadd e3 e5, PEadd e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false | PEsub e3 e5, PEsub e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false | PEmul e3 e5, PEmul e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false | PEopp e3, PEopp e4 => PExpr_eq e3 e4 - | PEpow e3 n3, PEpow e4 n4 => if N_eq n3 n4 then PExpr_eq e3 e4 else false + | PEpow e3 n3, PEpow e4 n4 => if N.eqb n3 n4 then PExpr_eq e3 e4 else false | _, _ => false end. @@ -460,8 +424,7 @@ intros l e1; elim e1. intros c1; intros e2; elim e2; simpl; (try (intros; discriminate)). intros c2; apply (morph_eq CRmorph). intros p1; intros e2; elim e2; simpl; (try (intros; discriminate)). -intros p2; generalize (positive_eq_correct p1 p2); case (positive_eq p1 p2); - (try (intros; discriminate)); intros H; rewrite H; auto. +intros p2; case Pos.eqb_spec; intros; now subst. intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)). intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4); (try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6); @@ -478,9 +441,8 @@ intros e3 rec e2; (case e2; simpl; (try (intros; discriminate))). intros e4; generalize (rec e4); case (PExpr_eq e3 e4); (try (intros; discriminate)); auto. intros e3 rec n3 e2;(case e2;simpl;(try (intros;discriminate))). -intros e4 n4;generalize (N_eq_correct n3 n4);destruct (N_eq n3 n4); -intros;try discriminate. -repeat rewrite pow_th.(rpow_pow_N);rewrite H;rewrite (rec _ H0);auto. +intros e4 n4; case N.eqb_spec; try discriminate; intros EQ H; subst. +repeat rewrite pow_th.(rpow_pow_N). rewrite (rec _ H);auto. Qed. (* add *) @@ -507,7 +469,7 @@ Definition NPEpow x n := match n with | N0 => PEc cI | Npos p => - if positive_eq p xH then x else + if Pos.eqb p xH then x else match x with | PEc c => if ceqb c cI then PEc cI else if ceqb c cO then PEc cO else PEc (pow_pos cmul c p) @@ -520,10 +482,10 @@ Theorem NPEpow_correct : forall l e n, Proof. destruct n;simpl. rewrite pow_th.(rpow_pow_N);simpl;auto. - generalize (positive_eq_correct p xH). - destruct (positive_eq p 1);intros. - rewrite H;rewrite pow_th.(rpow_pow_N). trivial. - clear H;destruct e;simpl;auto. + fold (p =? 1)%positive. + case Pos.eqb_spec; intros H; (rewrite H || clear H). + now rewrite pow_th.(rpow_pow_N). + destruct e;simpl;auto. repeat apply ceqb_rect;simpl;intros;rewrite pow_th.(rpow_pow_N);simpl. symmetry;induction p;simpl;trivial; ring [IHp H CRmorph.(morph1)]. symmetry; induction p;simpl;trivial;ring [IHp CRmorph.(morph0)]. @@ -539,7 +501,7 @@ Fixpoint NPEmul (x y : PExpr C) {struct x} : PExpr C := | _, PEc c => if ceqb c cI then x else if ceqb c cO then PEc cO else PEmul x y | PEpow e1 n1, PEpow e2 n2 => - if N_eq n1 n2 then NPEpow (NPEmul e1 e2) n1 else PEmul x y + if N.eqb n1 n2 then NPEpow (NPEmul e1 e2) n1 else PEmul x y | _, _ => PEmul x y end. @@ -554,10 +516,10 @@ induction e1;destruct e2; simpl in |- *;try reflexivity; try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; try reflexivity; try ring [(morph0 CRmorph) (morph1 CRmorph)]. apply (morph_mul CRmorph). -assert (H:=N_eq_correct n n0);destruct (N_eq n n0). +case N.eqb_spec; intros H; try rewrite <- H; clear H. rewrite NPEpow_correct. simpl. repeat rewrite pow_th.(rpow_pow_N). -rewrite IHe1;rewrite <- H;destruct n;simpl;try ring. +rewrite IHe1; destruct n;simpl;try ring. apply pow_pos_mul. simpl;auto. Qed. @@ -760,6 +722,14 @@ Fixpoint isIn (e1:PExpr C) (p1:positive) Notation pow_pos_plus := (Ring_theory.pow_pos_Pplus _ Rsth Reqe.(Rmul_ext) ARth.(ARmul_comm) ARth.(ARmul_assoc)). + Lemma Z_pos_sub_gt : forall p q, (p > q)%positive -> + Z.pos_sub p q = Zpos (p - q). + Proof. + intros. apply Z.pos_sub_gt. now apply Pos.gt_lt. + Qed. + + Ltac simpl_pos_sub := rewrite ?Z_pos_sub_gt in * by assumption. + Lemma isIn_correct_aux : forall l e1 e2 p1 p2, match (if PExpr_eq e1 e2 then @@ -779,10 +749,12 @@ Fixpoint isIn (e1:PExpr C) (p1:positive) Proof. intros l e1 e2 p1 p2; generalize (PExpr_eq_semi_correct l e1 e2); case (PExpr_eq e1 e2); simpl; auto; intros H. - case_eq ((p1 ?= p2)%positive Eq);intros;simpl. + rewrite Z.pos_sub_spec. + case_eq ((p1 ?= p2)%positive);intros;simpl. repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:refine (refl_equal _). rewrite (Pcompare_Eq_eq _ _ H0). rewrite H by trivial. ring [ (morph1 CRmorph)]. + fold (p2 - p1 =? 1)%positive. fold (NPEpow e2 (Npos (p2 - p1))). rewrite NPEpow_correct;simpl. repeat rewrite pow_th.(rpow_pow_N);simpl. @@ -790,22 +762,17 @@ Proof. rewrite <- pow_pos_plus; rewrite Pplus_minus;auto. apply ZC2;trivial. repeat rewrite pow_th.(rpow_pow_N);simpl. rewrite H;trivial. - change (ZtoN - match (p1 ?= p1 - p2)%positive Eq with - | Eq => 0 - | Lt => Zneg (p1 - p2 - p1) - | Gt => Zpos (p1 - (p1 - p2)) - end) with (ZtoN (Zpos p1 - Zpos (p1 -p2))). + change (Z.pos_sub p1 (p1-p2)) with (Zpos p1 - Zpos (p1 -p2))%Z. replace (Zpos (p1 - p2)) with (Zpos p1 - Zpos p2)%Z. split. repeat rewrite Zth.(Rsub_def). rewrite (Ring_theory.Ropp_add Zsth Zeqe Zth). - rewrite Zplus_assoc. simpl. rewrite Pcompare_refl. simpl. + rewrite Zplus_assoc, Z.add_opp_diag_r. simpl. ring [ (morph1 CRmorph)]. assert (Zpos p1 > 0 /\ Zpos p2 > 0)%Z. split;refine (refl_equal _). apply Zplus_gt_reg_l with (Zpos p2). rewrite Zplus_minus. change (Zpos p2 + Zpos p1 > 0 + Zpos p1)%Z. apply Zplus_gt_compat_r. refine (refl_equal _). - simpl;rewrite H0;trivial. + simpl. now simpl_pos_sub. Qed. Lemma pow_pos_pow_pos : forall x p1 p2, pow_pos rmul (pow_pos rmul x p1) p2 == pow_pos rmul x (p1*p2). @@ -835,7 +802,7 @@ destruct n. destruct n;simpl. rewrite NPEmul_correct;repeat rewrite pow_th.(rpow_pow_N);simpl. intros (H1,H2) (H3,H4). - unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3. + simpl_pos_sub. simpl in H3. rewrite pow_pos_mul. rewrite H1;rewrite H3. assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 * (pow_pos rmul (NPEeval l e1) p4 * NPEeval l p5) == @@ -845,11 +812,10 @@ destruct n. split. symmetry;apply ARth.(ARmul_assoc). refine (refl_equal _). trivial. repeat rewrite pow_th.(rpow_pow_N);simpl. intros (H1,H2) (H3,H4). - unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3. - rewrite H2 in H1;simpl in H1. + simpl_pos_sub. simpl in H1, H3. assert (Zpos p1 > Zpos p6)%Z. apply Zgt_trans with (Zpos p4). exact H4. exact H2. - unfold Zgt in H;simpl in H;rewrite H. + simpl_pos_sub. split. 2:exact H. rewrite pow_pos_mul. simpl;rewrite H1;rewrite H3. assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 * @@ -863,11 +829,11 @@ destruct n. (Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z. change ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z). rewrite <- Zplus_assoc. rewrite (Zplus_assoc (- Zpos p4)). - simpl. rewrite Pcompare_refl. simpl. reflexivity. + simpl. rewrite Z.pos_sub_diag. simpl. reflexivity. unfold Zminus, Zopp in H0. simpl in H0. - rewrite H2 in H0;rewrite H4 in H0;rewrite H in H0. inversion H0;trivial. + simpl_pos_sub. inversion H0; trivial. simpl. repeat rewrite pow_th.(rpow_pow_N). - intros H1 (H2,H3). unfold Zgt in H3;simpl in H3. rewrite H3 in H2;rewrite H3. + intros H1 (H2,H3). simpl_pos_sub. rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl. simpl in H2. rewrite pow_th.(rpow_pow_N);simpl. rewrite pow_pos_mul. split. ring [H2]. exact H3. @@ -878,8 +844,7 @@ destruct n. rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl. repeat rewrite pow_th.(rpow_pow_N);simpl. rewrite pow_pos_mul. intros (H1, H2);rewrite H1;split. - unfold Zgt in H2;simpl in H2;rewrite H2;rewrite H2 in H1. - simpl in H1;ring [H1]. trivial. + simpl_pos_sub. simpl in H1;ring [H1]. trivial. trivial. destruct n. trivial. generalize (H p1 (p0*p2)%positive);clear H;destruct (isIn e1 p1 p (p0*p2)). destruct p3. @@ -937,8 +902,7 @@ Proof. repeat rewrite NPEpow_correct;simpl; repeat rewrite pow_th.(rpow_pow_N);simpl). intros (H, Hgt);split;try ring [H CRmorph.(morph1)]. - intros (H, Hgt). unfold Zgt in Hgt;simpl in Hgt;rewrite Hgt in H. - simpl in H;split;try ring [H]. + intros (H, Hgt). simpl_pos_sub. simpl in H;split;try ring [H]. rewrite <- pow_pos_plus. rewrite Pplus_minus. reflexivity. trivial. simpl;intros. repeat rewrite NPEmul_correct;simpl. rewrite NPEpow_correct;simpl. split;ring [CRmorph.(morph1)]. @@ -1805,25 +1769,24 @@ Lemma gen_phiPOS_inj : forall x y, x = y. intros x y. repeat rewrite <- (same_gen Rsth Reqe ARth) in |- *. -ElimPcompare x y; intro. +case (Pos.compare_spec x y). + intros. + trivial. intros. - apply Pcompare_Eq_eq; trivial. - intro. elim gen_phiPOS_not_0 with (y - x)%positive. apply add_inj_r with x. symmetry in |- *. rewrite (ARadd_0_r Rsth ARth) in |- *. rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth) in |- *. rewrite Pplus_minus in |- *; trivial. - change Eq with (CompOpp Eq) in |- *. - rewrite <- Pcompare_antisym in |- *; trivial. - rewrite H in |- *; trivial. - intro. + now apply Pos.lt_gt. + intros. elim gen_phiPOS_not_0 with (x - y)%positive. apply add_inj_r with y. rewrite (ARadd_0_r Rsth ARth) in |- *. rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth) in |- *. rewrite Pplus_minus in |- *; trivial. + now apply Pos.lt_gt. Qed. @@ -1841,12 +1804,9 @@ Qed. Lemma gen_phiN_complete : forall x y, gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y -> - Neq_bool x y = true. -intros. - replace y with x. - unfold Neq_bool in |- *. - rewrite Ncompare_refl in |- *; trivial. - apply gen_phiN_inj; trivial. + N.eqb x y = true. +Proof. +intros. now apply N.eqb_eq, gen_phiN_inj. Qed. End AlmostField. |