# Library RelationAlgebra.dfa

Require Import comparisons positives ordinal pair lset.

Require Import monoid boolean prop sups bmx.

Set Implicit Arguments.

Unset Printing Implicit Defensive.

# DFA and associated language

Record t := mk {

n: nat;

u: ord n;

M: ord n → positive → ord n;

v: ord n → bool;

vars: list positive

}.

Notation "x ^u" := (u x) (at level 2, left associativity, format "x ^u").

Notation "x ^M" := (M x) (at level 2, left associativity, format "x ^M").

Notation "x ^v" := (v x) (at level 2, left associativity, format "x ^v").

changing the initial state

Definition reroot A i := mk i A^M A^v (vars A).

Lemma reroot_id A: A = reroot A (A^u).

Proof. destruct A; reflexivity. Qed.

Lemma reroot_id A: A = reroot A (A^u).

Proof. destruct A; reflexivity. Qed.

Fixpoint lang A i w :=

match w with

| nil ⇒ is_true (A^v i)

| cons a w ⇒ In a (vars A) ∧ lang A (A^M i a) w

end.

match w with

| nil ⇒ is_true (A^v i)

| cons a w ⇒ In a (vars A) ∧ lang A (A^M i a) w

end.

Definition diff := mk

(pair.mk (u A) (u B))

(fun p a ⇒ pair.mk (M A (pair.pi1 p) a) (M B (pair.pi2 p) a))

(fun p ⇒ v A (pair.pi1 p) ⊓ ! v B (pair.pi2 p))

(vars A).

(pair.mk (u A) (u B))

(fun p a ⇒ pair.mk (M A (pair.pi1 p) a) (M B (pair.pi2 p) a))

(fun p ⇒ v A (pair.pi1 p) ⊓ ! v B (pair.pi2 p))

(vars A).

specification of its language

Lemma diff_spec: vars A ≦ vars B →

∀ i j, lang A i ≦ lang B j ↔ lang diff (pair.mk i j) ≦ bot.

Proof.

intro H.

cut (∀ w i j, lang A i w ≦ lang B j w ↔ ¬ lang diff (pair.mk i j) w).

intros G i j. split. intros Hij w Hw. apply G in Hw as []. apply Hij.

intros Hij w. apply G. intro Hw. elim (Hij _ Hw).

induction w; intros i j; simpl lang; rewrite pair.pi1mk, pair.pi2mk.

case (v A i); case (v B j); firstorder discriminate.

split. intros Hij [HaB Hw]. apply IHw in Hw as []. intro Aw. apply Hij. now split.

intros Hw [Ha Aw]. split. apply H, Ha. eapply IHw. 2: eassumption. tauto.

Qed.

End diff.

∀ i j, lang A i ≦ lang B j ↔ lang diff (pair.mk i j) ≦ bot.

Proof.

intro H.

cut (∀ w i j, lang A i w ≦ lang B j w ↔ ¬ lang diff (pair.mk i j) w).

intros G i j. split. intros Hij w Hw. apply G in Hw as []. apply Hij.

intros Hij w. apply G. intro Hw. elim (Hij _ Hw).

induction w; intros i j; simpl lang; rewrite pair.pi1mk, pair.pi2mk.

case (v A i); case (v B j); firstorder discriminate.

split. intros Hij [HaB Hw]. apply IHw in Hw as []. intro Aw. apply Hij. now split.

intros Hw [Ha Aw]. split. apply H, Ha. eapply IHw. 2: eassumption. tauto.

Qed.

End diff.

# Decidability of DFA language emptiness

erased transition graph, represented as a Boolean matrix

reflexive transitive closure of this graph

basic properties of this closed graph

Lemma steps_refl: steps i i.

Proof. apply bmx_str_clot. constructor. Qed.

Lemma steps_snoc: ∀ j a, steps i j → In a (vars A) → steps i (M A j a).

Proof.

setoid_rewrite bmx_str_clot. intros. eapply clot_snoc. eassumption.

setoid_rewrite is_true_sup. eexists. split. eassumption. apply eqb_refl.

Qed.

Proof. apply bmx_str_clot. constructor. Qed.

Lemma steps_snoc: ∀ j a, steps i j → In a (vars A) → steps i (M A j a).

Proof.

setoid_rewrite bmx_str_clot. intros. eapply clot_snoc. eassumption.

setoid_rewrite is_true_sup. eexists. split. eassumption. apply eqb_refl.

Qed.

each unlabelled path in the erased graph corresponds to a labelled
path (word) in the DFA

Lemma steps_least: ∀ j, steps i j → ∃ w, w ≦ vars A ∧ j = Ms i w.

Proof.

intros j H. apply bmx_str_clot in H. induction H as [i|i j k Hij _ [w [Hw ->]]].

∃ nil. split. lattice. reflexivity.

setoid_rewrite is_true_sup in Hij. destruct Hij as [a [Ha Hij]].

∃ (a::w). split. intros b [<-|Hb]. assumption. now apply Hw.

revert Hij. case eqb_ord_spec. 2: discriminate. now intros <-.

Qed.

Proof.

intros j H. apply bmx_str_clot in H. induction H as [i|i j k Hij _ [w [Hw ->]]].

∃ nil. split. lattice. reflexivity.

setoid_rewrite is_true_sup in Hij. destruct Hij as [a [Ha Hij]].

∃ (a::w). split. intros b [<-|Hb]. assumption. now apply Hw.

revert Hij. case eqb_ord_spec. 2: discriminate. now intros <-.

Qed.

can we reach an accepting state from i

if not, all states reachable from i map to the empty language

Lemma empty_lang1 j: steps i j → empty → lang A j ≦ bot.

Proof.

intros Hj He. setoid_rewrite is_true_inf in He. setoid_rewrite le_bool_spec in He.

pose proof (fun i ⇒ He i (ordinal.in_seq _)) as H. clear He.

intro w. revert j Hj. induction w as [|a w IH]; simpl lang; intros j Hj.

apply (H j), negb_spec in Hj. rewrite Hj. discriminate.

intros [Ha Hj']. apply IH in Hj' as []. now apply steps_snoc.

Qed.

Proof.

intros Hj He. setoid_rewrite is_true_inf in He. setoid_rewrite le_bool_spec in He.

pose proof (fun i ⇒ He i (ordinal.in_seq _)) as H. clear He.

intro w. revert j Hj. induction w as [|a w IH]; simpl lang; intros j Hj.

apply (H j), negb_spec in Hj. rewrite Hj. discriminate.

intros [Ha Hj']. apply IH in Hj' as []. now apply steps_snoc.

Qed.

conversely, if i maps to them empty language, then there is no
reachable accepting state

Lemma empty_lang2: lang A i ≦ bot → empty.

Proof.

intro H. setoid_rewrite is_true_inf. intros j _.

rewrite le_bool_spec. intro Hj. apply steps_least in Hj as [w [Hw ->]].

generalize i (H w) Hw. clear. induction w; intros i Hi Hw.

simpl in ×. destruct (v A i). now elim Hi. reflexivity.

apply IHw. intro H. elim Hi. split. apply Hw. now left. assumption.

intros ? ?. apply Hw. now right.

Qed.

Proof.

intro H. setoid_rewrite is_true_inf. intros j _.

rewrite le_bool_spec. intro Hj. apply steps_least in Hj as [w [Hw ->]].

generalize i (H w) Hw. clear. induction w; intros i Hi Hw.

simpl in ×. destruct (v A i). now elim Hi. reflexivity.

apply IHw. intro H. elim Hi. split. apply Hw. now left. assumption.

intros ? ?. apply Hw. now right.

Qed.

decidability of language emptiness follows