aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/GenericMinMax.v
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-01-17 13:31:24 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-01-17 13:31:24 +0000
commitcd4f47d6aa9654b163a2494e462aa43001b55fda (patch)
tree524cf2c4138b9c973379915ed7558005db8ecdab /theories/Structures/GenericMinMax.v
parent0768a9c968dfc205334dabdd3e86d2a91bb7a33a (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/Structures/GenericMinMax.v')
-rw-r--r--theories/Structures/GenericMinMax.v14
1 files changed, 8 insertions, 6 deletions
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index 01c6134b2..a62d96aa0 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -175,9 +175,6 @@ Qed.
(** *** Least-upper bound properties of [max] *)
-Definition max_l := max_l.
-Definition max_r := max_r.
-
Lemma le_max_l : forall n m, n <= max n m.
Proof.
intros; destruct (max_spec n m); intuition; order.
@@ -329,9 +326,6 @@ Proof. intros. symmetry; apply MPRev.max_assoc. Qed.
Lemma min_comm : forall n m, min n m == min m n.
Proof. intros. exact (MPRev.max_comm m n). Qed.
-Definition min_l := min_l.
-Definition min_r := min_r.
-
Lemma le_min_r : forall n m, min n m <= m.
Proof. intros. exact (MPRev.le_max_l m n). Qed.
@@ -544,6 +538,10 @@ Module MinMaxProperties (Import O:OrderedTypeFull')(Import M:HasMinMax O).
Module OT := OTF_to_TotalOrder O.
Include MinMaxLogicalProperties OT M.
Include MinMaxDecProperties O M.
+ Definition max_l := max_l.
+ Definition max_r := max_r.
+ Definition min_l := min_l.
+ Definition min_r := min_r.
Notation max_monotone := max_mono.
Notation min_monotone := min_mono.
Notation max_min_antimonotone := max_min_antimono.
@@ -611,6 +609,10 @@ Module UsualMinMaxProperties
Module OT := OTF_to_TotalOrder O.
Include UsualMinMaxLogicalProperties OT M.
Include UsualMinMaxDecProperties O M.
+ Definition max_l := max_l.
+ Definition max_r := max_r.
+ Definition min_l := min_l.
+ Definition min_r := min_r.
End UsualMinMaxProperties.