diff options
Diffstat (limited to 'theories/Structures/GenericMinMax.v')
-rw-r--r-- | theories/Structures/GenericMinMax.v | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index 68f20189..5583142f 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -79,7 +79,7 @@ End GenericMinMax. (** ** Consequences of the minimalist interface: facts about [max]. *) Module MaxLogicalProperties (Import O:TotalOrder')(Import M:HasMax O). - Module Import T := !MakeOrderTac O. + Module Import Private_Tac := !MakeOrderTac O. (** An alternative caracterisation of [max], equivalent to [max_l /\ max_r] *) @@ -277,8 +277,9 @@ End MaxLogicalProperties. Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O). Include MaxLogicalProperties O M. - Import T. + Import Private_Tac. + Module Import Private_Rev. Module ORev := TotalOrderRev O. Module MRev <: HasMax ORev. Definition max x y := M.min y x. @@ -286,6 +287,7 @@ Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O). Definition max_r x y := M.min_l y x. End MRev. Module MPRev := MaxLogicalProperties ORev MRev. + End Private_Rev. Instance min_compat : Proper (eq==>eq==>eq) min. Proof. intros x x' Hx y y' Hy. apply MPRev.max_compat; assumption. Qed. @@ -578,29 +580,29 @@ End UsualMinMaxLogicalProperties. Module UsualMinMaxDecProperties (Import O:UsualOrderedTypeFull')(Import M:HasMinMax O). - Module P := MinMaxDecProperties O M. + Module Import Private_Dec := MinMaxDecProperties O M. Lemma max_case_strong : forall n m (P:t -> Type), (m<=n -> P n) -> (n<=m -> P m) -> P (max n m). - Proof. intros; apply P.max_case_strong; auto. congruence. Defined. + Proof. intros; apply max_case_strong; auto. congruence. Defined. Lemma max_case : forall n m (P:t -> Type), P n -> P m -> P (max n m). Proof. intros; apply max_case_strong; auto. Defined. Lemma max_dec : forall n m, {max n m = n} + {max n m = m}. - Proof. exact P.max_dec. Defined. + Proof. exact max_dec. Defined. Lemma min_case_strong : forall n m (P:O.t -> Type), (n<=m -> P n) -> (m<=n -> P m) -> P (min n m). - Proof. intros; apply P.min_case_strong; auto. congruence. Defined. + Proof. intros; apply min_case_strong; auto. congruence. Defined. Lemma min_case : forall n m (P:O.t -> Type), P n -> P m -> P (min n m). Proof. intros. apply min_case_strong; auto. Defined. Lemma min_dec : forall n m, {min n m = n} + {min n m = m}. - Proof. exact P.min_dec. Defined. + Proof. exact min_dec. Defined. End UsualMinMaxDecProperties. |