Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype path fingraph tuple finfun finset div.
Require Import misc regexp automata dfa_to_re myhill_nerode homomorphism.

Lemma regular_det (char : finType) L (w : word char): regular L -> L w \/ ~ L w.
Proof. case => e ->. by case: (w \in e); [left|right]. Qed.

Lemma regular_xm (char : finType) P : regular (fun _ : word char => P) <-> P \/ ~ P.
Proof.
  split => H; first exact: regular_det [::] (H).
  case: (H) => HP; last by exists (Void).
  exists (Neg Void) => w. by rewrite Neg_correct.
Qed.

Section NonRegular.
  Variables (char : finType) (a b : char).
  Hypothesis (Hab : a != b).

  Implicit Types (L : word char -> Prop) (l : dlang char).

  Lemma regular_eq L1 L2 : (forall w, L1 w <-> L2 w) -> regular L1 -> regular L2.
  Proof. move => H [e He]. exists e => w. transitivity (L1 w) => //. by symmetry. Qed.

  Lemma regularE (L : word char -> Prop) : regular L ->
    exists L' : dlang char, (forall w, L w <-> w \in L') /\ inhabited (nerodePar L').
  Proof.
    case => e He. exists (re_lang e). split => //.
    pose N := dfa_to_nerode (minimize_minimal (@dfa_prune_connected _ (re_to_dfa e))).
    eexists. apply: nerode_eq (re_to_dfa_correct _).
    apply: nerode_eq (dfa_prune_correct _).
    exact: nerode_eq (minimize_correct _).
  Qed.

  Lemma nerodeIN (f : nat -> word char) (L : dlang char) :
    (forall n1 n2, (forall w, (f n1 ++ w \in L) = (f n2 ++ w \in L)) -> n1 = n2) ->
    ~ regular L.
  Proof.
    move => n_spec /regularE => [[l' [e]]] [N].
    have {e} e : L =i l'. move => w. by rewrite unfold_in; apply/idP/idP; firstorder.
    pose f' (n : 'I_#|N|.+1) := N (f n).
    suff: injective f' by move/card_leq_inj ; rewrite card_ord ltnn.
    move => [n1 H1] [n2 H2] /nerodeP => H.
    apply/eqP; change (n1 == n2); apply/eqP. apply: n_spec => w.
    by rewrite !e.
  Qed.

  Lemma count_nseq (T : eqType) (c d : T) n :
    count (pred1 c) (nseq n d) = (c == d) * n.
  Proof. elim: n => //= n. rewrite [d == c]eq_sym. by case e: (c == d) => /= ->. Qed.

  Lemma countL n1 n2 : count (pred1 a) (nseq n1 a ++ nseq n2 b) = n1.
  Proof. by rewrite count_cat !count_nseq (negbTE Hab) eqxx //= mul1n mul0n addn0. Qed.

  Lemma countR n1 n2 : count (pred1 b) (nseq n1 a ++ nseq n2 b) = n2.
  Proof. by rewrite count_cat !count_nseq eq_sym (negbTE Hab) eqxx //= mul1n mul0n. Qed.

  Definition Lab w := exists n, w = nseq n a ++ nseq n b.

  Lemma Lab_eq n1 n2 : Lab (nseq n1 a ++ nseq n2 b) -> n1 = n2.
  Proof.
    move => [n H].
    by rewrite -[n1](countL _ n2) -{2}[n2](countR n1 n2) H countL countR.
  Qed.

  Lemma Lab_not_regular : ~ regular Lab.
  Proof.
    move => R. case/regularE : (R) => l [lP [N]].
    pose f n := nseq n a.
    apply: (@nerodeIN f l) (regular_eq _ _ lP R) => n1 n2.
    move/(_ (nseq n2 b)). rewrite /f (_ : _ n2 _ ++ _ \in l).
    move/lP. exact: Lab_eq. apply/lP. by exists n2.
  Qed.

End NonRegular.