From 1040f4258593fa6de309acb2c93b76c41e914188 Mon Sep 17 00:00:00 2001 From: barras Date: Thu, 28 Sep 2006 17:51:39 +0000 Subject: separation de RealField git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9187 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend.coq | 13 +- Makefile | 4 +- contrib/setoid_ring/Field.v | 1192 ------------------------------------ contrib/setoid_ring/Field_tac.v | 2 +- contrib/setoid_ring/Field_theory.v | 1192 ++++++++++++++++++++++++++++++++++++ contrib/setoid_ring/RealField.v | 547 ++--------------- contrib/setoid_ring/newring.ml4 | 4 +- doc/refman/Polynom.tex | 28 +- doc/refman/RefMan-tac.tex | 2 +- theories/QArith/Qcanon.v | 2 +- theories/Reals/RIneq.v | 129 +--- 11 files changed, 1287 insertions(+), 1828 deletions(-) delete mode 100644 contrib/setoid_ring/Field.v create mode 100644 contrib/setoid_ring/Field_theory.v diff --git a/.depend.coq b/.depend.coq index 9d2f498e60..881c88432a 100644 --- a/.depend.coq +++ b/.depend.coq @@ -28,7 +28,7 @@ theories/FSets/FMapAVL.vo: theories/FSets/FMapAVL.v theories/FSets/FSetInterface theories/FSets/FSetAVL.vo: theories/FSets/FSetAVL.v theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo theories/ZArith/ZArith.vo theories/ZArith/Int.vo theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith_base.vo theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.vo theories/Reals/Rdefinitions.vo -theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/setoid_ring/ZArithRing.vo contrib/omega/Omega.vo contrib/setoid_ring/Field_tac.vo +theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/setoid_ring/ZArithRing.vo contrib/omega/Omega.vo contrib/setoid_ring/RealField.vo contrib/field/LegacyField.vo theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contrib/omega/Omega.vo theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo @@ -271,7 +271,7 @@ theories/Wellfounded/Well_Ordering.vo: theories/Wellfounded/Well_Ordering.v theo theories/Wellfounded/Lexicographic_Product.vo: theories/Wellfounded/Lexicographic_Product.v theories/Logic/Eqdep.vo theories/Relations/Relation_Operators.vo theories/Wellfounded/Transitive_Closure.vo theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith_base.vo theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.vo theories/Reals/Rdefinitions.vo -theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/setoid_ring/ZArithRing.vo contrib/omega/Omega.vo contrib/setoid_ring/Field_tac.vo +theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/setoid_ring/ZArithRing.vo contrib/omega/Omega.vo contrib/setoid_ring/RealField.vo contrib/field/LegacyField.vo theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contrib/omega/Omega.vo theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo @@ -332,7 +332,7 @@ theories/QArith/Qreduction.vo: theories/QArith/Qreduction.v theories/QArith/QAri theories/QArith/Qring.vo: theories/QArith/Qring.v contrib/setoid_ring/Ring.vo theories/QArith/QArith_base.vo theories/QArith/Qreals.vo: theories/QArith/Qreals.v theories/Reals/Rbase.vo theories/QArith/QArith_base.vo theories/QArith/QArith.vo: theories/QArith/QArith.v theories/QArith/QArith_base.vo theories/QArith/Qring.vo theories/QArith/Qreduction.vo -theories/QArith/Qcanon.vo: theories/QArith/Qcanon.v contrib/setoid_ring/Field.vo contrib/setoid_ring/Field_tac.vo theories/QArith/QArith.vo theories/ZArith/Znumtheory.vo theories/Logic/Eqdep_dec.vo +theories/QArith/Qcanon.vo: theories/QArith/Qcanon.v contrib/setoid_ring/Field.vo theories/QArith/QArith.vo theories/ZArith/Znumtheory.vo theories/Logic/Eqdep_dec.vo contrib/omega/OmegaLemmas.vo: contrib/omega/OmegaLemmas.v theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/ZArith_base.vo contrib/omega/OmegaLemmas.vo theories/ZArith/Zhints.vo contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/List.vo theories/Bool/Bool.vo theories/ZArith/ZArith_base.vo contrib/omega/OmegaLemmas.vo theories/Logic/Decidable.vo @@ -370,6 +370,7 @@ contrib/setoid_ring/Ring.vo: contrib/setoid_ring/Ring.v theories/Bool/Bool.vo co contrib/setoid_ring/ArithRing.vo: contrib/setoid_ring/ArithRing.v theories/Arith/Arith.vo contrib/setoid_ring/Ring.vo contrib/setoid_ring/NArithRing.vo: contrib/setoid_ring/NArithRing.v theories/NArith/NArith.vo contrib/setoid_ring/Ring.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/ZArithRing.vo: contrib/setoid_ring/ZArithRing.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo -contrib/setoid_ring/Field.vo: contrib/setoid_ring/Field.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo -contrib/setoid_ring/Field_tac.vo: contrib/setoid_ring/Field_tac.v contrib/setoid_ring/Ring_tac.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Field.vo -contrib/setoid_ring/RealField.vo: contrib/setoid_ring/RealField.v contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Field.vo contrib/setoid_ring/Field_tac.vo contrib/setoid_ring/Ring.vo theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo +contrib/setoid_ring/Field_theory.vo: contrib/setoid_ring/Field_theory.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo +contrib/setoid_ring/Field_tac.vo: contrib/setoid_ring/Field_tac.v contrib/setoid_ring/Ring_tac.vo contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Field_theory.vo +contrib/setoid_ring/Field.vo: contrib/setoid_ring/Field.v contrib/setoid_ring/Field_theory.vo contrib/setoid_ring/Field_tac.vo +contrib/setoid_ring/RealField.vo: contrib/setoid_ring/RealField.v theories/Reals/Raxioms.vo theories/Reals/Rdefinitions.vo contrib/setoid_ring/Ring.vo contrib/setoid_ring/Field.vo diff --git a/Makefile b/Makefile index e1c7a87ee6..f111679b5c 100644 --- a/Makefile +++ b/Makefile @@ -1053,8 +1053,8 @@ NEWRINGVO=\ contrib/setoid_ring/Ring_equiv.vo contrib/setoid_ring/Ring.vo \ contrib/setoid_ring/ArithRing.vo contrib/setoid_ring/NArithRing.vo \ contrib/setoid_ring/ZArithRing.vo \ - contrib/setoid_ring/Field.vo contrib/setoid_ring/Field_tac.vo \ - contrib/setoid_ring/RealField.vo + contrib/setoid_ring/Field_theory.vo contrib/setoid_ring/Field_tac.vo \ + contrib/setoid_ring/Field.vo contrib/setoid_ring/RealField.vo XMLVO= diff --git a/contrib/setoid_ring/Field.v b/contrib/setoid_ring/Field.v deleted file mode 100644 index 469f2537c0..0000000000 --- a/contrib/setoid_ring/Field.v +++ /dev/null @@ -1,1192 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 / y" := (rdiv x y). - Notation "- x" := (ropp x). Notation "/ x" := (rinv x). - Notation "x == y" := (req x y) (at level 70, no associativity). - - (* Equality properties *) - Variable Rsth : Setoid_Theory R req. - Variable Reqe : ring_eq_ext radd rmul ropp req. - Variable SRinv_ext : forall p q, p == q -> / p == / q. - - (* Field properties *) - Record almost_field_theory : Prop := mk_afield { - AF_AR : almost_ring_theory rO rI radd rmul rsub ropp req; - AF_1_neq_0 : ~ 1 == 0; - AFdiv_def : forall p q, p / q == p * / q; - AFinv_l : forall p, ~ p == 0 -> / p * p == 1 - }. - -Section AlmostField. - - Variable AFth : almost_field_theory. - 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). - - (* Coefficients *) - Variable C: Type. - Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C). - Variable ceqb : C->C->bool. - Variable phi : C -> R. - - Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req - cO cI cadd cmul csub copp ceqb phi. - -Lemma ceqb_rect : forall c1 c2 (A:Type) (x y:A) (P:A->Type), - (phi c1 == phi c2 -> P x) -> P y -> P (if ceqb c1 c2 then x else y). -Proof. -intros. -generalize (fun h => X (morph_eq CRmorph c1 c2 h)). -case (ceqb c1 c2); auto. -Qed. - - - (* C notations *) - Notation "x +! y" := (cadd x y) (at level 50). - Notation "x *! y " := (cmul x y) (at level 40). - Notation "x -! y " := (csub x y) (at level 50). - Notation "-! x" := (copp x) (at level 35). - Notation " x ?=! y" := (ceqb x y) (at level 70, no associativity). - Notation "[ x ]" := (phi x) (at level 0). - - - (* Usefull tactics *) - Add Setoid R req Rsth as R_set1. - Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed. - Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. - Add Morphism rinv : rinv_ext. exact SRinv_ext. Qed. - -Let eq_trans := Setoid.Seq_trans _ _ Rsth. -Let eq_sym := Setoid.Seq_sym _ _ Rsth. -Let eq_refl := Setoid.Seq_refl _ _ Rsth. - -Hint Resolve eq_refl rdiv_def rinv_l rI_neq_rO CRmorph.(morph1) . -Hint Resolve (Rmul_ext Reqe) (Rmul_ext Reqe) (Radd_ext Reqe) - (ARsub_ext Rsth Reqe ARth) (Ropp_ext Reqe) SRinv_ext. -Hint Resolve (ARadd_0_l ARth) (ARadd_sym ARth) (ARadd_assoc ARth) - (ARmul_1_l ARth) (ARmul_0_l ARth) - (ARmul_sym ARth) (ARmul_assoc ARth) (ARdistr_l ARth) - (ARopp_mul_l ARth) (ARopp_add ARth) - (ARsub_def ARth) . - -Notation NPEeval := (PEeval rO radd rmul rsub ropp phi). -Notation Nnorm := (norm cO cI cadd cmul csub copp ceqb). -Notation NPphi_dev := (Pphi_dev rO rI radd rmul cO cI ceqb phi). - -(* add abstract semi-ring to help with some proofs *) -Add Ring Rring : (ARth_SRth ARth). - - -(* additional ring properties *) - -Lemma rsub_0_l : forall r, 0 - r == - r. -intros; rewrite (ARsub_def ARth) in |- *; ring. -Qed. - -Lemma rsub_0_r : forall r, r - 0 == r. -intros; rewrite (ARsub_def ARth) in |- *. -rewrite (ARopp_zero Rsth Reqe ARth) in |- *; ring. -Qed. - -(*************************************************************************** - - Properties of division - - ***************************************************************************) - -Theorem rdiv_simpl: forall p q, ~ q == 0 -> q * (p / q) == p. -intros p q H. -rewrite rdiv_def in |- *. -transitivity (/ q * q * p); [ ring | idtac ]. -rewrite rinv_l in |- *; auto. -Qed. -Hint Resolve rdiv_simpl . - -Theorem SRdiv_ext: - forall p1 p2, p1 == p2 -> forall q1 q2, q1 == q2 -> p1 / q1 == p2 / q2. -intros p1 p2 H q1 q2 H0. -transitivity (p1 * / q1); auto. -transitivity (p2 * / q2); auto. -Qed. -Hint Resolve SRdiv_ext . - - Add Morphism rdiv : rdiv_ext. exact SRdiv_ext. Qed. - -Lemma rmul_reg_l : forall p q1 q2, - ~ p == 0 -> p * q1 == p * q2 -> q1 == q2. -intros. -rewrite <- (rdiv_simpl q1 p) in |- *; trivial. -rewrite <- (rdiv_simpl q2 p) in |- *; trivial. -repeat rewrite rdiv_def in |- *. -repeat rewrite (ARmul_assoc ARth) in |- *. -auto. -Qed. - -Theorem field_is_integral_domain : forall r1 r2, - ~ r1 == 0 -> ~ r2 == 0 -> ~ r1 * r2 == 0. -Proof. -red in |- *; intros. -apply H0. -transitivity (1 * r2); auto. -transitivity (/ r1 * r1 * r2); auto. -rewrite <- (ARmul_assoc ARth) in |- *. -rewrite H1 in |- *. -apply ARmul_0_r with (1 := Rsth) (2 := ARth). -Qed. - -Theorem ropp_neq_0 : forall r, - ~ -(1) == 0 -> ~ r == 0 -> ~ -r == 0. -intros. -setoid_replace (- r) with (- (1) * r). - apply field_is_integral_domain; trivial. - rewrite <- (ARopp_mul_l ARth) in |- *. - rewrite (ARmul_1_l ARth) in |- *. - reflexivity. -Qed. - -Theorem rdiv_r_r : forall r, ~ r == 0 -> r / r == 1. -intros. -rewrite (AFdiv_def AFth) in |- *. -rewrite (ARmul_sym ARth) in |- *. -apply (AFinv_l AFth). -trivial. -Qed. - -Theorem rdiv1: forall r, r == r / 1. -intros r; transitivity (1 * (r / 1)); auto. -Qed. - -Theorem rdiv2: - forall r1 r2 r3 r4, - ~ r2 == 0 -> - ~ r4 == 0 -> - r1 / r2 + r3 / r4 == (r1 * r4 + r3 * r2) / (r2 * r4). -Proof. -intros r1 r2 r3 r4 H H0. -assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial). -apply rmul_reg_l with (r2 * r4); trivial. -rewrite rdiv_simpl in |- *; trivial. -rewrite (ARdistr_r Rsth Reqe ARth) in |- *. -apply (Radd_ext Reqe). - transitivity (r2 * (r1 / r2) * r4); [ ring | auto ]. - transitivity (r2 * (r4 * (r3 / r4))); auto. - transitivity (r2 * r3); auto. -Qed. - -Theorem rdiv5: forall r1 r2, - (r1 / r2) == - r1 / r2. -intros r1 r2. -transitivity (- (r1 * / r2)); auto. -transitivity (- r1 * / r2); auto. -Qed. -Hint Resolve rdiv5 . - -Theorem rdiv3: - forall r1 r2 r3 r4, - ~ r2 == 0 -> - ~ r4 == 0 -> - r1 / r2 - r3 / r4 == (r1 * r4 - r3 * r2) / (r2 * r4). -intros r1 r2 r3 r4 H H0. -assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial). -transitivity (r1 / r2 + - (r3 / r4)); auto. -transitivity (r1 / r2 + - r3 / r4); auto. -transitivity ((r1 * r4 + - r3 * r2) / (r2 * r4)); auto. -apply rdiv2; auto. -apply SRdiv_ext; auto. -transitivity (r1 * r4 + - (r3 * r2)); symmetry; auto. -Qed. - -Theorem rdiv6: - forall r1 r2, - ~ r1 == 0 -> ~ r2 == 0 -> / (r1 / r2) == r2 / r1. -intros r1 r2 H H0. -assert (~ r1 / r2 == 0) as Hk. - intros H1; case H. - transitivity (r2 * (r1 / r2)); auto. - rewrite H1 in |- *; ring. - apply rmul_reg_l with (r1 / r2); auto. - transitivity (/ (r1 / r2) * (r1 / r2)); auto. - transitivity 1; auto. - repeat rewrite rdiv_def in |- *. - transitivity (/ r1 * r1 * (/ r2 * r2)); [ idtac | ring ]. - repeat rewrite rinv_l in |- *; auto. -Qed. -Hint Resolve rdiv6 . - - Theorem rdiv4: - forall r1 r2 r3 r4, - ~ r2 == 0 -> - ~ r4 == 0 -> - (r1 / r2) * (r3 / r4) == (r1 * r3) / (r2 * r4). -Proof. -intros r1 r2 r3 r4 H H0. -assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial). -apply rmul_reg_l with (r2 * r4); trivial. -rewrite rdiv_simpl in |- *; trivial. -transitivity (r2 * (r1 / r2) * (r4 * (r3 / r4))); [ ring | idtac ]. -repeat rewrite rdiv_simpl in |- *; trivial. -Qed. - - Theorem rdiv7: - forall r1 r2 r3 r4, - ~ r2 == 0 -> - ~ r3 == 0 -> - ~ r4 == 0 -> - (r1 / r2) / (r3 / r4) == (r1 * r4) / (r2 * r3). -Proof. -intros. -rewrite (rdiv_def (r1 / r2)) in |- *. -rewrite rdiv6 in |- *; trivial. -apply rdiv4; trivial. -Qed. - -Theorem rdiv8: forall r1 r2, ~ r2 == 0 -> r1 == 0 -> r1 / r2 == 0. -intros r1 r2 H H0. -transitivity (r1 * / r2); auto. -transitivity (0 * / r2); auto. -Qed. - - -Theorem cross_product_eq : forall r1 r2 r3 r4, - ~ r2 == 0 -> ~ r4 == 0 -> r1 * r4 == r3 * r2 -> r1 / r2 == r3 / r4. -intros. -transitivity (r1 / r2 * (r4 / r4)). - rewrite rdiv_r_r in |- *; trivial. - symmetry in |- *. - apply (ARmul_1_r Rsth ARth). - rewrite rdiv4 in |- *; trivial. - rewrite H1 in |- *. - rewrite (ARmul_sym ARth r2 r4) in |- *. - rewrite <- rdiv4 in |- *; trivial. - rewrite rdiv_r_r in |- *. - trivial. - apply (ARmul_1_r Rsth ARth). -Qed. - -(*************************************************************************** - - Some equality test - - ***************************************************************************) - -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. - -(* 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 - | 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 - | _, _ => false - end. - -Theorem PExpr_eq_semi_correct: - forall l e1 e2, PExpr_eq e1 e2 = true -> NPEeval l e1 == NPEeval l e2. -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 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); - (try (intros; discriminate)); auto. -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); - (try (intros; discriminate)); auto. -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); - (try (intros; discriminate)); auto. -intros e3 rec e2; (case e2; simpl; (try (intros; discriminate))). -intros e4; generalize (rec e4); case (PExpr_eq e3 e4); - (try (intros; discriminate)); auto. -Qed. - -(* add *) -Definition NPEadd e1 e2 := - match e1, e2 with - PEc c1, PEc c2 => PEc (cadd c1 c2) - | PEc c, _ => if ceqb c cO then e2 else PEadd e1 e2 - | _, PEc c => if ceqb c cO then e1 else PEadd e1 e2 - | _, _ => PEadd e1 e2 - end. - -Theorem NPEadd_correct: - forall l e1 e2, NPEeval l (NPEadd e1 e2) == NPEeval l (PEadd e1 e2). -Proof. -intros l e1 e2. -destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect; - try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; - try rewrite (morph0 CRmorph) in |- *; try ring. -apply (morph_add CRmorph). -Qed. - -(* mul *) -Definition NPEmul x y := - match x, y with - PEc c1, PEc c2 => PEc (cmul c1 c2) - | PEc c, _ => - if ceqb c cI then y else if ceqb c cO then PEc cO else PEmul x y - | _, PEc c => - if ceqb c cI then x else if ceqb c cO then PEc cO else PEmul x y - | _, _ => PEmul x y - end. - -Theorem NPEmul_correct : forall l e1 e2, - NPEeval l (NPEmul e1 e2) == NPEeval l (PEmul e1 e2). -intros l e1 e2. -destruct e1; destruct e2; simpl in |- *; try reflexivity; - repeat apply ceqb_rect; - try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; - try rewrite (morph0 CRmorph) in |- *; - try rewrite (morph1 CRmorph) in |- *; - try ring. -apply (morph_mul CRmorph). -Qed. - -(* sub *) -Definition NPEsub e1 e2 := - match e1, e2 with - PEc c1, PEc c2 => PEc (csub c1 c2) - | PEc c, _ => if ceqb c cO then PEopp e2 else PEsub e1 e2 - | _, PEc c => if ceqb c cO then e1 else PEsub e1 e2 - | _, _ => PEsub e1 e2 - end. - -Theorem NPEsub_correct: - forall l e1 e2, NPEeval l (NPEsub e1 e2) == NPEeval l (PEsub e1 e2). -intros l e1 e2. -destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect; - try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; - try rewrite (morph0 CRmorph) in |- *; try reflexivity; - try (symmetry; apply rsub_0_l); try (symmetry; apply rsub_0_r). -apply (morph_sub CRmorph). -Qed. - -(* opp *) -Definition NPEopp e1 := - match e1 with PEc c1 => PEc (copp c1) | _ => PEopp e1 end. - -Theorem NPEopp_correct: - forall l e1, NPEeval l (NPEopp e1) == NPEeval l (PEopp e1). -intros l e1; case e1; simpl; auto. -intros; apply (morph_opp CRmorph). -Qed. - -(* simplification *) -Fixpoint PExpr_simp (e : PExpr C) : PExpr C := - match e with - PEadd e1 e2 => NPEadd (PExpr_simp e1) (PExpr_simp e2) - | PEmul e1 e2 => NPEmul (PExpr_simp e1) (PExpr_simp e2) - | PEsub e1 e2 => NPEsub (PExpr_simp e1) (PExpr_simp e2) - | PEopp e1 => NPEopp (PExpr_simp e1) - | _ => e - end. - -Theorem PExpr_simp_correct: - forall l e, NPEeval l (PExpr_simp e) == NPEeval l e. -intros l e; elim e; simpl; auto. -intros e1 He1 e2 He2. -transitivity (NPEeval l (PEadd (PExpr_simp e1) (PExpr_simp e2))); auto. -apply NPEadd_correct. -simpl; auto. -intros e1 He1 e2 He2. -transitivity (NPEeval l (PEsub (PExpr_simp e1) (PExpr_simp e2))); auto. -apply NPEsub_correct. -simpl; auto. -intros e1 He1 e2 He2. -transitivity (NPEeval l (PEmul (PExpr_simp e1) (PExpr_simp e2))); auto. -apply NPEmul_correct. -simpl; auto. -intros e1 He1. -transitivity (NPEeval l (PEopp (PExpr_simp e1))); auto. -apply NPEopp_correct. -simpl; auto. -Qed. - - -(**************************************************************************** - - Datastructure - - ***************************************************************************) - -(* The input: syntax of a field expression *) - -Inductive FExpr : Type := - FEc: C -> FExpr - | FEX: positive -> FExpr - | FEadd: FExpr -> FExpr -> FExpr - | FEsub: FExpr -> FExpr -> FExpr - | FEmul: FExpr -> FExpr -> FExpr - | FEopp: FExpr -> FExpr - | FEinv: FExpr -> FExpr - | FEdiv: FExpr -> FExpr -> FExpr . - -Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R := - match pe with - | FEc c => phi c - | FEX x => BinList.nth 0 x l - | FEadd x y => FEeval l x + FEeval l y - | FEsub x y => FEeval l x - FEeval l y - | FEmul x y => FEeval l x * FEeval l y - | FEopp x => - FEeval l x - | FEinv x => / FEeval l x - | FEdiv x y => FEeval l x / FEeval l y - end. - -(* The result of the normalisation *) - -Record linear : Type := mk_linear { - num : PExpr C; - denum : PExpr C; - condition : list (PExpr C) }. - -(*************************************************************************** - - Semantics and properties of side condition - - ***************************************************************************) - -Fixpoint PCond (l : list R) (le : list (PExpr C)) {struct le} : Prop := - match le with - | nil => True - | e1 :: nil => ~ req (PEeval rO radd rmul rsub ropp phi l e1) rO - | e1 :: l1 => ~ req (PEeval rO radd rmul rsub ropp phi l e1) rO /\ PCond l l1 - end. - -Theorem PCond_cons_inv_l : - forall l a l1, PCond l (a::l1) -> ~ NPEeval l a == 0. -intros l a l1 H. -destruct l1; simpl in H |- *; trivial. -destruct H; trivial. -Qed. - -Theorem PCond_cons_inv_r : forall l a l1, PCond l (a :: l1) -> PCond l l1. -intros l a l1 H. -destruct l1; simpl in H |- *; trivial. -destruct H; trivial. -Qed. - -Theorem PCond_app_inv_l: forall l l1 l2, PCond l (l1 ++ l2) -> PCond l l1. -intros l l1 l2; elim l1; simpl app in |- *. - simpl in |- *; auto. - destruct l0; simpl in *. - destruct l2; firstorder. - firstorder. -Qed. - -Theorem PCond_app_inv_r: forall l l1 l2, PCond l (l1 ++ l2) -> PCond l l2. -intros l l1 l2; elim l1; simpl app; auto. -intros a l0 H H0; apply H; apply PCond_cons_inv_r with ( 1 := H0 ). -Qed. - -(* An unsatisfiable condition: issued when a division by zero is detected *) -Definition absurd_PCond := cons (PEc cO) nil. - -Lemma absurd_PCond_bottom : forall l, ~ PCond l absurd_PCond. -unfold absurd_PCond in |- *; simpl in |- *. -red in |- *; intros. -apply H. -apply (morph0 CRmorph). -Qed. - -(*************************************************************************** - - Normalisation - - ***************************************************************************) - -Fixpoint Fnorm (e : FExpr) : linear := - match e with - | FEc c => mk_linear (PEc c) (PEc cI) nil - | FEX x => mk_linear (PEX C x) (PEc cI) nil - | FEadd e1 e2 => - let x := Fnorm e1 in - let y := Fnorm e2 in - mk_linear - (NPEadd (NPEmul (num x) (denum y)) (NPEmul (num y) (denum x))) - (NPEmul (denum x) (denum y)) - (condition x ++ condition y) - | FEsub e1 e2 => - let x := Fnorm e1 in - let y := Fnorm e2 in - mk_linear - (NPEsub (NPEmul (num x) (denum y)) - (NPEmul (num y) (denum x))) - (NPEmul (denum x) (denum y)) - (condition x ++ condition y) - | FEmul e1 e2 => - let x := Fnorm e1 in - let y := Fnorm e2 in - mk_linear (NPEmul (num x) (num y)) - (NPEmul (denum x) (denum y)) - (condition x ++ condition y) - | FEopp e1 => - let x := Fnorm e1 in - mk_linear (NPEopp (num x)) (denum x) (condition x) - | FEinv e1 => - let x := Fnorm e1 in - mk_linear (denum x) (num x) (num x :: condition x) - | FEdiv e1 e2 => - let x := Fnorm e1 in - let y := Fnorm e2 in - mk_linear (NPEmul (num x) (denum y)) - (NPEmul (denum x) (num y)) - (num y :: condition x ++ condition y) - end. - - -(* Example *) -(* -Eval compute - in (Fnorm - (FEdiv - (FEc cI) - (FEadd (FEinv (FEX xH%positive)) (FEinv (FEX (xO xH)%positive))))). -*) - -Theorem Pcond_Fnorm: - forall l e, - PCond l (condition (Fnorm e)) -> ~ NPEeval l (denum (Fnorm e)) == 0. -intros l e; elim e. - simpl in |- *; intros _ _; rewrite (morph1 CRmorph) in |- *; exact rI_neq_rO. - simpl in |- *; intros _ _; rewrite (morph1 CRmorph) in |- *; exact rI_neq_rO. - intros e1 Hrec1 e2 Hrec2 Hcond. - simpl condition in Hcond. - simpl denum in |- *. - rewrite NPEmul_correct in |- *. - simpl in |- *. - apply field_is_integral_domain. - apply Hrec1. - apply PCond_app_inv_l with (1 := Hcond). - apply Hrec2. - apply PCond_app_inv_r with (1 := Hcond). - intros e1 Hrec1 e2 Hrec2 Hcond. - simpl condition in Hcond. - simpl denum in |- *. - rewrite NPEmul_correct in |- *. - simpl in |- *. - apply field_is_integral_domain. - apply Hrec1. - apply PCond_app_inv_l with (1 := Hcond). - apply Hrec2. - apply PCond_app_inv_r with (1 := Hcond). - intros e1 Hrec1 e2 Hrec2 Hcond. - simpl condition in Hcond. - simpl denum in |- *. - rewrite NPEmul_correct in |- *. - simpl in |- *. - apply field_is_integral_domain. - apply Hrec1. - apply PCond_app_inv_l with (1 := Hcond). - apply Hrec2. - apply PCond_app_inv_r with (1 := Hcond). - intros e1 Hrec1 Hcond. - simpl condition in Hcond. - simpl denum in |- *. - auto. - intros e1 Hrec1 Hcond. - simpl condition in Hcond. - simpl denum in |- *. - apply PCond_cons_inv_l with (1:=Hcond). - intros e1 Hrec1 e2 Hrec2 Hcond. - simpl condition in Hcond. - simpl denum in |- *. - rewrite NPEmul_correct in |- *. - simpl in |- *. - apply field_is_integral_domain. - apply Hrec1. - specialize PCond_cons_inv_r with (1:=Hcond); intro Hcond1. - apply PCond_app_inv_l with (1 := Hcond1). - apply PCond_cons_inv_l with (1:=Hcond). -Qed. -Hint Resolve Pcond_Fnorm. - - -(*************************************************************************** - - Main theorem - - ***************************************************************************) - -Theorem Fnorm_FEeval_PEeval: - forall l fe, - PCond l (condition (Fnorm fe)) -> - FEeval l fe == NPEeval l (num (Fnorm fe)) / NPEeval l (denum (Fnorm fe)). -Proof. -intros l fe; elim fe; simpl. -intros c H; rewrite CRmorph.(morph1); apply rdiv1. -intros p H; rewrite CRmorph.(morph1); apply rdiv1. -intros e1 He1 e2 He2 HH. -assert (HH1: PCond l (condition (Fnorm e1))). -apply PCond_app_inv_l with ( 1 := HH ). -assert (HH2: PCond l (condition (Fnorm e2))). -apply PCond_app_inv_r with ( 1 := HH ). -rewrite (He1 HH1); rewrite (He2 HH2). -rewrite NPEadd_correct; simpl. -repeat rewrite NPEmul_correct; simpl. -apply rdiv2; auto. - -intros e1 He1 e2 He2 HH. -assert (HH1: PCond l (condition (Fnorm e1))). -apply PCond_app_inv_l with ( 1 := HH ). -assert (HH2: PCond l (condition (Fnorm e2))). -apply PCond_app_inv_r with ( 1 := HH ). -rewrite (He1 HH1); rewrite (He2 HH2). -rewrite NPEsub_correct; simpl. -repeat rewrite NPEmul_correct; simpl. -apply rdiv3; auto. - -intros e1 He1 e2 He2 HH. -assert (HH1: PCond l (condition (Fnorm e1))). -apply PCond_app_inv_l with ( 1 := HH ). -assert (HH2: PCond l (condition (Fnorm e2))). -apply PCond_app_inv_r with ( 1 := HH ). -rewrite (He1 HH1); rewrite (He2 HH2). -repeat rewrite NPEmul_correct; simpl. -apply rdiv4; auto. - -intros e1 He1 HH. -rewrite NPEopp_correct; simpl; rewrite (He1 HH); apply rdiv5; auto. - -intros e1 He1 HH. -assert (HH1: PCond l (condition (Fnorm e1))). -apply PCond_cons_inv_r with ( 1 := HH ). -rewrite (He1 HH1); apply rdiv6; auto. -apply PCond_cons_inv_l with ( 1 := HH ). - -intros e1 He1 e2 He2 HH. -assert (HH1: PCond l (condition (Fnorm e1))). -apply PCond_app_inv_l with (condition (Fnorm e2)). -apply PCond_cons_inv_r with ( 1 := HH ). -assert (HH2: PCond l (condition (Fnorm e2))). -apply PCond_app_inv_r with (condition (Fnorm e1)). -apply PCond_cons_inv_r with ( 1 := HH ). -rewrite (He1 HH1); rewrite (He2 HH2). -repeat rewrite NPEmul_correct;simpl. -apply rdiv7; auto. -apply PCond_cons_inv_l with ( 1 := HH ). -Qed. - -Theorem Fnorm_crossproduct: - forall l fe1 fe2, - let nfe1 := Fnorm fe1 in - let nfe2 := Fnorm fe2 in - NPEeval l (PEmul (num nfe1) (denum nfe2)) == - NPEeval l (PEmul (num nfe2) (denum nfe1)) -> - PCond l (condition nfe1 ++ condition nfe2) -> - FEeval l fe1 == FEeval l fe2. -intros l fe1 fe2 nfe1 nfe2 Hcrossprod Hcond; subst nfe1 nfe2. -rewrite Fnorm_FEeval_PEeval in |- *. - apply PCond_app_inv_l with (1 := Hcond). - rewrite Fnorm_FEeval_PEeval in |- *. - apply PCond_app_inv_r with (1 := Hcond). - apply cross_product_eq; trivial. - apply Pcond_Fnorm. - apply PCond_app_inv_l with (1 := Hcond). - apply Pcond_Fnorm. - apply PCond_app_inv_r with (1 := Hcond). -Qed. - -(* Correctness lemmas of reflexive tactics *) - -Theorem Fnorm_correct: - forall l fe, - Peq ceqb (Nnorm (num (Fnorm fe))) (Pc cO) = true -> - PCond l (condition (Fnorm fe)) -> FEeval l fe == 0. -intros l fe H H1; - apply eq_trans with (1 := Fnorm_FEeval_PEeval l fe H1). -apply rdiv8; auto. -transitivity (NPEeval l (PEc cO)); auto. -apply (ring_correct Rsth Reqe ARth CRmorph); auto. -simpl; apply (morph0 CRmorph); auto. -Qed. - -(* simplify a field expression into a fraction *) -Theorem Pphi_dev_div_ok: - forall l fe nfe, - Fnorm fe = nfe -> - PCond l (condition nfe) -> - FEeval l fe == - NPphi_dev l (Nnorm (num nfe)) / NPphi_dev l (Nnorm (denum nfe)). -Proof. - intros l fe nfe eq_nfe H; subst nfe. - apply eq_trans with (1 := Fnorm_FEeval_PEeval _ _ H). - apply SRdiv_ext; - apply (Pphi_dev_ok Rsth Reqe ARth CRmorph); reflexivity. -Qed. - -(* solving a field equation *) -Theorem Fnorm_correct2: - forall l fe1 fe2 nfe1 nfe2, - Fnorm fe1 = nfe1 -> - Fnorm fe2 = nfe2 -> - Peq ceqb (Nnorm (PEmul (num nfe1) (denum nfe2))) - (Nnorm (PEmul (num nfe2) (denum nfe1))) = true -> - PCond l (condition nfe1 ++ condition nfe2) -> - FEeval l fe1 == FEeval l fe2. -Proof. -intros l fe1 fe2 nfe1 nfe2 eq1 eq2 Hnorm Hcond; subst nfe1 nfe2. -apply Fnorm_crossproduct; trivial. -apply (ring_correct Rsth Reqe ARth CRmorph); trivial. -Qed. - -(* simplify a field equation : generate the crossproduct and simplify - polynomials *) -Theorem Field_simplify_eq_correct : - forall l fe1 fe2 nfe1 nfe2, - Fnorm fe1 = nfe1 -> - Fnorm fe2 = nfe2 -> - NPphi_dev l (Nnorm (PEmul (num nfe1) (denum nfe2))) == - NPphi_dev l (Nnorm (PEmul (num nfe2) (denum nfe1))) -> - PCond l (condition nfe1 ++ condition nfe2) -> - FEeval l fe1 == FEeval l fe2. -Proof. -intros l fe1 fe2 nfe1 nfe2 eq1 eq2 Hcrossprod Hcond; subst nfe1 nfe2. -apply Fnorm_crossproduct; trivial. -rewrite (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in |- *. -rewrite (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in |- *. -trivial. -Qed. - -Section Fcons_impl. - -Variable Fcons : PExpr C -> list (PExpr C) -> list (PExpr C). - -Hypothesis PCond_fcons_inv : forall l a l1, - PCond l (Fcons a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. - -Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) := - match l with - | nil => m - | cons a l1 => Fcons a (Fapp l1 m) - end. - -Lemma fcons_correct : forall l l1, - PCond l (Fapp l1 nil) -> PCond l l1. -induction l1; simpl in |- *; intros. - trivial. - elim PCond_fcons_inv with (1 := H); intros. - destruct l1; auto. -Qed. - -End Fcons_impl. - -Section Fcons_simpl. - -(* Some general simpifications of the condition: eliminate duplicates, - split multiplications *) - -Fixpoint Fcons (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) := - match l with - nil => cons e nil - | cons a l1 => if PExpr_eq e a then l else cons a (Fcons e l1) - end. - -Theorem PFcons_fcons_inv: - forall l a l1, PCond l (Fcons a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. -intros l a l1; elim l1; simpl Fcons; auto. -simpl; auto. -intros a0 l0. -generalize (PExpr_eq_semi_correct l a a0); case (PExpr_eq a a0). -intros H H0 H1; split; auto. -rewrite H; auto. -generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto. -intros H H0 H1; - assert (Hp: ~ NPEeval l a0 == 0 /\ (~ NPEeval l a == 0 /\ PCond l l0)). -split. -generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto. -apply H0. -generalize (PCond_cons_inv_r _ _ _ H1); simpl; auto. -generalize Hp; case l0; simpl; intuition. -Qed. - -(* equality of normal forms rather than syntactic equality *) -Fixpoint Fcons0 (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) := - match l with - nil => cons e nil - | cons a l1 => - if Peq ceqb (Nnorm e) (Nnorm a) then l else cons a (Fcons0 e l1) - end. - -Theorem PFcons0_fcons_inv: - forall l a l1, PCond l (Fcons0 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. -intros l a l1; elim l1; simpl Fcons0; auto. -simpl; auto. -intros a0 l0. -generalize (ring_correct Rsth Reqe ARth CRmorph l a a0); - case (Peq ceqb (Nnorm a) (Nnorm a0)). -intros H H0 H1; split; auto. -rewrite H; auto. -generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto. -intros H H0 H1; - assert (Hp: ~ NPEeval l a0 == 0 /\ (~ NPEeval l a == 0 /\ PCond l l0)). -split. -generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto. -apply H0. -generalize (PCond_cons_inv_r _ _ _ H1); simpl; auto. -generalize Hp; case l0; simpl; intuition. -Qed. - -Fixpoint Fcons00 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) := - match e with - PEmul e1 e2 => Fcons00 e1 (Fcons00 e2 l) - | _ => Fcons0 e l - end. - -Theorem PFcons00_fcons_inv: - forall l a l1, PCond l (Fcons00 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. -intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail). - intros p H p0 H0 l1 H1. - simpl in H1. - case (H _ H1); intros H2 H3. - case (H0 _ H3); intros H4 H5; split; auto. - simpl in |- *. - apply field_is_integral_domain; trivial. -Qed. - - -Definition Pcond_simpl_gen := - fcons_correct _ PFcons00_fcons_inv. - - -(* Specific case when the equality test of coefs is complete w.r.t. the - field equality: non-zero coefs can be eliminated, and opposite can - be simplified (if -1 <> 0) *) - -Hypothesis ceqb_complete : forall c1 c2, phi c1 == phi c2 -> ceqb c1 c2 = true. - -Lemma ceqb_rect_complete : forall c1 c2 (A:Type) (x y:A) (P:A->Type), - (phi c1 == phi c2 -> P x) -> - (~ phi c1 == phi c2 -> P y) -> - P (if ceqb c1 c2 then x else y). -Proof. -intros. -generalize (fun h => X (morph_eq CRmorph c1 c2 h)). -generalize (ceqb_complete c1 c2). -case (c1 ?=! c2); auto; intros. -apply X0. -red in |- *; intro. -absurd (false = true); auto; discriminate. -Qed. - -Fixpoint Fcons1 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) := - match e with - PEmul e1 e2 => Fcons1 e1 (Fcons1 e2 l) - | PEopp e => if ceqb (copp cI) cO then absurd_PCond else Fcons1 e l - | PEc c => if ceqb c cO then absurd_PCond else l - | _ => Fcons0 e l - end. - -Theorem PFcons1_fcons_inv: - forall l a l1, PCond l (Fcons1 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. -intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail). - simpl in |- *; intros c l1. - apply ceqb_rect_complete; intros. - elim (absurd_PCond_bottom l H0). - split; trivial. - rewrite <- (morph0 CRmorph) in |- *; trivial. - intros p H p0 H0 l1 H1. - simpl in H1. - case (H _ H1); intros H2 H3. - case (H0 _ H3); intros H4 H5; split; auto. - simpl in |- *. - apply field_is_integral_domain; trivial. - simpl in |- *; intros p H l1. - apply ceqb_rect_complete; intros. - elim (absurd_PCond_bottom l H1). - destruct (H _ H1). - split; trivial. - apply ropp_neq_0; trivial. - rewrite (morph_opp CRmorph) in H0. - rewrite (morph1 CRmorph) in H0. - rewrite (morph0 CRmorph) in H0. - trivial. -Qed. - -Definition Fcons2 e l := Fcons1 (PExpr_simp e) l. - -Theorem PFcons2_fcons_inv: - forall l a l1, PCond l (Fcons2 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. -unfold Fcons2 in |- *; intros l a l1 H; split; - case (PFcons1_fcons_inv l (PExpr_simp a) l1); auto. -intros H1 H2 H3; case H1. -transitivity (NPEeval l a); trivial. -apply PExpr_simp_correct. -Qed. - -Definition Pcond_simpl_complete := - fcons_correct _ PFcons2_fcons_inv. - -End Fcons_simpl. - -End AlmostField. - -Section FieldAndSemiField. - - Record field_theory : Prop := mk_field { - F_R : ring_theory rO rI radd rmul rsub ropp req; - F_1_neq_0 : ~ 1 == 0; - Fdiv_def : forall p q, p / q == p * / q; - Finv_l : forall p, ~ p == 0 -> / p * p == 1 - }. - - Definition F2AF f := - mk_afield - (Rth_ARth Rsth Reqe f.(F_R)) f.(F_1_neq_0) f.(Fdiv_def) f.(Finv_l). - - Record semi_field_theory : Prop := mk_sfield { - SF_SR : semi_ring_theory rO rI radd rmul req; - SF_1_neq_0 : ~ 1 == 0; - SFdiv_def : forall p q, p / q == p * / q; - SFinv_l : forall p, ~ p == 0 -> / p * p == 1 - }. - -End FieldAndSemiField. - -End MakeFieldPol. - - Definition SF2AF R rO rI radd rmul rdiv rinv req Rsth - (sf:semi_field_theory R rO rI radd rmul rdiv rinv req) := - mk_afield _ _ _ _ _ _ _ _ _ _ - (SRth_ARth Rsth sf.(SF_SR _ _ _ _ _ _ _ _)) - sf.(SF_1_neq_0 _ _ _ _ _ _ _ _) - sf.(SFdiv_def _ _ _ _ _ _ _ _) - sf.(SFinv_l _ _ _ _ _ _ _ _). - - -Section Complete. - 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. - 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 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 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 |- *. -ElimPcompare x y; intro. - 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. - 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. -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. - -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. -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 (same_gen Rsth Reqe ARth) in |- *. - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) 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 (same_gen Rsth Reqe ARth) in |- *. - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) 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 -> - 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. - diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v index 802dd1d530..b16afad8dd 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_theory.v b/contrib/setoid_ring/Field_theory.v new file mode 100644 index 0000000000..469f2537c0 --- /dev/null +++ b/contrib/setoid_ring/Field_theory.v @@ -0,0 +1,1192 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 / y" := (rdiv x y). + Notation "- x" := (ropp x). Notation "/ x" := (rinv x). + Notation "x == y" := (req x y) (at level 70, no associativity). + + (* Equality properties *) + Variable Rsth : Setoid_Theory R req. + Variable Reqe : ring_eq_ext radd rmul ropp req. + Variable SRinv_ext : forall p q, p == q -> / p == / q. + + (* Field properties *) + Record almost_field_theory : Prop := mk_afield { + AF_AR : almost_ring_theory rO rI radd rmul rsub ropp req; + AF_1_neq_0 : ~ 1 == 0; + AFdiv_def : forall p q, p / q == p * / q; + AFinv_l : forall p, ~ p == 0 -> / p * p == 1 + }. + +Section AlmostField. + + Variable AFth : almost_field_theory. + 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). + + (* Coefficients *) + Variable C: Type. + Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C). + Variable ceqb : C->C->bool. + Variable phi : C -> R. + + Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req + cO cI cadd cmul csub copp ceqb phi. + +Lemma ceqb_rect : forall c1 c2 (A:Type) (x y:A) (P:A->Type), + (phi c1 == phi c2 -> P x) -> P y -> P (if ceqb c1 c2 then x else y). +Proof. +intros. +generalize (fun h => X (morph_eq CRmorph c1 c2 h)). +case (ceqb c1 c2); auto. +Qed. + + + (* C notations *) + Notation "x +! y" := (cadd x y) (at level 50). + Notation "x *! y " := (cmul x y) (at level 40). + Notation "x -! y " := (csub x y) (at level 50). + Notation "-! x" := (copp x) (at level 35). + Notation " x ?=! y" := (ceqb x y) (at level 70, no associativity). + Notation "[ x ]" := (phi x) (at level 0). + + + (* Usefull tactics *) + Add Setoid R req Rsth as R_set1. + Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. + Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed. + Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism rinv : rinv_ext. exact SRinv_ext. Qed. + +Let eq_trans := Setoid.Seq_trans _ _ Rsth. +Let eq_sym := Setoid.Seq_sym _ _ Rsth. +Let eq_refl := Setoid.Seq_refl _ _ Rsth. + +Hint Resolve eq_refl rdiv_def rinv_l rI_neq_rO CRmorph.(morph1) . +Hint Resolve (Rmul_ext Reqe) (Rmul_ext Reqe) (Radd_ext Reqe) + (ARsub_ext Rsth Reqe ARth) (Ropp_ext Reqe) SRinv_ext. +Hint Resolve (ARadd_0_l ARth) (ARadd_sym ARth) (ARadd_assoc ARth) + (ARmul_1_l ARth) (ARmul_0_l ARth) + (ARmul_sym ARth) (ARmul_assoc ARth) (ARdistr_l ARth) + (ARopp_mul_l ARth) (ARopp_add ARth) + (ARsub_def ARth) . + +Notation NPEeval := (PEeval rO radd rmul rsub ropp phi). +Notation Nnorm := (norm cO cI cadd cmul csub copp ceqb). +Notation NPphi_dev := (Pphi_dev rO rI radd rmul cO cI ceqb phi). + +(* add abstract semi-ring to help with some proofs *) +Add Ring Rring : (ARth_SRth ARth). + + +(* additional ring properties *) + +Lemma rsub_0_l : forall r, 0 - r == - r. +intros; rewrite (ARsub_def ARth) in |- *; ring. +Qed. + +Lemma rsub_0_r : forall r, r - 0 == r. +intros; rewrite (ARsub_def ARth) in |- *. +rewrite (ARopp_zero Rsth Reqe ARth) in |- *; ring. +Qed. + +(*************************************************************************** + + Properties of division + + ***************************************************************************) + +Theorem rdiv_simpl: forall p q, ~ q == 0 -> q * (p / q) == p. +intros p q H. +rewrite rdiv_def in |- *. +transitivity (/ q * q * p); [ ring | idtac ]. +rewrite rinv_l in |- *; auto. +Qed. +Hint Resolve rdiv_simpl . + +Theorem SRdiv_ext: + forall p1 p2, p1 == p2 -> forall q1 q2, q1 == q2 -> p1 / q1 == p2 / q2. +intros p1 p2 H q1 q2 H0. +transitivity (p1 * / q1); auto. +transitivity (p2 * / q2); auto. +Qed. +Hint Resolve SRdiv_ext . + + Add Morphism rdiv : rdiv_ext. exact SRdiv_ext. Qed. + +Lemma rmul_reg_l : forall p q1 q2, + ~ p == 0 -> p * q1 == p * q2 -> q1 == q2. +intros. +rewrite <- (rdiv_simpl q1 p) in |- *; trivial. +rewrite <- (rdiv_simpl q2 p) in |- *; trivial. +repeat rewrite rdiv_def in |- *. +repeat rewrite (ARmul_assoc ARth) in |- *. +auto. +Qed. + +Theorem field_is_integral_domain : forall r1 r2, + ~ r1 == 0 -> ~ r2 == 0 -> ~ r1 * r2 == 0. +Proof. +red in |- *; intros. +apply H0. +transitivity (1 * r2); auto. +transitivity (/ r1 * r1 * r2); auto. +rewrite <- (ARmul_assoc ARth) in |- *. +rewrite H1 in |- *. +apply ARmul_0_r with (1 := Rsth) (2 := ARth). +Qed. + +Theorem ropp_neq_0 : forall r, + ~ -(1) == 0 -> ~ r == 0 -> ~ -r == 0. +intros. +setoid_replace (- r) with (- (1) * r). + apply field_is_integral_domain; trivial. + rewrite <- (ARopp_mul_l ARth) in |- *. + rewrite (ARmul_1_l ARth) in |- *. + reflexivity. +Qed. + +Theorem rdiv_r_r : forall r, ~ r == 0 -> r / r == 1. +intros. +rewrite (AFdiv_def AFth) in |- *. +rewrite (ARmul_sym ARth) in |- *. +apply (AFinv_l AFth). +trivial. +Qed. + +Theorem rdiv1: forall r, r == r / 1. +intros r; transitivity (1 * (r / 1)); auto. +Qed. + +Theorem rdiv2: + forall r1 r2 r3 r4, + ~ r2 == 0 -> + ~ r4 == 0 -> + r1 / r2 + r3 / r4 == (r1 * r4 + r3 * r2) / (r2 * r4). +Proof. +intros r1 r2 r3 r4 H H0. +assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial). +apply rmul_reg_l with (r2 * r4); trivial. +rewrite rdiv_simpl in |- *; trivial. +rewrite (ARdistr_r Rsth Reqe ARth) in |- *. +apply (Radd_ext Reqe). + transitivity (r2 * (r1 / r2) * r4); [ ring | auto ]. + transitivity (r2 * (r4 * (r3 / r4))); auto. + transitivity (r2 * r3); auto. +Qed. + +Theorem rdiv5: forall r1 r2, - (r1 / r2) == - r1 / r2. +intros r1 r2. +transitivity (- (r1 * / r2)); auto. +transitivity (- r1 * / r2); auto. +Qed. +Hint Resolve rdiv5 . + +Theorem rdiv3: + forall r1 r2 r3 r4, + ~ r2 == 0 -> + ~ r4 == 0 -> + r1 / r2 - r3 / r4 == (r1 * r4 - r3 * r2) / (r2 * r4). +intros r1 r2 r3 r4 H H0. +assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial). +transitivity (r1 / r2 + - (r3 / r4)); auto. +transitivity (r1 / r2 + - r3 / r4); auto. +transitivity ((r1 * r4 + - r3 * r2) / (r2 * r4)); auto. +apply rdiv2; auto. +apply SRdiv_ext; auto. +transitivity (r1 * r4 + - (r3 * r2)); symmetry; auto. +Qed. + +Theorem rdiv6: + forall r1 r2, + ~ r1 == 0 -> ~ r2 == 0 -> / (r1 / r2) == r2 / r1. +intros r1 r2 H H0. +assert (~ r1 / r2 == 0) as Hk. + intros H1; case H. + transitivity (r2 * (r1 / r2)); auto. + rewrite H1 in |- *; ring. + apply rmul_reg_l with (r1 / r2); auto. + transitivity (/ (r1 / r2) * (r1 / r2)); auto. + transitivity 1; auto. + repeat rewrite rdiv_def in |- *. + transitivity (/ r1 * r1 * (/ r2 * r2)); [ idtac | ring ]. + repeat rewrite rinv_l in |- *; auto. +Qed. +Hint Resolve rdiv6 . + + Theorem rdiv4: + forall r1 r2 r3 r4, + ~ r2 == 0 -> + ~ r4 == 0 -> + (r1 / r2) * (r3 / r4) == (r1 * r3) / (r2 * r4). +Proof. +intros r1 r2 r3 r4 H H0. +assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial). +apply rmul_reg_l with (r2 * r4); trivial. +rewrite rdiv_simpl in |- *; trivial. +transitivity (r2 * (r1 / r2) * (r4 * (r3 / r4))); [ ring | idtac ]. +repeat rewrite rdiv_simpl in |- *; trivial. +Qed. + + Theorem rdiv7: + forall r1 r2 r3 r4, + ~ r2 == 0 -> + ~ r3 == 0 -> + ~ r4 == 0 -> + (r1 / r2) / (r3 / r4) == (r1 * r4) / (r2 * r3). +Proof. +intros. +rewrite (rdiv_def (r1 / r2)) in |- *. +rewrite rdiv6 in |- *; trivial. +apply rdiv4; trivial. +Qed. + +Theorem rdiv8: forall r1 r2, ~ r2 == 0 -> r1 == 0 -> r1 / r2 == 0. +intros r1 r2 H H0. +transitivity (r1 * / r2); auto. +transitivity (0 * / r2); auto. +Qed. + + +Theorem cross_product_eq : forall r1 r2 r3 r4, + ~ r2 == 0 -> ~ r4 == 0 -> r1 * r4 == r3 * r2 -> r1 / r2 == r3 / r4. +intros. +transitivity (r1 / r2 * (r4 / r4)). + rewrite rdiv_r_r in |- *; trivial. + symmetry in |- *. + apply (ARmul_1_r Rsth ARth). + rewrite rdiv4 in |- *; trivial. + rewrite H1 in |- *. + rewrite (ARmul_sym ARth r2 r4) in |- *. + rewrite <- rdiv4 in |- *; trivial. + rewrite rdiv_r_r in |- *. + trivial. + apply (ARmul_1_r Rsth ARth). +Qed. + +(*************************************************************************** + + Some equality test + + ***************************************************************************) + +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. + +(* 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 + | 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 + | _, _ => false + end. + +Theorem PExpr_eq_semi_correct: + forall l e1 e2, PExpr_eq e1 e2 = true -> NPEeval l e1 == NPEeval l e2. +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 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); + (try (intros; discriminate)); auto. +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); + (try (intros; discriminate)); auto. +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); + (try (intros; discriminate)); auto. +intros e3 rec e2; (case e2; simpl; (try (intros; discriminate))). +intros e4; generalize (rec e4); case (PExpr_eq e3 e4); + (try (intros; discriminate)); auto. +Qed. + +(* add *) +Definition NPEadd e1 e2 := + match e1, e2 with + PEc c1, PEc c2 => PEc (cadd c1 c2) + | PEc c, _ => if ceqb c cO then e2 else PEadd e1 e2 + | _, PEc c => if ceqb c cO then e1 else PEadd e1 e2 + | _, _ => PEadd e1 e2 + end. + +Theorem NPEadd_correct: + forall l e1 e2, NPEeval l (NPEadd e1 e2) == NPEeval l (PEadd e1 e2). +Proof. +intros l e1 e2. +destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect; + try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; + try rewrite (morph0 CRmorph) in |- *; try ring. +apply (morph_add CRmorph). +Qed. + +(* mul *) +Definition NPEmul x y := + match x, y with + PEc c1, PEc c2 => PEc (cmul c1 c2) + | PEc c, _ => + if ceqb c cI then y else if ceqb c cO then PEc cO else PEmul x y + | _, PEc c => + if ceqb c cI then x else if ceqb c cO then PEc cO else PEmul x y + | _, _ => PEmul x y + end. + +Theorem NPEmul_correct : forall l e1 e2, + NPEeval l (NPEmul e1 e2) == NPEeval l (PEmul e1 e2). +intros l e1 e2. +destruct e1; destruct e2; simpl in |- *; try reflexivity; + repeat apply ceqb_rect; + try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; + try rewrite (morph0 CRmorph) in |- *; + try rewrite (morph1 CRmorph) in |- *; + try ring. +apply (morph_mul CRmorph). +Qed. + +(* sub *) +Definition NPEsub e1 e2 := + match e1, e2 with + PEc c1, PEc c2 => PEc (csub c1 c2) + | PEc c, _ => if ceqb c cO then PEopp e2 else PEsub e1 e2 + | _, PEc c => if ceqb c cO then e1 else PEsub e1 e2 + | _, _ => PEsub e1 e2 + end. + +Theorem NPEsub_correct: + forall l e1 e2, NPEeval l (NPEsub e1 e2) == NPEeval l (PEsub e1 e2). +intros l e1 e2. +destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect; + try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; + try rewrite (morph0 CRmorph) in |- *; try reflexivity; + try (symmetry; apply rsub_0_l); try (symmetry; apply rsub_0_r). +apply (morph_sub CRmorph). +Qed. + +(* opp *) +Definition NPEopp e1 := + match e1 with PEc c1 => PEc (copp c1) | _ => PEopp e1 end. + +Theorem NPEopp_correct: + forall l e1, NPEeval l (NPEopp e1) == NPEeval l (PEopp e1). +intros l e1; case e1; simpl; auto. +intros; apply (morph_opp CRmorph). +Qed. + +(* simplification *) +Fixpoint PExpr_simp (e : PExpr C) : PExpr C := + match e with + PEadd e1 e2 => NPEadd (PExpr_simp e1) (PExpr_simp e2) + | PEmul e1 e2 => NPEmul (PExpr_simp e1) (PExpr_simp e2) + | PEsub e1 e2 => NPEsub (PExpr_simp e1) (PExpr_simp e2) + | PEopp e1 => NPEopp (PExpr_simp e1) + | _ => e + end. + +Theorem PExpr_simp_correct: + forall l e, NPEeval l (PExpr_simp e) == NPEeval l e. +intros l e; elim e; simpl; auto. +intros e1 He1 e2 He2. +transitivity (NPEeval l (PEadd (PExpr_simp e1) (PExpr_simp e2))); auto. +apply NPEadd_correct. +simpl; auto. +intros e1 He1 e2 He2. +transitivity (NPEeval l (PEsub (PExpr_simp e1) (PExpr_simp e2))); auto. +apply NPEsub_correct. +simpl; auto. +intros e1 He1 e2 He2. +transitivity (NPEeval l (PEmul (PExpr_simp e1) (PExpr_simp e2))); auto. +apply NPEmul_correct. +simpl; auto. +intros e1 He1. +transitivity (NPEeval l (PEopp (PExpr_simp e1))); auto. +apply NPEopp_correct. +simpl; auto. +Qed. + + +(**************************************************************************** + + Datastructure + + ***************************************************************************) + +(* The input: syntax of a field expression *) + +Inductive FExpr : Type := + FEc: C -> FExpr + | FEX: positive -> FExpr + | FEadd: FExpr -> FExpr -> FExpr + | FEsub: FExpr -> FExpr -> FExpr + | FEmul: FExpr -> FExpr -> FExpr + | FEopp: FExpr -> FExpr + | FEinv: FExpr -> FExpr + | FEdiv: FExpr -> FExpr -> FExpr . + +Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R := + match pe with + | FEc c => phi c + | FEX x => BinList.nth 0 x l + | FEadd x y => FEeval l x + FEeval l y + | FEsub x y => FEeval l x - FEeval l y + | FEmul x y => FEeval l x * FEeval l y + | FEopp x => - FEeval l x + | FEinv x => / FEeval l x + | FEdiv x y => FEeval l x / FEeval l y + end. + +(* The result of the normalisation *) + +Record linear : Type := mk_linear { + num : PExpr C; + denum : PExpr C; + condition : list (PExpr C) }. + +(*************************************************************************** + + Semantics and properties of side condition + + ***************************************************************************) + +Fixpoint PCond (l : list R) (le : list (PExpr C)) {struct le} : Prop := + match le with + | nil => True + | e1 :: nil => ~ req (PEeval rO radd rmul rsub ropp phi l e1) rO + | e1 :: l1 => ~ req (PEeval rO radd rmul rsub ropp phi l e1) rO /\ PCond l l1 + end. + +Theorem PCond_cons_inv_l : + forall l a l1, PCond l (a::l1) -> ~ NPEeval l a == 0. +intros l a l1 H. +destruct l1; simpl in H |- *; trivial. +destruct H; trivial. +Qed. + +Theorem PCond_cons_inv_r : forall l a l1, PCond l (a :: l1) -> PCond l l1. +intros l a l1 H. +destruct l1; simpl in H |- *; trivial. +destruct H; trivial. +Qed. + +Theorem PCond_app_inv_l: forall l l1 l2, PCond l (l1 ++ l2) -> PCond l l1. +intros l l1 l2; elim l1; simpl app in |- *. + simpl in |- *; auto. + destruct l0; simpl in *. + destruct l2; firstorder. + firstorder. +Qed. + +Theorem PCond_app_inv_r: forall l l1 l2, PCond l (l1 ++ l2) -> PCond l l2. +intros l l1 l2; elim l1; simpl app; auto. +intros a l0 H H0; apply H; apply PCond_cons_inv_r with ( 1 := H0 ). +Qed. + +(* An unsatisfiable condition: issued when a division by zero is detected *) +Definition absurd_PCond := cons (PEc cO) nil. + +Lemma absurd_PCond_bottom : forall l, ~ PCond l absurd_PCond. +unfold absurd_PCond in |- *; simpl in |- *. +red in |- *; intros. +apply H. +apply (morph0 CRmorph). +Qed. + +(*************************************************************************** + + Normalisation + + ***************************************************************************) + +Fixpoint Fnorm (e : FExpr) : linear := + match e with + | FEc c => mk_linear (PEc c) (PEc cI) nil + | FEX x => mk_linear (PEX C x) (PEc cI) nil + | FEadd e1 e2 => + let x := Fnorm e1 in + let y := Fnorm e2 in + mk_linear + (NPEadd (NPEmul (num x) (denum y)) (NPEmul (num y) (denum x))) + (NPEmul (denum x) (denum y)) + (condition x ++ condition y) + | FEsub e1 e2 => + let x := Fnorm e1 in + let y := Fnorm e2 in + mk_linear + (NPEsub (NPEmul (num x) (denum y)) + (NPEmul (num y) (denum x))) + (NPEmul (denum x) (denum y)) + (condition x ++ condition y) + | FEmul e1 e2 => + let x := Fnorm e1 in + let y := Fnorm e2 in + mk_linear (NPEmul (num x) (num y)) + (NPEmul (denum x) (denum y)) + (condition x ++ condition y) + | FEopp e1 => + let x := Fnorm e1 in + mk_linear (NPEopp (num x)) (denum x) (condition x) + | FEinv e1 => + let x := Fnorm e1 in + mk_linear (denum x) (num x) (num x :: condition x) + | FEdiv e1 e2 => + let x := Fnorm e1 in + let y := Fnorm e2 in + mk_linear (NPEmul (num x) (denum y)) + (NPEmul (denum x) (num y)) + (num y :: condition x ++ condition y) + end. + + +(* Example *) +(* +Eval compute + in (Fnorm + (FEdiv + (FEc cI) + (FEadd (FEinv (FEX xH%positive)) (FEinv (FEX (xO xH)%positive))))). +*) + +Theorem Pcond_Fnorm: + forall l e, + PCond l (condition (Fnorm e)) -> ~ NPEeval l (denum (Fnorm e)) == 0. +intros l e; elim e. + simpl in |- *; intros _ _; rewrite (morph1 CRmorph) in |- *; exact rI_neq_rO. + simpl in |- *; intros _ _; rewrite (morph1 CRmorph) in |- *; exact rI_neq_rO. + intros e1 Hrec1 e2 Hrec2 Hcond. + simpl condition in Hcond. + simpl denum in |- *. + rewrite NPEmul_correct in |- *. + simpl in |- *. + apply field_is_integral_domain. + apply Hrec1. + apply PCond_app_inv_l with (1 := Hcond). + apply Hrec2. + apply PCond_app_inv_r with (1 := Hcond). + intros e1 Hrec1 e2 Hrec2 Hcond. + simpl condition in Hcond. + simpl denum in |- *. + rewrite NPEmul_correct in |- *. + simpl in |- *. + apply field_is_integral_domain. + apply Hrec1. + apply PCond_app_inv_l with (1 := Hcond). + apply Hrec2. + apply PCond_app_inv_r with (1 := Hcond). + intros e1 Hrec1 e2 Hrec2 Hcond. + simpl condition in Hcond. + simpl denum in |- *. + rewrite NPEmul_correct in |- *. + simpl in |- *. + apply field_is_integral_domain. + apply Hrec1. + apply PCond_app_inv_l with (1 := Hcond). + apply Hrec2. + apply PCond_app_inv_r with (1 := Hcond). + intros e1 Hrec1 Hcond. + simpl condition in Hcond. + simpl denum in |- *. + auto. + intros e1 Hrec1 Hcond. + simpl condition in Hcond. + simpl denum in |- *. + apply PCond_cons_inv_l with (1:=Hcond). + intros e1 Hrec1 e2 Hrec2 Hcond. + simpl condition in Hcond. + simpl denum in |- *. + rewrite NPEmul_correct in |- *. + simpl in |- *. + apply field_is_integral_domain. + apply Hrec1. + specialize PCond_cons_inv_r with (1:=Hcond); intro Hcond1. + apply PCond_app_inv_l with (1 := Hcond1). + apply PCond_cons_inv_l with (1:=Hcond). +Qed. +Hint Resolve Pcond_Fnorm. + + +(*************************************************************************** + + Main theorem + + ***************************************************************************) + +Theorem Fnorm_FEeval_PEeval: + forall l fe, + PCond l (condition (Fnorm fe)) -> + FEeval l fe == NPEeval l (num (Fnorm fe)) / NPEeval l (denum (Fnorm fe)). +Proof. +intros l fe; elim fe; simpl. +intros c H; rewrite CRmorph.(morph1); apply rdiv1. +intros p H; rewrite CRmorph.(morph1); apply rdiv1. +intros e1 He1 e2 He2 HH. +assert (HH1: PCond l (condition (Fnorm e1))). +apply PCond_app_inv_l with ( 1 := HH ). +assert (HH2: PCond l (condition (Fnorm e2))). +apply PCond_app_inv_r with ( 1 := HH ). +rewrite (He1 HH1); rewrite (He2 HH2). +rewrite NPEadd_correct; simpl. +repeat rewrite NPEmul_correct; simpl. +apply rdiv2; auto. + +intros e1 He1 e2 He2 HH. +assert (HH1: PCond l (condition (Fnorm e1))). +apply PCond_app_inv_l with ( 1 := HH ). +assert (HH2: PCond l (condition (Fnorm e2))). +apply PCond_app_inv_r with ( 1 := HH ). +rewrite (He1 HH1); rewrite (He2 HH2). +rewrite NPEsub_correct; simpl. +repeat rewrite NPEmul_correct; simpl. +apply rdiv3; auto. + +intros e1 He1 e2 He2 HH. +assert (HH1: PCond l (condition (Fnorm e1))). +apply PCond_app_inv_l with ( 1 := HH ). +assert (HH2: PCond l (condition (Fnorm e2))). +apply PCond_app_inv_r with ( 1 := HH ). +rewrite (He1 HH1); rewrite (He2 HH2). +repeat rewrite NPEmul_correct; simpl. +apply rdiv4; auto. + +intros e1 He1 HH. +rewrite NPEopp_correct; simpl; rewrite (He1 HH); apply rdiv5; auto. + +intros e1 He1 HH. +assert (HH1: PCond l (condition (Fnorm e1))). +apply PCond_cons_inv_r with ( 1 := HH ). +rewrite (He1 HH1); apply rdiv6; auto. +apply PCond_cons_inv_l with ( 1 := HH ). + +intros e1 He1 e2 He2 HH. +assert (HH1: PCond l (condition (Fnorm e1))). +apply PCond_app_inv_l with (condition (Fnorm e2)). +apply PCond_cons_inv_r with ( 1 := HH ). +assert (HH2: PCond l (condition (Fnorm e2))). +apply PCond_app_inv_r with (condition (Fnorm e1)). +apply PCond_cons_inv_r with ( 1 := HH ). +rewrite (He1 HH1); rewrite (He2 HH2). +repeat rewrite NPEmul_correct;simpl. +apply rdiv7; auto. +apply PCond_cons_inv_l with ( 1 := HH ). +Qed. + +Theorem Fnorm_crossproduct: + forall l fe1 fe2, + let nfe1 := Fnorm fe1 in + let nfe2 := Fnorm fe2 in + NPEeval l (PEmul (num nfe1) (denum nfe2)) == + NPEeval l (PEmul (num nfe2) (denum nfe1)) -> + PCond l (condition nfe1 ++ condition nfe2) -> + FEeval l fe1 == FEeval l fe2. +intros l fe1 fe2 nfe1 nfe2 Hcrossprod Hcond; subst nfe1 nfe2. +rewrite Fnorm_FEeval_PEeval in |- *. + apply PCond_app_inv_l with (1 := Hcond). + rewrite Fnorm_FEeval_PEeval in |- *. + apply PCond_app_inv_r with (1 := Hcond). + apply cross_product_eq; trivial. + apply Pcond_Fnorm. + apply PCond_app_inv_l with (1 := Hcond). + apply Pcond_Fnorm. + apply PCond_app_inv_r with (1 := Hcond). +Qed. + +(* Correctness lemmas of reflexive tactics *) + +Theorem Fnorm_correct: + forall l fe, + Peq ceqb (Nnorm (num (Fnorm fe))) (Pc cO) = true -> + PCond l (condition (Fnorm fe)) -> FEeval l fe == 0. +intros l fe H H1; + apply eq_trans with (1 := Fnorm_FEeval_PEeval l fe H1). +apply rdiv8; auto. +transitivity (NPEeval l (PEc cO)); auto. +apply (ring_correct Rsth Reqe ARth CRmorph); auto. +simpl; apply (morph0 CRmorph); auto. +Qed. + +(* simplify a field expression into a fraction *) +Theorem Pphi_dev_div_ok: + forall l fe nfe, + Fnorm fe = nfe -> + PCond l (condition nfe) -> + FEeval l fe == + NPphi_dev l (Nnorm (num nfe)) / NPphi_dev l (Nnorm (denum nfe)). +Proof. + intros l fe nfe eq_nfe H; subst nfe. + apply eq_trans with (1 := Fnorm_FEeval_PEeval _ _ H). + apply SRdiv_ext; + apply (Pphi_dev_ok Rsth Reqe ARth CRmorph); reflexivity. +Qed. + +(* solving a field equation *) +Theorem Fnorm_correct2: + forall l fe1 fe2 nfe1 nfe2, + Fnorm fe1 = nfe1 -> + Fnorm fe2 = nfe2 -> + Peq ceqb (Nnorm (PEmul (num nfe1) (denum nfe2))) + (Nnorm (PEmul (num nfe2) (denum nfe1))) = true -> + PCond l (condition nfe1 ++ condition nfe2) -> + FEeval l fe1 == FEeval l fe2. +Proof. +intros l fe1 fe2 nfe1 nfe2 eq1 eq2 Hnorm Hcond; subst nfe1 nfe2. +apply Fnorm_crossproduct; trivial. +apply (ring_correct Rsth Reqe ARth CRmorph); trivial. +Qed. + +(* simplify a field equation : generate the crossproduct and simplify + polynomials *) +Theorem Field_simplify_eq_correct : + forall l fe1 fe2 nfe1 nfe2, + Fnorm fe1 = nfe1 -> + Fnorm fe2 = nfe2 -> + NPphi_dev l (Nnorm (PEmul (num nfe1) (denum nfe2))) == + NPphi_dev l (Nnorm (PEmul (num nfe2) (denum nfe1))) -> + PCond l (condition nfe1 ++ condition nfe2) -> + FEeval l fe1 == FEeval l fe2. +Proof. +intros l fe1 fe2 nfe1 nfe2 eq1 eq2 Hcrossprod Hcond; subst nfe1 nfe2. +apply Fnorm_crossproduct; trivial. +rewrite (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in |- *. +rewrite (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in |- *. +trivial. +Qed. + +Section Fcons_impl. + +Variable Fcons : PExpr C -> list (PExpr C) -> list (PExpr C). + +Hypothesis PCond_fcons_inv : forall l a l1, + PCond l (Fcons a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. + +Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) := + match l with + | nil => m + | cons a l1 => Fcons a (Fapp l1 m) + end. + +Lemma fcons_correct : forall l l1, + PCond l (Fapp l1 nil) -> PCond l l1. +induction l1; simpl in |- *; intros. + trivial. + elim PCond_fcons_inv with (1 := H); intros. + destruct l1; auto. +Qed. + +End Fcons_impl. + +Section Fcons_simpl. + +(* Some general simpifications of the condition: eliminate duplicates, + split multiplications *) + +Fixpoint Fcons (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) := + match l with + nil => cons e nil + | cons a l1 => if PExpr_eq e a then l else cons a (Fcons e l1) + end. + +Theorem PFcons_fcons_inv: + forall l a l1, PCond l (Fcons a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. +intros l a l1; elim l1; simpl Fcons; auto. +simpl; auto. +intros a0 l0. +generalize (PExpr_eq_semi_correct l a a0); case (PExpr_eq a a0). +intros H H0 H1; split; auto. +rewrite H; auto. +generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto. +intros H H0 H1; + assert (Hp: ~ NPEeval l a0 == 0 /\ (~ NPEeval l a == 0 /\ PCond l l0)). +split. +generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto. +apply H0. +generalize (PCond_cons_inv_r _ _ _ H1); simpl; auto. +generalize Hp; case l0; simpl; intuition. +Qed. + +(* equality of normal forms rather than syntactic equality *) +Fixpoint Fcons0 (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) := + match l with + nil => cons e nil + | cons a l1 => + if Peq ceqb (Nnorm e) (Nnorm a) then l else cons a (Fcons0 e l1) + end. + +Theorem PFcons0_fcons_inv: + forall l a l1, PCond l (Fcons0 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. +intros l a l1; elim l1; simpl Fcons0; auto. +simpl; auto. +intros a0 l0. +generalize (ring_correct Rsth Reqe ARth CRmorph l a a0); + case (Peq ceqb (Nnorm a) (Nnorm a0)). +intros H H0 H1; split; auto. +rewrite H; auto. +generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto. +intros H H0 H1; + assert (Hp: ~ NPEeval l a0 == 0 /\ (~ NPEeval l a == 0 /\ PCond l l0)). +split. +generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto. +apply H0. +generalize (PCond_cons_inv_r _ _ _ H1); simpl; auto. +generalize Hp; case l0; simpl; intuition. +Qed. + +Fixpoint Fcons00 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) := + match e with + PEmul e1 e2 => Fcons00 e1 (Fcons00 e2 l) + | _ => Fcons0 e l + end. + +Theorem PFcons00_fcons_inv: + forall l a l1, PCond l (Fcons00 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. +intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail). + intros p H p0 H0 l1 H1. + simpl in H1. + case (H _ H1); intros H2 H3. + case (H0 _ H3); intros H4 H5; split; auto. + simpl in |- *. + apply field_is_integral_domain; trivial. +Qed. + + +Definition Pcond_simpl_gen := + fcons_correct _ PFcons00_fcons_inv. + + +(* Specific case when the equality test of coefs is complete w.r.t. the + field equality: non-zero coefs can be eliminated, and opposite can + be simplified (if -1 <> 0) *) + +Hypothesis ceqb_complete : forall c1 c2, phi c1 == phi c2 -> ceqb c1 c2 = true. + +Lemma ceqb_rect_complete : forall c1 c2 (A:Type) (x y:A) (P:A->Type), + (phi c1 == phi c2 -> P x) -> + (~ phi c1 == phi c2 -> P y) -> + P (if ceqb c1 c2 then x else y). +Proof. +intros. +generalize (fun h => X (morph_eq CRmorph c1 c2 h)). +generalize (ceqb_complete c1 c2). +case (c1 ?=! c2); auto; intros. +apply X0. +red in |- *; intro. +absurd (false = true); auto; discriminate. +Qed. + +Fixpoint Fcons1 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) := + match e with + PEmul e1 e2 => Fcons1 e1 (Fcons1 e2 l) + | PEopp e => if ceqb (copp cI) cO then absurd_PCond else Fcons1 e l + | PEc c => if ceqb c cO then absurd_PCond else l + | _ => Fcons0 e l + end. + +Theorem PFcons1_fcons_inv: + forall l a l1, PCond l (Fcons1 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. +intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail). + simpl in |- *; intros c l1. + apply ceqb_rect_complete; intros. + elim (absurd_PCond_bottom l H0). + split; trivial. + rewrite <- (morph0 CRmorph) in |- *; trivial. + intros p H p0 H0 l1 H1. + simpl in H1. + case (H _ H1); intros H2 H3. + case (H0 _ H3); intros H4 H5; split; auto. + simpl in |- *. + apply field_is_integral_domain; trivial. + simpl in |- *; intros p H l1. + apply ceqb_rect_complete; intros. + elim (absurd_PCond_bottom l H1). + destruct (H _ H1). + split; trivial. + apply ropp_neq_0; trivial. + rewrite (morph_opp CRmorph) in H0. + rewrite (morph1 CRmorph) in H0. + rewrite (morph0 CRmorph) in H0. + trivial. +Qed. + +Definition Fcons2 e l := Fcons1 (PExpr_simp e) l. + +Theorem PFcons2_fcons_inv: + forall l a l1, PCond l (Fcons2 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. +unfold Fcons2 in |- *; intros l a l1 H; split; + case (PFcons1_fcons_inv l (PExpr_simp a) l1); auto. +intros H1 H2 H3; case H1. +transitivity (NPEeval l a); trivial. +apply PExpr_simp_correct. +Qed. + +Definition Pcond_simpl_complete := + fcons_correct _ PFcons2_fcons_inv. + +End Fcons_simpl. + +End AlmostField. + +Section FieldAndSemiField. + + Record field_theory : Prop := mk_field { + F_R : ring_theory rO rI radd rmul rsub ropp req; + F_1_neq_0 : ~ 1 == 0; + Fdiv_def : forall p q, p / q == p * / q; + Finv_l : forall p, ~ p == 0 -> / p * p == 1 + }. + + Definition F2AF f := + mk_afield + (Rth_ARth Rsth Reqe f.(F_R)) f.(F_1_neq_0) f.(Fdiv_def) f.(Finv_l). + + Record semi_field_theory : Prop := mk_sfield { + SF_SR : semi_ring_theory rO rI radd rmul req; + SF_1_neq_0 : ~ 1 == 0; + SFdiv_def : forall p q, p / q == p * / q; + SFinv_l : forall p, ~ p == 0 -> / p * p == 1 + }. + +End FieldAndSemiField. + +End MakeFieldPol. + + Definition SF2AF R rO rI radd rmul rdiv rinv req Rsth + (sf:semi_field_theory R rO rI radd rmul rdiv rinv req) := + mk_afield _ _ _ _ _ _ _ _ _ _ + (SRth_ARth Rsth sf.(SF_SR _ _ _ _ _ _ _ _)) + sf.(SF_1_neq_0 _ _ _ _ _ _ _ _) + sf.(SFdiv_def _ _ _ _ _ _ _ _) + sf.(SFinv_l _ _ _ _ _ _ _ _). + + +Section Complete. + 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. + 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 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 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 |- *. +ElimPcompare x y; intro. + 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. + 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. +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. + +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. +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 (same_gen Rsth Reqe ARth) in |- *. + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) 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 (same_gen Rsth Reqe ARth) in |- *. + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) 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 -> + 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. + diff --git a/contrib/setoid_ring/RealField.v b/contrib/setoid_ring/RealField.v index 8793e36226..256354d78c 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 77653c3ac5..7c41ed63eb 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"]) diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex index 49616ff69d..0b8e094522 100644 --- a/doc/refman/Polynom.tex +++ b/doc/refman/Polynom.tex @@ -110,9 +110,9 @@ The tactic must be loaded by \texttt{Require Import Ring}. The ring structures must be declared with the \texttt{Add Ring} command (see below). The ring of booleans is predefined; if one wants to use the tactic on \texttt{nat} one must first require the module -\texttt{NewArithRing}; for \texttt{Z}, do \texttt{Require Import -NewZArithRing}; for \texttt{N}, do \texttt{Require Import -NewNArithRing}. +\texttt{ArithRing}; for \texttt{Z}, do \texttt{Require Import +ZArithRing}; for \texttt{N}, do \texttt{Require Import +NArithRing}. \Example \begin{coq_eval} @@ -121,7 +121,7 @@ Require Import ZArith. Open Scope Z_scope. \end{coq_eval} \begin{coq_example} -Require Import NewZArithRing. +Require Import ZArithRing. Goal forall a b c:Z, (a + b + c) * (a + b + c) = a * a + b * b + c * c + 2 * a * b + 2 * a * c + 2 * b * c. @@ -159,11 +159,11 @@ avoided for terms belonging to the same ring theory. Declaring a new ring consists in proving that a ring signature (a carrier set, an equality, and ring operations: {\tt -Ring\_th.ring\_theory} and {\tt Ring\_th.semi\_ring\_theory}) +Ring\_theory.ring\_theory} and {\tt Ring\_theory.semi\_ring\_theory}) satisfies the ring axioms. Semi-rings (rings without $+$ inverse) are also supported. The equality can be either Leibniz equality, or any relation declared as a setoid (see~\ref{setoidtactics}). The definition -of ring and semi-rings (see module {\tt Ring\_th}) is: +of ring and semi-rings (see module {\tt Ring\_theory}) is: \begin{verbatim} Record ring_theory : Prop := mk_rt { Radd_0_l : forall x, 0 + x == x; @@ -251,13 +251,13 @@ describes their syntax and effects: the form {\tt forall x y, x?=!y = true $\rightarrow$ x == y}. \item[morphism \term] declares the ring as a customized one. \term{} is a proof that there exists a morphism between a set of coefficient - and the ring carrier (see {\tt Ring\_th.ring\_morph} and {\tt - Ring\_th.semi\_morph}). + and the ring carrier (see {\tt Ring\_theory.ring\_morph} and {\tt + Ring\_theory.semi\_morph}). \item[setoid \term$_1$ \term$_2$] forces the use of given setoid. \term$_1$ is a proof that the equality is indeed a setoid (see {\tt Setoid.Setoid\_Theory}), and \term$_2$ a proof that the - ring operations are morphisms (see {\tt Ring\_th.ring\_eq\_ext} and - {\tt Ring\_th.sring\_eq\_ext}). This modifier need not be used if the + ring operations are morphisms (see {\tt Ring\_theory.ring\_eq\_ext} and + {\tt Ring\_theory.sring\_eq\_ext}). This modifier need not be used if the setoid and morphisms have been declared. \item[constants [\ltac]] specifies a tactic expression that, given a term, returns either an object of the coefficient set that is mapped to @@ -297,7 +297,7 @@ tactic we used \Coq\ as a programming language and also as a proof environment to build a tactic and to prove it correctness. The interested reader is strongly advised to have a look at the file -\texttt{Pol.v}. Here a type for polynomials is defined: +\texttt{Ring_polynom.v}. Here a type for polynomials is defined: \begin{small} \begin{flushleft} @@ -402,9 +402,9 @@ associative commutative rewriting on every ring. The tactic must be loaded by \texttt{Require Import LegacyRing}. The ring must be declared in the \texttt{Add Ring} command. The ring of booleans is predefined; if one wants to use the tactic on \texttt{nat} one must -first require the module \texttt{ArithRing}; for \texttt{Z}, do -\texttt{Require Import ZArithRing}; for \texttt{N}, do \texttt{Require -Import NArithRing}. +first require the module \texttt{LegacyArithRing}; for \texttt{Z}, do +\texttt{Require Import LegacyZArithRing}; for \texttt{N}, do \texttt{Require +Import LegacyNArithRing}. The terms \term$_1$, \dots, \term$_n$ must be subterms of the goal conclusion. The tactic \texttt{ring} normalizes these terms diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 85499fe100..5f38017b7c 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2710,7 +2710,7 @@ Goal forall x y:R, \end{coq_example*} \begin{coq_example} -intros; legacy field. +intros; field. \end{coq_example} \begin{coq_eval} diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index ade0cd5ebb..65644d0eac 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require Import Field Field_tac. +Require Import Field. Require Import QArith. Require Import Znumtheory. Require Import Eqdep_dec. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index c6feb4ac6e..ff3a975e04 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -15,7 +15,8 @@ Require Export Raxioms. Require Export ZArithRing. Require Import Omega. -Require Export Field_tac. Import Field. +Require Export RealField. +Require Export LegacyField. Open Local Scope Z_scope. Open Local Scope R_scope. @@ -23,109 +24,33 @@ Open Local Scope R_scope. Implicit Type r : R. (***************************************************************************) -(** Instantiating Ring tactic on reals *) +(** Instantiating Field tactic on reals *) (***************************************************************************) -Lemma RTheory : ring_theory 0 1 Rplus Rmult Rminus Ropp (eq (A:=R)). -Proof. -constructor. - intro; apply Rplus_0_l. - exact Rplus_comm. - symmetry in |- *; apply Rplus_assoc. - intro; apply Rmult_1_l. - exact Rmult_comm. - symmetry in |- *; apply Rmult_assoc. - intros m n p. - rewrite Rmult_comm in |- *. - rewrite (Rmult_comm n p) in |- *. - rewrite (Rmult_comm m p) in |- *. - apply Rmult_plus_distr_l. - reflexivity. - exact Rplus_opp_r. -Qed. - -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. -Proof. -intro. -elim archimed with x; intros. -destruct H0. - apply Rlt_trans with (IZR (up x)); trivial. - replace (IZR (up x)) with (x + (IZR (up x) - x))%R. - apply Rplus_lt_compat_l; trivial. - unfold Rminus in |- *. - rewrite (Rplus_comm (IZR (up x)) (- x)) in |- *. - rewrite <- Rplus_assoc in |- *. - rewrite Rplus_opp_r in |- *. - apply Rplus_0_l. - elim H0. - unfold Rminus in |- *. - rewrite (Rplus_comm (IZR (up x)) (- x)) in |- *. - rewrite <- Rplus_assoc in |- *. - rewrite Rplus_opp_r in |- *. - rewrite Rplus_0_l in |- *; trivial. -Qed. - -Notation Rset := (Eqsth R). -Notation Rext := (Eq_ext Rplus Rmult Ropp). - -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. - replace 1 with (0 + 1). - apply Rlt_n_Sn. - apply Rplus_0_l. -Qed. - -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). - rewrite Rplus_comm in |- *. - apply Rlt_n_Sn. - apply Rplus_lt_compat_l. - rewrite <- (Rmul_0_l Rset Rext RTheory 2) in |- *. - rewrite Rmult_comm in |- *. - apply Rmult_lt_compat_l. - apply Rlt_0_2. - trivial. - rewrite <- (Rmul_0_l Rset Rext RTheory 2) in |- *. - rewrite Rmult_comm in |- *. - apply Rmult_lt_compat_l. - apply Rlt_0_2. - trivial. - replace 1 with (0 + 1). - apply Rlt_n_Sn. - apply Rplus_0_l. -Qed. - - -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. - -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. -Proof gen_phiZ_complete _ _ _ _ _ _ _ _ _ _ Rset Rext Rfield Rgen_phiPOS_not_0. - -Add Field RField : Rfield (infinite Zeq_bool_complete). +(* Legacy Field *) +Require Export LegacyField. +Import LegacyRing_theory. + +Lemma RLegacyTheory : Ring_Theory Rplus Rmult 1 0 Ropp (fun x y:R => false). + split. + exact Rplus_comm. + symmetry in |- *; apply Rplus_assoc. + exact Rmult_comm. + symmetry in |- *; apply Rmult_assoc. + intro; apply Rplus_0_l. + intro; apply Rmult_1_l. + exact Rplus_opp_r. + intros. + rewrite Rmult_comm. + rewrite (Rmult_comm n p). + rewrite (Rmult_comm m p). + apply Rmult_plus_distr_l. + intros; contradiction. +Defined. + +Add Legacy Field + R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RLegacyTheory Rinv_l + with minus := Rminus div := Rdiv. (**************************************************************************) (** Relation between orders and equality *) -- cgit v1.2.3