# Library OrderProduct

Require Import Utf8.
Require Export Orders.
Require Import Common Notations.

Set Implicit Arguments.

Generalizable All Variables.

# Order Products

We define R × R' (a, a') (b, b') to be R a b R' a' b'.
Definition relation_product {A A'}
(R : Relation_Definitions.relation A)
(R' : Relation_Definitions.relation A')
: Relation_Definitions.relation (A × A')
:= fun aa' bb'R (fst aa') (fst bb')
R' (snd aa') (snd bb').

Infix "×" := relation_product : relation_scope.

Section order_product.
Local Open Scope relation_scope.

Local Ltac t :=
repeat (esplit
|| (progress compute in *; split_and)
|| (progress (hnf in *; simpl in *; compute in *; intuition eauto))
|| (etransitivity; solve [ eauto ])
|| (progress firstorder)).

Local Obligation Tactic := abstract t.

Global Program Instance product_refl `(RelationClasses.Reflexive A R) `(RelationClasses.Reflexive A' R') : RelationClasses.Reflexive (R × R').
Global Program Instance product_irefl `(RelationClasses.Irreflexive A R) `(RelationClasses.Irreflexive A' R') : RelationClasses.Irreflexive (R × R').
Global Program Instance product_sym `(RelationClasses.Symmetric A R) `(RelationClasses.Symmetric A' R') : RelationClasses.Symmetric (R × R').
Global Program Instance product_asym `(RelationClasses.Asymmetric A R) `(RelationClasses.Asymmetric A' R') : RelationClasses.Asymmetric (R × R').
Global Program Instance product_trans `(RelationClasses.Transitive A R) `(RelationClasses.Transitive A' R') : RelationClasses.Transitive (R × R').
Global Program Instance product_pre_order `(RelationClasses.PreOrder A R) `(RelationClasses.PreOrder A' R') : RelationClasses.PreOrder (R × R').
Global Program Instance product_PER `(RelationClasses.PER A R) `(RelationClasses.PER A' R') : RelationClasses.PER (R × R').
Global Program Instance product_equiv `(RelationClasses.Equivalence A R) `(RelationClasses.Equivalence A' R') : RelationClasses.Equivalence (R × R').
Global Program Instance product_antisym `(@RelationClasses.Antisymmetric A eqA equA R) `(@RelationClasses.Antisymmetric A' eqA' equA' R') : @RelationClasses.Antisymmetric (A × A') (eqA × eqA') _ (R × R').
Global Program Instance product_partial_order `(@RelationClasses.PartialOrder A eqA equA R preoA) `(@RelationClasses.PartialOrder A' eqA' equA' R' preoA')
: @PartialOrder (A × A') (eqA × eqA') _ (R × R') _.
Global Program Instance product_strict_order `(RelationClasses.StrictOrder A R) `(RelationClasses.StrictOrder A' R') : RelationClasses.StrictOrder (R × R').
Global Instance product_decidable `(RelationDecidable A R) `(RelationDecidable A' R') : RelationDecidable (R × R')
:= fun xx' yy'
let (x, x') as p
return ({(R × R')%relation p yy'} + {¬(R × R')%relation p yy'}) :=
xx' in
let (y, y') as p
return ({(R × R')%relation (x, x') p} + {¬(R × R')%relation (x, x') p}) :=
yy' in
match Relation_dec x y, Relation_dec x' y' with
| left pf, left pf'left (conj pf pf')
| right pf, _right (fun pfpf'pf (proj1 pfpf'))
| _, right pf'right (fun pfpf'pf' (proj2 pfpf'))
end.
End order_product.