aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Raxioms.v
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2017-03-05 21:03:51 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-22 17:31:30 +0100
commite1ef9491edaf8f7e6f553c49b24163b7e2a53825 (patch)
tree08f89d143cfc92de4a4d7fe80aa13cb8d5137f20 /theories/Reals/Raxioms.v
parenta4a76c253474ac4ce523b70d0150ea5dcf546385 (diff)
Change the parser and printer so that they use IZR for real constants.
There are two main issues. First, (-cst)%R is no longer syntactically equal to (-(cst))%R (though they are still convertible). This breaks some rewriting rules. Second, the ring/field_simplify tactics did not know how to refold real constants. This defect is no longer hidden by the pretty-printer, which makes these tactics almost unusable on goals containing large constants. This commit also modifies the ring/field tactics so that real constant reification is now constant time rather than linear. Note that there is now a bit of code duplication between z_syntax and r_syntax. This should be fixed once plugin interdependencies are supported. Ideally the r_syntax plugin should just disappear by declaring IZR as a coercion. Unfortunately the coercion mechanism is not powerful enough yet, be it for parsing (need the ability for a scope to delegate constant parsing to another scope) or printing (too many visible coercions left).
Diffstat (limited to 'theories/Reals/Raxioms.v')
-rw-r--r--theories/Reals/Raxioms.v29
1 files changed, 0 insertions, 29 deletions
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index e9098104c..7f9db3b18 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -115,35 +115,6 @@ Arguments INR n%nat.
(**********************************************************)
-(** * Injection from [Z] to [R] *)
-(**********************************************************)
-
-(* compact representation for 2*p *)
-Fixpoint IPR_2 (p:positive) : R :=
- match p with
- | xH => 1 + 1
- | xO p => (1 + 1) * IPR_2 p
- | xI p => (1 + 1) * (1 + IPR_2 p)
- end.
-
-Definition IPR (p:positive) : R :=
- match p with
- | xH => 1
- | xO p => IPR_2 p
- | xI p => 1 + IPR_2 p
- end.
-Arguments IPR p%positive : simpl never.
-
-(**********)
-Definition IZR (z:Z) : R :=
- match z with
- | Z0 => 0
- | Zpos n => IPR n
- | Zneg n => - IPR n
- end.
-Arguments IZR z%Z : simpl never.
-
-(**********************************************************)
(** * [R] Archimedean *)
(**********************************************************)