Library ATBR.DKA_Epsilon

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 Utils_WF.
Require Import Relations.
Require Import Eqdep_dec.


Section fold'.
  Variable A: Type.
  Definition stateset_fold p (f: forall i, A -> StateSet.mem i p = true -> A) a :=
    StateSet.fold
      (fun i a =>
        match StateSet.mem i p as x return StateSet.mem i p = x -> A with
          | true => fun H => f i a H
          | false => fun _ => a
        end refl_equal) p a.
  Implicit Arguments stateset_fold [].

  Lemma bool_dec' : forall a b: bool, a=b \/ a<>b.

  Lemma stateset_fold_rec_bis:
    forall (P : stateset -> A -> Type) p (f : forall i, A -> StateSet.mem i p = true -> A) i,
      (forall u v a, StateSet.Equal u v -> P u a -> P v a) ->
      P StateSet.empty i ->
      (forall x a q (H: StateSet.mem x p = true),
        ~StateSet.In x q -> P q a -> P (StateSet.add x q) (f x a H)) ->
      P p (stateset_fold p f i).
End fold'.
Implicit Arguments stateset_fold [A].

Section map_transitive_closure.

  Variable f: state -> stateset.
  Let R: relation state := fun i j => StateSet.mem i (f j) = true.

  Definition terminates := Init.Wf.well_founded R.
  Hypothesis Hwf: terminates.

  Definition rt_closure_aux: state -> statemap stateset -> statemap stateset * stateset :=
    Fix Hwf (fun _ => statemap stateset -> statemap stateset * stateset)
      (fun i rt_closure_aux acc =>
        match StateMap.find i acc with
          | Some pi => (acc,pi)
          | None =>
            let (acc,pi) :=
              stateset_fold (f i) (fun j accp Hj =>
                let '(acc,p) := accp in
                  let (acc,pj) := rt_closure_aux j Hj acc in
                    (acc,StateSet.union pj p)
              ) (acc,StateSet.singleton i) in
              (StateMap.add i pi acc, pi)
        end).

  Definition rt_closure_aux' i acc := fst (rt_closure_aux i acc).

  Definition rt_closure size: state -> stateset :=
    statemap_set_to_fun (fold_states rt_closure_aux' size (StateMap.empty _)).

End map_transitive_closure.

Definition set_closure (c: state -> stateset) (p: stateset): stateset :=
  StateSet.fold (fun i => StateSet.union (c i)) p StateSet.empty.

Definition statelabelmap_set_to_fun d := fun a i => optionset_to_set (StateLabelMap.find (i,a) d).

Definition eNFA_to_NFA A (Hwf: eNFA.well_founded A) :=
  let (size,_,delta,initial,final,max_label) := A in
  let eps := rt_closure (guard 100 Hwf) size in
    NFA.mk size
    (statelabelmap_set_to_fun (StateLabelMap.map (set_closure eps) delta))
    (eps initial)
    (StateSet.singleton final)
    max_label.
Implicit Arguments eNFA_to_NFA [].

Definition step f: relation state := fun i j => StateSet.mem j (f i) = true.
Definition steps f: relation state := clos_refl_trans_1n _ (step f).

Definition valid f i p := forall j, StateSet.In j p <-> steps f i j.
Definition approx f acc := forall i p, StateMap.MapsTo i p acc -> valid f i p.

Lemma add_valid: forall acc f i p B, valid f i p /\ approx f acc /\ B ->
  StateMap.MapsTo i p (StateMap.add i p acc) /\ approx f (StateMap.add i p acc) /\ B.

Ltac destruct_fold_pair H :=
  match type of H with
    context [stateset_fold ?x ?f ?acc] =>
    case_eq (stateset_fold x f acc);
    let acc' := fresh "acc" in
    let p' := fresh "p" in
    let H' := fresh "H" in
      intros acc' p' H';
      rewrite H' in H; simpl in H;
      injection H; intros; subst; clear H
  end.

Import Common.
Lemma rt_closure_aux_spec: forall f (Hwf: terminates f) i acc acc' p,
  approx f acc -> rt_closure_aux Hwf i acc = (acc',p) ->
  StateMap.MapsTo i p acc' /\ approx f acc' /\ (forall j, StateMap.In j acc -> StateMap.In j acc').

Lemma rt_closure_aux'_spec: forall f Hwf n acc,
  approx f acc ->
  approx f (@rt_closure_aux' f Hwf n acc)
  /\ forall i, StateMap.In i acc \/ i=n -> StateMap.In i (@rt_closure_aux' f Hwf n acc).

Lemma rt_closure_prespec: forall f Hwf size acc,
  approx f acc ->
  approx f (fold_states (@rt_closure_aux' f Hwf) size acc)
  /\ forall i, below i size \/ StateMap.In i acc ->
    StateMap.In i (fold_states (rt_closure_aux' Hwf) size acc).

Theorem rt_closure_spec: forall f Hwf size i, below i size ->
  forall j, steps f i j <-> StateSet.In j (@rt_closure f Hwf size i).

Section algebraic_lemmas.

  Context `{KA: KleeneAlgebra}.

  Lemma algebraic_correctness: forall A B C (j' j n m': X B B) (u u': X A B) (v v': X B C),
    j'==j# -> m'==n*j' -> u'==u*j' -> v'==v -> u*(j+n)#*v == u'*m'#*v'.

  Lemma algebraic_rt_closure: forall A (j' j : X A A), 1 <== j' -> j' * j' <== j' -> j<==j' -> j# <== j'.

  Lemma xif_bool_incr: forall A B b c (x : X A B), (b=true -> c=true) -> xif b x 0 <== xif c x 0.

End algebraic_lemmas.

Notation ns := nat_of_state.
Notation sn := state_of_nat.

Lemma rt_closure_star: forall f Hwf size, (forall i, below i size -> setbelow (f i) size) ->
  (mx_bool tt (ns size) (ns size) (fun i j => StateSet.mem (sn j) (f (sn i)))) #
  ==
  (mx_bool tt (ns size) (ns size) (fun i j => StateSet.mem (sn j) (@rt_closure f Hwf size (sn i)))).

Local Opaque star dot plus zero one equal leq guard .

Lemma mem_set_closure: forall f i p,
  StateSet.mem i (set_closure f p) = StateSet.exists_ (fun j => StateSet.mem i (f j)) p.

Lemma delta_bounded: forall A, eNFA.bounded A ->
  forall i a n x, StateLabelMap.MapsTo (i, a) x (eNFA.deltamap A) -> StateSet.In n x -> below n (eNFA.size A).

Theorem correct: forall A HA, eNFA.bounded A -> NFA.eval (eNFA_to_NFA A HA) == eNFA.eval A.
  Local Transparent dot plus zero one equal.



Qed.

Lemma rt_closure_bounded: forall f Hwf size,
  (forall i, below i size -> setbelow (f i) size) ->
   forall i, below i size -> setbelow (@rt_closure f Hwf size i) size.

Lemma bounded: forall A HA, eNFA.bounded A -> NFA.bounded (eNFA_to_NFA A HA).

Lemma preserve_max_label: forall A HA, NFA.max_label (@eNFA_to_NFA A HA) = eNFA.max_label A.