diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-03-05 21:03:51 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-22 17:31:30 +0100 |
commit | e1ef9491edaf8f7e6f553c49b24163b7e2a53825 (patch) | |
tree | 08f89d143cfc92de4a4d7fe80aa13cb8d5137f20 /plugins/setoid_ring/RealField.v | |
parent | a4a76c253474ac4ce523b70d0150ea5dcf546385 (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 'plugins/setoid_ring/RealField.v')
-rw-r--r-- | plugins/setoid_ring/RealField.v | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v index 293722125..facd2e062 100644 --- a/plugins/setoid_ring/RealField.v +++ b/plugins/setoid_ring/RealField.v @@ -59,11 +59,12 @@ Notation Rset := (Eqsth R). Notation Rext := (Eq_ext Rplus Rmult Ropp). Lemma Rlt_0_2 : 0 < 2. +Proof. apply Rlt_trans with (0 + 1). apply Rlt_n_Sn. rewrite Rplus_comm. apply Rplus_lt_compat_l. - replace 1 with (0 + 1). + replace R1 with (0 + 1). apply Rlt_n_Sn. apply Rplus_0_l. Qed. @@ -126,9 +127,17 @@ Ltac Rpow_tac t := | _ => constr:(N.of_nat t) end. -Add Field RField : Rfield - (completeness Zeq_bool_complete, power_tac R_power_theory [Rpow_tac]). - - - +Ltac IZR_tac t := + match t with + | R0 => constr:(0%Z) + | R1 => constr:(1%Z) + | IZR ?u => + match isZcst u with + | true => u + | _ => constr:(InitialRing.NotConstant) + end + | _ => constr:(InitialRing.NotConstant) + end. +Add Field RField : Rfield + (completeness Zeq_bool_complete, constants [IZR_tac], power_tac R_power_theory [Rpow_tac]). |