Authors: Christian Doczkal and Jan-Oliver Kaiser
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype path fingraph finfun finset.
Require Import misc regexp.

Set Implicit Arguments.

Section FA.
Variable char : finType.
Definition word := regexp.word char.

Finite Automata

Deterministic Finite Automata


Record dfa : Type := {
    dfa_state :> finType;
    dfa_s : dfa_state;
    dfa_fin : pred dfa_state;
    dfa_trans : dfa_state -> char -> dfa_state
    }.

For DFAs, we use the direct recursive defintion of acceptance as well as a definition in terms of runs. The latter is used in the translation of DFAs to regular expressions.

Fixpoint dfa_accept (A : dfa) (x : A) w :=
  if w is a :: w' then dfa_accept A (dfa_trans A x a) w' else x \in dfa_fin A.

Arguments dfa_trans [d] x a.
Arguments dfa_accept [A] x w.

Section DFA_Acceptance.
Variable A : dfa.

Lemma dfa_accept_cons (x : A) a w :
  a :: w \in dfa_accept x = (w \in dfa_accept (dfa_trans x a)).
Proof. by rewrite -simpl_predE /=. Qed.

We define a run of w on the automaton A to be the list of states x_1 .. x|w| traversed when following the edges labeled w_1 .. w|w| starting in x. So the run on x does not include x

Fixpoint dfa_run (x : A) (w : word) : seq A :=
  if w is a :: w' then dfa_trans x a :: dfa_run (dfa_trans x a) w' else [::].

Lemma dfa_run_take x w n : take n (dfa_run x w) = dfa_run x (take n w).
Proof. elim: w x n => [|a w IHw] x n //. case: n => [|n] //=. by rewrite IHw. Qed.

Lemma dfa_run_cat x w1 w2 :
  dfa_run x (w1 ++ w2) = dfa_run x w1 ++ dfa_run (last x (dfa_run x w1)) w2.
Proof. elim: w1 w2 x => [|a w1 IHw1] w2 x //. simpl. by rewrite IHw1. Qed.

Definition delta x w := last x (dfa_run x w).

Lemma delta_cons x a w : delta x (a :: w) = delta (dfa_trans x a) w.
Proof. by []. Qed.

Lemma delta_cat x w1 w2 : delta x (w1 ++ w2) = delta (delta x w1) w2.
Proof. by rewrite /delta dfa_run_cat last_cat. Qed.

Definition delta_s w := delta (dfa_s A) w.

Lemma delta_accept (x : A) w : (w \in dfa_accept x) = (delta x w \in dfa_fin A).
Proof. elim: w x => [|a w IHw] x //. by rewrite /= -IHw. Qed.

Lemma dfa_trans1 x w a :
  dfa_trans (delta x w) a = delta x (w ++ [::a]).
Proof. elim: w x a => [|b w IHw] x a //=. by rewrite !delta_cons IHw. Qed.

End DFA_Acceptance.

Definition dfa_lang A := [pred w | dfa_accept (dfa_s A) w].

Arguments delta_s A w.
Arguments delta [A] x w.
Arguments dfa_accept A x w.

Nondeterministic Finite Automata.

Record nfa : Type := {
    nfa_state :> finType;
    nfa_s : nfa_state;
    nfa_fin : pred nfa_state;
    nfa_trans : nfa_state -> char -> nfa_state -> bool
    }.

Non-deterministic acceptance.
Fixpoint nfa_accept (A : nfa) (x : A) w :=
  if w is a :: w' then [exists y, nfa_trans A x a y && nfa_accept A y w']
                  else x \in nfa_fin A.

Definition nfa_lang (A : nfa) := [pred w | nfa_accept A (nfa_s A) w].

Definition nfa_char a :=
  {| nfa_s := false ;
     nfa_fin := id ;
     nfa_trans x b y := [&& (b == a), ~~ x & y] |}.

Lemma nfa_char_correct a : nfa_lang (nfa_char a) =1 pred1 [:: a].
Proof.
 move => [|b w] => //.
 apply/existsP/eqP => [[x] /andP [/and3P [/eqP -> _ Hx]] |[-> ->]].
 - case: w => //= c w /existsP [y] /=. by rewrite Hx andbF.
 - exists true. by rewrite /= eqxx.
Qed.

Equivalence of DFAs and NFAs

We use the powerset construction to obtain a deterministic automaton from a non-deterministic one.
Section PowersetConstruction.

Variable A : nfa.

Definition nfa_to_dfa := {|
  dfa_s := [set nfa_s A];
  dfa_fin X := [exists x: A, (x \in X) && nfa_fin A x];
  dfa_trans X a := \bigcup_(x | x \in X) [set y | nfa_trans A x a y] |}.

Lemma nfa_to_dfa_aux2 (x : A) w (X : nfa_to_dfa) :
  x \in X -> nfa_accept A x w -> dfa_accept X w.
Proof. move => H0.
  elim: w X x H0 => [|a w IHw] X x H0 /=.
    move => H1. apply/existsP. by eexists; erewrite H0.
  move => /= /existsP [] y /andP [] H1 H2.
  apply: (IHw _ y) => //.
  apply/bigcupP. exists x => //=. by rewrite in_set.
Qed.

Lemma nfa_to_dfa_aux1 (X : nfa_to_dfa) w :
  dfa_accept X w -> exists2 x, (x \in X) & nfa_accept A x w.
Proof. elim: w X => [|a w IHw] X => //=.
    move/existsP => [x] /andP [] H0 H1. by eexists; eassumption.
  move/IHw => [] y /bigcupP [x] H0. rewrite inE => H1 H2.
  eexists. eassumption.
  apply/existsP. exists y. by apply/andP.
Qed.

Lemma nfa_to_dfa_correct : nfa_lang A =i dfa_lang nfa_to_dfa.
Proof. move => w. apply/idP/idP => /=.
  apply: nfa_to_dfa_aux2. by apply/set1P.
  by move/nfa_to_dfa_aux1 => [x] /set1P ->.
Qed.

End PowersetConstruction.

Embedding deterministic automata in non-deterministic automata.
Section Embed.

Variable A : dfa.

Definition dfa_to_nfa : nfa := {|
  nfa_s := dfa_s A;
  nfa_fin := dfa_fin A;
  nfa_trans x a y := y == dfa_trans x a |}.

Lemma dfa_to_nfa_correct : dfa_lang A =i nfa_lang dfa_to_nfa.
Proof.
  move => w. rewrite /dfa_lang /nfa_lang /=. move: (dfa_s A) => x.
  elim: w x => [|b w IHw] x //=.
  rewrite dfa_accept_cons IHw !inE /=. apply/idP/existsP.
    move => H0. exists (dfa_trans x b). by rewrite eq_refl.
  by move => [] y /andP [] /eqP ->.
Qed.

End Embed.

Regular Operations on Automata

Primitive automata
Definition dfa_void :=
  {| dfa_s := tt; dfa_fin x := false; dfa_trans x a := tt |}.

Lemma dfa_void_correct (x: dfa_void) w: ~~ dfa_accept x w.
Proof. by elim: w x => [|a w IHw] //=. Qed.

Definition dfa_eps :=
 {| dfa_s := true; dfa_fin := id ; dfa_trans x a := false |}.

Lemma dfa_eps_correct : dfa_lang dfa_eps =i pred1 [::].
Proof.
  have H: (forall w, ~~ @dfa_accept dfa_eps false w) by elim => [|a v IHv] //=.
  elim => [|a w IHw] //. apply/idP/idP. exact: H.
Qed.

Operations on deterministic automata.
Section DFAOps.

Variable op : bool -> bool -> bool.
Variable A1 A2 : dfa.

Complement automaton
Definition dfa_compl :=
 {|
    dfa_s := dfa_s A1;
    dfa_fin := [predC (dfa_fin A1)];
    dfa_trans := (@dfa_trans A1)
  |}.

Lemma dfa_compl_correct w :
  w \in dfa_lang dfa_compl = (w \notin dfa_lang A1).
Proof.
  rewrite /dfa_lang !inE {2}/dfa_compl /=.
  elim: w (dfa_s _) => [| a w IHw] x //=.
Qed.

BinOp Automaton

Definition dfa_op :=
  {| dfa_s := (dfa_s A1, dfa_s A2);
     dfa_fin q := let (x1,x2) := q in op (dfa_fin A1 x1) (dfa_fin A2 x2);
     dfa_trans x a := (dfa_trans x.1 a, dfa_trans x.2 a) |}.

Lemma dfa_op_correct w :
  w \in dfa_lang dfa_op = op (w \in dfa_lang A1) (w \in dfa_lang A2).
Proof.
  rewrite /dfa_lang /=. move: (dfa_s A1) (dfa_s A2) => x y.
  elim: w x y => [| a w IHw] //= x y. by rewrite dfa_accept_cons IHw.
Qed.

End DFAOps.

Operations on non-deterministic automata.
Section NFAOps.

Implicit Type A : nfa.

Concatenation of two non-deterministic automata. This construction looks more complicated than the ususal construction with epsilon edges, but the construction is essentially the same

Definition nfa_conc A1 A2 : nfa :=
 {| nfa_s := inl _ (nfa_s A1);
    nfa_fin := [pred x |
        match x with
          | inl x => (x \in nfa_fin A1) && (nfa_s A2 \in nfa_fin A2)
          | inr x => x \in nfa_fin A2
        end];
     nfa_trans := fun x a y =>
        match x,y with
          | inl x, inl y => nfa_trans A1 x a y
          | inl x, inr y => (x \in nfa_fin A1) && nfa_trans A2 (nfa_s A2) a y
          | inr x, inr y => nfa_trans A2 x a y
          | inr x, inl y => false
        end
 |}.

Lemma conc_inrP A1 A2 x w :
  nfa_accept (nfa_conc A1 A2) (inr x) w = nfa_accept A2 x w.
Proof. elim: w x => [|a w IHw] x //=; apply/exists_inP/exists_inP.
  move => [[y //|y Y1 Y2]]. exists y; by rewrite // -IHw.
  case => y Y1 Y2. exists (inr y); by rewrite // IHw.
Qed.

Lemma conc_inlP A1 A2 x w : reflect
  (exists w1 w2, [/\ w = w1 ++ w2 , nfa_accept A1 x w1 & w2 \in nfa_lang A2])
  (nfa_accept (nfa_conc A1 A2) (inl x) w).
Proof. elim: w x => [x|a w IHw x] /=.
  - rewrite inE. apply: (iffP andP) => [[H1 H2] | [[|a w1]] [[|b w2]] [] //].
    do 2 exists [::]; by split.
  - apply: (iffP exists_inP).
    + move => [[y Hy /IHw [w1 [w2 [e W1 W2]]] |y /andP [Y1 Y2 Y3] ]].
      * exists (a::w1); exists w2 => //=. rewrite e; split => //.
        apply/existsP; exists y. by rewrite Hy.
      * exists [::]. exists (a::w). rewrite inE -(@conc_inrP A1 A2); split => //=.
        apply/existsP; exists (inr y). by rewrite Y2 Y3.
    + move => [[|b w1] /= [w2 [e W1 W2]]].
      * rewrite -e /= in W2. case/exists_inP : W2 => y Y1 Y2.
        exists (inr y) ; by rewrite ?W1 ?conc_inrP.
      * case : e => e1 e2. case/exists_inP : W1 => y Y1 Y2.
        exists (inl y). by rewrite e1. apply/IHw. exists w1; exists w2. by split.
Qed.

Lemma nfa_conc_correct A1 A2 :
  nfa_lang (nfa_conc A1 A2) =i conc (nfa_lang A1) (nfa_lang A2).
Proof. move => w.
  apply/conc_inlP/concP => [[w1] [w2] [H1 [H2 H3]] | [v1] [v2] [E [H1 H2]]].
  exists w1. exists w2. by split.
  exists v1. by exists v2.
Qed.

For nfa_star we again have to duplicate some edges since we have no epsilon transitions.

Definition nfa_star A : nfa :=
 {| nfa_s := None;
    nfa_fin x := x == None;
    nfa_trans x a y :=
      match x,y with
        | Some x, Some y => nfa_trans A x a y
        | None, Some y => nfa_trans A (nfa_s A) a y
        | Some x, None => [exists z, (nfa_trans A x a z) && (z \in nfa_fin A)]
        | None, None => [exists z, (nfa_trans A (nfa_s A) a z) && (z \in nfa_fin A)]
      end |}.

Since we need at least one step to get back to None, acceptance in A can only be lifted to nfa_star A for nonempty words.

Lemma nfa_star_cont A x w :
  ~~ nilp w -> nfa_accept A x w -> nfa_accept (nfa_star A) (Some x) w.
Proof.
  elim: w x => [|b [|c w] IHw] x //= _ H.
  - apply/existsP; exists None. by rewrite H.
  - case/exists_inP : H => y xy H. apply/exists_inP; exists (Some y) =>//.
    exact: IHw.
Qed.

Lemma nfa_star_clone A w :
  w \in nfa_lang A -> w \in nfa_lang (nfa_star A).
Proof. case: w => [|a w] //. rewrite !inE. exact: nfa_star_cont. Qed.

Lemma nfa_star_cat A x w1 w2 :
  nfa_accept (nfa_star A) x w1 -> w2 \in nfa_lang (nfa_star A) ->
  nfa_accept (nfa_star A) x (w1 ++ w2).
Proof.
  elim: w1 x => [|a w1 IHw] x. by rewrite !inE /= => /eqP->.
  case/exists_inP => y xy H1 H2. rewrite /=. apply/exists_inP; exists y => //.
  exact: IHw.
Qed.

Lemma nfa_starE_aux {A x w} :
  nfa_accept (nfa_star A) (Some x) w ->
  (exists w1 w2, [/\ w = w1 ++ w2, nfa_accept A x w1 & nfa_accept (nfa_star A) None w2]).
Proof.
  elim: w x => // a w IHw x /= /exists_inP [[y Hy|]].
  - move/IHw => [w1] [w2] [H1 H2 H4].
    exists (a::w1); exists w2.
    split => // ; by [rewrite /= H1 | apply/existsP; exists y; rewrite Hy].
  - move => E N. exists [::a]; exists w. by split.
Qed.

Lemma nfa_starE A a w: (a :: w) \in nfa_lang (nfa_star A) ->
  exists w1 w2, [/\ w = w1 ++ w2, a::w1 \in nfa_lang A & w2 \in nfa_lang (nfa_star A)].
Proof.
  rewrite inE /=. case/exists_inP => [] [y Y1 Y2|].
  - case: (nfa_starE_aux Y2) => w1 [w2] [e acc1 acc2].
    exists w1;exists w2; split => //.
    by apply/exists_inP; exists y.
  - case/exists_inP => y Y1 Y2 Hw. exists [::]; exists w; split => //.
    rewrite inE /=. by apply/exists_inP; exists y.
Qed.

Lemma nfa_star_correct A : nfa_lang (nfa_star A) =i star (nfa_lang A).
Proof.
  move => w. apply/idP/starP => [| [vv] H -> {w}].
  + move: {2}(size w) (leqnn (size w)) => n.
    elim: n w => [[_ _|//]|n IHn [|a w] s]; try by exists [::].
    case/nfa_starE => w1 [w2] [e H H'].
    have w2_le_n : size w2 <= n.
      apply: (@leq_trans (size w)) => //. by rewrite e size_cat leq_addl.
    case (IHn _ w2_le_n H') => vv' Hvv e'.
    exists [:: (a::w1) & vv'] => /=; by [rewrite H | subst].
  + elim: vv H => //= [] [|a w] // vv IHvv. (do 2 case/andP) => _ HA /IHvv.
    apply: nfa_star_cat. by move/nfa_star_clone : HA.
Qed.

End NFAOps.

Translation of Regular Expressions to Finite Automata


Fixpoint re_to_dfa (r : regexp char): dfa :=
  match r with
  | Void => dfa_void
  | Eps => dfa_eps
  | Atom a => nfa_to_dfa (nfa_char a)
  | Star s => nfa_to_dfa (nfa_star (dfa_to_nfa (re_to_dfa s)))
  | Plus s t => dfa_op orb (re_to_dfa s) (re_to_dfa t)
  | Conc s t => nfa_to_dfa (nfa_conc (dfa_to_nfa (re_to_dfa s)) (dfa_to_nfa (re_to_dfa t)))
  end.

Lemma re_to_dfa_correct r : dfa_lang (re_to_dfa r) =i r.
Proof with rewrite -?(nfa_to_dfa_correct,dfa_to_nfa_correct) //.
  elim: r => [||a|s IHs |s IHs t IHt |s IHs t IHt] w //=...
  - apply/negbTE; exact: dfa_void_correct.
  - exact: dfa_eps_correct.
  - exact: nfa_char_correct.
  - rewrite nfa_star_correct. apply: star_eq => {w} w...
  - by rewrite dfa_op_correct IHs IHt.
  - rewrite nfa_conc_correct. apply: conc_eq => {w} w...
Qed.

Decidability of Language Equivalence


Section Reachability.
  Variable A : dfa.

  Definition dfa_trans_some (x y : A) := [exists a, dfa_trans x a == y].

  Lemma step_someP x y :
    reflect (exists w, delta x w == y) (connect dfa_trans_some x y).
  Proof.
    apply: (iffP connectP) => [[p]|[w]].
    - elim: p x y => [x y _ -> |z p IHp x y /= /andP[H1 H2 e]]; first by exists [::].
      case: (IHp _ _ H2 e) => w e'.
      case/existsP : H1 => [a /eqP Ha]. exists (a::w). by rewrite delta_cons Ha.
    - elim: w x y => [x y /eqP e | a w IHw x y /IHw [p p1 p2]]; first by exists [::].
      exists (dfa_trans x a::p) => //. rewrite /= p1 andbT. by apply/existsP; exists a.
  Qed.

  Definition reachable := connect dfa_trans_some (dfa_s A).
End Reachability.

Definition dfa_lang_empty A := [forall (x | reachable A x), x \notin dfa_fin A].

Lemma dfa_lang_emptyP A :
  reflect (dfa_lang A =i pred0) (dfa_lang_empty A).
Proof.
  apply: (iffP forall_inP) => [H w| H x R].
  - apply/negbTE. rewrite /dfa_lang delta_accept H //.
    apply/step_someP. by exists w.
  - apply/negP => F. case/step_someP : R => w /eqP Hw.
    suff: w \in dfa_lang A by rewrite H.
    by rewrite delta_accept Hw.
Qed.

Section Equivalence.

  Definition dfa_sym_diff A1 A2 := dfa_op addb A1 A2.

  Definition dfa_equiv A1 A2 := dfa_lang_empty (dfa_sym_diff A1 A2).

  Lemma dfa_equiv_correct A1 A2 :
    reflect (dfa_lang A1 =i dfa_lang A2) (dfa_equiv A1 A2).
  Proof.
    apply: (iffP (dfa_lang_emptyP _)) => H w.
    - move/negbT: (H w). rewrite !dfa_op_correct -addNb.
      move/addbP. by rewrite negbK.
    - apply/negbTE. by rewrite !dfa_op_correct H addbb.
  Qed.
End Equivalence.

Decidability of regular expression equivalence

Definition re_equiv r s := dfa_equiv (re_to_dfa r) (re_to_dfa s).

Lemma re_equiv_correct r s : reflect (r =i s) (re_equiv r s).
Proof.
  apply: (iffP (dfa_equiv_correct _ _)) => H w;
    move/(_ w) : H; by rewrite !re_to_dfa_correct.
Qed.

Arguments reachable [dfa] x : rename.

Construction of the Connected Sub-Automaton


Section Connected.
  Variable A : dfa.

  Definition reachable_type := { x:A | reachable x }.

  Lemma reachable_trans_proof (x : reachable_type) a : reachable (dfa_trans (val x) a).
  Proof.
    apply: connect_trans (svalP x) _.
    apply: connect1. by apply/existsP; eexists.
  Qed.

  Definition reachable_trans (x : reachable_type) a : reachable_type :=
    Sub (dfa_trans (val x) a) (reachable_trans_proof x a).

  Definition reachable_s : reachable_type := Sub (dfa_s A) (connect0 _ _).

  Definition dfa_prune := {|
      dfa_s := reachable_s;
      dfa_fin x := val x \in dfa_fin A;
      dfa_trans := reachable_trans
  |}.

  Lemma dfa_prune_correct : dfa_lang dfa_prune =i dfa_lang A.
  Proof.
    rewrite /dfa_lang /= (_: dfa_s A = val reachable_s) //.
    move: (reachable_s) => x w. elim: w x => [|a w IHw] [x Hx] //.
    by rewrite 2!dfa_accept_cons IHw.
  Qed.

  Definition connected (A : dfa) := surjective (delta_s A).
  Definition connectedb (A : dfa) := [forall x: A, reachable x].

  Lemma connectedP (B : dfa) : reflect (connected B) (connectedb B).
  Proof.
    apply: (iffP forallP) => [H x|H x]; last exact/step_someP.
    by move/step_someP : (H x).
  Qed.

  Lemma dfa_prune_connectedb_aux x y :
    connect (dfa_trans_some A) (val x) (val y) ->
    connect (dfa_trans_some dfa_prune) x y.
  Proof.
    have H_step: forall x y : reachable_type,
      dfa_trans_some A (val x) (val y) -> dfa_trans_some dfa_prune x y by [].
    case/connectP => p.
    elim: p x y => //= [x y _ /val_inj -> //|z p IHp x y /andP [H1 H2] e].
    case/existsP : H1 => a Ha.
    have/H_step H: dfa_trans_some A (val x) (val (reachable_trans x a)).
      rewrite /= (eqP Ha). by apply/existsP; exists a.
    apply: connect_trans (connect1 H) _. apply: IHp; by rewrite /= ?(eqP Ha) ?e.
  Qed.

  Lemma dfa_prune_connected : connected dfa_prune.
  Proof.
    apply/connectedP.
    apply/forallP. move => /= [x Hx]. by apply: dfa_prune_connectedb_aux.
  Qed.

  Hint Resolve dfa_prune_connected.

For connected DFAs, we can use xchoose to obtain for every state a word leading to that state. We use this in the Myhill-Nerode theorem to obtain Myhill partitions from DFAs

  Lemma dfa_prune_size : #|dfa_prune | <= #|A|.
  Proof. by rewrite card_sig subset_leq_card // subset_predT. Qed.

A DFA is connected, if it has the same size as ist connected sub automaton
  Lemma prune_eq_connected : #|A| = #|dfa_prune| -> connected A.
  Proof.
    move => H. apply/connectedP. apply/forallP => x.
    by move: (cardT_eq (Logic.eq_sym H)) ->.
  Qed.

End Connected.

DFA Minimization


Section Minimize.
  Variable A : dfa.

  Definition coll x y := forall w, (delta x w \in dfa_fin A) = (delta y w \in dfa_fin A).

Computation of the collapsing Relation


  Definition dist0 : {set A*A} := [set x | (x.1 \in dfa_fin A) != (x.2 \in dfa_fin A)].

  Definition distS (dist : {set A*A}) :=
    [set x | [exists a, (dfa_trans x.1 a, dfa_trans x.2 a) \in dist]].

  Lemma distSP (dist : {set A*A}) (x y : A) :
    reflect (exists a, (dfa_trans x a, dfa_trans y a) \in dist)
            ((x,y) \in distS dist).
  Proof. by apply: (iffP idP); rewrite !inE => /existsP. Qed.

  Lemma distS_mono: mono distS.
  Proof. move => s t /subsetP H.
   apply/subsetP => [[x y]] /distSP [a H1]. apply/distSP. exists a. exact: H _ H1.
  Qed.

  Definition one_step_dist dist := dist0 :|: distS dist.

  Lemma one_step_dist_mono : mono one_step_dist.
  Proof.
    move => D1 D2 H. apply/subsetP.
    move => x. rewrite /one_step_dist ![_ \in _ :|: _]inE.
    case (_ \in dist0) => //=. apply/subsetP : (distS_mono H) x.
  Qed.

  Definition dist := lfp one_step_dist.

  Lemma distP x y :
    reflect (exists w, (delta x w \in dfa_fin A) != (delta y w \in dfa_fin A))
            ((x,y) \in dist).
  Proof.
    rewrite /dist. apply: (iffP idP).
    move: x y. apply lfp_ind => [x y | D IHD x y]; first by rewrite inE.
      rewrite inE; case/orP => [H|/distSP [a]].
      + exists [::]. by rewrite inE in H.
      + case/IHD => w /= H. by exists (a::w).
    - case => w. elim: w x y => [|a w IHw] u v.
      + by rewrite /delta /= (lfpE one_step_dist_mono) /dist0 !inE /= => ->.
      + rewrite -cat1s delta_cat => /IHw H.
        rewrite (lfpE one_step_dist_mono) inE ( _ : _ \in distS _) ?orbT //.
        apply/distSP. by exists a.
  Qed.

  Definition collb x y := (x,y) \notin dist.

  Lemma collP x y : reflect (coll x y) (collb x y).
  Proof.
    rewrite /coll /collb. apply: (iffP idP) => [H w|H].
    - apply/eqP. apply: negbNE. move: H. apply: contra => H.
      apply/distP. by exists w.
    - apply/distP => [[w]]. by rewrite H eqxx.
  Qed.

  Lemma collb_refl x : collb x x.
  Proof. apply/collP. rewrite /coll. auto. Qed.

  Lemma collb_sym : symmetric collb.
  Proof. move => x y. by apply/collP/collP; move => H w; rewrite H. Qed.

  Lemma collb_trans : transitive collb.
  Proof. move => x y z /collP H1 /collP H2. apply/collP => w. by rewrite H1 H2. Qed.

  Definition min_state := quot collb.
  Definition class (x:A) : min_state :=
    Repr (collb_refl) (collb_sym) (collb_trans) x.

  Lemma collb_step a x y : collb x y -> collb (dfa_trans x a) (dfa_trans y a).
  Proof. move => /collP H. apply/collP => w. by rewrite -!delta_cons H. Qed.

  Lemma class_eq x y : reflect (class x = class y) (collb x y).
  Proof. exact: Repr_id. Qed.

  Definition minimize : dfa := {|
    dfa_s := class (dfa_s A);
    dfa_trans x a := class (dfa_trans (val x) a);
    dfa_fin := [pred x | val x \in dfa_fin A ] |}.

  Canonical fin_app_pred := ApplicativePred (dfa_fin minimize).

  Lemma minimize_delta (x : A) w :
    @delta minimize (class x) w = class (delta x w).
  Proof.
    elim: w x => //= a w IHw x. rewrite -cat1s !delta_cat /= -IHw.
    f_equal. rewrite /delta /=. apply/class_eq. apply: collb_step.
    by rewrite collb_sym (repr_rel collb_refl).
  Qed.

  Lemma minstate_exp (x : minimize) : x = class (val x).
  Proof. case: x => x Hx /=. exact/eqP. Qed.

  Lemma minimize_val (x : minimize) w : class (delta (val x) w) = (delta x w).
  Proof. by rewrite {2}[x]minstate_exp minimize_delta. Qed.

  Lemma minimal_fin (x : A) :
    (class x \in dfa_fin minimize) = (x \in dfa_fin A).
  Proof.
    rewrite /class /minimize inE /=. symmetry.
    by move/collP : (repr_rel collb_refl x) => /(_ [::]).
  Qed.

End Minimize.

Arguments coll [A] x y.

Correctness of Minimization


Lemma minimize_correct A : dfa_lang (minimize A) =i dfa_lang A.
Proof.
  move => w. rewrite !delta_accept {1}/dfa_s /=.
  rewrite minimize_delta -topredE /=.
  set x:= delta _ _. symmetry.
  have:= (repr_rel (collb_refl A)) x. by move/collP => /(_ [::]).
Qed.

Lemma minimize_size A : #|minimize A| <= #|A|.
Proof. rewrite card_sig. exact: max_card. Qed.

Definition minimal (A : dfa) := forall B, dfa_lang A =i dfa_lang B -> #|A| <= #|B|.

Definition collapsed (A : dfa) := forall x y: A, coll x y <-> x = y.

Lemma minimize_collapsed (A : dfa) : collapsed (minimize A).
Proof.
  split => [H|->]; last by apply/collP; exact: collb_refl.
  rewrite [x]minstate_exp [y]minstate_exp. apply/class_eq. apply/collP => w.
  by rewrite -!minimal_fin !minimize_val.
Qed.

Uniqueness of Minimal DFAs


Definition dfa_iso (A1 A2 : dfa) :=
  exists i: A1 -> A2,
    [/\ bijective i,
        forall x a, i (dfa_trans x a) = dfa_trans (i x) a,
        forall x, i (x) \in dfa_fin A2 = (x \in dfa_fin A1) &
        i (dfa_s A1) = dfa_s A2 ].

Section Isomopism.
  Variables (A B : dfa).
  Hypothesis L_AB : dfa_lang A =i dfa_lang B.

  Hypothesis (A_coll: collapsed A) (B_coll: collapsed B).
  Hypothesis (A_conn : connected A) (B_conn : connected B).

  Definition iso (x : A) : B := delta (dfa_s B) (cr A_conn x).
  Definition iso_inv (x : B) : A := delta (dfa_s A) (cr B_conn x).

  Lemma delta_iso w x : delta (iso x) w \in dfa_fin B = (delta x w \in dfa_fin A).
  Proof.
    rewrite -{2}[x](crK (Sf := A_conn)).
    by rewrite /iso -!delta_cat -!delta_accept -!L_AB !delta_accept !delta_cat.
  Qed.

  Lemma delta_iso_inv w x : delta (iso_inv x) w \in dfa_fin A = (delta x w \in dfa_fin B).
  Proof.
    rewrite -{2}[x](crK (Sf:=B_conn)).
    by rewrite /iso -!delta_cat -!delta_accept -!L_AB !delta_accept !delta_cat.
  Qed.

  Lemma can_iso : cancel iso_inv iso.
  Proof. move => x. apply/B_coll => w. by rewrite delta_iso delta_iso_inv. Qed.

  Lemma can_iso_inv : cancel iso iso_inv.
  Proof. move => x. apply/A_coll => w. by rewrite delta_iso_inv delta_iso. Qed.

  Lemma coll_iso : dfa_iso A B.
  Proof.
    exists iso. split.
    - exact: Bijective can_iso_inv can_iso.
    - move => x a. apply/B_coll => w. rewrite dfa_trans1 delta_cat -/(iso _).
      by rewrite -delta_cat -!delta_iso_inv !can_iso_inv.
    - move => x. by rewrite -[iso x]/(delta _ [::]) delta_iso.
    - apply/B_coll => w. by rewrite delta_iso -!delta_accept.
  Qed.

  Lemma dfa_iso_size : dfa_iso A B -> #|A| = #|B|.
  Proof. move => [iso [H _ _ _]]. exact (bij_card H). Qed.

End Isomopism.

Lemma minimize_connected A : connected A -> connected (minimize A).
Proof.
  move => H [x Hx]. case: (H x) => w /eqP Hw. exists w.
  rewrite /delta_s /minimize /= minimize_delta.
  apply/eqP. apply/val_inj => //=. by rewrite (eqP Hx) -Hw.
Qed.

Lemma minimal_connected A : minimal A -> connected A.
Proof.
  move => MA. apply: prune_eq_connected. apply: leq_eq _ (dfa_prune_size _).
  exact: MA (psym (dfa_prune_correct _)).
Qed.

Lemma minimal_size_eq A B :
  minimal A -> minimal B -> dfa_lang A =i dfa_lang B -> #|A| = #|B|.
Proof. move => MinA MinB H. by apply: leq_eq (MinA _ H) (MinB _ _) => w. Qed.

Lemma minimize_minimal A (CA : connected A) : minimal (minimize A).
Proof.
  move => B L_AB. apply: leq_trans _ (dfa_prune_size _).
  apply: leq_trans _ (minimize_size _). apply eq_leq.
  apply: dfa_iso_size.
  apply: coll_iso; auto using minimize_collapsed, dfa_prune_connected, minimize_connected.
  move => w. by rewrite L_AB minimize_correct dfa_prune_correct.
Qed.


Lemma minimize_idem_size A : collapsed A -> #|A| = #|minimize A|.
Proof.
  move => H. apply: leq_eq _ (minimize_size _).
  apply: (card_leq_inj (_:injective (class A))).
  move => x y. move: (H x y) => H1 H2. apply/H1.
  apply/collP. by apply/class_eq.
Qed.

Lemma minimal_idem A : minimal A -> collapsed A.
Proof.
  move => MA.
  have S: surjective (class A).
  - move => [x Hx]. exists x. apply/eqP. apply/val_inj.
    rewrite /=. by rewrite -(eqP Hx).
  have Bf: bijective (class A). apply: surj_card_bij => //.
  - apply/eqP. rewrite eqn_leq minimize_size andbT.
    exact: (MA (minimize A) (psym (minimize_correct _))).
  move => x y. split.
  - move/collP. move/class_eq.
    by move/(bij_inj Bf).
  - move => ->. apply/collP. exact: collb_refl.
Qed.

Lemma minimalP A : minimal A <-> (connected A /\ collapsed A).
Proof.
  split.
  - move => H. split. exact: minimal_connected. exact: minimal_idem.
  - move => [H1 H2] B L_AB. rewrite minimize_idem_size //.
    apply: minimize_minimal => // w. by rewrite minimize_correct.
Qed.

Lemma minimal_iso A B :
  dfa_lang A =i dfa_lang B -> minimal A -> minimal B -> dfa_iso A B.
Proof. move => L_AB MA MB.
  apply: coll_iso; auto using minimal_idem, minimal_connected.
Qed.

End FA.

Arguments delta [char] [A] x w.
Arguments dfa_run [char] [A] x w.