RIS.binding_finite: binding-finite and memory-finite expressions.

Set Implicit Arguments.

Require Import tools algebra language regexp alpha_regexp factors.

Section s.
  Context {atom : Set}{๐€ : Atom atom}.
  Context {X : Set} {๐— : Alphabet ๐€ X}.

Definitions


  Fixpoint bindings (e : regexp) a : list ๐–ก :=
    match e with
    | e_un โ‡’ [ฮต]
    | e_zero โ‡’ []
    | e_add e f โ‡’ bindings e a ++ bindings f a
    | e_prod e f โ‡’ lift_prod prod_binding (bindings e a) (bindings f a)
    | e_star e โ‡’ ฮต::(is_square :> bindings e a)
    | โŸชxโŸซ โ‡’ [๐—ณ a x]
    end.

  Definition is_binding_finite e := โˆƒ A, โˆ€ a u, โŸฆeโŸง u โ†’ ๐—™ a u โˆˆ A.

  Fixpoint binding_finite e :=
    match e with
    | e_un | e_zero | โŸช_โŸซ โ‡’ true
    | e_add e f โ‡’ binding_finite e && binding_finite f
    | e_prod e f โ‡’ test0 e || test0 f || (binding_finite e && binding_finite f)
    | e_star e โ‡’ binding_finite e && (forallb (fun a โ‡’ forallb is_square (bindings e a)) โŒŠeโŒ‹)
    end.

  Definition sqExpr e := is_binding_finite e โˆง โˆ€ a b, b โˆˆ bindings e a โ†’ square b.

  Definition weight u := sum (fun a โ‡’ size (๐—™ a u)) {{โŒŠuโŒ‹}}.

  Definition MaxBind L := fold_right (fun ฮฒ N โ‡’ max (size ฮฒ) N) 0 L.

  Definition weightExpr e := sum (fun a โ‡’ MaxBind (bindings e a)) {{โŒŠeโŒ‹}}.

  Definition bindFinList L := โˆ€ e, e โˆˆ L โ†’ is_binding_finite e.

  Definition sqListExpr L := โˆ€ e, e โˆˆ L โ†’ sqExpr e.

  Definition homogeneous e := โˆ€ a, โˆƒ ฮฒ, โˆ€ u, โŸฆeโŸง u โ†’ ๐—™ a u = ฮฒ.

  Fixpoint bindPref e a : list ๐–ก :=
    match e with
    | e_zero โ‡’ []
    | e_un โ‡’ [ฮต]
    | โŸชxโŸซ โ‡’ [ฮต;๐—ณ a x]
    | e_add e f โ‡’ (bindPref e a) ++ (bindPref f a)
    | e_prod e f โ‡’
      if test0 e || test0 f
      then []
      else (bindPref e a) ++ lift_prod prod_binding (bindings e a) (bindPref f a)
    | e_star e โ‡’ ฮต::(bindPref e a)++(lift_prod prod_binding (bindings e a) (bindPref e a))
    end.

Elementary facts


  Remark homogeneous_is_binding_finite e : homogeneous e โ†’ is_binding_finite e.

  Remark bindings_witness e a ฮฒ : ฮฒ โˆˆ bindings e a โ†’ โˆƒ u, โŸฆeโŸง u โˆง ๐—™ a u = ฮฒ.

  Remark unbounded_binding e a u :
    โŸฆ e โŸง u โ†’ c_binding (๐—™ a u) โ‰  d_binding (๐—™ a u) โ†’
    โˆ€ N, โˆƒ v, โŸฆ e โ‹†โŸง v โˆง N < size (๐—™ a v).

  Lemma bindings_ฮฃ L a : bindings (ฮฃ L) a โ‰ˆ flat_map (fun e โ‡’ bindings e a) L.

  Lemma bindings_fresh a e : a # e โ†’ bindings e a = [] โˆจ bindings e a โ‰ˆ [ฮต].

  Lemma test0_bindings e : test0 e = true โ†’ โˆ€ a, bindings e a = [].

  Lemma bindings_ฮต f a : โŸฆ f โŸง [] โ†’ ฮต โˆˆ bindings f a.

  Lemma binding_finite_false e :
    binding_finite e = false โ†’ ยฌ is_binding_finite e.

  Lemma binding_finite_true e :
    binding_finite e = true โ†’ โˆ€ a u, โŸฆeโŸง u โ†’ ๐—™ a u โˆˆ bindings e a.

  Lemma binding_finite_spec e : binding_finite e = true โ†” is_binding_finite e.

  Lemma is_binding_finite_bindings e :
    is_binding_finite e โ†’ โˆ€ a u, โŸฆeโŸง u โ†’ (๐—™ a u) โˆˆ bindings e a.

  Lemma sqExpr_bindings_finite_star e : sqExpr e โ†’ is_binding_finite (eโ‹†).

  Lemma bind_fin_ind e (P : regexp โ†’ Prop) :
    is_binding_finite e โ†’
    P ๐Ÿฌ โ†’
    P ๐Ÿญ โ†’
    (โˆ€ x, P โŸชxโŸซ) โ†’
    (โˆ€ e f, is_binding_finite e โ†’ is_binding_finite f โ†’ P e โ†’ P f โ†’ P (e โˆช f)) โ†’
    (โˆ€ e f, is_binding_finite e โ†’ is_binding_finite f โ†’ P e โ†’ P f โ†’ test0 e || test0 f = false โ†’
            P (e ยท f)) โ†’
    (โˆ€ e f, test0 e || test0 f = true โ†’ P (e ยท f)) โ†’
    (โˆ€ e, sqExpr e โ†’ P e โ†’ P (eโ‹†)) โ†’ P e.

  Ltac induction_bin_fin e B:=
    apply bind_fin_ind with (e:=e);
    [ apply B | | | | | | | ];
    clear B e;
    [ |
    |let x:= fresh "x" in intro x
    |let e1:= fresh "e1" in
     let e2:= fresh "e2" in
     let B1:= fresh "B1" in
     let B2:= fresh "B2" in
     let IH1:= fresh "IHe1" in
     let IH2:= fresh "IHe2" in
     intros e1 e2 B1 B2 IH1 IH2
    |let e1:= fresh "e1" in
     let e2:= fresh "e2" in
     let B1:= fresh "B1" in
     let B2:= fresh "B2" in
     let IH1:= fresh "IHe1" in
     let IH2:= fresh "IHe2" in
     let T:= fresh "T" in
     intros e1 e2 B1 B2 IH1 IH2 T
    |let e1:= fresh "e1" in
     let e2:= fresh "e2" in
     let T:= fresh "T" in
     intros e1 e2 T
    |let IH:= fresh "IHe" in
     let Sq:= fresh "Sq" in
     let e:= fresh "e" in
     intros e Sq IH].


  Lemma weight_incr_sup l u : weight u = sum (fun a โ‡’ size (๐—™ a u)) {{โŒŠuโŒ‹++l}}.


  Lemma weight_app u v : weight (u++v) โ‰ค weight u + weight v.
  Lemma weight_app_left v u : weight u โ‰ค weight (u++v) + weight v.
  Lemma weight_app_right u v : weight v โ‰ค weight (u++v) + weight u.


  Lemma bindFind_weight_weightExpr e :
    is_binding_finite e โ†’ โˆ€ u, โŸฆeโŸง u โ†’ weight u โ‰ค weightExpr e.

  Lemma MaxBind_app L M : MaxBind (L++M) = max (MaxBind L) (MaxBind M).


  Lemma MaxBind_fresh a e : a # e โ†’ MaxBind (bindings e a) = 0.

  Lemma weightExpr_incr_sup_left l e : weightExpr e = sum (fun a โ‡’ MaxBind (bindings e a)) {{l++โŒŠeโŒ‹}}.

  Lemma weightExpr_incr_sup_right l e : weightExpr e = sum (fun a โ‡’ MaxBind (bindings e a)) {{โŒŠeโŒ‹++l}}.

  Lemma MaxBind_filter f L : MaxBind (f :> L) โ‰ค MaxBind L.

  Lemma bounded_weightExpr e : weightExpr e โ‰ค sizeExpr e.


  Lemma bindPref_ฮต e a : test0 e = false โ†’ ฮต โˆˆ bindPref e a.
  Lemma test0_bindPref e a : test0 e = true โ†’ bindPref e a = [].

  Lemma bindPref_prefixes e a :
    is_binding_finite e โ†’ bindPref e a โ‰ˆ flat_map (fun f โ‡’ bindings f a) (prefixes e).

  Lemma bindPref_binding_finite e :
    is_binding_finite e โ†’ โˆ€ u v a, โŸฆeโŸง (u++v) โ†’ ๐—™ a u โˆˆ bindPref e a.

  Lemma bindings_finite_prefixes e : is_binding_finite e โ†’ โˆ€ f, f โˆˆ prefixes e โ†’ is_binding_finite f.

  Lemma bindings_prefixes_support e a : a # prefixes e โ†’ bindings e a โŠ† [ฮต].

  Lemma bindPref_prefixes_support e a : a # prefixes e โ†’ bindPref e a โŠ† [ฮต].

  Lemma bindPref_get_witness e a b : b โˆˆ bindPref e a โ†’ โˆƒ u v, โŸฆeโŸง (u++v) โˆง ๐—™ a u = b.

  Lemma MaxBind_cons a L : a โˆˆ L โ†’ MaxBind L = MaxBind (a::Lโˆ– a).

  Global Instance MaxBind_equiv : Proper (@equivalent _ ==> eq) MaxBind.

  Lemma MaxBind_lub n L :
    MaxBind L โ‰ค n โ†” โˆ€ ฮฒ, ฮฒ โˆˆ L โ†’ (size ฮฒ) โ‰ค n.

  Lemma MaxBind_le n L :
    n โ‰ค MaxBind L โ†” n = 0 โˆจ โˆƒ ฮฒ, ฮฒ โˆˆ L โˆง n โ‰ค (size ฮฒ).

  Lemma MaxBind_fresh_Pref e a : a # e โ†’ MaxBind (bindPref e a) = 0.

  Lemma bindings_bindPref e a : bindings e a โŠ† bindPref e a.


  Lemma MaxBind_sizeAt e a : MaxBind (bindings e a) โ‰ค sizeAt e a.

  Lemma MaxBind_In a L : a โˆˆ L โ†’ size a โ‰ค MaxBind L.

  Lemma MaxBind_lift_prod L M : MaxBind (lift_prod prod_binding L M) โ‰ค MaxBind L + MaxBind M.

  Lemma memory_bound_aux e a b :
    binding_finite e = true โ†’
    b โˆˆ bindPref e a โ†’
    size b โ‰ค 2 ร— sizeAt e a
    โˆง c_binding b - sizeAt e a โ‰ค d_binding b โ‰ค c_binding b + sizeAt e a.

  Lemma binding_finite_memory_bindPref e :
    is_binding_finite e โ†’ weightExpr (ฮฃ (prefixes e)) = sum (fun a โ‡’ MaxBind (bindPref e a)) {{โŒŠeโŒ‹}}.

  Lemma memory_bound e :
    is_binding_finite e โ†’ weightExpr (ฮฃ (prefixes e)) โ‰ค 2 ร— sizeExpr e.

  Proposition is_binding_finite_memory_finite e :
    is_binding_finite e โ†” โˆ€ a, โˆƒ N,โˆ€ u v, โŸฆeโŸง (u++v) โ†’ size (๐—™ a u) โ‰ค N.

  Corollary is_binding_finite_memory_bound e :
    is_binding_finite e โ†” โˆ€ u v, โŸฆeโŸง (u++v) โ†’ weight u โ‰ค 2ร—sizeExpr e.

  Lemma bindFinList_incl L M : bindFinList M โ†’ L โŠ† M โ†’ bindFinList L.

  Lemma bindFin_inf e f : is_binding_finite f โ†’ โŸฆeโŸง โ‰ฒ โŸฆfโŸง โ†’ is_binding_finite e.

Square expressions



  Lemma sqExpr_inf e f : sqExpr f โ†’ โŸฆeโŸง โ‰ฒ โŸฆfโŸง โ†’ sqExpr e.

  Lemma sqExpr_prod e f : sqExpr e โ†’ sqExpr f โ†’ sqExpr (eยทf).
  Lemma sqExpr_add e f : sqExpr e โ†’ sqExpr f โ†’ sqExpr (eโˆชf).

  Lemma binding_finite_sqExpr_star e : is_binding_finite (eโ‹†) โ†’ sqExpr (eโ‹†).

  Lemma sqExpr_star e : sqExpr e โ†’ sqExpr (eโ‹†).

  Lemma sqExpr_ฮ  L : sqListExpr L โ†’ sqExpr (ฮ  L).
  Lemma sqExpr_ฮฃ L : sqListExpr L โ†’ sqExpr (ฮฃ L).

  Lemma sqListExpr_ฮ _In L a : sqListExpr L โ†’ bindings (ฮ  L) a โŠ† ฮต::flat_map (fun e โ‡’ bindings e a) L.
        Opaque regProduct.

Homogeneous expressions


  Remark homogeneous_alt e :
    homogeneous e โ†” โˆ€ u v a, โŸฆeโŸง u โ†’ โŸฆeโŸง v โ†’ ๐—™ a u = ๐—™ a v.

  Lemma homogeneous_prod e f : homogeneous e โ†’ homogeneous f โ†’ homogeneous (eยทf).

  Fixpoint ๐‡ (e : @regexp letter) :=
    match e with
    | e_un โ‡’ [un]
    | e_zero โ‡’ []
    | โŸชxโŸซ โ‡’ [โŸชxโŸซ]
    | e_add e1 e2 โ‡’ ๐‡ e1 ++ ๐‡ e2
    | e_prod e1 e2 โ‡’ lift_prod prod (๐‡ e1) (๐‡ e2)
    | e_star e โ‡’
      flat_map
        (fun P โ‡’ map (fun l โ‡’ ฮ  (pad ((ฮฃ l) โ‹†) l)) (shuffles P))
        (subsets (๐‡ e))
    end.
  Lemma test0_๐‡ e : test0 e = true โ†’ ๐‡ e = [].

  Lemma ๐‡_eq e : e =KA ฮฃ (๐‡ e).

  Corollary ๐‡_lang e : โŸฆeโŸง โ‰ƒ โŸฆฮฃ (๐‡ e)โŸง.

  Transparent regProduct.
  Lemma homogeneous_๐‡ e f : is_binding_finite e โ†’ f โˆˆ ๐‡ e โ†’ homogeneous f.
  Lemma ฯต_๐‡ e f : e โˆˆ ๐‡ f โ†’ ฯต e = e_un โ†’ e =KA un.

  Opaque ๐‡.

Spines


  Fixpoint spines (e : @regexp letter) :=
    match e with
    | e_zero โ‡’ []
    | e_un โ‡’ [(e_un,e_un)]
    | โŸชxโŸซ โ‡’ [(โŸชxโŸซ,e_un);(e_un,โŸชxโŸซ)]
    | e_add e1 e2 โ‡’ spines e1 ++ spines e2
    | e_prod e1 e2 โ‡’
      flat_map (fun s โ‡’ map (fun f โ‡’ (fst s,snd sยทf))(๐‡ e2)) (spines e1)
               ++ flat_map (fun s โ‡’ map (fun f โ‡’ (f ยท fst s,snd s))(๐‡ e1)) (spines e2)
    | e_star e โ‡’
      flat_map (fun s โ‡’ flat_map (fun e1 โ‡’ map (fun e2 โ‡’ (e1ยทfst s,snd sยทe2))
                                           (๐‡ (eโ‹†)))
                               (๐‡ (eโ‹†)))
               ((e_un,e_un)::(spines e))
    end.

  Transparent ๐‡.
  Lemma test0_spines e : test0 e = true โ†’ spines e = [].
  Opaque ๐‡.

  Lemma spines_eq e : e =KA ฮฃ (map (fun s โ‡’ fst s ยท snd s) (spines e)).


  Lemma spines_split e u v : โŸฆeโŸง (u++v) โ†’ โˆƒ e1 e2, (e1,e2) โˆˆ spines e โˆง โŸฆe1โŸง u โˆง โŸฆe2โŸง v.

  Lemma spines_homogeneous e e1 e2 :
    is_binding_finite e โ†’ (e1,e2) โˆˆ spines e โ†’ homogeneous e1 โˆง homogeneous e2.

  Lemma ฯต_spines e1 e2 f : (e1,e2) โˆˆ spines f โ†’ (ฯต e1 = e_un โ†’ e1 =KA un) โˆง (ฯต e2 = e_un โ†’ e2 =KA un).

  Lemma binding_finite_ฮฃ L :
    binding_finite (ฮฃ L) = forallb binding_finite L.

  Lemma is_binding_finite_ฮฃ L : (โˆ€ e , e โˆˆ L โ†’ is_binding_finite e) โ†’ is_binding_finite (ฮฃ L).

  Lemma bindings_act a p e : bindings (p โˆ™ e) a = bindings e (pโˆ—โˆ™a).

  Lemma is_binding_finite_act p e : is_binding_finite (pโˆ™e) โ†” is_binding_finite e.

End s.

Ltac induction_bin_fin e B:=
  apply (@bind_fin_ind _ _ _ _ e);
  [ apply B | | | | | | | ];
  clear B e;
  [ |
    |let x:= fresh "x" in intro x
    |let e1:= fresh "e1" in
     let e2:= fresh "e2" in
     let B1:= fresh "B1" in
     let B2:= fresh "B2" in
     let IH1:= fresh "IHe1" in
     let IH2:= fresh "IHe2" in
     intros e1 e2 B1 B2 IH1 IH2
    |let e1:= fresh "e1" in
     let e2:= fresh "e2" in
     let B1:= fresh "B1" in
     let B2:= fresh "B2" in
     let IH1:= fresh "IHe1" in
     let IH2:= fresh "IHe2" in
     let T:= fresh "T" in
     intros e1 e2 B1 B2 IH1 IH2 T
    |let e1:= fresh "e1" in
     let e2:= fresh "e2" in
     let T:= fresh "T" in
     intros e1 e2 T
    |let IH:= fresh "IHe" in
     let Sq:= fresh "Sq" in
     let e:= fresh "e" in
     intros e Sq IH].