# 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
end.

Infix "+" := relation_sum : relation_scope.

Section relation_coproduct.
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 ])
|| 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.
End relation_coproduct.