Library ATBR.DecideKleeneAlgebra

Require Import Common.
Require Import Classes.
Require Import Graph.
Require Import Converse.
Require Import DKA_Definitions.
Require DKA_CheckLabels.
Require DKA_Construction.
Require DKA_Epsilon.
Require DKA_Determinisation.
Require DKA_Merge.
Require DKA_DFA_Equiv.
Require StrictStarForm.
Require Reification.

Require Import List.

Definition word := list positive.
Inductive CounterExample: Set :=
| NotLeq: word -> CounterExample
| NotGeq: word -> CounterExample
| DifferentAtomSets: CounterExample.

Definition X_to_DFA (a: regex) :=
  let a' := StrictStarForm.ssf a in
  let A := DKA_Construction.X_to_eNFA a' in
  let A := DKA_Epsilon.eNFA_to_NFA A (DKA_Construction.well_founded (StrictStarForm.ssf_complete a)) in
  let A := DKA_Determinisation.NFA_to_DFA A in
      A.

Definition translate_ce (ce: option (bool*word)) :=
  match ce with
    | None => None
    | Some(b,w) => Some ((if b then NotLeq else NotGeq) (List.rev w))
  end.

Notation clean := RegExp.Clean.rewrite.

Definition decide_kleene a b :=
  let a := clean a in
  let b := clean b in
    if negb (DKA_CheckLabels.same_labels a b) then Some DifferentAtomSets
    else translate_ce (DKA_Merge.compare_DFAs DKA_DFA_Equiv.equiv (X_to_DFA a) (X_to_DFA b)).

Lemma X_to_DFA_correct: forall a, DFA.eval (X_to_DFA a) == a.

Lemma X_to_DFA_bounded: forall a, DFA.bounded (X_to_DFA a).

Lemma X_to_DFA_labels: forall a b,
  DKA_CheckLabels.same_labels (clean a) (clean b) = true ->
  DFA.max_label (X_to_DFA (clean a)) = DFA.max_label (X_to_DFA (clean b)).

Lemma translate_correct: forall ce, translate_ce ce = None <-> ce = None.

Theorem Kozen94: forall a b, decide_kleene a b = None <-> a == b.


Import RegExp.Untype.
Import Reification.

Corollary dk_erase_correct `{KA: KleeneAlgebra} {env: Env}:
  forall n m (a b: KA.X n m), decide_kleene (erase a) (erase b) = None -> KA.eval a == KA.eval b.

Ltac display_counter_example e ce :=
  let eval_word w :=
    let rec build w :=
      lazymatch w with
      | nil => fail 1
      | ?x::nil => constr:(Reification.unpack (@Reification.val _ e x))
      | ?x::?q => let q := build q in constr:(q * Reification.unpack (@Reification.val _ e x))
      end
    in
    let x := build w in
    let x := eval compute [e Reification.unpack Reification.tgt Reification.src
      Reification.sigma_get Reification.sigma_add Reification.sigma_empty
      FMapPositive.PositiveMap.find FMapPositive.PositiveMap.add
      FMapPositive.PositiveMap.empty Reification.val] in x
    in x
  in
  match ce with
    | DifferentAtomSets => fail 2 "Not a Kleene algebra theorem: different atom sets"
    | NotGeq ?w =>
      (try let u := eval_word w in
        fail 3 "Not a Kleene Algebra theorem: " u "does not belong to the left-hand side");
      fail 2 "Not a Kleene Algebra theorem: the empty word (1) does not belong to the left-hand side"
    | NotLeq ?w =>
      (try let u := eval_word w in
        fail 3 "Not a Kleene Algebra theorem: " u "does not belong to the right-hand side");
      fail 2 "Not a Kleene Algebra theorem: the empty word (1) does not belong to the right-hand side"
  end.

Ltac kleene_reflexivity :=
  let e := fresh "e" in
  unfold leq;
  kleene_reify; intros t e l r;
  apply dk_erase_correct; vm_compute;
  (reflexivity || lazymatch goal with |- Some ?w = None => display_counter_example e w end).

Ltac ckleene_reflexivity := converse_down; kleene_reflexivity.

Ltac kleene_ssf := StrictStarForm.kleene_ssf.
Ltac kleene_clean_zeros := Model_RegExp.kleene_clean_zeros.