diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-05 14:20:28 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-05 23:47:32 +0200 |
commit | 6526933e3d6a6392aa6bd5235ea0180bb68b6f94 (patch) | |
tree | 83fdc73e5ef1c0e7bdb8b083b7887d09855ce38d /plugins/setoid_ring/Ring_theory.v | |
parent | 2aac4ae818fec0d409da31ef9da83796d871d687 (diff) |
[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.
The manual has long stated that these forms are deprecated. We add a
warning for them, as indeed `Add Morphism` is an "proof evil" [*]
command, and we may want to remove it in the future.
We've also fixed the stdlib not to emit the warning.
[*] https://ncatlab.org/nlab/show/principle+of+equivalence
Diffstat (limited to 'plugins/setoid_ring/Ring_theory.v')
-rw-r--r-- | plugins/setoid_ring/Ring_theory.v | 39 |
1 files changed, 30 insertions, 9 deletions
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 8dda5ecd3..335a68d70 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -254,8 +254,12 @@ Section ALMOST_RING. Section SEMI_RING. Variable SReqe : sring_eq_ext radd rmul req. - Add Morphism radd : radd_ext1. exact (SRadd_ext SReqe). Qed. - Add Morphism rmul : rmul_ext1. exact (SRmul_ext SReqe). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext1. + Proof. exact (SRadd_ext SReqe). Qed. + + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext1. + Proof. exact (SRmul_ext SReqe). Qed. + Variable SRth : semi_ring_theory 0 1 radd rmul req. (** Every semi ring can be seen as an almost ring, by taking : @@ -323,9 +327,15 @@ Section ALMOST_RING. Notation "- x" := (ropp x). Variable Reqe : ring_eq_ext radd rmul ropp req. - Add Morphism radd : radd_ext2. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext2. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext2. exact (Ropp_ext Reqe). Qed. + + Add Morphism radd with signature (req ==> req ==> req) as radd_ext2. + Proof. exact (Radd_ext Reqe). Qed. + + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext2. + Proof. exact (Rmul_ext Reqe). Qed. + + Add Morphism ropp with signature (req ==> req) as ropp_ext2. + Proof. exact (Ropp_ext Reqe). Qed. Section RING. Variable Rth : ring_theory 0 1 radd rmul rsub ropp req. @@ -393,14 +403,25 @@ Section ALMOST_RING. Notation "?=!" := ceqb. Notation "[ x ]" := (phi x). Variable Csth : Equivalence ceq. Variable Ceqe : ring_eq_ext cadd cmul copp ceq. + Add Setoid C ceq Csth as C_setoid. - Add Morphism cadd : cadd_ext. exact (Radd_ext Ceqe). Qed. - Add Morphism cmul : cmul_ext. exact (Rmul_ext Ceqe). Qed. - Add Morphism copp : copp_ext. exact (Ropp_ext Ceqe). Qed. + + Add Morphism cadd with signature (ceq ==> ceq ==> ceq) as cadd_ext. + Proof. exact (Radd_ext Ceqe). Qed. + + Add Morphism cmul with signature (ceq ==> ceq ==> ceq) as cmul_ext. + Proof. exact (Rmul_ext Ceqe). Qed. + + Add Morphism copp with signature (ceq ==> ceq) as copp_ext. + Proof. exact (Ropp_ext Ceqe). Qed. + Variable Cth : ring_theory cO cI cadd cmul csub copp ceq. Variable Smorph : semi_morph 0 1 radd rmul req cO cI cadd cmul ceqb phi. Variable phi_ext : forall x y, ceq x y -> [x] == [y]. - Add Morphism phi : phi_ext1. exact phi_ext. Qed. + + Add Morphism phi with signature (ceq ==> req) as phi_ext1. + Proof. exact phi_ext. Qed. + Lemma Smorph_opp x : [-!x] == -[x]. Proof. rewrite <- (Rth.(Radd_0_l) [-!x]). |