regexp.abstract.relation

Definition t (s1 s2 : finType) := {ffun s1 → {set s2}}.
Definition empty {s1 s2} : t s1 s2 := [ffun _ ⇒ set0].
Definition full {s1 s2} : t s1 s2 := [ffun _ ⇒ setT].
Definition img {s1 s2}(r : t s1 s2)(A : {set s1}) : {set s2} :=
  \bigcup_(a in A) r a.

Lemma emptyE {s1 s2 : finType} : ∀ x : s1, (empty : t s1 s2) x = set0.
  move ⇒ x; by rewrite ffunE.
Qed.

Section Matrix.
  Context {a1 a2 b1 b2 : finType}.
    Definition matrix : (t a1 b1 → t a1 b2
                         → t a2 b1 → t a2 b2
                         → t (a1 + a2) (b1 + b2))%type :=

      (fun r11 r12
           r21 r22 ⇒ [ ffun u ⇒ match u with
                                | inl ul ⇒ inl @: r11 ul :|: inr @: r12 ul
                                | inr ur ⇒ inl @: r21 ur :|: inr @: r22 ur
                                end
      ]).

    Lemma matrix_eq {r11 r12 r21 r22} {R11 R12 R21 R22} :
      r11 = R11 ∧ r12 = R12 ∧ r21 = R21 ∧ r22 = R22 → matrix r11 r12 r21 r22 = matrix R11 R12 R21 R22.
      case ⇒ h11 [h12 [h21 h22]].
      rewrite /matrix -ffunP ⇒ x; case: x ⇒ x; rewrite ?ffunE;
                                              by rewrite ?h11 ?h12 ?h21 ?h22.
    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) := [ ffun u ⇒ match u with
                                                                              | inl ul ⇒ inl @: r1 ul
                                                                              | inr ur ⇒ inr @: r2 ur
                                                                              end ].

Lemma diagonal_matrix {s1 s2}(r1 : binary.t s1)(r2 : binary.t s2) : diagonal r1 r2 = matrix r1 empty empty r2.
  apply/eq_ffun ⇒ x; case x ⇒ u; by rewrite emptyE imset0 ?setU0 ?set0U.
Qed.