Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix some structures arguments #1243

Merged
merged 1 commit into from
May 19, 2022
Merged

Fix some structures arguments #1243

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions src/Util/Structures/Equalities.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
2 changes: 2 additions & 0 deletions src/Util/Structures/Equalities/Bool.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
2 changes: 2 additions & 0 deletions src/Util/Structures/Equalities/Empty.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
14 changes: 8 additions & 6 deletions src/Util/Structures/Equalities/List.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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).
Expand Down
18 changes: 10 additions & 8 deletions src/Util/Structures/Equalities/Option.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ];
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
20 changes: 11 additions & 9 deletions src/Util/Structures/Equalities/Prod.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
22 changes: 12 additions & 10 deletions src/Util/Structures/Equalities/Sum.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
2 changes: 2 additions & 0 deletions src/Util/Structures/Equalities/Unit.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion src/Util/Structures/Orders/List.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion src/Util/Structures/Orders/Option.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
35 changes: 1 addition & 34 deletions src/Util/Structures/Orders/Prod.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.
*)
Loading