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 destruct_head_hnf @prod)
              || (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 order_product.