diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-17 13:31:24 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-17 13:31:24 +0000 |
| commit | cd4f47d6aa9654b163a2494e462aa43001b55fda (patch) | |
| tree | 524cf2c4138b9c973379915ed7558005db8ecdab /theories/QArith | |
| parent | 0768a9c968dfc205334dabdd3e86d2a91bb7a33a (diff) | |
BigN, BigZ, BigQ: presentation via unique module with both ops and props
We use the <+ operation to regroup all known facts about BigN
(resp BigZ, ...) in a unique module. This uses also the new ! feature
for controling inlining. By the way, we also make sure that these
new BigN and BigZ modules implements OrderedTypeFull and TotalOrder,
and also contains facts about min and max (cf. GenericMinMax).
Side effects:
- In NSig and ZSig, specification of compare and eq_bool is now
done with respect to Zcompare and Zeq_bool, as for other ops.
The order <= and < are also defined via Zle and Zlt, instead
of using compare. Min and max are axiomatized instead of being
macros.
- Some proofs rework in QMake
- QOrderedType and Qminmax were in fact not compiled by make world
Still todo: OrderedType + MinMax for BigQ, etc etc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12680 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/QArith')
| -rw-r--r-- | theories/QArith/QOrderedType.v | 6 | ||||
| -rw-r--r-- | theories/QArith/Qminmax.v | 6 | ||||
| -rw-r--r-- | theories/QArith/vo.itarget | 2 |
3 files changed, 9 insertions, 5 deletions
diff --git a/theories/QArith/QOrderedType.v b/theories/QArith/QOrderedType.v index 4d92aadb1..692bfd929 100644 --- a/theories/QArith/QOrderedType.v +++ b/theories/QArith/QOrderedType.v @@ -15,12 +15,12 @@ Local Open Scope Q_scope. Module Q_as_DT <: DecidableTypeFull. Definition t := Q. Definition eq := Qeq. - Definition eq_equiv := Q_setoid. + Definition eq_equiv := Q_Setoid. Definition eqb := Qeq_bool. Definition eqb_eq := Qeq_bool_iff. - Include Backport_ET_fun. (** eq_refl, eq_sym, eq_trans *) - Include Bool2Dec_fun. (** eq_dec *) + Include BackportEq. (** eq_refl, eq_sym, eq_trans *) + Include HasEqBool2Dec. (** eq_dec *) End Q_as_DT. diff --git a/theories/QArith/Qminmax.v b/theories/QArith/Qminmax.v index d20396c86..d05a85947 100644 --- a/theories/QArith/Qminmax.v +++ b/theories/QArith/Qminmax.v @@ -21,8 +21,10 @@ Module QHasMinMax <: HasMinMax Q_as_OT. Module QMM := GenericMinMax Q_as_OT. Definition max := Qmax. Definition min := Qmin. - Definition max_spec := QMM.max_spec. - Definition min_spec := QMM.min_spec. + Definition max_l := QMM.max_l. + Definition max_r := QMM.max_r. + Definition min_l := QMM.min_l. + Definition min_r := QMM.min_r. End QHasMinMax. Module Q. diff --git a/theories/QArith/vo.itarget b/theories/QArith/vo.itarget index bc13ae242..b3faef881 100644 --- a/theories/QArith/vo.itarget +++ b/theories/QArith/vo.itarget @@ -8,3 +8,5 @@ Qreals.vo Qreduction.vo Qring.vo Qround.vo +QOrderedType.vo +Qminmax.vo
\ No newline at end of file |