Indexed relations

A few standard constructions to work with indexed relations.

From OGS Require Import Prelude.
From OGS.Utils Require Import Psh.

From Coq.Classes Require Export RelationClasses.
From Coinduction Require Export lattice.

#[export] Existing Instance CompleteLattice_dfun.

#[global] Notation "∀ₕ x , R" := (forall_relation (fun x => R%signature))
   (x binder, at level 60).
Notation relᵢ A B := (forall i, A i -> B i -> Prop).

#[global] Notation Reflexiveᵢ R := (forall i, Reflexive (R i)).
#[global] Notation Symmetricᵢ R := (forall i, Symmetric (R i)).
#[global] Notation Transitiveᵢ R := (forall i, Transitive (R i)).
#[global] Notation Equivalenceᵢ R := (forall i, Equivalence (R i)).
#[global] Notation Subrelationᵢ R S := (forall i, subrelation (R i) (S i)).
#[global] Notation PreOrderᵢ R := (forall i, PreOrder (R i)).

Definition eqᵢ {I} (X : psh I) : relᵢ X X := fun _ x y => x = y.
Arguments eqᵢ _ _ _ /.

#[global] Instance Reflexive_eqᵢ {I} {X : psh I} : Reflexiveᵢ (eqᵢ X).
I: Type
X: psh I
Reflexiveᵢ (eqᵢ X)
Proof.
I: Type
X: psh I
Reflexiveᵢ (eqᵢ X) intros ? ?; reflexivity. Qed.

#[global] Instance Symmetric_eqᵢ {I} {X : psh I} : Symmetricᵢ (eqᵢ X).
I: Type
X: psh I
Symmetricᵢ (eqᵢ X)
Proof.
I: Type
X: psh I
Symmetricᵢ (eqᵢ X) intros ? ? ? ?; now symmetry. Qed.

#[global] Instance Transitive_eqᵢ {I} {X : psh I} : Transitiveᵢ (eqᵢ X).
I: Type
X: psh I
Transitiveᵢ (eqᵢ X)
Proof.
I: Type
X: psh I
Transitiveᵢ (eqᵢ X) intros i x y z a b; now transitivity y. Qed.

Variant sumᵣ {I} {X1 X2 Y1 Y2 : psh I} (R : relᵢ X1 X2) (S : relᵢ Y1 Y2) : relᵢ (X1 +ᵢ Y1) (X2 +ᵢ Y2) :=
  | RLeft {i x1 x2} : R i x1 x2 -> sumᵣ R S i (inl x1) (inl x2)
  | RRight {i y1 y2} : S i y1 y2 -> sumᵣ R S i (inr y1) (inr y2)
.
#[global] Hint Constructors sumᵣ : core.

#[global] Instance sum_equiv {I} {X Y : psh I} {R : relᵢ X X} (_ : Equivalenceᵢ R) {S : relᵢ Y Y} (_ : Equivalenceᵢ S): Equivalenceᵢ (sumᵣ R S).
I: Type
X, Y: psh I
R: relᵢ X X
H: Equivalenceᵢ R
S: relᵢ Y Y
H0: Equivalenceᵢ S
Equivalenceᵢ (sumᵣ R S)
econstructor.
I: Type
X, Y: psh I
R: relᵢ X X
H: Equivalenceᵢ R
S: relᵢ Y Y
H0: Equivalenceᵢ S
i: I
Reflexive (sumᵣ R S i)
I: Type
X, Y: psh I
R: relᵢ X X
H: Equivalenceᵢ R
S: relᵢ Y Y
H0: Equivalenceᵢ S
i: I
Symmetric (sumᵣ R S i)
I: Type
X, Y: psh I
R: relᵢ X X
H: Equivalenceᵢ R
S: relᵢ Y Y
H0: Equivalenceᵢ S
i: I
Transitive (sumᵣ R S i)
-
I: Type
X, Y: psh I
R: relᵢ X X
H: Equivalenceᵢ R
S: relᵢ Y Y
H0: Equivalenceᵢ S
i: I
Reflexive (sumᵣ R S i) intros []; eauto.
-
I: Type
X, Y: psh I
R: relᵢ X X
H: Equivalenceᵢ R
S: relᵢ Y Y
H0: Equivalenceᵢ S
i: I
Symmetric (sumᵣ R S i) intros ? ? []; econstructor; symmetry; eauto.
-
I: Type
X, Y: psh I
R: relᵢ X X
H: Equivalenceᵢ R
S: relᵢ Y Y
H0: Equivalenceᵢ S
i: I
Transitive (sumᵣ R S i) intros ? ? ? ? ?.
I: Type
X, Y: psh I
R: relᵢ X X
H: Equivalenceᵢ R
S: relᵢ Y Y
H0: Equivalenceᵢ S
i: I
x, y, z: (X +ᵢ Y) i
H1: sumᵣ R S i x y
H2: sumᵣ R S i y z
sumᵣ R S i x z dependent destruction H1; dependent destruction H2; econstructor; etransitivity; eauto.
Qed.

Definition seqᵢ {I} {X Y Z : psh I} (R0 : relᵢ X Y) (R1 : relᵢ Y Z) : relᵢ X Z :=
  fun i x z => exists y, R0 i x y /\ R1 i y z.
#[global] Infix "⨟" := (seqᵢ) (at level 120).
#[global] Notation "u ⨟⨟ v" := (ex_intro _ _ (conj u v)) (at level 70).
#[global] Hint Unfold seqᵢ : core.

#[global] Instance seq_mon {I} {X Y Z : psh I} : Proper (leq ==> leq ==> leq) (@seqᵢ I X Y Z).
I: Type
X, Y, Z: psh I
Proper (leq ==> leq ==> leq) seqᵢ
Proof.
I: Type
X, Y, Z: psh I
Proper (leq ==> leq ==> leq) seqᵢ intros ? ? H1 ? ? H2 ? ? ? [z []].
I: Type
X, Y, Z: psh I
x, y: relᵢ X Y
H1: x <= y
x0, y0: relᵢ Y Z
H2: x0 <= y0
a: I
a0: X a
a1: Z a
z: Y a
H: x a a0 z
H0: x0 a z a1
(y ⨟ y0) a a0 a1 exists z.
I: Type
X, Y, Z: psh I
x, y: relᵢ X Y
H1: x <= y
x0, y0: relᵢ Y Z
H2: x0 <= y0
a: I
a0: X a
a1: Z a
z: Y a
H: x a a0 z
H0: x0 a z a1
y a a0 z /\ y0 a z a1 split.
I: Type
X, Y, Z: psh I
x, y: relᵢ X Y
H1: x <= y
x0, y0: relᵢ Y Z
H2: x0 <= y0
a: I
a0: X a
a1: Z a
z: Y a
H: x a a0 z
H0: x0 a z a1
y a a0 z
I: Type
X, Y, Z: psh I
x, y: relᵢ X Y
H1: x <= y
x0, y0: relᵢ Y Z
H2: x0 <= y0
a: I
a0: X a
a1: Z a
z: Y a
H: x a a0 z
H0: x0 a z a1
y0 a z a1 now apply H1.
I: Type
X, Y, Z: psh I
x, y: relᵢ X Y
H1: x <= y
x0, y0: relᵢ Y Z
H2: x0 <= y0
a: I
a0: X a
a1: Z a
z: Y a
H: x a a0 z
H0: x0 a z a1
y0 a z a1 now apply H2. Qed.

Definition squareᵢ {I} {X : psh I} : mon (relᵢ X X) :=
  {| body R := R ⨟ R ; Hbody _ _ H := seq_mon _ _ H _ _ H |}.

Definition revᵢ {I} {X Y : psh I} (R : relᵢ X Y) : relᵢ Y X := fun i x y => R i y x.
#[global] Hint Unfold revᵢ : core.

#[global] Instance rev_mon {I} {X Y : psh I} : Proper (leq ==> leq) (@revᵢ I X Y).
I: Type
X, Y: psh I
Proper (leq ==> leq) revᵢ
Proof.
I: Type
X, Y: psh I
Proper (leq ==> leq) revᵢ firstorder. Qed.

Definition converseᵢ {I} {X : psh I} : mon (relᵢ X X) :=
  {| body := revᵢ ; Hbody := rev_mon |}.

Definition orᵢ {I} {X Y : psh I} (R S : relᵢ X Y) : relᵢ X Y := fun i x y => R i x y \/ S i x y.
#[global] Infix "∨ᵢ" := (orᵢ) (at level 70).
#[global] Instance or_mon {I} {X Y : psh I} : Proper (leq ==> leq ==> leq) (@orᵢ I X Y).
I: Type
X, Y: psh I
Proper (leq ==> leq ==> leq) orᵢ
Proof.
I: Type
X, Y: psh I
Proper (leq ==> leq ==> leq) orᵢ firstorder. Qed.

Lemma build_reflexive {I} {X : psh I} {R : relᵢ X X} : eqᵢ X <= R -> Reflexiveᵢ R.
I: Type
X: psh I
R: relᵢ X X
eqᵢ X <= R -> Reflexiveᵢ R
Proof.
I: Type
X: psh I
R: relᵢ X X
eqᵢ X <= R -> Reflexiveᵢ R intros H ? ?.
I: Type
X: psh I
R: relᵢ X X
H: eqᵢ X <= R
i: I
x: X i
R i x x now apply H. Qed.

Lemma use_reflexive {I} {X : psh I} {R : relᵢ X X} (H : Reflexiveᵢ R) : eqᵢ X <= R.
I: Type
X: psh I
R: relᵢ X X
H: Reflexiveᵢ R
eqᵢ X <= R
Proof.
I: Type
X: psh I
R: relᵢ X X
H: Reflexiveᵢ R
eqᵢ X <= R intros ? ? ? ->; now reflexivity. Qed.

Lemma build_symmetric {I} {X : psh I} {R : relᵢ X X} : converseᵢ R <= R -> Symmetricᵢ R.
I: Type
X: psh I
R: relᵢ X X
converseᵢ R <= R -> Symmetricᵢ R
Proof.
I: Type
X: psh I
R: relᵢ X X
converseᵢ R <= R -> Symmetricᵢ R intros H ? ? ? ?.
I: Type
X: psh I
R: relᵢ X X
H: converseᵢ R <= R
i: I
x, y: X i
H0: R i x y
R i y x now apply H. Qed.

Lemma use_symmetric {I} {X : psh I} {R : relᵢ X X} (H : Symmetricᵢ R) : converseᵢ R <= R.
I: Type
X: psh I
R: relᵢ X X
H: Symmetricᵢ R
converseᵢ R <= R
Proof.
I: Type
X: psh I
R: relᵢ X X
H: Symmetricᵢ R
converseᵢ R <= R intros ? ? ? ?; now symmetry. Qed.

Lemma build_transitive {I} {X : psh I} {R : relᵢ X X} : squareᵢ R <= R -> Transitiveᵢ R.
I: Type
X: psh I
R: relᵢ X X
squareᵢ R <= R -> Transitiveᵢ R
Proof.
I: Type
X: psh I
R: relᵢ X X
squareᵢ R <= R -> Transitiveᵢ R intros H i x y z r s.
I: Type
X: psh I
R: relᵢ X X
H: squareᵢ R <= R
i: I
x, y, z: X i
r: R i x y
s: R i y z
R i x z apply H; now exists y. Qed.

Lemma use_transitive {I} {X : psh I} {R : relᵢ X X} (H : Transitiveᵢ R) : squareᵢ R <= R.
I: Type
X: psh I
R: relᵢ X X
H: Transitiveᵢ R
squareᵢ R <= R
Proof.
I: Type
X: psh I
R: relᵢ X X
H: Transitiveᵢ R
squareᵢ R <= R intros ? ? ? [ y [ ? ? ] ].
I: Type
X: psh I
R: relᵢ X X
H: Transitiveᵢ R
a: I
a0, a1, y: X a
H0: R a a0 y
H1: R a y a1
R a a0 a1 now transitivity y. Qed.

Lemma build_equivalence {I} {X : psh I} {R : relᵢ X X}
      : eqᵢ X <= R -> converseᵢ R <= R -> squareᵢ R <= R -> Equivalenceᵢ R.
I: Type
X: psh I
R: relᵢ X X
eqᵢ X <= R ->
converseᵢ R <= R -> squareᵢ R <= R -> Equivalenceᵢ R
Proof.
I: Type
X: psh I
R: relᵢ X X
eqᵢ X <= R ->
converseᵢ R <= R -> squareᵢ R <= R -> Equivalenceᵢ R
  econstructor.
I: Type
X: psh I
R: relᵢ X X
H: eqᵢ X <= R
H0: converseᵢ R <= R
H1: squareᵢ R <= R
i: I
Reflexive (R i)
I: Type
X: psh I
R: relᵢ X X
H: eqᵢ X <= R
H0: converseᵢ R <= R
H1: squareᵢ R <= R
i: I
Symmetric (R i)
I: Type
X: psh I
R: relᵢ X X
H: eqᵢ X <= R
H0: converseᵢ R <= R
H1: squareᵢ R <= R
i: I
Transitive (R i)
  now apply build_reflexive.
I: Type
X: psh I
R: relᵢ X X
H: eqᵢ X <= R
H0: converseᵢ R <= R
H1: squareᵢ R <= R
i: I
Symmetric (R i)
I: Type
X: psh I
R: relᵢ X X
H: eqᵢ X <= R
H0: converseᵢ R <= R
H1: squareᵢ R <= R
i: I
Transitive (R i)
  now apply build_symmetric.
I: Type
X: psh I
R: relᵢ X X
H: eqᵢ X <= R
H0: converseᵢ R <= R
H1: squareᵢ R <= R
i: I
Transitive (R i)
  now apply build_transitive.
Qed.