diff options
Diffstat (limited to 'theories/Structures')
| -rw-r--r-- | theories/Structures/DecidableType2.v | 97 | ||||
| -rw-r--r-- | theories/Structures/OrderedType2.v | 157 |
2 files changed, 171 insertions, 83 deletions
diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v index 585b98136..2679d25b0 100644 --- a/theories/Structures/DecidableType2.v +++ b/theories/Structures/DecidableType2.v @@ -13,33 +13,47 @@ Require Export RelationClasses. Set Implicit Arguments. Unset Strict Implicit. -(** * Types with Equality, and nothing more (for subtyping purpose) *) +(** * Structure with just a base type [t] *) -Module Type BareEquality. +Module Type Typ. Parameter Inline t : Type. +End Typ. + +(** * Structure with an equality relation [eq] *) + +Module Type HasEq (Import T:Typ). Parameter Inline eq : t -> t -> Prop. -End BareEquality. +End HasEq. + +Module Type Eq := Typ <+ HasEq. -(** * Specification of the equality by the Type Classe [Equivalence] *) +Module Type EqNotation (Import E:Eq). + Infix "==" := eq (at level 70, no associativity). + Notation "x ~= y" := (~eq x y) (at level 70, no associativity). +End EqNotation. -Module Type IsEq (Import E:BareEquality). +Module Type Eq' := Eq <+ EqNotation. + +(** * Specification of the equality via the [Equivalence] type class *) + +Module Type IsEq (Import E:Eq). Declare Instance eq_equiv : Equivalence eq. End IsEq. (** * Earlier specification of equality by three separate lemmas. *) -Module Type IsEqOrig (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. +Module Type IsEqOrig (Import E:Eq'). + Axiom eq_refl : forall x : t, x==x. + Axiom eq_sym : forall x y : t, x==y -> y==x. + Axiom eq_trans : forall x y z : t, x==y -> y==z -> x==z. Hint Immediate eq_sym. Hint Resolve eq_refl eq_trans. End IsEqOrig. (** * Types with decidable equality *) -Module Type HasEqDec (Import E:BareEquality). - Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }. +Module Type HasEqDec (Import E:Eq'). + Parameter eq_dec : forall x y : t, { x==y } + { ~ x==y }. End HasEqDec. (** * Boolean Equality *) @@ -47,50 +61,61 @@ End HasEqDec. (** Having [eq_dec] is the same as having a boolean equality plus a correctness proof. *) -Module Type HasEqBool (Import E:BareEquality). +Module Type HasEqBool (Import E:Eq'). Parameter Inline eqb : t -> t -> bool. - Parameter eqb_eq : forall x y, eqb x y = true <-> eq x y. + Parameter eqb_eq : forall x y, eqb x y = true <-> x==y. End HasEqBool. (** From these basic blocks, we can build many combinations of static standalone module types. *) -Module Type EqualityType := BareEquality <+ IsEq. +Module Type EqualityType := Eq <+ IsEq. -Module Type EqualityTypeOrig := BareEquality <+ IsEqOrig. +Module Type EqualityTypeOrig := Eq <+ IsEqOrig. Module Type EqualityTypeBoth <: EqualityType <: EqualityTypeOrig - := BareEquality <+ IsEq <+ IsEqOrig. + := Eq <+ IsEq <+ IsEqOrig. Module Type DecidableType <: EqualityType - := BareEquality <+ IsEq <+ HasEqDec. + := Eq <+ IsEq <+ HasEqDec. Module Type DecidableTypeOrig <: EqualityTypeOrig - := BareEquality <+ IsEqOrig <+ HasEqDec. + := Eq <+ IsEqOrig <+ HasEqDec. Module Type DecidableTypeBoth <: DecidableType <: DecidableTypeOrig := EqualityTypeBoth <+ HasEqDec. Module Type BooleanEqualityType <: EqualityType - := BareEquality <+ IsEq <+ HasEqBool. + := Eq <+ IsEq <+ HasEqBool. Module Type BooleanDecidableType <: DecidableType <: BooleanEqualityType - := BareEquality <+ IsEq <+ HasEqDec <+ HasEqBool. + := Eq <+ IsEq <+ HasEqDec <+ HasEqBool. Module Type DecidableTypeFull <: DecidableTypeBoth <: BooleanDecidableType - := BareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool. + := Eq <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool. + +(** Same, with notation for [eq] *) +Module Type EqualityType' := EqualityType <+ EqNotation. +Module Type EqualityTypeOrig' := EqualityTypeOrig <+ EqNotation. +Module Type EqualityTypeBoth' := EqualityTypeBoth <+ EqNotation. +Module Type DecidableType' := DecidableType <+ EqNotation. +Module Type DecidableTypeOrig' := DecidableTypeOrig <+ EqNotation. +Module Type DecidableTypeBoth' := DecidableTypeBoth <+ EqNotation. +Module Type BooleanEqualityType' := BooleanEqualityType <+ EqNotation. +Module Type BooleanDecidableType' := BooleanDecidableType <+ EqNotation. +Module Type DecidableTypeFull' := DecidableTypeFull <+ EqNotation. (** * Compatibility wrapper from/to the old version of [EqualityType] and [DecidableType] *) -Module BackportEq (E:BareEquality)(F:IsEq E) <: IsEqOrig E. +Module BackportEq (E:Eq)(F:IsEq E) <: IsEqOrig 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 BackportEq. -Module UpdateEq (E:BareEquality)(F:IsEqOrig E) <: IsEq E. +Module UpdateEq (E:Eq)(F:IsEqOrig E) <: IsEq E. Instance eq_equiv : Equivalence E.eq. Proof. exact (Build_Equivalence _ _ F.eq_refl F.eq_sym F.eq_trans). Qed. End UpdateEq. @@ -110,7 +135,7 @@ Module Update_DT (E:DecidableTypeOrig) <: DecidableTypeBoth (** * Having [eq_dec] is equivalent to having [eqb] and its spec. *) -Module HasEqDec2Bool (E:BareEquality)(F:HasEqDec E) <: HasEqBool E. +Module HasEqDec2Bool (E:Eq)(F:HasEqDec E) <: HasEqBool 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. @@ -120,7 +145,7 @@ Module HasEqDec2Bool (E:BareEquality)(F:HasEqDec E) <: HasEqBool E. Qed. End HasEqDec2Bool. -Module HasEqBool2Dec (E:BareEquality)(F:HasEqBool E) <: HasEqDec E. +Module HasEqBool2Dec (E:Eq)(F:HasEqBool E) <: HasEqDec 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). @@ -143,45 +168,45 @@ Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType A particular case of [DecidableType] where the equality is the usual one of Coq. *) -Module Type UsualBareEquality <: BareEquality. +Module Type UsualEq <: Eq. Parameter Inline t : Type. Definition eq := @eq t. -End UsualBareEquality. +End UsualEq. -Module UsualIsEq (E:UsualBareEquality) <: IsEq E. +Module UsualIsEq (E:UsualEq) <: IsEq E. Program Instance eq_equiv : Equivalence E.eq. End UsualIsEq. -Module UsualIsEqOrig (E:UsualBareEquality) <: IsEqOrig E. +Module UsualIsEqOrig (E:UsualEq) <: IsEqOrig E. Definition eq_refl := @eq_refl E.t. Definition eq_sym := @eq_sym E.t. Definition eq_trans := @eq_trans E.t. End UsualIsEqOrig. Module Type UsualEqualityType <: EqualityType - := UsualBareEquality <+ IsEq. + := UsualEq <+ IsEq. Module Type UsualDecidableType <: DecidableType - := UsualBareEquality <+ IsEq <+ HasEqDec. + := UsualEq <+ IsEq <+ HasEqDec. Module Type UsualDecidableTypeBoth <: DecidableTypeBoth - := UsualBareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec. + := UsualEq <+ IsEq <+ IsEqOrig <+ HasEqDec. -Module Type UsualBoolEq := UsualBareEquality <+ HasEqBool. +Module Type UsualBoolEq := UsualEq <+ HasEqBool. Module Type UsualDecidableTypeFull <: DecidableTypeFull - := UsualBareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool. + := UsualEq <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool. (** Some shortcuts for easily building a [UsualDecidableType] *) Module Type MiniDecidableType. Parameter t : Type. - Parameter eq_dec : forall x y : t, {eq x y}+{~eq x y}. + Parameter eq_dec : forall x y : t, {x=y}+{~x=y}. End MiniDecidableType. Module Make_UDT (M:MiniDecidableType) <: UsualDecidableTypeBoth. - Definition eq := @eq M.t. + Definition eq := @Logic.eq M.t. Include M <+ UsualIsEq <+ UsualIsEqOrig. End Make_UDT. diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v index be7ec153b..5b669db4e 100644 --- a/theories/Structures/OrderedType2.v +++ b/theories/Structures/OrderedType2.v @@ -14,82 +14,145 @@ Unset Strict Implicit. (** * Ordered types *) -Module Type MiniOrderedType. - Include Type EqualityType. +(** First, signatures with only the order relations *) +Module Type HasLt (Import T:Typ). Parameter Inline lt : t -> t -> Prop. +End HasLt. + +Module Type HasLe (Import T:Typ). + Parameter Inline le : t -> t -> Prop. +End HasLe. + +Module Type EqLt := Typ <+ HasEq <+ HasLt. +Module Type EqLe := Typ <+ HasEq <+ HasLe. +Module Type EqLtLe := Typ <+ HasEq <+ HasLt <+ HasLe. + +(** Versions with nice notations *) + +Module Type LtNotation (E:EqLt). + Infix "<" := E.lt. + Notation "x < y < z" := (x<y /\ y<z). +End LtNotation. + +Module Type LeNotation (E:EqLe). + Infix "<=" := E.le. + Notation "x <= y <= z" := (x<=y /\ y<=z). +End LeNotation. + +Module Type LtLeNotation (E:EqLtLe). + Include Type LtNotation E <+ LeNotation E. + Notation "x <= y < z" := (x<=y /\ y<z). + Notation "x < y <= z" := (x<y /\ y<=z). +End LtLeNotation. + +Module Type EqLtNotation (E:EqLt) := EqNotation E <+ LtNotation E. +Module Type EqLeNotation (E:EqLe) := EqNotation E <+ LeNotation E. +Module Type EqLtLeNotation (E:EqLtLe) := EqNotation E <+ LtLeNotation E. + +Module Type EqLt' := EqLt <+ EqLtNotation. +Module Type EqLe' := EqLe <+ EqLeNotation. +Module Type EqLtLe' := EqLtLe <+ EqLtLeNotation. + +(** Versions with logical specifications *) + +Module Type IsStrOrder (Import E:EqLt). Declare Instance lt_strorder : StrictOrder lt. Declare Instance lt_compat : Proper (eq==>eq==>iff) lt. +End IsStrOrder. +Module Type LeIsLtEq (Import E:EqLtLe'). + Axiom le_lteq : forall x y, x<=y <-> x<y \/ x==y. +End LeIsLtEq. + +Module Type HasCompare (Import E:EqLt). Parameter Inline compare : t -> t -> comparison. Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y). +End HasCompare. -End MiniOrderedType. - +Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder. +Module Type DecStrOrder := StrOrder <+ HasCompare. +Module Type OrderedType <: DecidableType := DecStrOrder <+ HasEqDec. +Module Type OrderedTypeFull := OrderedType <+ HasLe <+ LeIsLtEq. -Module Type OrderedType. - Include Type MiniOrderedType. +Module Type StrOrder' := StrOrder <+ EqLtNotation. +Module Type DecStrOrder' := DecStrOrder <+ EqLtNotation. +Module Type OrderedType' := OrderedType <+ EqLtNotation. +Module Type OrderedTypeFull' := OrderedTypeFull <+ EqLtLeNotation. - (** A [eq_dec] can be deduced from [compare] below. But adding this - redundant field allows to see an OrderedType as a DecidableType. *) - Parameter eq_dec : forall x y, { eq x y } + { ~ eq x y }. -End OrderedType. +(** NB: in [OrderedType], an [eq_dec] could be deduced from [compare]. + But adding this redundant field allows to see an [OrderedType] as a + [DecidableType]. *) +(** * Versions with [eq] being the usual Leibniz equality of Coq *) -Module MOT_to_OT (Import O : MiniOrderedType) <: OrderedType. - Include O. +Module Type UsualStrOrder := UsualEqualityType <+ HasLt <+ IsStrOrder. +Module Type UsualDecStrOrder := UsualStrOrder <+ HasCompare. +Module Type UsualOrderedType <: UsualDecidableType <: OrderedType + := UsualDecStrOrder <+ HasEqDec. +Module Type UsualOrderedTypeFull := UsualOrderedType <+ HasLe <+ LeIsLtEq. - Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}. - Proof. - intros. - assert (H:=compare_spec x y); destruct (compare x y). - left; inversion_clear H; auto. - right; inversion_clear H. intro H'. rewrite H' in *. - apply (StrictOrder_Irreflexive y); auto. - right; inversion_clear H. intro H'. rewrite H' in *. - apply (StrictOrder_Irreflexive y); auto. - Defined. +(** NB: in [UsualOrderedType], the field [lt_compat] is + useless since [eq] is [Leibniz], but it should be + there for subtyping. *) -End MOT_to_OT. +Module Type UsualStrOrder' := UsualStrOrder <+ LtNotation. +Module Type UsualDecStrOrder' := UsualDecStrOrder <+ LtNotation. +Module Type UsualOrderedType' := UsualOrderedType <+ LtNotation. +Module Type UsualOrderedTypeFull' := UsualOrderedTypeFull <+ LtLeNotation. +(** * Purely logical versions *) -(** * UsualOrderedType +Module Type LtIsTotal (Import E:EqLt'). + Axiom lt_total : forall x y, x<y \/ x==y \/ y<x. +End LtIsTotal. - A particular case of [OrderedType] where the equality is - the usual one of Coq. *) +Module Type TotalOrder := StrOrder <+ HasLe <+ LeIsLtEq <+ LtIsTotal. +Module Type UsualTotalOrder <: TotalOrder + := UsualStrOrder <+ HasLe <+ LeIsLtEq <+ LtIsTotal. -Module Type UsualOrderedType. - Include Type UsualDecidableType. +Module Type TotalOrder' := TotalOrder <+ EqLtLeNotation. +Module Type UsualTotalOrder' := UsualTotalOrder <+ LtLeNotation. - Parameter Inline lt : t -> t -> Prop. - Declare Instance lt_strorder : StrictOrder lt. - (* The following is useless since eq is Leibniz, but should be there - for subtyping... *) - Declare Instance lt_compat : Proper (eq==>eq==>iff) lt. +(** * Conversions *) - Parameter Inline compare : t -> t -> comparison. - Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y). +(** From [compare] to [eqb], and then [eq_dec] *) -End UsualOrderedType. +Module Compare2EqBool (Import O:DecStrOrder') <: HasEqBool O. -(** a [UsualOrderedType] is in particular an [OrderedType]. *) + Definition eqb x y := + match compare x y with Eq => true | _ => false end. -Module UOT_to_OT (U:UsualOrderedType) <: OrderedType := U. + Lemma eqb_eq : forall x y, eqb x y = true <-> x==y. + Proof. + unfold eqb. intros x y. + destruct (compare_spec x y) as [H|H|H]; split; auto; try discriminate. + intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H). + intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H). + Qed. +End Compare2EqBool. -(** * OrderedType with also a [<=] predicate *) +Module DSO_to_OT (O:DecStrOrder) <: OrderedType := + O <+ Compare2EqBool <+ HasEqBool2Dec. -Module Type OrderedTypeFull. - Include Type OrderedType. - Parameter Inline le : t -> t -> Prop. - Axiom le_lteq : forall x y, le x y <-> lt x y \/ eq x y. -End OrderedTypeFull. +(** From [OrderedType] To [OrderedTypeFull] (adding [<=]) *) -Module OT_to_Full (O:OrderedType) <: OrderedTypeFull. +Module OT_to_Full (O:OrderedType') <: OrderedTypeFull. Include O. - Definition le x y := lt x y \/ eq x y. - Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y. + Definition le x y := x<y \/ x==y. + Lemma le_lteq : forall x y, le x y <-> x<y \/ x==y. Proof. unfold le; split; auto. Qed. End OT_to_Full. +(** From computational to logical versions *) + +Module OTF_LtIsTotal (Import O:OrderedTypeFull') <: LtIsTotal O. + Lemma lt_total : forall x y, x<y \/ x==y \/ y<x. + Proof. intros; destruct (compare_spec x y); auto. Qed. +End OTF_LtIsTotal. + +Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder + := O <+ OTF_LtIsTotal. + |