Library ATBR.DKA_Merge

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.


Import DFA.

Definition merge_DFAs A B :=
  let s := max (pi0 (size A)) (pi1 (size B)) in
  let k := max_label A in
  let delta := (fun a p =>
    match pimatch p with
      | inl p => pi0 (DFA.delta A a p)
      | inr p => pi1 (DFA.delta B a p)
    end)
  in
  let finaux :=
    StateSet.fold (fun x acc => StateSet.add (pi0 x) acc) (finaux A)
      (StateSet.fold (fun x acc => StateSet.add (pi1 x) acc) (finaux B) StateSet.empty)
  in
    DFA.mk s delta 0 finaux k.

Definition compare_DFAs T (equiv: DFA.t -> state -> state -> option T) A B :=
  equiv (merge_DFAs A B) (pi0 (initial A)) (pi1 (initial B)).

Lemma below_max_pi0: forall n m m', below n m -> below (pi0 n) (max (pi0 m) (pi1 m')).

Lemma below_max_pi1: forall n m m', below n m' -> below (pi1 n) (max (pi0 m) (pi1 m')).


Lemma merge_bounded: forall A B, bounded A -> bounded B -> bounded (merge_DFAs A B).

Lemma sum_collapse': forall k f b (j: state), (j<k)%nat ->
  sum 0 k (fun i => xif (eqb (state_of_nat i) j && b i) (f i) (0: regex)) == xif (b j) (f j) 0.

Lemma and_neutral_left: forall (A B: Prop), A -> (A/\B <-> B).

Lemma compare_compat: SetoidList.compat_op eq NumSet.Equal (fun x acc => NumSet.add (pi0 x) acc).

Local Opaque dot star plus one zero eq_state_bool leq NumSet.add.
Lemma eval_left: forall (A B: DFA.t), bounded A ->
  eval (change_initial (merge_DFAs A B) (pi0 (initial A))) == eval A.
Transparent dot. Opaque dot.
Transparent dot. Opaque dot.
Transparent dot. Opaque dot.

Lemma eval_right: forall (A B: DFA.t), bounded B -> max_label A = max_label B ->
  eval (change_initial (merge_DFAs A B) (pi1 (initial B))) == eval B.
Transparent dot. Opaque dot.
Transparent dot. Opaque dot.
Transparent dot. Opaque dot.

Section S.

  Variable T: Type.
  Variable equiv: t -> state -> state -> option T.
  Hypothesis equiv_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)).

  Theorem correct: forall A B,
    bounded A -> bounded B -> max_label A = max_label B -> (compare_DFAs equiv A B = None <-> eval A == eval B).

End S.