diff --git a/src/Util/Structures/Equalities.v b/src/Util/Structures/Equalities.v index 485f7c160c..ec1b708716 100644 --- a/src/Util/Structures/Equalities.v +++ b/src/Util/Structures/Equalities.v @@ -2,6 +2,11 @@ Require Import Coq.Classes.Morphisms. Require Import Coq.Structures.Equalities. Require Export Crypto.Util.FixCoqMistakes. +Module Type UsualEqualityTypeOrig <: EqualityTypeOrig + := UsualEq <+ UsualIsEqOrig. +Module Type UsualEqualityTypeBoth <: EqualityTypeBoth + := UsualEq <+ UsualIsEq <+ UsualIsEqOrig. + Local Coercion is_true : bool >-> Sortclass. Module Type IsEqb (Import E : Typ) (Import Eb:HasEqb E). #[global] diff --git a/src/Util/Structures/Equalities/Bool.v b/src/Util/Structures/Equalities/Bool.v index e83fc12c76..cad851deb8 100644 --- a/src/Util/Structures/Equalities/Bool.v +++ b/src/Util/Structures/Equalities/Bool.v @@ -73,6 +73,8 @@ Module BoolBooleanDecidableType' := BoolBooleanDecidableType <+ EqNotation <+ Eq Module BoolDecidableTypeFull' := BoolDecidableTypeFull <+ EqNotation. Module BoolUsualEqualityType <: UsualEqualityType := BoolUsualEq <+ UsualIsEq. +Module BoolUsualEqualityTypeOrig <: UsualEqualityTypeOrig := BoolUsualEq <+ UsualIsEqOrig. +Module BoolUsualEqualityTypeBoth <: UsualEqualityTypeBoth := BoolUsualEq <+ UsualIsEq <+ UsualIsEqOrig. Module BoolUsualDecidableType <: UsualDecidableType := BoolUsualEq <+ UsualIsEq <+ BoolUsualHasEqDec. diff --git a/src/Util/Structures/Equalities/Empty.v b/src/Util/Structures/Equalities/Empty.v index 58fba719d8..f088c59c8a 100644 --- a/src/Util/Structures/Equalities/Empty.v +++ b/src/Util/Structures/Equalities/Empty.v @@ -81,6 +81,8 @@ Module EmptyBooleanDecidableType' := EmptyBooleanDecidableType <+ EqNotation <+ Module EmptyDecidableTypeFull' := EmptyDecidableTypeFull <+ EqNotation. Module EmptyUsualEqualityType <: UsualEqualityType := EmptyUsualEq <+ UsualIsEq. +Module EmptyUsualEqualityTypeOrig <: UsualEqualityTypeOrig := EmptyUsualEq <+ UsualIsEqOrig. +Module EmptyUsualEqualityTypeBoth <: UsualEqualityTypeBoth := EmptyUsualEq <+ UsualIsEq <+ UsualIsEqOrig. Module EmptyUsualDecidableType <: UsualDecidableType := EmptyUsualEq <+ UsualIsEq <+ EmptyUsualHasEqDec. diff --git a/src/Util/Structures/Equalities/List.v b/src/Util/Structures/Equalities/List.v index 24adb4bc14..f847cae428 100644 --- a/src/Util/Structures/Equalities/List.v +++ b/src/Util/Structures/Equalities/List.v @@ -67,9 +67,9 @@ End ListEqbSpec. Module ListHasEqBool (E : Eq) (Es : HasEqBool E) := ListHasEqb E Es <+ ListEqbSpec E E Es Es. -Module ListUsualHasEqDec (E : UsualDecidableType). +Module ListUsualHasEqDec (E : UsualEq) (EDec : HasEqDec E). Definition eq_dec (x y : list E.t) : {eq x y} + {~eq x y} - := List.list_eq_dec E.eq_dec x y. + := List.list_eq_dec EDec.eq_dec x y. End ListUsualHasEqDec. Module ListUsualEqbSpec (E : UsualBoolEq). @@ -108,7 +108,7 @@ Module ListMiniDecidableType (E : MiniDecidableType) <: MiniDecidableType. Module Import _ListMiniDecidableType. Module E' := Make_UDT E. End _ListMiniDecidableType. - Include ListUsualHasEqDec E'. + Include ListUsualHasEqDec E' E'. End ListMiniDecidableType. Module ListUsualHasEqBool (E : UsualBoolEq) := ListHasEqb E E <+ ListUsualEqbSpec E. @@ -136,17 +136,19 @@ Module ListBooleanDecidableType' (E : BooleanDecidableType) := ListBooleanDecida Module ListDecidableTypeFull' (E : DecidableTypeFull) := ListDecidableTypeFull E <+ EqNotation. Module ListUsualEqualityType (E : UsualEqualityType) <: UsualEqualityType := ListUsualEq E <+ UsualIsEq. +Module ListUsualEqualityTypeOrig (E : UsualEqualityTypeOrig) <: UsualEqualityTypeOrig := ListUsualEq E <+ UsualIsEqOrig. +Module ListUsualEqualityTypeBoth (E : UsualEqualityTypeBoth) <: UsualEqualityTypeBoth := ListUsualEq E <+ UsualIsEq <+ UsualIsEqOrig. Module ListUsualDecidableType (E : UsualDecidableType) <: UsualDecidableType -:= ListUsualEq E <+ UsualIsEq <+ ListUsualHasEqDec E. +:= ListUsualEq E <+ UsualIsEq <+ ListUsualHasEqDec E E. Module ListUsualDecidableTypeOrig (E : UsualDecidableType) <: UsualDecidableTypeOrig -:= ListUsualEq E <+ UsualIsEqOrig <+ ListUsualHasEqDec E. +:= ListUsualEq E <+ UsualIsEqOrig <+ ListUsualHasEqDec E E. Module ListUsualDecidableTypeBoth (E : UsualDecidableType) <: UsualDecidableTypeBoth := ListUsualDecidableType E <+ UsualIsEqOrig. Module ListUsualBoolEq (E : UsualBoolEq) <: UsualBoolEq := ListUsualEq E <+ ListUsualHasEqBool E. Module ListUsualDecidableTypeFull (E : UsualDecidableTypeFull) <: UsualDecidableTypeFull - := ListUsualEq E <+ UsualIsEq <+ UsualIsEqOrig <+ ListUsualHasEqDec E <+ ListUsualHasEqBool E. + := ListUsualEq E <+ UsualIsEq <+ UsualIsEqOrig <+ ListUsualHasEqDec E E <+ ListUsualHasEqBool E. Local Coercion is_true : bool >-> Sortclass. Module ListIsEqb (E : EqbType). diff --git a/src/Util/Structures/Equalities/Option.v b/src/Util/Structures/Equalities/Option.v index 0279c22486..308def66ff 100644 --- a/src/Util/Structures/Equalities/Option.v +++ b/src/Util/Structures/Equalities/Option.v @@ -66,11 +66,11 @@ End OptionEqbSpec. Module OptionHasEqBool (E : Eq) (Es : HasEqBool E) := OptionHasEqb E Es <+ OptionEqbSpec E E Es Es. -Module OptionUsualHasEqDec (E : UsualDecidableType). +Module OptionUsualHasEqDec (E : UsualEq) (EDec : HasEqDec E). Definition eq_dec (x y : option E.t) : {eq x y} + {~eq x y}. Proof. destruct x as [x|], y as [y|]; - [ destruct (E.eq_dec x y); [ left | right ] + [ destruct (EDec.eq_dec x y); [ left | right ] | right | right | left ]; @@ -120,7 +120,7 @@ Module OptionMiniDecidableType (E : MiniDecidableType) <: MiniDecidableType. Module Import _OptionMiniDecidableType. Module E' := Make_UDT E. End _OptionMiniDecidableType. - Include OptionUsualHasEqDec E'. + Include OptionUsualHasEqDec E' E'. End OptionMiniDecidableType. Local Coercion is_true : bool >-> Sortclass. @@ -157,16 +157,18 @@ Module OptionBooleanDecidableType' (E : BooleanDecidableType) := OptionBooleanDe Module OptionDecidableTypeFull' (E : DecidableTypeFull) := OptionDecidableTypeFull E <+ EqNotation. Module OptionUsualEqualityType (E : UsualEqualityType) <: UsualEqualityType := OptionUsualEq E <+ UsualIsEq. +Module OptionUsualEqualityTypeOrig (E : UsualEqualityTypeOrig) <: UsualEqualityTypeOrig := OptionUsualEq E <+ UsualIsEqOrig. +Module OptionUsualEqualityTypeBoth (E : UsualEqualityTypeBoth) <: UsualEqualityTypeBoth := OptionUsualEq E <+ UsualIsEq <+ UsualIsEqOrig. Module OptionUsualDecidableType (E : UsualDecidableType) <: UsualDecidableType -:= OptionUsualEq E <+ UsualIsEq <+ OptionUsualHasEqDec E. -Module OptionUsualDecidableTypeOrig (E : UsualDecidableType) <: UsualDecidableTypeOrig -:= OptionUsualEq E <+ UsualIsEqOrig <+ OptionUsualHasEqDec E. -Module OptionUsualDecidableTypeBoth (E : UsualDecidableType) <: UsualDecidableTypeBoth +:= OptionUsualEq E <+ UsualIsEq <+ OptionUsualHasEqDec E E. +Module OptionUsualDecidableTypeOrig (E : UsualDecidableTypeOrig) <: UsualDecidableTypeOrig +:= OptionUsualEq E <+ UsualIsEqOrig <+ OptionUsualHasEqDec E E. +Module OptionUsualDecidableTypeBoth (E : UsualDecidableTypeBoth) <: UsualDecidableTypeBoth := OptionUsualDecidableType E <+ UsualIsEqOrig. Module OptionUsualBoolEq (E : UsualBoolEq) <: UsualBoolEq := OptionUsualEq E <+ OptionUsualHasEqBool E. Module OptionUsualDecidableTypeFull (E : UsualDecidableTypeFull) <: UsualDecidableTypeFull - := OptionUsualEq E <+ UsualIsEq <+ UsualIsEqOrig <+ OptionUsualHasEqDec E <+ OptionUsualHasEqBool E. + := OptionUsualEq E <+ UsualIsEq <+ UsualIsEqOrig <+ OptionUsualHasEqDec E E <+ OptionUsualHasEqBool E. Module OptionEqbType (E : EqbType) <: EqbType := OptionTyp E <+ OptionHasEqb E E <+ OptionIsEqb E. diff --git a/src/Util/Structures/Equalities/Prod.v b/src/Util/Structures/Equalities/Prod.v index 03c0c5870f..4b5bde615f 100644 --- a/src/Util/Structures/Equalities/Prod.v +++ b/src/Util/Structures/Equalities/Prod.v @@ -67,10 +67,10 @@ End ProdEqbSpec. Module ProdHasEqBool (E1 : Eq) (E2 : Eq) (E1s : HasEqBool E1) (E2s : HasEqBool E2) := ProdHasEqb E1 E2 E1s E2s <+ ProdEqbSpec E1 E2 E1 E2 E1s E2s E1s E2s. -Module ProdUsualHasEqDec (E1 : UsualDecidableType) (E2 : UsualDecidableType). +Module ProdUsualHasEqDec (E1 : UsualEq) (E2 : UsualEq) (E1Dec : HasEqDec E1) (E2Dec : HasEqDec E2). Definition eq_dec (x y : E1.t * E2.t) : {eq x y} + {~eq x y}. Proof. - destruct (E1.eq_dec (fst x) (fst y)); [ destruct (E2.eq_dec (snd x) (snd y)); [ left; destruct x, y | right; intro; subst y; destruct x ] | right; intro; subst y; destruct x ]; cbn in *; subst; try reflexivity; eauto using eq_refl with nocore. + destruct (E1Dec.eq_dec (fst x) (fst y)); [ destruct (E2Dec.eq_dec (snd x) (snd y)); [ left; destruct x, y | right; intro; subst y; destruct x ] | right; intro; subst y; destruct x ]; cbn in *; subst; try reflexivity; eauto using eq_refl with nocore. Defined. End ProdUsualHasEqDec. @@ -112,7 +112,7 @@ Module ProdMiniDecidableType (E1 : MiniDecidableType) (E2 : MiniDecidableType) < Module E1' := Make_UDT E1. Module E2' := Make_UDT E2. End _ProdMiniDecidableType. - Include ProdUsualHasEqDec E1' E2'. + Include ProdUsualHasEqDec E1' E2' E1' E2'. End ProdMiniDecidableType. Local Coercion is_true : bool >-> Sortclass. @@ -151,17 +151,19 @@ Module ProdBooleanEqualityType' (E1 : BooleanEqualityType) (E2 : BooleanEquality Module ProdBooleanDecidableType' (E1 : BooleanDecidableType) (E2 : BooleanDecidableType) := ProdBooleanDecidableType E1 E2 <+ EqNotation <+ EqbNotation. Module ProdDecidableTypeFull' (E1 : DecidableTypeFull) (E2 : DecidableTypeFull) := ProdDecidableTypeFull E1 E2 <+ EqNotation. -Module ProdUsualEqualityType (E1 : UsualEqualityType) (E2 : UsualEqualityType) <: UsualEqualityType := ProdUsualEq E1 E2 <+ UsualIsEq. +Module ProdUsualEqualityType (E1 : UsualEq) (E2 : UsualEq) <: UsualEqualityType := ProdUsualEq E1 E2 <+ UsualIsEq. +Module ProdUsualEqualityTypeOrig (E1 : UsualEq) (E2 : UsualEq) <: UsualEqualityTypeOrig := ProdUsualEq E1 E2 <+ UsualIsEqOrig. +Module ProdUsualEqualityTypeBoth (E1 : UsualEq) (E2 : UsualEq) <: UsualEqualityTypeBoth := ProdUsualEq E1 E2 <+ UsualIsEq <+ UsualIsEqOrig. Module ProdUsualDecidableType (E1 : UsualDecidableType) (E2 : UsualDecidableType) <: UsualDecidableType -:= ProdUsualEq E1 E2 <+ UsualIsEq <+ ProdUsualHasEqDec E1 E2. -Module ProdUsualDecidableTypeOrig (E1 : UsualDecidableType) (E2 : UsualDecidableType) <: UsualDecidableTypeOrig -:= ProdUsualEq E1 E2 <+ UsualIsEqOrig <+ ProdUsualHasEqDec E1 E2. -Module ProdUsualDecidableTypeBoth (E1 : UsualDecidableType) (E2 : UsualDecidableType) <: UsualDecidableTypeBoth +:= ProdUsualEq E1 E2 <+ UsualIsEq <+ ProdUsualHasEqDec E1 E2 E1 E2. +Module ProdUsualDecidableTypeOrig (E1 : UsualDecidableTypeOrig) (E2 : UsualDecidableTypeOrig) <: UsualDecidableTypeOrig +:= ProdUsualEq E1 E2 <+ UsualIsEqOrig <+ ProdUsualHasEqDec E1 E2 E1 E2. +Module ProdUsualDecidableTypeBoth (E1 : UsualDecidableTypeBoth) (E2 : UsualDecidableTypeBoth) <: UsualDecidableTypeBoth := ProdUsualDecidableType E1 E2 <+ UsualIsEqOrig. Module ProdUsualBoolEq (E1 : UsualBoolEq) (E2 : UsualBoolEq) <: UsualBoolEq := ProdUsualEq E1 E2 <+ ProdUsualHasEqBool E1 E2. Module ProdUsualDecidableTypeFull (E1 : UsualDecidableTypeFull) (E2 : UsualDecidableTypeFull) <: UsualDecidableTypeFull - := ProdUsualEq E1 E2 <+ UsualIsEq <+ UsualIsEqOrig <+ ProdUsualHasEqDec E1 E2 <+ ProdUsualHasEqBool E1 E2. + := ProdUsualEq E1 E2 <+ UsualIsEq <+ UsualIsEqOrig <+ ProdUsualHasEqDec E1 E2 E1 E2 <+ ProdUsualHasEqBool E1 E2. Module ProdEqbType (E1 : EqbType) (E2 : EqbType) <: EqbType := ProdTyp E1 E2 <+ ProdHasEqb E1 E2 E1 E2 <+ ProdIsEqb E1 E2. diff --git a/src/Util/Structures/Equalities/Sum.v b/src/Util/Structures/Equalities/Sum.v index fcd708480e..3aeac3e4c5 100644 --- a/src/Util/Structures/Equalities/Sum.v +++ b/src/Util/Structures/Equalities/Sum.v @@ -67,14 +67,14 @@ End SumEqbSpec. Module SumHasEqBool (E1 : Eq) (E2 : Eq) (E1s : HasEqBool E1) (E2s : HasEqBool E2) := SumHasEqb E1 E2 E1s E2s <+ SumEqbSpec E1 E2 E1 E2 E1s E2s E1s E2s. -Module SumUsualHasEqDec (E1 : UsualDecidableType) (E2 : UsualDecidableType). +Module SumUsualHasEqDec (E1 : UsualEq) (E2 : UsualEq) (E1Dec : HasEqDec E1) (E2Dec : HasEqDec E2). Definition eq_dec (x y : E1.t + E2.t) : {eq x y} + {~eq x y}. Proof. destruct x as [x|x], y as [y|y]; - [ destruct (E1.eq_dec x y); [ left | right ] + [ destruct (E1Dec.eq_dec x y); [ left | right ] | right | right - | destruct (E2.eq_dec x y); [ left | right ] ]; + | destruct (E2Dec.eq_dec x y); [ left | right ] ]; repeat first [ apply f_equal | assumption | intro @@ -121,7 +121,7 @@ Module SumMiniDecidableType (E1 : MiniDecidableType) (E2 : MiniDecidableType) <: Module E1' := Make_UDT E1. Module E2' := Make_UDT E2. End _SumMiniDecidableType. - Include SumUsualHasEqDec E1' E2'. + Include SumUsualHasEqDec E1' E2' E1' E2'. End SumMiniDecidableType. Local Coercion is_true : bool >-> Sortclass. @@ -157,17 +157,19 @@ Module SumBooleanEqualityType' (E1 : BooleanEqualityType) (E2 : BooleanEqualityT Module SumBooleanDecidableType' (E1 : BooleanDecidableType) (E2 : BooleanDecidableType) := SumBooleanDecidableType E1 E2 <+ EqNotation <+ EqbNotation. Module SumDecidableTypeFull' (E1 : DecidableTypeFull) (E2 : DecidableTypeFull) := SumDecidableTypeFull E1 E2 <+ EqNotation. -Module SumUsualEqualityType (E1 : UsualEqualityType) (E2 : UsualEqualityType) <: UsualEqualityType := SumUsualEq E1 E2 <+ UsualIsEq. +Module SumUsualEqualityType (E1 : UsualEq) (E2 : UsualEq) <: UsualEqualityType := SumUsualEq E1 E2 <+ UsualIsEq. +Module SumUsualEqualityTypeOrig (E1 : UsualEq) (E2 : UsualEq) <: UsualEqualityTypeOrig := SumUsualEq E1 E2 <+ UsualIsEqOrig. +Module SumUsualEqualityTypeBoth (E1 : UsualEq) (E2 : UsualEq) <: UsualEqualityTypeBoth := SumUsualEq E1 E2 <+ UsualIsEq <+ UsualIsEqOrig. Module SumUsualDecidableType (E1 : UsualDecidableType) (E2 : UsualDecidableType) <: UsualDecidableType -:= SumUsualEq E1 E2 <+ UsualIsEq <+ SumUsualHasEqDec E1 E2. -Module SumUsualDecidableTypeOrig (E1 : UsualDecidableType) (E2 : UsualDecidableType) <: UsualDecidableTypeOrig -:= SumUsualEq E1 E2 <+ UsualIsEqOrig <+ SumUsualHasEqDec E1 E2. -Module SumUsualDecidableTypeBoth (E1 : UsualDecidableType) (E2 : UsualDecidableType) <: UsualDecidableTypeBoth +:= SumUsualEq E1 E2 <+ UsualIsEq <+ SumUsualHasEqDec E1 E2 E1 E2. +Module SumUsualDecidableTypeOrig (E1 : UsualDecidableTypeOrig) (E2 : UsualDecidableTypeOrig) <: UsualDecidableTypeOrig +:= SumUsualEq E1 E2 <+ UsualIsEqOrig <+ SumUsualHasEqDec E1 E2 E1 E2. +Module SumUsualDecidableTypeBoth (E1 : UsualDecidableTypeBoth) (E2 : UsualDecidableTypeBoth) <: UsualDecidableTypeBoth := SumUsualDecidableType E1 E2 <+ UsualIsEqOrig. Module SumUsualBoolEq (E1 : UsualBoolEq) (E2 : UsualBoolEq) <: UsualBoolEq := SumUsualEq E1 E2 <+ SumUsualHasEqBool E1 E2. Module SumUsualDecidableTypeFull (E1 : UsualDecidableTypeFull) (E2 : UsualDecidableTypeFull) <: UsualDecidableTypeFull - := SumUsualEq E1 E2 <+ UsualIsEq <+ UsualIsEqOrig <+ SumUsualHasEqDec E1 E2 <+ SumUsualHasEqBool E1 E2. + := SumUsualEq E1 E2 <+ UsualIsEq <+ UsualIsEqOrig <+ SumUsualHasEqDec E1 E2 E1 E2 <+ SumUsualHasEqBool E1 E2. Module SumEqbType (E1 : EqbType) (E2 : EqbType) <: EqbType := SumTyp E1 E2 <+ SumHasEqb E1 E2 E1 E2 <+ SumIsEqb E1 E2. diff --git a/src/Util/Structures/Equalities/Unit.v b/src/Util/Structures/Equalities/Unit.v index d4c3259118..5ac406644a 100644 --- a/src/Util/Structures/Equalities/Unit.v +++ b/src/Util/Structures/Equalities/Unit.v @@ -82,6 +82,8 @@ Module UnitBooleanDecidableType' := UnitBooleanDecidableType <+ EqNotation <+ Eq Module UnitDecidableTypeFull' := UnitDecidableTypeFull <+ EqNotation. Module UnitUsualEqualityType <: UsualEqualityType := UnitUsualEq <+ UsualIsEq. +Module UnitUsualEqualityTypeOrig <: UsualEqualityTypeOrig := UnitUsualEq <+ UsualIsEqOrig. +Module UnitUsualEqualityTypeBoth <: UsualEqualityTypeBoth := UnitUsualEq <+ UsualIsEq <+ UsualIsEqOrig. Module UnitUsualDecidableType <: UsualDecidableType := UnitUsualEq <+ UsualIsEq <+ UnitUsualHasEqDec. diff --git a/src/Util/Structures/Orders/List.v b/src/Util/Structures/Orders/List.v index c967c5e8bf..220babf0ed 100644 --- a/src/Util/Structures/Orders/List.v +++ b/src/Util/Structures/Orders/List.v @@ -428,7 +428,7 @@ Module ListUsualStrOrder (E : UsualStrOrder) <: UsualStrOrder := ListUsualEquali Module ListUsualHasCompare (E : UsualEqLt) (Ec : HasCompare E) := ListHasCmp E Ec <+ ListUsualCmpSpec E Ec. Module ListUsualDecStrOrder (E : UsualDecStrOrder) <: UsualDecStrOrder := ListUsualStrOrder E <+ ListUsualHasCompare E E. -Module ListUsualOrderedType (E : UsualOrderedType) <: UsualOrderedType := ListUsualDecStrOrder E <+ ListUsualHasEqDec E. +Module ListUsualOrderedType (E : UsualOrderedType) <: UsualOrderedType := ListUsualDecStrOrder E <+ ListUsualHasEqDec E E. Module ListUsualOrderedTypeFull (E : UsualOrderedTypeFull) <: UsualOrderedTypeFull := ListUsualOrderedType E <+ ListHasLe E <+ ListUsualLeIsLtEq E E E. Module ListUsualStrOrder' (E : UsualStrOrder) <: UsualStrOrder' := ListUsualStrOrder E <+ LtNotation. diff --git a/src/Util/Structures/Orders/Option.v b/src/Util/Structures/Orders/Option.v index 67bad45499..e43b13b7fd 100644 --- a/src/Util/Structures/Orders/Option.v +++ b/src/Util/Structures/Orders/Option.v @@ -323,7 +323,7 @@ Module OptionUsualStrOrder (E : UsualStrOrder) <: UsualStrOrder := OptionUsualEq Module OptionUsualHasCompare (E : UsualEqLt) (Ec : HasCompare E) := OptionHasCmp E Ec <+ OptionUsualCmpSpec E Ec. Module OptionUsualDecStrOrder (E : UsualDecStrOrder) <: UsualDecStrOrder := OptionUsualStrOrder E <+ OptionUsualHasCompare E E. -Module OptionUsualOrderedType (E : UsualOrderedType) <: UsualOrderedType := OptionUsualDecStrOrder E <+ OptionUsualHasEqDec E. +Module OptionUsualOrderedType (E : UsualOrderedType) <: UsualOrderedType := OptionUsualDecStrOrder E <+ OptionUsualHasEqDec E E. Module OptionUsualOrderedTypeFull (E : UsualOrderedTypeFull) <: UsualOrderedTypeFull := OptionUsualOrderedType E <+ OptionHasLe E <+ OptionUsualLeIsLtEq E E E. Module OptionUsualStrOrder' (E : UsualStrOrder) <: UsualStrOrder' := OptionUsualStrOrder E <+ LtNotation. diff --git a/src/Util/Structures/Orders/Prod.v b/src/Util/Structures/Orders/Prod.v index 8bb662933a..b8c232ba42 100644 --- a/src/Util/Structures/Orders/Prod.v +++ b/src/Util/Structures/Orders/Prod.v @@ -418,7 +418,7 @@ Module ProdUsualStrOrder (E1 : UsualStrOrder) (E2 : UsualStrOrder) <: UsualStrOr Module ProdUsualHasCompare (E1 : UsualEqLt) (E2 : UsualEqLt) (E1c : HasCompare E1) (E2c : HasCompare E2) := ProdHasCmp E1 E2 E1c E2c <+ ProdUsualCmpSpec E1 E2 E1c E2c. Module ProdUsualDecStrOrder (E1 : UsualDecStrOrder) (E2 : UsualDecStrOrder) <: UsualDecStrOrder := ProdUsualStrOrder E1 E2 <+ ProdUsualHasCompare E1 E2 E1 E2. -Module ProdUsualOrderedType (E1 : UsualOrderedType) (E2 : UsualOrderedType) <: UsualOrderedType := ProdUsualDecStrOrder E1 E2 <+ ProdUsualHasEqDec E1 E2. +Module ProdUsualOrderedType (E1 : UsualOrderedType) (E2 : UsualOrderedType) <: UsualOrderedType := ProdUsualDecStrOrder E1 E2 <+ ProdUsualHasEqDec E1 E2 E1 E2. Module ProdUsualOrderedTypeFull (E1 : UsualOrderedTypeFull) (E2 : UsualOrderedTypeFull) <: UsualOrderedTypeFull := ProdUsualOrderedType E1 E2 <+ ProdHasLe E1 E2 <+ ProdUsualLeIsLtEq E1 E2 E1 E2 E1. Module ProdUsualStrOrder' (E1 : UsualStrOrder) (E2 : UsualStrOrder) <: UsualStrOrder' := ProdUsualStrOrder E1 E2 <+ LtNotation. @@ -523,36 +523,3 @@ Module ProdBoolOrdSpecs (O1 : EqLtLe) (O2 : EqLtLe) (F1 : HasBoolOrdFuns O1) (F2 Module ProdOrderFunctions (O1 : EqLtLe) (O2 : EqLtLe) (F1 : OrderFunctions O1) (F2 : OrderFunctions O2) (O1e : IsEq O1) := ProdHasCompare O1 O2 F1 F2 O1e <+ ProdHasBoolOrdFuns O1 O2 F1 F2 <+ ProdBoolOrdSpecs O1 O2 F1 F2 F1 F2. Module ProdOrderFunctions' (O1 : EqLtLe) (O2 : EqLtLe) (F1 : OrderFunctions O1) (F2 : OrderFunctions O2) (O1e : IsEq O1) := ProdHasCompare O1 O2 F1 F2 O1e <+ ProdCmpNotation O1 O2 F1 F2 <+ ProdHasBoolOrdFuns' O1 O2 F1 F2 <+ ProdBoolOrdSpecs O1 O2 F1 F2 F1 F2. - - - - - - - - - - - - -(* -Module ProdTotalLeBool (E1 : CompatibleTotalEqLtLeBool) (E2 : TotalLeBool) <: TotalLeBool := ProdLeBool E1 E2 <+ ProdLebIsTotal E1 E2 E1 E2 E1 E1. -Module ProdTotalLeBool' (E1 : TotalLeBool) (E2 : TotalLeBool) <: TotalLeBool' := ProdLeBool' E1 E2 <+ ProdLebIsTotal E1 E2. -Module ProdTotalEqLtLeBool (E1 : TotalEqLtLeBool) (E2 : TotalEqLtLeBool) <: TotalEqLtLeBool := ProdEqLtLeBool E1 E2 <+ ProdEqLtLebIsTotal E1 E2. -Module ProdTotalEqLtLeBool' (E1 : TotalEqLtLeBool) (E2 : TotalEqLtLeBool) <: TotalEqLtLeBool' := ProdEqLtLeBool' E1 E2 <+ ProdEqLtLebIsTotal E1 E2. - -Module ProdTotalTransitiveLeBool (E1 : TotalTransitiveLeBool) (E2 : TotalTransitiveLeBool) <: TotalTransitiveLeBool := ProdTotalLeBool E1 E2 <+ ProdLebIsTransitive E1 E2 E1 E2. -Module ProdTotalTransitiveLeBool' (E1 : TotalTransitiveLeBool) (E2 : TotalTransitiveLeBool) <: TotalTransitiveLeBool' := ProdTotalLeBool' E1 E2 <+ ProdLebIsTransitive E1 E2 E1 E2. - -Module ProdHasBoolOrdFuns (E1 : Typ) (E2 : Typ) (E1s : HasBoolOrdFuns E1) (E2s : HasBoolOrdFuns E2) := ProdTyp E1 E2 <+ ProdHasEqb E1 E2 E1s E2s <+ ProdHasLtb E1 E2 E1s E2s <+ ProdHasLeb E1 E2 E1s E2s. - -Module ProdHasBoolOrdFuns' (E1 : Typ) (E2 : Typ) (E1s : HasBoolOrdFuns E1) (E2s : HasBoolOrdFuns E2) := ProdHasBoolOrdFuns E1 E2 E1s E2s <+ ProdEqbNotation E1 E2 E1s E2s <+ ProdLtbNotation E1 E2 E1s E2s <+ ProdLebNotation E1 E2 E1s E2s. - -Module ProdBoolOrdSpecs (E1 : EqLtLe) (E2 : EqLtLe) (F1 : HasBoolOrdFuns E1) (F2 : HasBoolOrdFuns E2) (E1s : BoolOrdSpecs E1 F1) (E2s : BoolOrdSpecs E2 F2) -:= ProdEqbSpec E1 E2 E1 E2 F1 F2 E1s E2s <+ ProdLtbSpec E1 E2 E1 E2 F1 F2 E1s E2s <+ ProdLebSpec E1 E2 E1 E2 F1 F2 E1s E2s. - -Module ProdOrderFunctions (E1 : EqLtLe) (E2 : EqLtLe) (E1f : OrderFunctions E1) (E2f : OrderFunctions E2) -:= ProdHasCompare E1 E2 E1f E2f <+ ProdHasBoolOrdFuns E1 E2 E1f E2f <+ ProdBoolOrdSpecs E1 E2 E1f E2f E1f E2f. -Module ProdOrderFunctions' (E1 : EqLtLe) (E2 : EqLtLe) (E1f : OrderFunctions E1) (E2f : OrderFunctions E2) -:= ProdHasCompare E1 E2 E1f E2f <+ ProdCmpNotation E1 E2 E1f E2f <+ ProdHasBoolOrdFuns' E1 E2 E1f E2f <+ ProdBoolOrdSpecs E1 E2 E1f E2f E1f E2f. -*) diff --git a/src/Util/Structures/Orders/Sum.v b/src/Util/Structures/Orders/Sum.v index 478e3fe290..980cba508c 100644 --- a/src/Util/Structures/Orders/Sum.v +++ b/src/Util/Structures/Orders/Sum.v @@ -238,7 +238,7 @@ Module SumUsualStrOrder (E1 : UsualStrOrder) (E2 : UsualStrOrder) <: UsualStrOrd Module SumUsualHasCompare (E1 : UsualEqLt) (E2 : UsualEqLt) (E1c : HasCompare E1) (E2c : HasCompare E2) := SumHasCmp E1 E2 E1c E2c <+ SumUsualCmpSpec E1 E2 E1c E2c. Module SumUsualDecStrOrder (E1 : UsualDecStrOrder) (E2 : UsualDecStrOrder) <: UsualDecStrOrder := SumUsualStrOrder E1 E2 <+ SumUsualHasCompare E1 E2 E1 E2. -Module SumUsualOrderedType (E1 : UsualOrderedType) (E2 : UsualOrderedType) <: UsualOrderedType := SumUsualDecStrOrder E1 E2 <+ SumUsualHasEqDec E1 E2. +Module SumUsualOrderedType (E1 : UsualOrderedType) (E2 : UsualOrderedType) <: UsualOrderedType := SumUsualDecStrOrder E1 E2 <+ SumUsualHasEqDec E1 E2 E1 E2. Module SumUsualOrderedTypeFull (E1 : UsualOrderedTypeFull) (E2 : UsualOrderedTypeFull) <: UsualOrderedTypeFull := SumUsualOrderedType E1 E2 <+ SumHasLe E1 E2 <+ SumUsualLeIsLtEq E1 E2 E1 E2. Module SumUsualStrOrder' (E1 : UsualStrOrder) (E2 : UsualStrOrder) <: UsualStrOrder' := SumUsualStrOrder E1 E2 <+ LtNotation.