Library OrderCoproduct

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

Set Implicit Arguments.

Generalizable All Variables.

Order Coproducts

We define R + R' (a, a') (b, b') to be R a b R' a' b'.
Definition relation_sum {A A'}
           (R : Relation_Definitions.relation A)
           (R' : Relation_Definitions.relation A')
: Relation_Definitions.relation (A + A')
  := fun aa' bb'match aa', bb' with
                      | inl a, inl bR a b
                      | inr a', inr b'R' a' b'
                      | _, _False

Infix "+" := relation_sum : relation_scope.

Section relation_coproduct.
  Local Open Scope relation_scope.

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

  Local Obligation Tactic := abstract t.

  Global Program Instance sum_refl `(RelationClasses.Reflexive A R) `(RelationClasses.Reflexive A' R') : RelationClasses.Reflexive (R + R').
  Global Program Instance sum_irefl `(RelationClasses.Irreflexive A R) `(RelationClasses.Irreflexive A' R') : RelationClasses.Irreflexive (R + R').
  Global Program Instance sum_sym `(RelationClasses.Symmetric A R) `(RelationClasses.Symmetric A' R') : RelationClasses.Symmetric (R + R').
  Global Program Instance sum_asym `(RelationClasses.Asymmetric A R) `(RelationClasses.Asymmetric A' R') : RelationClasses.Asymmetric (R + R').
  Global Program Instance sum_trans `(RelationClasses.Transitive A R) `(RelationClasses.Transitive A' R') : RelationClasses.Transitive (R + R').
  Global Program Instance sum_pre_order `(RelationClasses.PreOrder A R) `(RelationClasses.PreOrder A' R') : RelationClasses.PreOrder (R + R').
  Global Program Instance sum_PER `(RelationClasses.PER A R) `(RelationClasses.PER A' R') : RelationClasses.PER (R + R').
  Global Program Instance sum_equiv `(RelationClasses.Equivalence A R) `(RelationClasses.Equivalence A' R') : RelationClasses.Equivalence (R + R').
  Global Program Instance sum_antisym `(@RelationClasses.Antisymmetric A eqA equA R) `(@RelationClasses.Antisymmetric A' eqA' equA' R') : @RelationClasses.Antisymmetric (A + A') (eqA + eqA') _ (R + R').
  Global Program Instance sum_partial_order `(@RelationClasses.PartialOrder A eqA equA R preoA) `(@RelationClasses.PartialOrder A' eqA' equA' R' preoA')
  : @RelationClasses.PartialOrder (A + A') (eqA + eqA') _ (R + R') _.
  Global Program Instance sum_strict_order `(RelationClasses.StrictOrder A R) `(RelationClasses.StrictOrder A' R') : RelationClasses.StrictOrder (R + R').
  Global Instance coproduct_decidable `(H : RelationDecidable A R) `(H' : RelationDecidable A' R') : RelationDecidable (R + R')
    := fun xx yy
         match (xx, yy) as p return {(R + R')%relation (fst p) (snd p)} + {¬(R + R')%relation (fst p) (snd p)} with
           | (inl _, inl _)H _ _
           | (inr _, inr _)H' _ _
           | (_, _)right (fun x : Falsex)
End relation_coproduct.