diff options
Diffstat (limited to 'plugins/setoid_ring/Field_theory.v')
| -rw-r--r-- | plugins/setoid_ring/Field_theory.v | 40 |
1 files changed, 27 insertions, 13 deletions
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 2932d379..d9e32dbb 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Ring. @@ -56,11 +58,16 @@ Let rI_neq_rO := AFth.(AF_1_neq_0). Let rdiv_def := AFth.(AFdiv_def). Let rinv_l := AFth.(AFinv_l). -Add Morphism radd : radd_ext. Proof. exact (Radd_ext Reqe). Qed. -Add Morphism rmul : rmul_ext. Proof. exact (Rmul_ext Reqe). Qed. -Add Morphism ropp : ropp_ext. Proof. exact (Ropp_ext Reqe). Qed. -Add Morphism rsub : rsub_ext. Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. -Add Morphism rinv : rinv_ext. Proof. exact SRinv_ext. Qed. +Add Morphism radd with signature (req ==> req ==> req) as radd_ext. +Proof. exact (Radd_ext Reqe). Qed. +Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext. +Proof. exact (Rmul_ext Reqe). Qed. +Add Morphism ropp with signature (req ==> req) as ropp_ext. +Proof. exact (Ropp_ext Reqe). Qed. +Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext. +Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. +Add Morphism rinv with signature (req ==> req) as rinv_ext. +Proof. exact SRinv_ext. Qed. Let eq_trans := Setoid.Seq_trans _ _ Rsth. Let eq_sym := Setoid.Seq_sym _ _ Rsth. @@ -1607,11 +1614,18 @@ Section Complete. 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. + Add Parametric Relation : R req + reflexivity proved by Rsth.(@Equivalence_Reflexive _ _) + symmetry proved by Rsth.(@Equivalence_Symmetric _ _) + transitivity proved by Rsth.(@Equivalence_Transitive _ _) + 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. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext3. + Proof. exact (Radd_ext Reqe). Qed. + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext3. + Proof. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp with signature (req ==> req) as ropp_ext3. + Proof. exact (Ropp_ext Reqe). Qed. Section AlmostField. |