RIS.completenessKA: Link with relation-algebra to import the completeness proof of Kleene algebra.

Require Import tools algebra language regexp.
Require Import RelationAlgebra.syntax RelationAlgebra.kleene RelationAlgebra.boolean RelationAlgebra.lang RelationAlgebra.lset RelationAlgebra.sums RelationAlgebra.normalisation.
Require Import RelationAlgebra.regex RelationAlgebra.ka_completeness RelationAlgebra.kat_tac.

Set Implicit Arguments.

Section proof.

  Global Instance dec_sigma : decidable_set sigma :=
    Build_decidable_set (fun x y ⇒ Bool.iff_reflect _ _ (iff_Symmetric _ _ (BinPos.Pos.eqb_eq x y))).

  Notation E := (@regexp regex.sigma).

  Fixpoint regexp_to_regex' (e : E) : regex :=
    match e with
    | e_un ⇒ r_one
    | e_zero ⇒ r_zer
    | e_add e f ⇒ r_pls (regexp_to_regex' e) (regexp_to_regex' f)
    | e_prod e f ⇒ r_dot (regexp_to_regex' e) (regexp_to_regex' f)
    | e_star e ⇒ r_str (regexp_to_regex' e)
    | ⟪a⟫ ⇒ r_var a
    end.

  Fixpoint regexp_to_expr (e : E) : expr_(BKA) (fun _ ⇒ xH) (fun _ ⇒ xH) xH xH :=
    match e with
    | e_un ⇒ (syntax.e_one BinNums.xH)
    | e_zero ⇒ (syntax.e_zer BinNums.xH BinNums.xH)
    | e_add e f ⇒ syntax.e_pls (regexp_to_expr e) (regexp_to_expr f)
    | e_prod e f ⇒ syntax.e_dot (regexp_to_expr e) (regexp_to_expr f)
    | e_star e ⇒ syntax.e_str (regexp_to_expr e)
    | ⟪a⟫ ⇒ syntax.e_var a
    end.
  Fixpoint regex'_to_regexp (e : regex) : E :=
    match e with
    | r_one ⇒ e_un
    | r_zer ⇒ e_zero
    | r_pls e f ⇒ e_add (regex'_to_regexp e) (regex'_to_regexp f)
    | r_dot e f ⇒ e_prod (regex'_to_regexp e) (regex'_to_regexp f)
    | r_str e ⇒ e_star (regex'_to_regexp e)
    | r_var a ⇒ ⟪a⟫
    end.

  Lemma regex'_to_regexp_id e : regex'_to_regexp (regexp_to_regex' e) = e.

  Lemma regexp_to_regex'_id e : regexp_to_regex' (regex'_to_regexp e) = e.

  Lemma to_expr_id e : to_expr e = regexp_to_expr (regex'_to_regexp e).

  Lemma equiv_id (l m : lang' sigma) : l ≃ m ↔ l == m.

  Lemma regex'_to_regexp_lang e : ⟦regex'_to_regexp e⟧ ≃ lang e.
  Lemma regexp_to_regex'_lang e : ⟦e⟧ ≃ lang (regexp_to_regex' e).

  Canonical Structure regexp_lattice_ops : lattice.ops :=
    lattice.mk_ops E (ax_inf regexp.KA KA') (ax_eq regexp.KA KA')
                   join join star zero zero.

  CoInductive regexp_unit := regexp_tt.

  Definition lat_ops := (fun _ _ : regexp_unit ⇒ regexp_lattice_ops).
  Definition mon_prod := (fun _ _ _ : regexp_unit ⇒ fun e f : E ⇒ e · f).
  Definition mon_un := (fun _ : regexp_unit ⇒ un : E).
  Definition mon_star := (fun _ : regexp_unit ⇒ star : E → E).
  Definition mon_itr := (fun _ : regexp_unit ⇒ fun e : E ⇒ e · e⋆).
  Definition mon_neg := (fun _ _ : regexp_unit ⇒ fun e : E ⇒ e).

  Hint Unfold lat_ops mon_prod mon_un mon_star mon_itr.

  Canonical Structure regexp_ops :=
    monoid.mk_ops regexp_unit
                  lat_ops
                  mon_prod
                  mon_un
                  mon_itr
                  mon_star
                  mon_neg
                  mon_prod
                  mon_prod.


  Lemma KA_regexp_to_expr e f :
    e =KA f → regexp_to_expr e == regexp_to_expr f.

  Instance regexp_laws: monoid.laws level.BKA regexp_ops.

  Definition inject : expr_(BKA) (fun _ ⇒ xH) (fun _ ⇒ xH) xH xH → E :=
    @eval _ (fun _ ⇒ xH) (fun _ ⇒ xH) regexp_ops (fun _ ⇒ regexp_tt)
     (fun x ⇒ ⟪x⟫) _ _.

  Lemma inject_regexp_to_expr e : inject (regexp_to_expr e) = e.

  Lemma CompletenessKA_sigma (e f : E) : ⟦e⟧ ≃ ⟦f⟧ → e =KA f.

  Context {X : Set} {decX : decidable_set X}.

  Lemma to_nat : ∀ Σ : list X, ∃ f : X → nat, ∃ g, ∀ x, x ∈ Σ → Some x = g (f x).

  Lemma to_sigma : ∀ Σ : list X, ∃ f : X → sigma, ∃ g, ∀ x, x ∈ Σ → Some x = g (f x).


  Lemma no_var_no_fun : (∀ e : @regexp X, Var e = [] → e =KA 𝟭 ∨ e =KA 𝟬).

  Fixpoint map_expr {A B : Set} (σ : A → B) (e : @regexp A) :=
    match e with
    | e_zero ⇒ 𝟬
    | e_un ⇒ 𝟭
    | ⟪a⟫ ⇒ ⟪σ a⟫
    | e_add e f ⇒ map_expr σ e ∪ map_expr σ f
    | e_prod e f ⇒ map_expr σ e · map_expr σ f
    | e_star e ⇒ map_expr σ e ⋆
    end.

  Lemma map_expr_ax_eq {A B : Set} (σ : A → B) e f :
    e =KA f → map_expr σ e =KA map_expr σ f.

  Lemma get_terms :
    ∀ e f : @regexp X, ∃ e' f' : E, (e' =KA f' → e =KA f) ∧ (⟦e⟧ ≃ ⟦f⟧ → ⟦e'⟧ ≃ ⟦f'⟧).

  Theorem CompletenessKA (e f : @regexp X) : e =KA f ↔ ⟦e⟧ ≃ ⟦f⟧.
End proof.