diff options
| -rw-r--r-- | theories/Arith/NatOrderedType.v | 17 | ||||
| -rw-r--r-- | theories/NArith/NOrderedType.v | 16 | ||||
| -rw-r--r-- | theories/NArith/POrderedType.v | 16 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZAxioms.v | 114 | ||||
| -rw-r--r-- | theories/QArith/QOrderedType.v | 17 | ||||
| -rw-r--r-- | theories/Reals/ROrderedType.v | 17 | ||||
| -rw-r--r-- | theories/Structures/DecidableType2.v | 276 | ||||
| -rw-r--r-- | theories/ZArith/ZOrderedType.v | 15 |
8 files changed, 322 insertions, 166 deletions
diff --git a/theories/Arith/NatOrderedType.v b/theories/Arith/NatOrderedType.v index 01e84a525..287d0c955 100644 --- a/theories/Arith/NatOrderedType.v +++ b/theories/Arith/NatOrderedType.v @@ -12,20 +12,17 @@ Require Import Lt Peano_dec Compare_dec EqNat (** * DecidableType structure for Peano numbers *) -Module Nat_as_MiniDT <: MiniDecidableType. +Module Nat_as_UBE <: UsualBoolEq. Definition t := nat. - Definition eq_dec := eq_nat_dec. -End Nat_as_MiniDT. - -Module Nat_as_DT <: UsualDecidableType. - Include Make_UDT Nat_as_MiniDT. - (** The next fields aren't mandatory but allow more subtyping. *) + Definition eq := @eq nat. Definition eqb := beq_nat. Definition eqb_eq := beq_nat_true_iff. -End Nat_as_DT. +End Nat_as_UBE. + +Module Nat_as_DT <: UsualDecidableTypeFull := Make_UDTF Nat_as_UBE. -(** Note that [Nat_as_DT] can also be seen as a [DecidableType], - or a [DecidableTypeOrig] or a [BooleanEqualityType]. *) +(** Note that the last module fulfills by subtyping many other + interfaces, such as [DecidableType] or [EqualityType]. *) diff --git a/theories/NArith/NOrderedType.v b/theories/NArith/NOrderedType.v index c47b4b4fe..08391d33f 100644 --- a/theories/NArith/NOrderedType.v +++ b/theories/NArith/NOrderedType.v @@ -13,19 +13,17 @@ Local Open Scope N_scope. (** * DecidableType structure for [N] binary natural numbers *) -Module N_as_MiniDT <: MiniDecidableType. +Module N_as_UBE <: UsualBoolEq. Definition t := N. - Definition eq_dec := N_eq_dec. -End N_as_MiniDT. - -Module N_as_DT <: UsualDecidableType. - Include Make_UDT N_as_MiniDT. + Definition eq := @eq N. Definition eqb := Neqb. Definition eqb_eq := Neqb_eq. -End N_as_DT. +End N_as_UBE. + +Module N_as_DT <: UsualDecidableTypeFull := Make_UDTF N_as_UBE. -(** Note that [N_as_DT] can also be seen as a [DecidableType] - and a [DecidableTypeOrig] and a [BooleanEqualityType] *) +(** Note that the last module fulfills by subtyping many other + interfaces, such as [DecidableType] or [EqualityType]. *) diff --git a/theories/NArith/POrderedType.v b/theories/NArith/POrderedType.v index b5629eabe..85667e29a 100644 --- a/theories/NArith/POrderedType.v +++ b/theories/NArith/POrderedType.v @@ -13,20 +13,18 @@ Local Open Scope positive_scope. (** * DecidableType structure for [positive] numbers *) -Module Positive_as_MiniDT <: MiniDecidableType. +Module Positive_as_UBE <: UsualBoolEq. Definition t := positive. - Definition eq_dec := positive_eq_dec. -End Positive_as_MiniDT. - -Module Positive_as_DT <: UsualDecidableType. - Include Make_UDT Positive_as_MiniDT. + Definition eq := @eq positive. Definition eqb := Peqb. Definition eqb_eq := Peqb_eq. -End Positive_as_DT. +End Positive_as_UBE. +Module Positive_as_DT <: UsualDecidableTypeFull + := Make_UDTF Positive_as_UBE. -(** Note that [Positive_as_DT] can also be seen as a [DecidableType] - and a [DecidableTypeOrig] and a [BooleanEqualityType]. *) +(** Note that the last module fulfills by subtyping many other + interfaces, such as [DecidableType] or [EqualityType]. *) diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 9dd6eaf05..c85e84b04 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -10,40 +10,36 @@ (*i $Id$ i*) +Require Import DecidableType2 OrderedType2. Require Export NumPrelude. -Module Type NZAxiomsSig. - -Parameter Inline t : Type. -Parameter Inline eq : t -> t -> Prop. -Parameter Inline zero : t. -Parameter Inline succ : t -> t. -Parameter Inline pred : t -> t. -Parameter Inline add : t -> t -> t. -Parameter Inline sub : t -> t -> t. -Parameter Inline mul : t -> t -> t. +Delimit Scope NumScope with Num. +Local Open Scope NumScope. -(* Unary subtraction (opp) is not defined on natural numbers, so we have - it for integers only *) +(** Axiomatization of a domain with zero, successor, predecessor, + and a bi-directional induction principle. We require [P (S n) = n] + but not the other way around, since this domain is meant + to be either N or Z. In fact it can be a few other things, + for instance [Z/nZ] (See file [NZDomain for a study of that). +*) -Instance eq_equiv : Equivalence eq. -Instance succ_wd : Proper (eq ==> eq) succ. -Instance pred_wd : Proper (eq ==> eq) pred. -Instance add_wd : Proper (eq ==> eq ==> eq) add. -Instance sub_wd : Proper (eq ==> eq ==> eq) sub. -Instance mul_wd : Proper (eq ==> eq ==> eq) mul. +Module Type NZDomain_fun (Import E : EqualityType). + (** [E] provides [t], [eq], [eq_equiv : Equivalence eq] *) -Delimit Scope NumScope with Num. -Local Open Scope NumScope. Notation "x == y" := (eq x y) (at level 70) : NumScope. Notation "x ~= y" := (~ eq x y) (at level 70) : NumScope. + +Parameter Inline zero : t. +Parameter Inline succ : t -> t. +Parameter Inline pred : t -> t. + Notation "0" := zero : NumScope. Notation S := succ. Notation P := pred. Notation "1" := (S 0) : NumScope. -Notation "x + y" := (add x y) : NumScope. -Notation "x - y" := (sub x y) : NumScope. -Notation "x * y" := (mul x y) : NumScope. + +Instance succ_wd : Proper (eq ==> eq) S. +Instance pred_wd : Proper (eq ==> eq) P. Axiom pred_succ : forall n, P (S n) == n. @@ -51,7 +47,35 @@ Axiom bi_induction : forall A : t -> Prop, Proper (eq==>iff) A -> A 0 -> (forall n, A n <-> A (S n)) -> forall n, A n. -Axiom add_0_l : forall n, 0 + n == n. +End NZDomain_fun. + +Module Type NZDomainSig. + Include Type EqualityType. + Include Self Type NZDomain_fun. +End NZDomainSig. + +Module Type NZDecDomainSig. + Include Type DecidableType. + Include Self Type NZDomain_fun. +End NZDecDomainSig. + +(** Axiomatization of basic operations : [+] [-] [*] *) + +Module Type NZBasicFuns_fun (Import NZ : NZDomainSig). + +Parameter Inline add : t -> t -> t. +Parameter Inline sub : t -> t -> t. +Parameter Inline mul : t -> t -> t. + +Notation "x + y" := (add x y) : NumScope. +Notation "x - y" := (sub x y) : NumScope. +Notation "x * y" := (mul x y) : NumScope. + +Instance add_wd : Proper (eq ==> eq ==> eq) add. +Instance sub_wd : Proper (eq ==> eq ==> eq) sub. +Instance mul_wd : Proper (eq ==> eq ==> eq) mul. + +Axiom add_0_l : forall n, (0 + n) == n. Axiom add_succ_l : forall n m, (S n) + m == S (n + m). Axiom sub_0_r : forall n, n - 0 == n. @@ -60,11 +84,21 @@ Axiom sub_succ_r : forall n m, n - (S m) == P (n - m). Axiom mul_0_l : forall n, 0 * n == 0. Axiom mul_succ_l : forall n m, S n * m == n * m + m. -End NZAxiomsSig. +End NZBasicFuns_fun. -Module Type NZOrdAxiomsSig. -Include Type NZAxiomsSig. -Local Open Scope NumScope. +Module Type NZBasicFunsSig. + Include Type NZDomainSig. + Include Self Type NZBasicFuns_fun. +End NZBasicFunsSig. + +(** Old name for the same interface: *) + +Module Type NZAxiomsSig := NZBasicFunsSig. + + +(** Axiomatization of order *) + +Module Type NZOrd_fun (Import NZ : NZDomainSig). Parameter Inline lt : t -> t -> Prop. Parameter Inline le : t -> t -> Prop. @@ -75,18 +109,40 @@ Notation "x > y" := (lt y x) (only parsing) : NumScope. Notation "x >= y" := (le y x) (only parsing) : NumScope. Instance lt_wd : Proper (eq ==> eq ==> iff) lt. -(** Compatibility of [le] can be proved later from [lt_wd] and [lt_eq_cases] *) +(** Compatibility of [le] can be proved later from [lt_wd] + and [lt_eq_cases] *) Axiom lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m. Axiom lt_irrefl : forall n, ~ (n < n). Axiom lt_succ_r : forall n m, n < S m <-> n <= m. +End NZOrd_fun. + +Module Type NZOrdSig. + Include Type NZDomainSig. + Include Self Type NZOrd_fun. +End NZOrdSig. + + +(** Axiomatization of minimum and maximum *) + +Module Type NZMinMax_fun (Import NZ : NZOrdSig). + Parameter Inline min : t -> t -> t. Parameter Inline max : t -> t -> t. + (** Compatibility of [min] and [max] can be proved later *) + Axiom min_l : forall n m, n <= m -> min n m == n. Axiom min_r : forall n m, m <= n -> min n m == m. Axiom max_l : forall n m, m <= n -> max n m == n. Axiom max_r : forall n m, n <= m -> max n m == m. +End NZMinMax_fun. + +Module Type NZOrdAxiomsSig. + Include Type NZDomainSig. + Include Self Type NZBasicFuns_fun. + Include Self Type NZOrd_fun. + Include Self Type NZMinMax_fun. End NZOrdAxiomsSig. diff --git a/theories/QArith/QOrderedType.v b/theories/QArith/QOrderedType.v index f383491d9..cad77b4eb 100644 --- a/theories/QArith/QOrderedType.v +++ b/theories/QArith/QOrderedType.v @@ -13,23 +13,22 @@ Local Open Scope Q_scope. (** * DecidableType structure for rational numbers *) -Module Q_as_DT <: DecidableType. +Module Q_as_DT <: DecidableTypeFull. Definition t := Q. Definition eq := Qeq. Instance eq_equiv : Equivalence Qeq. - Definition eq_dec := Qeq_dec. - - (** The next fields are not mandatory, but allow [Q_as_DT] to be - also a [DecidableTypeOrig] (resp. a [BooleanEqualityType]). *) - Definition eq_refl := Qeq_refl. - Definition eq_sym := Qeq_sym. - Definition eq_trans := eq_trans. - Definition eqb := Qeq_bool. Definition eqb_eq := Qeq_bool_iff. + Include Self Backport_ET_fun. (** eq_refl, eq_sym, eq_trans *) + Include Self Bool2Dec_fun. (** eq_dec *) + End Q_as_DT. +(** Note that the last module fulfills by subtyping many other + interfaces, such as [DecidableType] or [EqualityType]. *) + + (** * OrderedType structure for rational numbers *) diff --git a/theories/Reals/ROrderedType.v b/theories/Reals/ROrderedType.v index ec229abd9..4ef8d7bcc 100644 --- a/theories/Reals/ROrderedType.v +++ b/theories/Reals/ROrderedType.v @@ -25,16 +25,19 @@ Proof. split; try discriminate. intro EQ; elim NEQ; auto. Qed. -Module R_as_MiniDT <: MiniDecidableType. +Module R_as_UBE <: UsualBoolEq. Definition t := R. - Definition eq_dec := Req_dec. -End R_as_MiniDT. - -Module R_as_DT <: UsualDecidableType. - Include Make_UDT R_as_MiniDT. + Definition eq := @eq R. Definition eqb := Reqb. Definition eqb_eq := Reqb_eq. -End R_as_DT. +End R_as_UBE. + +Module R_as_DT <: UsualDecidableTypeFull := Make_UDTF R_as_UBE. + +(** Note that the last module fulfills by subtyping many other + interfaces, such as [DecidableType] or [EqualityType]. *) + + (** Note that [R_as_DT] can also be seen as a [DecidableType] and a [DecidableTypeOrig]. *) diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v index 102572b5b..7cae4358b 100644 --- a/theories/Structures/DecidableType2.v +++ b/theories/Structures/DecidableType2.v @@ -15,138 +15,246 @@ Unset Strict Implicit. (** * Types with Equality, and nothing more (for subtyping purpose) *) -Module Type EqualityType. +Module Type BareEquality. Parameter Inline t : Type. Parameter Inline eq : t -> t -> Prop. - Instance eq_equiv : Equivalence eq. +End BareEquality. + +(** * Specification of the equality by the Type Classe [Equivalence] *) +Module Type Equality_fun (Import E:BareEquality). + Instance eq_equiv : Equivalence eq. Hint Resolve (@Equivalence_Reflexive _ _ eq_equiv). Hint Resolve (@Equivalence_Transitive _ _ eq_equiv). Hint Immediate (@Equivalence_Symmetric _ _ eq_equiv). -End EqualityType. +End Equality_fun. -(** * Types with decidable Equality (but no ordering) *) - -Module Type DecidableType. - Include Type EqualityType. - Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }. -End DecidableType. - -(** * Old versions of [DecidableType], with reflexivity, symmetry, - transitivity as three separate axioms. *) - -Module Type EqualityTypeOrig. - Parameter Inline t : Type. - Parameter Inline eq : t -> t -> Prop. +(** * Earlier specification of equality by three separate lemmas. *) +Module Type EqualityOrig_fun(Import E:BareEquality). Axiom eq_refl : forall x : t, eq x x. Axiom eq_sym : forall x y : t, eq x y -> eq y x. Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. - Hint Immediate eq_sym. Hint Resolve eq_refl eq_trans. -End EqualityTypeOrig. +End EqualityOrig_fun. -Module Type DecidableTypeOrig. - Include Type EqualityTypeOrig. +(** * Types with decidable equality *) + +Module Type Decidable_fun (Import E:BareEquality). Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }. +End Decidable_fun. + +(** * Boolean Equality *) + +(** Having [eq_dec] is the same as having a boolean equality plus + a correctness proof. *) + +Module Type BoolEq_fun (Import E:BareEquality). + Parameter Inline eqb : t -> t -> bool. + Parameter eqb_eq : forall x y, eqb x y = true <-> eq x y. +End BoolEq_fun. + +(** From these basic blocks, we can build many combinations + of static standalone module types. *) + +Module Type EqualityType. + Include Type BareEquality. + Include Self Type Equality_fun. +End EqualityType. + +Module Type EqualityTypeOrig. + Include Type BareEquality. + Include Self Type EqualityOrig_fun. +End EqualityTypeOrig. + +Module Type EqualityTypeBoth. (* <: EqualityType <: EqualityTypeOrig *) + Include Type BareEquality. + Include Self Type Equality_fun. + Include Self Type EqualityOrig_fun. +End EqualityTypeBoth. + +Module Type DecidableType. (* <: EqualityType *) + Include Type BareEquality. + Include Self Type Equality_fun. + Include Self Type Decidable_fun. +End DecidableType. + +Module Type DecidableTypeOrig. (* <: EqualityTypeOrig *) + Include Type BareEquality. + Include Self Type EqualityOrig_fun. + Include Self Type Decidable_fun. End DecidableTypeOrig. -(** * Compatibility wrapper from/to the old version of [DecidableType] *) +Module Type DecidableTypeBoth. (* <: DecidableType <: DecidableTypeOrig *) + Include Type EqualityTypeBoth. + Include Self Type Decidable_fun. +End DecidableTypeBoth. -(** Interestingly, a module can be at the same time a [DecidableType] - and a [DecidableTypeOrig]. For the sake of compatibility, - this will be the case of all [DecidableType] modules provided here. -*) +Module Type BooleanEqualityType. (* <: EqualityType *) + Include Type BareEquality. + Include Self Type Equality_fun. + Include Self Type BoolEq_fun. +End BooleanEqualityType. -Module Backport_ET (E:EqualityType) <: EqualityTypeOrig. +Module Type BooleanDecidableType. (* <: DecidableType <: BooleanEqualityType *) + Include Type BareEquality. + Include Self Type Equality_fun. + Include Self Type Decidable_fun. + Include Self Type BoolEq_fun. +End BooleanDecidableType. + +Module Type DecidableTypeFull. (* <: all previous interfaces *) + Include Type BareEquality. + Include Self Type Equality_fun. + Include Self Type EqualityOrig_fun. + Include Self Type Decidable_fun. + Include Self Type BoolEq_fun. +End DecidableTypeFull. + + +(** * Compatibility wrapper from/to the old version of + [EqualityType] and [DecidableType] *) + +Module Backport_ET_fun (E:BareEquality)(F:Equality_fun E) <: EqualityOrig_fun E. + Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv. + Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv. + Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv. +End Backport_ET_fun. + +Module Update_ET_fun (E:BareEquality)(F:EqualityOrig_fun E) <: Equality_fun E. + Instance eq_equiv : Equivalence E.eq. + Proof. exact (Build_Equivalence _ _ F.eq_refl F.eq_sym F.eq_trans). Qed. +End Update_ET_fun. + +Module Backport_ET (E:EqualityType) <: EqualityTypeBoth. Include E. - Definition eq_refl := @Equivalence_Reflexive _ _ eq_equiv. - Definition eq_sym := @Equivalence_Symmetric _ _ eq_equiv. - Definition eq_trans := @Equivalence_Transitive _ _ eq_equiv. + Include Backport_ET_fun E E. End Backport_ET. -Module Update_ET (E:EqualityTypeOrig) <: EqualityType. +Module Update_ET (E:EqualityTypeOrig) <: EqualityTypeBoth. Include E. - Instance eq_equiv : Equivalence eq. - Proof. exact (Build_Equivalence _ _ eq_refl eq_sym eq_trans). Qed. + Include Update_ET_fun E E. End Update_ET. -Module Backport_DT (E:DecidableType) <: DecidableTypeOrig. - Include Backport_ET E. - Definition eq_dec := E.eq_dec. +Module Backport_DT (E:DecidableType) <: DecidableTypeBoth. + Include E. + Include Backport_ET_fun E E. End Backport_DT. -Module Update_DT (E:DecidableTypeOrig) <: DecidableType. - Include Update_ET E. - Definition eq_dec := E.eq_dec. +Module Update_DT (E:DecidableTypeOrig) <: DecidableTypeBoth. + Include E. + Include Update_ET_fun E E. End Update_DT. +(** * Having [eq_dec] is equivalent to having [eqb] and its spec. *) + +Module Dec2Bool_fun (E:BareEquality)(F:Decidable_fun E) <: BoolEq_fun E. + Definition eqb x y := if F.eq_dec x y then true else false. + Lemma eqb_eq : forall x y, eqb x y = true <-> E.eq x y. + Proof. + intros x y. unfold eqb. destruct F.eq_dec as [EQ|NEQ]. + auto with *. + split. discriminate. intro EQ; elim NEQ; auto. + Qed. +End Dec2Bool_fun. + +Module Bool2Dec_fun (E:BareEquality)(F:BoolEq_fun E) <: Decidable_fun E. + Lemma eq_dec : forall x y, {E.eq x y}+{~E.eq x y}. + Proof. + intros x y. assert (H:=F.eqb_eq x y). + destruct (F.eqb x y); [left|right]. + apply -> H; auto. + intro EQ. apply H in EQ. discriminate. + Defined. +End Bool2Dec_fun. + +Module Dec2Bool (E:DecidableType) <: BooleanDecidableType. + Include E. + Include Dec2Bool_fun E E. +End Dec2Bool. + +Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType. + Include E. + Include Bool2Dec_fun E E. +End Bool2Dec. + + + (** * UsualDecidableType A particular case of [DecidableType] where the equality is the usual one of Coq. *) -Module Type UsualDecidableType. +Module Type UsualBareEquality. (* <: BareEquality *) Parameter Inline t : Type. Definition eq := @eq t. - Program Instance eq_equiv : Equivalence eq. - Parameter eq_dec : forall x y, { eq x y }+{~eq x y }. +End UsualBareEquality. + +Module UsualEquality_fun (E:UsualBareEquality) <: Equality_fun E. + Program Instance eq_equiv : Equivalence E.eq. +End UsualEquality_fun. + +Module UsualEqualityOrig_fun (E:UsualBareEquality) <: EqualityOrig_fun E. + Definition eq_refl := @eq_refl E.t. + Definition eq_sym := @eq_sym E.t. + Definition eq_trans := @eq_trans E.t. +End UsualEqualityOrig_fun. + +Module Type UsualEqualityType. (* <: EqualityType *) + Include Type UsualBareEquality. + Include Self Type Equality_fun. +End UsualEqualityType. + +Module Type UsualDecidableType. (* <: DecidableType *) + Include Type UsualBareEquality. + Include Self Type Equality_fun. + Include Self Type Decidable_fun. End UsualDecidableType. +Module Type UsualDecidableTypeBoth. (* <: DecidableTypeBoth *) + Include Type UsualBareEquality. + Include Self Type Equality_fun. + Include Self Type EqualityOrig_fun. + Include Self Type Decidable_fun. +End UsualDecidableTypeBoth. + +Module Type UsualBoolEq. + Include Type UsualBareEquality. + Include Self Type BoolEq_fun. +End UsualBoolEq. + +Module Type UsualDecidableTypeFull. (* <: DecidableTypeFull *) + Include Type UsualBareEquality. + Include Self Type Equality_fun. + Include Self Type EqualityOrig_fun. + Include Self Type Decidable_fun. + Include Self Type BoolEq_fun. +End UsualDecidableTypeFull. + (** a [UsualDecidableType] is in particular an [DecidableType]. *) Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U. -(** an shortcut for easily building a UsualDecidableType *) +(** Some shortcuts for easily building a UsualDecidableType *) Module Type MiniDecidableType. - Parameter Inline t : Type. - Parameter eq_dec : forall x y:t, { x=y }+{ x<>y }. + Parameter t : Type. + Parameter eq_dec : forall x y : t, {eq x y}+{~eq x y}. End MiniDecidableType. -Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType. - Definition t:=M.t. +Module Make_UDT (M:MiniDecidableType) <: UsualDecidableTypeBoth. + Include M. Definition eq := @eq M.t. - Program Instance eq_equiv : Equivalence eq. - Definition eq_dec := M.eq_dec. - (* For building DecidableTypeOrig at the same time: *) - Definition eq_refl := @Equivalence_Reflexive _ _ eq_equiv. - Definition eq_sym := @Equivalence_Symmetric _ _ eq_equiv. - Definition eq_trans := @Equivalence_Transitive _ _ eq_equiv. + Include Self UsualEquality_fun. + Include Self UsualEqualityOrig_fun. End Make_UDT. +Module Make_UDTF (M:UsualBoolEq) <: UsualDecidableTypeFull. + Include M. (* t, eq, eqb, eqb_eq *) + Include UsualEquality_fun M. + Include UsualEqualityOrig_fun M. + Include Bool2Dec_fun M M. +End Make_UDTF. -(** * Boolean Equality *) - -(** Having [eq_dec] is the same as having a boolean equality plus - a correctness proof. *) - -Module Type BooleanEqualityType. - Include Type EqualityType. - Parameter Inline eqb : t -> t -> bool. - Parameter eqb_eq : forall x y, eqb x y = true <-> eq x y. -End BooleanEqualityType. - -Module Bool_to_Dec (E:BooleanEqualityType) <: DecidableType. - Include E. - Lemma eq_dec : forall x y, {eq x y}+{~eq x y}. - Proof. - intros x y. assert (H:=eqb_eq x y). - destruct (eqb x y); [left|right]. - apply -> H; auto. - intro EQ. apply H in EQ. discriminate. - Defined. -End Bool_to_Dec. - -Module Dec_to_Bool (E:DecidableType) <: BooleanEqualityType. - Include E. - Definition eqb x y := if eq_dec x y then true else false. - Lemma eqb_eq : forall x y, eqb x y = true <-> eq x y. - Proof. - intros x y. unfold eqb. destruct eq_dec as [EQ|NEQ]. - auto with *. - split. discriminate. intro EQ; elim NEQ; auto. - Qed. -End Dec_to_Bool. diff --git a/theories/ZArith/ZOrderedType.v b/theories/ZArith/ZOrderedType.v index b5ba8290c..c717284fd 100644 --- a/theories/ZArith/ZOrderedType.v +++ b/theories/ZArith/ZOrderedType.v @@ -13,20 +13,17 @@ Local Open Scope Z_scope. (** * DecidableType structure for binary integers *) -Module Z_as_MiniDT <: MiniDecidableType. +Module Z_as_UBE <: UsualBoolEq. Definition t := Z. - Definition eq_dec := Z_eq_dec. -End Z_as_MiniDT. - -Module Z_as_DT <: UsualDecidableType. - Include Make_UDT Z_as_MiniDT. + Definition eq := @eq Z. Definition eqb := Zeq_bool. Definition eqb_eq x y := iff_sym (Zeq_is_eq_bool x y). -End Z_as_DT. +End Z_as_UBE. -(** Note that [Z_as_DT] can also be seen as a [DecidableType] - and a [DecidableTypeOrig] and a [BooleanEqualityType] *) +Module Z_as_DT <: UsualDecidableTypeFull := Make_UDTF Z_as_UBE. +(** Note that the last module fulfills by subtyping many other + interfaces, such as [DecidableType] or [EqualityType]. *) (** * OrderedType structure for binary integers *) |