regexp.concrete.relation

Definition t s1 s2 := s1 ~> subset.t s2.
Definition empty {s1 s2} : t s1 s2 := function.constant ∅.
Definition full {s1 s2} : t s1 s2 := function.constant subset.full.
Definition img {s1 s2}(r : t s1 s2)(A : subset.t s1) : subset.t s2 :=
  subset.big.union r A.

Definition or {s1 s2} : t s1 s2 → t s1 s2 → t s1 s2 := function.zipWith subset.union.
Definition and {s1 s2} : t s1 s2 → t s1 s2 → t s1 s2 := function.zipWith subset.intersection.

Definition compose {s1 s2 s3} (r1 : t s1 s2)(r2 : t s2 s3) : t s1 s3 :=
  map (fun a ⇒ img r2 a) r1.

Infix "∘" := compose (at level 40, left associativity) : concrete_scope.

Definition denote {s1 s2} (r : t s1 s2) : abstract.relation.t s1 s2 := function.denote (function.map (subset.denote) r).

Lemma empty_spec {s1 s2} : denote (empty : t s1 s2) = abstract.relation.empty.
  apply/ffunP ⇒ x; by rewrite /empty /denote function.denoteE to_map constantE /abstract.relation.empty ffunE //= subset.empty_spec.
Qed.

Lemma full_spec {s1 s2} : denote (full : t s1 s2) = abstract.relation.full.
  apply/ffunP ⇒ x; by rewrite /full /denote function.denoteE to_map constantE /abstract.relation.full ?ffunE //= subset.full_spec.
Qed.

Lemma composeP {s1 s2 s3} (r1 : t s1 s2)(r2 : t s2 s3) u v : reflect (∃ x, r1 u x ∧ r2 x v) ((r1 ∘ r2) u v).
  apply /(iffP idP); rewrite /compose to_map /img -denoteE big.union_spec.
  - by case/bigcupP ⇒ x; rewrite ?denoteE ⇒ h1 h2; ∃ x.
  - by case ⇒ x [h1 h2]; apply /bigcupP; ∃ x; rewrite ?denoteE.
Qed.

Section Matrix.
  Context {a1 a2 b1 b2 : sort}.
  Definition matrix : t a1 b1 → t a1 b2
                    → t a2 b1 → t a2 b2
                    → t (a1 ∐ a2) (b1 ∐ b2) :=
    fun r11 r12
        r21 r22 ⇒ function.zipWith concat r11 r12 ++ function.zipWith concat r21 r22.

  Lemma matrix_spec r11 r12 r21 r22 :
    denote (matrix r11 r12 r21 r22) = abstract.relation.matrix (denote r11) (denote r12) (denote r21)(denote r22).
    apply eq_ffun ⇒ x.
    by case x ⇒ a; rewrite /relation.denote ?ffunE ?to_map
                     /matrix //= function.zip_pointwise -/disjoint_union injDU union_spec injl_spec injr_spec.
  Qed.

End Matrix.

Module binary.
  Definition t s := relation.t s s.
End binary.

Definition diagonal {s1 s2}(r1 : binary.t s1)(r2 : binary.t s2) :=
  function.map subset.injl r1 ++ function.map (subset.injr) r2.

Lemma diagonal_spec {s1 s2}(r1 : binary.t s1)(r2 : binary.t s2) :
  denote (diagonal r1 r2) = abstract.relation.diagonal (denote r1) (denote r2).
  apply eq_ffun ⇒ x; case x ⇒ u; repeat rewrite /diagonal //= ?injl_spec ?injr_spec ?ffunE ?to_map.
Qed.