Library ATBR.DKA_DFA_Equiv

Require Import Common.
Require Import Classes.
Require Import Graph.
Require Import Monoid.
Require Import SemiLattice.
Require Import SemiRing.
Require Import KleeneAlgebra.
Require Import MxGraph.
Require Import MxSemiLattice.
Require Import MxSemiRing.
Require Import MxKleeneAlgebra.

Require Import DKA_Definitions.
Require Import DKA_StateSetSets.
Require DKA_DFA_Language.

Require Import Utils_WF.
Require Import Relations.
Require Import List.

Import DSUtils.Notations.


Section e.
  Import Numbers.Positive.

  Variable A : DFA.t.
  Let f := DFA.finaux A.
  Let d := DFA.delta A.

  Let m := DFA.max_label A.
  Let final s := StateSet.mem s f.

  Fixpoint loop n (w: list label) tarjan (x y: state) :=
    match n with
      | Datatypes.S n =>
        let '(b,tarjan) := DS.test_and_unify tarjan x y in
        if b then inl tarjan else
        let fx := final x in
        let fy := final y in
        if eq_bool_bool fx fy
        then fold_num_sum (fun a tarjan => loop n (a::w) tarjan (d a x) (d a y)) m tarjan
        else inr (fx, rev w)
      
      | O => inl tarjan
    end.

End e.

Import DFA.

Definition equiv A x y :=
  match loop A (Datatypes.S (size A)) nil DS.empty x y with
    | inl _ => None
    | inr e => Some e
  end.

Lemma bounded_change_initial: forall A i, bounded A -> belong i A -> bounded (change_initial A i).

Section comb.

  Local Hint Resolve @DS.union_WF @DS.empty_WF: typeclass_instances.

  Inductive combine_no_length X Y : list X -> list Y -> Type :=
  |cnl_nil : combine_no_length nil nil
  |cnl_cons : forall lx ly x y, combine_no_length lx ly -> combine_no_length (x::lx) (y::ly).

  Program Definition build_combine X Y lx ly (H : List.length lx = List.length ly) : @combine_no_length X Y lx ly.

  Fixpoint complete (tarjan : DS.T) (l : list (state * state)) : DS.T :=
    match l with
      | nil => tarjan
      | (x,y)::l => complete (DS.union tarjan x y) l
    end.
  Notation "t +++ l" := (complete t l) (at level 60).

  Fixpoint comb_aux l r acc : list (state * state):= match l,r with |x::l,y::r => comb_aux l r ((x,y)::acc) | _,_ => acc end.
  Definition comb l r := comb_aux l r nil.

  Lemma add_incr : forall {tar} `{DS.WF tar} l, tar <T= (tar +++ l).

  Lemma le_proxy : forall t t' x y, {{t}} x y -> t <T= t' -> {{t'}} x y.

  Lemma complete_incr : forall {tar} `{DS.WF tar} l x y, {{tar}} x y -> {{tar +++ l}} x y.

  Lemma complete_incr_left : forall {tar} `{DS.WF tar} {tar'} `{DS.WF tar'} l,
    tar <T= tar' ->
    tar +++l <T= tar' +++ l.

  Lemma complete_compat_left : forall {tar} `{DS.WF tar} {tar'} `{DS.WF tar'} l,
    tar [=T=] tar' ->
    tar +++l [=T=] tar' +++ l.

  Instance complete_WF : forall {tar} `{DS.WF tar} l, DS.WF (tar +++ l).

End comb.
Notation "t +++ l" := (complete t l) (at level 60).

Section correctness.

  Variable A: DFA.t.
  Hypothesis Hbounds: bounded A.

  Notation delta := (delta A).
  Notation size := (size A).
  Notation ml := (max_label A).
  Notation final x := (StateSet.mem x (finaux A)).
  Notation kt := (list label -> DS.UF -> state -> state -> DS.UF + bool*list label)%type.
  Notation measure := (measure size).

  Definition diag (R S : relation state) :=
    forall a x y, below x size -> below y size -> a < ml ->
      R x y -> S (delta a x) (delta a y).

  Definition prog (t t' : DS.T) := forall R, diag {{t}} {{t +++ R}} -> diag {{t'}} {{t' +++ R}}.

  Local Hint Resolve @DS.union_WF @DS.empty_WF: typeclass_instances.

  Instance preorder_prog : PreOrder prog.

  Instance diag_compat: Proper (same_relation _ ==> same_relation _ ==> iff) diag.

  Class invariant tarjan : Prop :=
    {
      i_wf_tarjan :> DS.WF tarjan ;
      i_final : forall x y, {{tarjan}} x y -> final x = final y
    }.

  Record correct_ind tarjan tarjan' (x y : state) : Prop :=
    {
      ci_prog : prog tarjan tarjan';
      ci_le : tarjan <T= tarjan';
      ci_measure : measure tarjan' <= measure tarjan;
      ci_sameclass : {{tarjan'}} x y
    }.

  Fixpoint add_lists x y a l :=
    match a with O => l | Datatypes.S a => (delta a x, delta a y)::add_lists x y a l end.

  Record correct_fold_ind tarjan tarjan' x y ml :=
    {
      cfi_prog : forall l, diag {{tarjan}} {{tarjan +++ add_lists x y ml l}} -> diag {{tarjan'}} {{tarjan' +++ l}};
      cfi_le : tarjan <T= tarjan';
      cfi_measure : measure tarjan' <= measure tarjan
    }.

  Lemma diag_compat_left : forall {tar} `{DS.WF tar} {tar'} `{DS.WF tar'},
    tar [=T=] tar' ->
    forall l,
      diag {{tar}} {{tar +++ l}} ->
      diag {{tar' }} {{tar'+++l}}.

  Lemma correct_ind_idem : forall x y tarjan,
     {{tarjan}} x y ->
     invariant tarjan ->
     correct_ind tarjan ( DS.union tarjan x y ) x y.

  Lemma invariant_idem : forall tarjan x y,
    invariant tarjan ->
    {{tarjan}} x y ->
    invariant (DS.union tarjan x y).

  Lemma tarjan_equiv_true : forall {tarjan} `{DS.WF tarjan} x y u,
    DS.equiv tarjan x y = (true, u) -> {{tarjan}} x y.
  Hint Resolve tarjan_equiv_true.

  Lemma invariant_prog : forall tarjan x y,
    invariant tarjan ->
    final x = final y ->
    invariant (DS.union tarjan x y).

  Lemma in_union: forall {tar} `{DS.WF tar} x y, {{DS.union tar x y}} x y.

  Lemma add_lists_S: forall {tar} `{DS.WF tar} x y a l,
    {{tar}} (delta a x) (delta a y) -> tar+++add_lists x y (Datatypes.S a) l [=T=] tar+++add_lists x y a l.

  Lemma add_lists_sameclass: forall {tar} `{DS.WF tar} ml a x y l, a < ml ->
    {{tar +++ add_lists x y ml l}} (delta a x) (delta a y).

  Lemma diag_ok : forall {tarjan} `{DS.WF tarjan} x y l,
      below x size ->
      below y size ->
      diag {{tarjan}} {{tarjan +++ l}} ->
      diag {{DS.union tarjan x y}} {{DS.union tarjan x y +++ add_lists x y ml l}}.

  Import Numbers.Positive.
  Lemma loop_correct : forall n w t t' x y,
    measure t < n ->
    invariant t -> below x size -> below y size -> loop A n w t x y = inl t' ->
    correct_ind t t' x y /\ invariant t'.

  Section Correction.

    Variables i' j' : state.
    Hypothesis Hi' : below i' size.
    Hypothesis Hj' : below j' size.
    Variable tarjan : DS.T.
    Hypothesis _H : (loop A (Datatypes.S size) nil DS.empty i' j') = inl tarjan.

    Lemma invariant_empty : invariant DS.empty.

    Lemma tarjan_correct : correct_ind DS.empty tarjan i' j' /\ invariant tarjan.

    Instance tarjan_wf : DS.WF tarjan.

    Definition equivalent x y := (fst (DS.equiv tarjan x y)).

    Notation "A =&&= B" := (eq_state_bool A B) (at level 75).
    Notation "A =T= B" := (equivalent A B) (at level 75).

    Ltac xif_simpl :=
      repeat match goal with
               | |- context [xif true ?x ?y] => change (xif true x y) with x
               | |- context [xif false ?x ?y] => change (xif false x y) with y
             end.

    Ltac xif_destruct :=
      match goal with
        | |- context [xif ?b ?x ?y] => case_eq b; intros; xif_simpl
      end.

    Lemma T_true : forall a b, (a =T= b) = true <-> {{tarjan}} a b.

    Lemma T_finaux : forall x y, (x =T= y) = true -> StateSet.mem x (finaux A) = StateSet.mem y (finaux A).

    Lemma T_refl : forall x, (x =T= x) = true.
    Hint Rewrite T_refl : bool_simpl.

    Lemma zero_leq : forall x, 0 <= x.
    Lemma leq_zero_plus : forall a b, a < b -> a < 0 + b.
    Hint Resolve zero_leq leq_zero_plus: size.

    Ltac leq_sum n := apply leq_sum; exists n; split ; [ auto with size | split; [ auto with size |]].

    Lemma diag_empty : diag {{DS.empty}} {{DS.empty +++ nil}}.

    Lemma simulation: forall i j, (i =T= j) = true -> belong i A -> belong j A ->
      forall a, a < max_label A -> (delta a i =T= delta a j) = true.

    Lemma eval_change_initial : eval (change_initial A i') == eval (change_initial A j').
  End Correction.

  Theorem valid i j: belong i A -> belong j A -> equiv A i j = None ->
    eval (change_initial A i) == eval (change_initial A j).

End correctness.

Import DKA_DFA_Language.

Section completeness.

  Variable A: DFA.t.
  Hypothesis HA: bounded A.
  Variables i j: state.
  Hypothesis Hi: belong i A.
  Hypothesis Hj: belong j A.

  Definition select (b: bool) (i j: state) := if b then i else j.

  Lemma counter_exemple_loop: forall b w n v t,
    bounded_word A v ->
    loop A n v t (read A (rev v) i) (read A (rev v) j) = inr (b,w) ->
    DFA_language (change_initial A (select b i j)) w
    /\ ~ DFA_language (change_initial A (select b j i)) w.

  Lemma counter_exemple_equiv: forall b w,
    equiv A i j = Some (b,w) ->
    DFA_language (change_initial A (select b i j)) w
    /\ ~ DFA_language (change_initial A (select b j i)) w.

  Theorem completeness: equiv A i j <> None -> ~ eval (change_initial A i) == eval (change_initial A j).

End completeness.

Theorem correct: forall A i j, bounded A -> belong i A -> belong j A ->
  (equiv A i j = None <-> eval (change_initial A i) == eval (change_initial A j)).