diff options
Diffstat (limited to 'contrib/setoid_ring')
-rw-r--r-- | contrib/setoid_ring/Field_tac.v | 2 | ||||
-rw-r--r-- | contrib/setoid_ring/Field_theory.v (renamed from contrib/setoid_ring/Field.v) | 0 | ||||
-rw-r--r-- | contrib/setoid_ring/RealField.v | 547 | ||||
-rw-r--r-- | contrib/setoid_ring/newring.ml4 | 4 |
4 files changed, 43 insertions, 510 deletions
diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v index 802dd1d53..b16afad8d 100644 --- a/contrib/setoid_ring/Field_tac.v +++ b/contrib/setoid_ring/Field_tac.v @@ -7,7 +7,7 @@ (************************************************************************) Require Import Ring_tac Ring_polynom InitialRing. -Require Export Field. +Require Export Field_theory. (* syntaxification *) Ltac mkFieldexpr C Cst radd rmul rsub ropp rdiv rinv t fv := diff --git a/contrib/setoid_ring/Field.v b/contrib/setoid_ring/Field_theory.v index 469f2537c..469f2537c 100644 --- a/contrib/setoid_ring/Field.v +++ b/contrib/setoid_ring/Field_theory.v diff --git a/contrib/setoid_ring/RealField.v b/contrib/setoid_ring/RealField.v index 8793e3622..256354d78 100644 --- a/contrib/setoid_ring/RealField.v +++ b/contrib/setoid_ring/RealField.v @@ -1,18 +1,10 @@ -Require Import Ring_polynom InitialRing Field Field_tac Ring. - +Require Import Raxioms. Require Export Rdefinitions. -Require Export Raxioms. -Require Export RIneq. +Require Import Ring Field. -Section RField. +Open Local Scope R_scope. -Notation NPEeval := (PEeval 0%R Rplus Rmult Rminus Ropp - (gen_phiZ 0%R 1%R Rplus Rmult Ropp)). -Notation NPCond := - (PCond _ 0%R Rplus Rmult Rminus Ropp (@eq R) _ - (gen_phiZ 0%R 1%R Rplus Rmult Ropp)). -(* -Lemma RTheory : ring_theory 0%R 1%R Rplus Rmult Rminus Ropp (eq (A:=R)). +Lemma RTheory : ring_theory 0 1 Rplus Rmult Rminus Ropp (eq (A:=R)). Proof. constructor. intro; apply Rplus_0_l. @@ -29,17 +21,18 @@ constructor. reflexivity. exact Rplus_opp_r. Qed. -Add Ring Rring : RTheory Abstract. -*) -Notation Rset := (Eqsth R). -Notation Rext := (Eq_ext Rplus Rmult Ropp). -Notation Rmorph := (gen_phiZ_morph Rset Rext RTheory). -(* -Adds Field RF : Rfield Abstract. -*) +Lemma Rfield : + field_theory R 0 1 Rplus Rmult Rminus Ropp Rdiv Rinv (eq(A:=R)). +Proof. +constructor. + exact RTheory. + exact R1_neq_R0. + reflexivity. + exact Rinv_l. +Qed. -Lemma Rlt_n_Sn : forall x, (x < x + 1)%R. +Lemma Rlt_n_Sn : forall x, x < x + 1. Proof. intro. elim archimed with x; intros. @@ -60,514 +53,54 @@ destruct H0. rewrite Rplus_0_l in |- *; trivial. Qed. +Notation Rset := (Eqsth R). +Notation Rext := (Eq_ext Rplus Rmult Ropp). -(* -Lemma Rdiscr_0_2 : (2 <> 0)%R. -red in |- *; intro. -assert (0 < 1)%R. - elim (archimed 0); intros. - unfold Rminus in H1. - rewrite (ARopp_zero Rset Rext (Rth_ARth Rset Rext RTheory)) in H1. - rewrite (ARadd_0_r Rset (Rth_ARth Rset Rext RTheory)) in H1. - destruct H1. - apply Rlt_trans with (IZR (up 0)); trivial. - elim H1; trivial. - assert (1 < 2)%R. - pattern 1%R at 1 in |- *. - replace 1%R with (1 + 0)%R. +Lemma Rlt_0_2 : 0 < 2. +apply Rlt_trans with (0 + 1). + apply Rlt_n_Sn. + rewrite Rplus_comm in |- *. apply Rplus_lt_compat_l. - trivial. - rewrite (ARadd_0_r Rset (Rth_ARth Rset Rext RTheory)) in |- *. - trivial. - apply (Rlt_asym 0 1); trivial. - elim H; trivial. + replace 1 with (0 + 1). + apply Rlt_n_Sn. + apply Rplus_0_l. Qed. -*) -Lemma Rgen_phiPOS : forall x, (gen_phiPOS1 1 Rplus Rmult x > 0)%R. +Lemma Rgen_phiPOS : forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x > 0. unfold Rgt in |- *. induction x; simpl in |- *; intros. - apply Rlt_trans with (1 + 0)%R. + apply Rlt_trans with (1 + 0). rewrite Rplus_comm in |- *. apply Rlt_n_Sn. apply Rplus_lt_compat_l. - rewrite <- (Rmul_0_l Rset Rext RTheory 2%R) in |- *. + rewrite <- (Rmul_0_l Rset Rext RTheory 2) in |- *. rewrite Rmult_comm in |- *. apply Rmult_lt_compat_l. - apply Rlt_trans with (0 + 1)%R. - apply Rlt_n_Sn. - rewrite Rplus_comm in |- *. - apply Rplus_lt_compat_l. - replace 1%R with (0 + 1)%R; auto with real. + apply Rlt_0_2. trivial. - rewrite <- (Rmul_0_l Rset Rext RTheory 2%R) in |- *. + rewrite <- (Rmul_0_l Rset Rext RTheory 2) in |- *. rewrite Rmult_comm in |- *. apply Rmult_lt_compat_l. - apply Rlt_trans with (0 + 1)%R. - apply Rlt_n_Sn. - rewrite Rplus_comm in |- *. - apply Rplus_lt_compat_l. - replace 1%R with (0 + 1)%R; auto with real. + apply Rlt_0_2. trivial. - auto with real. + replace 1 with (0 + 1). + apply Rlt_n_Sn. + apply Rplus_0_l. Qed. -(* -unfold Rgt in |- *. -induction x; simpl in |- *; intros. - apply Rplus_lt_0_compat; auto with real. - apply Rmult_lt_0_compat; auto with real. - apply Rmult_lt_0_compat; auto with real. - auto with real. -*) -Lemma Rgen_phiPOS_not_0 : forall x, (gen_phiPOS1 1 Rplus Rmult x <> 0)%R. + +Lemma Rgen_phiPOS_not_0 : + forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x <> 0. red in |- *; intros. specialize (Rgen_phiPOS x). rewrite H in |- *; intro. apply (Rlt_asym 0 0); trivial. Qed. - - -Let ARfield := - F2AF _ _ _ _ _ _ _ _ _ _ Rset Rext Rfield. - -(*Let Rring := AF_AR _ _ _ _ _ _ _ _ _ _ ARfield.*) - -Notation NPFcons_inv := - (PFcons_fcons_inv - _ _ _ _ _ _ _ _ Rset Rext ARfield _ _ _ _ _ _ _ _ _ Rmorph). - - -(* -Theorem SRinv_ext: forall p q:R, p=q -> (/p = /q)%R. -intros p q; apply f_equal with ( f := Rinv ); auto. -Qed. - -Add Morphism Rinv : Rinv_morph. -Proof. -exact SRinv_ext. -Qed. -*) -Notation Rphi := (gen_phiZ 0%R 1%R Rplus Rmult Ropp). - -Theorem gen_phiPOS1_IZR : - forall p, gen_phiPOS 1%R Rplus Rmult p = IZR (Zpos p). -intros p; elim p; simpl gen_phiPOS. -intros p0; case p0. -intros p1 H; rewrite H. -unfold IZR; rewrite (nat_of_P_xI (xI p1)); (try rewrite S_INR); - (try rewrite plus_INR); (try rewrite mult_INR). -pose (x:= INR (nat_of_P (xI p1))); fold x; simpl; ring. -intros p1 H; rewrite H. -unfold IZR; rewrite (nat_of_P_xI (xO p1)); (try rewrite S_INR); - (try rewrite plus_INR); (try rewrite mult_INR). -pose (x:= INR (nat_of_P (xO p1))); fold x; simpl; ring. -simpl; intros; ring. -intros p0; case p0. -intros p1 H; rewrite H. -unfold IZR; rewrite (nat_of_P_xO (xI p1)); (try rewrite S_INR); - (try rewrite plus_INR); (try rewrite mult_INR). -pose (x:= INR (nat_of_P (xO p1))); fold x; simpl; ring. -intros p1 H; rewrite H. -unfold IZR; rewrite (nat_of_P_xO (xO p1)); (try rewrite S_INR); - (try rewrite plus_INR); (try rewrite mult_INR). -pose (x:= INR (nat_of_P (xO p1))); fold x; simpl; ring. -simpl; intros; ring. -simpl; trivial. -Qed. - -Theorem gen_phiZ1_IZR: forall p, Rphi p = IZR p. -intros p; case p; simpl; auto. -intros p0; rewrite gen_phiPOS1_IZR; auto. -intros p0; rewrite gen_phiPOS1_IZR; auto. -Qed. - -Lemma Zeq_bool_complete : forall x y, Rphi x = Rphi y -> Zeq_bool x y = true. -Proof. -intros. - replace y with x. - unfold Zeq_bool in |- *. - rewrite Zcompare_refl in |- *; trivial. - assert (IZR x = IZR y); auto. - repeat rewrite <- gen_phiZ1_IZR in |- *; trivial. - apply eq_IZR; trivial. -Qed. - - -Section Complete. -Import Setoid. - Variable R : Type. - Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). - Variable (rdiv : R -> R -> R) (rinv : R -> R). - Variable req : R -> R -> Prop. - Notation "0" := rO. Notation "1" := rI. - Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y). - Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). - Notation "x / y " := (rdiv x y). Notation "/ x" := (rinv x). - Notation "x == y" := (req x y) (at level 70, no associativity). - Variable Rsth : Setoid_Theory R req. - Add Setoid R req Rsth as R_setoid3. - Ltac rrefl := gen_reflexivity Rsth. - Variable Reqe : ring_eq_ext radd rmul ropp req. - Add Morphism radd : radd_ext3. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext3. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext3. exact (Ropp_ext Reqe). Qed. - -Section AlmostField. - - Variable AFth : almost_field_theory R rO rI radd rmul rsub ropp rdiv rinv req. - Let ARth := AFth.(AF_AR _ _ _ _ _ _ _ _ _ _). - Let rI_neq_rO := AFth.(AF_1_neq_0 _ _ _ _ _ _ _ _ _ _). - Let rdiv_def := AFth.(AFdiv_def _ _ _ _ _ _ _ _ _ _). - Let rinv_l := AFth.(AFinv_l _ _ _ _ _ _ _ _ _ _). - -Hypothesis S_inj : forall x y, 1+x==1+y -> x==y. - -Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0. - -Lemma discr_0_2 : ~ 1+1 == 0. -change (~ gen_phiPOS 1 radd rmul 2 == 0) in |- *. -rewrite <- (same_gen Rsth Reqe ARth) in |- *. -apply gen_phiPOS_not_0. -Qed. -Hint Resolve discr_0_2. - - -Lemma double_inj : forall x y, (1+1)*x==(1+1)*y -> x==y. -intros. -assert (/ (1 + 1) * ((1 + 1) * x) == / (1 + 1) * ((1 + 1) * y)). - rewrite H in |- *; trivial. - reflexivity. - generalize H0; clear H0. - repeat rewrite (ARmul_assoc ARth) in |- *. - repeat rewrite (AFinv_l _ _ _ _ _ _ _ _ _ _ AFth) in |- *; trivial. - repeat rewrite (ARmul_1_l ARth) in |- *; trivial. -Qed. - -Lemma discr_even_1 : forall x, - ~ (1+1) * gen_phiPOS1 rI radd rmul x == 1. -intros. -rewrite (same_gen Rsth Reqe ARth) in |- *. -elim x using Pcase; simpl in |- *; intros. - rewrite (ARmul_1_r Rsth ARth) in |- *. - red in |- *; intro. - apply rI_neq_rO. - apply S_inj. - rewrite H in |- *. - rewrite (ARadd_0_r Rsth ARth) in |- *; reflexivity. - rewrite <- (same_gen Rsth Reqe ARth) in |- *. - rewrite (ARgen_phiPOS_Psucc Rsth Reqe ARth) in |- *. - rewrite (ARdistr_r Rsth Reqe ARth) in |- *. - rewrite (ARmul_1_r Rsth ARth) in |- *. - red in |- *; intro. - apply (gen_phiPOS_not_0 (xI n)). - apply S_inj; simpl in |- *. - rewrite (ARadd_assoc ARth) in |- *. - rewrite H in |- *. - rewrite (ARadd_0_r Rsth ARth) in |- *; reflexivity. -Qed. - -Lemma discr_odd_0 : forall x, - ~ 1 + (1+1) * gen_phiPOS1 rI radd rmul x == 0. -red in |- *; intros. -apply discr_even_1 with (Psucc x). -rewrite (ARgen_phiPOS_Psucc Rsth Reqe ARth) in |- *. -rewrite (ARdistr_r Rsth Reqe ARth) in |- *. -rewrite (ARmul_1_r Rsth ARth) in |- *. -rewrite <- (ARadd_assoc ARth) in |- *. -rewrite H in |- *. -apply (ARadd_0_r Rsth ARth). -Qed. - - -Lemma add_inj_r : forall p x y, - gen_phiPOS1 rI radd rmul p + x == gen_phiPOS1 rI radd rmul p + y -> x==y. -intros p x y. -elim p using Pind; simpl in |- *; intros. - apply S_inj; trivial. - apply H. - apply S_inj. - repeat rewrite (ARadd_assoc ARth) in |- *. - rewrite <- (ARgen_phiPOS_Psucc Rsth Reqe ARth) in |- *; trivial. -Qed. - -Lemma discr_0_1: ~ 1 == 0. -red in |- *; intro. -apply (discr_even_1 1). -simpl in |- *. -rewrite H in |- *. -apply (ARmul_0_r Rsth ARth). -Qed. - - -Lemma discr_diag : forall x, - ~ 1 + gen_phiPOS1 rI radd rmul x == gen_phiPOS1 rI radd rmul x. -intro. -elim x using Pind; simpl in |- *; intros. - red in |- *; intro; apply discr_0_1. - apply S_inj. - rewrite (ARadd_0_r Rsth ARth) in |- *. - trivial. - rewrite (ARgen_phiPOS_Psucc Rsth Reqe ARth) in |- *. - red in |- *; intro; apply H. - apply S_inj; trivial. -Qed. - -Lemma even_odd_discr : forall x y, - ~ 1 + (1+1) * gen_phiPOS1 rI radd rmul x == - (1+1) * gen_phiPOS1 rI radd rmul y. -intros. -ElimPcompare x y; intro. - replace y with x. - apply (discr_diag (xO x)). - apply Pcompare_Eq_eq; trivial. - replace y with (x + (y - x))%positive. - rewrite (ARgen_phiPOS_add Rsth Reqe ARth) in |- *. - rewrite (ARadd_sym ARth) in |- *. - rewrite (ARdistr_r Rsth Reqe ARth) in |- *. - red in |- *; intros. - apply discr_even_1 with (y - x)%positive. - symmetry in |- *. - apply add_inj_r with (xO x); trivial. - apply Pplus_minus. - change Eq with (CompOpp Eq) in |- *. - rewrite <- Pcompare_antisym in |- *; trivial. - simpl in |- *. - rewrite H in |- *; trivial. - replace x with (y + (x - y))%positive. - rewrite (ARgen_phiPOS_add Rsth Reqe ARth) in |- *. - rewrite (ARdistr_r Rsth Reqe ARth) in |- *. - rewrite (ARadd_assoc ARth) in |- *. - red in |- *; intro. - apply discr_odd_0 with (x - y)%positive. - apply add_inj_r with (xO y). - simpl in |- *. - rewrite (ARadd_0_r Rsth ARth) in |- *. - rewrite (ARadd_assoc ARth) in |- *. - rewrite (ARadd_sym ARth ((1 + 1) * gen_phiPOS1 1 radd rmul y)) in |- *. - trivial. - apply Pplus_minus; trivial. -Qed. - -(* unused fact *) -Lemma even_0_inv : forall x, (1+1) * x == 0 -> x == 0. -Proof. -intros. -apply double_inj. -rewrite (ARmul_0_r Rsth ARth) in |- *. -trivial. -Qed. - -Lemma gen_phiPOS_inj : forall x y, - gen_phiPOS rI radd rmul x == gen_phiPOS rI radd rmul y -> - x = y. -intros x y. -repeat rewrite <- (same_gen Rsth Reqe ARth) in |- *. -generalize y; clear y. -induction x; destruct y; simpl in |- *; intros. - replace y with x; trivial. - apply IHx. - apply double_inj; apply S_inj; trivial. - elim even_odd_discr with (1 := H). - elim gen_phiPOS_not_0 with (xO x). - apply S_inj. - rewrite (ARadd_0_r Rsth ARth) in |- *. - trivial. - elim even_odd_discr with y x. - symmetry in |- *. - trivial. - replace y with x; trivial. - apply IHx. - apply double_inj; trivial. - elim discr_even_1 with x. - trivial. - elim gen_phiPOS_not_0 with (xO y). - apply S_inj. - rewrite (ARadd_0_r Rsth ARth) in |- *. - symmetry in |- *; trivial. - elim discr_even_1 with y. - symmetry in |- *; trivial. - trivial. -Qed. - - -Lemma gen_phiN_inj : forall x y, - gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y -> - x = y. -destruct x; destruct y; simpl in |- *; intros; trivial. - elim gen_phiPOS_not_0 with p. - symmetry in |- *. - rewrite (same_gen Rsth Reqe ARth) in |- *; trivial. - elim gen_phiPOS_not_0 with p. - rewrite (same_gen Rsth Reqe ARth) in |- *; trivial. - rewrite gen_phiPOS_inj with (1 := H) in |- *; trivial. -Qed. - -End AlmostField. - -Section Field. - - Variable Fth : field_theory R rO rI radd rmul rsub ropp rdiv rinv req. - Let Rth := Fth.(F_R _ _ _ _ _ _ _ _ _ _). - Let rI_neq_rO := Fth.(F_1_neq_0 _ _ _ _ _ _ _ _ _ _). - Let rdiv_def := Fth.(Fdiv_def _ _ _ _ _ _ _ _ _ _). - Let rinv_l := Fth.(Finv_l _ _ _ _ _ _ _ _ _ _). - Let AFth := F2AF _ _ _ _ _ _ _ _ _ _ Rsth Reqe Fth. - Let ARth := Rth_ARth Rsth Reqe Rth. - -Lemma ring_S_inj : forall x y, 1+x==1+y -> x==y. -intros. -transitivity (x + (1 + - (1))). - rewrite (Ropp_def Rth) in |- *. - symmetry in |- *. - apply (ARadd_0_r Rsth ARth). - transitivity (y + (1 + - (1))). - repeat rewrite <- (ARplus_assoc ARth) in |- *. - repeat rewrite (ARadd_assoc ARth) in |- *. - apply (Radd_ext Reqe). - repeat rewrite <- (ARadd_sym ARth 1) in |- *. - trivial. - reflexivity. - rewrite (Ropp_def Rth) in |- *. - apply (ARadd_0_r Rsth ARth). -Qed. - - - Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0. - -Let gen_phiPOS_inject := - gen_phiPOS_inj AFth ring_S_inj gen_phiPOS_not_0. - -Lemma gen_phiPOS_discr_sgn : forall x y, - ~ gen_phiPOS rI radd rmul x == - gen_phiPOS rI radd rmul y. -red in |- *; intros. -apply gen_phiPOS_not_0 with (y + x)%positive. -rewrite (ARgen_phiPOS_add Rsth Reqe ARth) in |- *. -transitivity (gen_phiPOS1 1 radd rmul y + - gen_phiPOS1 1 radd rmul y). - apply (Radd_ext Reqe); trivial. - reflexivity. - rewrite (same_gen Rsth Reqe ARth) in |- *. - rewrite (same_gen Rsth Reqe ARth) in |- *. - trivial. - apply (Ropp_def Rth). -Qed. - -Lemma gen_phiZ_inj : forall x y, - gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y -> - x = y. -destruct x; destruct y; simpl in |- *; intros. - trivial. - elim gen_phiPOS_not_0 with p. - rewrite (same_gen Rsth Reqe ARth) in |- *. - symmetry in |- *; trivial. - elim gen_phiPOS_not_0 with p. - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS1 1 radd rmul p)) in |- *. - rewrite (same_gen Rsth Reqe ARth) in |- *. - rewrite <- H in |- *. - apply (ARopp_zero Rsth Reqe ARth). - elim gen_phiPOS_not_0 with p. - rewrite (same_gen Rsth Reqe ARth) in |- *. - trivial. - rewrite gen_phiPOS_inject with (1 := H) in |- *; trivial. - elim gen_phiPOS_discr_sgn with (1 := H). - elim gen_phiPOS_not_0 with p. - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS1 1 radd rmul p)) in |- *. - rewrite (same_gen Rsth Reqe ARth) in |- *. - rewrite H in |- *. - apply (ARopp_zero Rsth Reqe ARth). - elim gen_phiPOS_discr_sgn with p0 p. - symmetry in |- *; trivial. - replace p0 with p; trivial. - apply gen_phiPOS_inject. - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *. - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p0)) in |- *. - rewrite H in |- *; trivial. - reflexivity. -Qed. - -Lemma gen_phiZ_complete : forall x y, - gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y -> +Lemma Zeq_bool_complete : forall x y, + InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp x = + InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp y -> Zeq_bool x y = true. -intros. - replace y with x. - unfold Zeq_bool in |- *. - rewrite Zcompare_refl in |- *; trivial. - apply gen_phiZ_inj; trivial. -Qed. - -End Field. - -End Complete. - - - - - -(* -Definition Rlemma1 := - (Pphi_dev_div_ok_compl _ _ _ _ _ _ _ _ _ _ Rset Rext SRinv_ext ARfield - _ _ _ _ _ _ _ _ _ Rmorph Zeq_bool_complete). - -Definition Rlemma2 := - (Fnorm_correct_gen _ _ _ _ _ _ _ _ _ _ Rset Rext SRinv_ext ARfield - _ _ _ _ _ _ _ _ _ Rmorph). - -Definition Rlemma2' := - (Fnorm_correct_compl _ _ _ _ _ _ _ _ _ _ Rset Rext SRinv_ext ARfield - _ _ _ _ _ _ _ _ _ Rmorph Zeq_bool_complete). - -Definition Rlemma3 := - (Field_simplify_eq_correct_compl - _ _ _ _ _ _ _ _ _ _ Rset Rext SRinv_ext ARfield - _ _ _ _ _ _ _ _ _ Rmorph Zeq_bool_complete). - -Notation Fcons := (Fcons2 Z 0%Z Zplus Zmult Zminus Zopp Zeq_bool). -*) - -End RField. -(* -Ltac newfield := - Make_field_tac - Rlemma2' (eq (A:=R)) ltac:(inv_gen_phiZ 0%R 1%R Rplus Rmult Ropp). - -Section Compat. -Open Scope R_scope. - -(** Inverse *) -Lemma Rinv_1 : / 1 = 1. -newfield; auto with real. -Qed. - -(*********) -Lemma Rinv_involutive : forall r, r <> 0 -> / / r = r. -intros; newfield; auto with real. -Qed. - -(*********) -Lemma Rinv_mult_distr : - forall r1 r2, r1 <> 0 -> r2 <> 0 -> / (r1 * r2) = / r1 * / r2. -intros; newfield; auto with real. -Qed. - -(*********) -Lemma Ropp_inv_permute : forall r, r <> 0 -> - / r = / - r. -intros; newfield; auto with real. -Qed. -End Compat. - -Ltac field := newfield. -Ltac field_simplify_eq := - Make_field_simplify_eq_tac - Rlemma3 (eq (A:=R)) ltac:(inv_gen_phiZ 0%R 1%R Rplus Rmult Ropp). -Ltac field_simplify := - Field_rewrite_list - Rlemma1 (eq (A:=R)) ltac:(inv_gen_phiZ 0%R 1%R Rplus Rmult Ropp). -*) -(* -Ltac newfield_rewrite r := - let T := Rfield.Make_field_rewrite in - T Rplus Rmult Rminus Ropp Rinv Rdiv Fcons2 PFcons2_fcons_inv RCst r; - unfold_field. -*) +Proof gen_phiZ_complete _ _ _ _ _ _ _ _ _ _ Rset Rext Rfield Rgen_phiPOS_not_0. +Add Field RField : Rfield (infinite Zeq_bool_complete). diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index 77653c3ac..7c41ed63e 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -714,11 +714,11 @@ TACTIC EXTEND setoid_ring END (***********************************************************************) -let fld_cst s = mk_cst [contrib_name;"Field"] s ;; +let fld_cst s = mk_cst [contrib_name;"Field_theory"] s ;; let field_modules = List.map (fun f -> ["Coq";contrib_name;f]) - ["Field";"Field_tac"] + ["Field_theory";"Field_tac"] let new_field_path = make_dirpath (List.map id_of_string ["Field_tac";contrib_name;"Coq"]) |