RIS.alphaKA: axiomatisation of regular languages up-to α-equivalence.
Set Implicit Arguments.
Require Import tools algebra language regexp aeq_facts alpha_regexp closed_languages binding_finite.
Require Import positive_regexp.
Section s.
Context {atom : Set}{𝐀 : Atom atom}.
Context {X : Set} {𝐗 : Alphabet 𝐀 X}.
Inductive αKA : relation regexp :=
| αKA_αα a b e : (∀ u, ⟦e⟧ u → a #α u ∧ b #α u) → αKA e ([(a,b)]∙e)
| αKA_KA e f : KA e f → αKA e f.
Hint Constructors αKA.
Lemma KA_αKA e f : {|KA,KA'|} ⊢ e == f → {|αKA,KA'|} ⊢ e == f.
Global Instance goodαKA : GoodEnoughAxiom αKA.
Global Instance verygoodαKA : VeryGoodAxioms αKA.
Lemma KA_αKA_inf e f : {|KA,KA'|} ⊢ e =<= f → {|αKA,KA'|} ⊢ e =<= f.
Lemma αKA_lang e f : {|αKA,KA'|} ⊢ e == f → cl_α⟦e⟧≃cl_α⟦f⟧.
Opaque prodLang.
Opaque joinLang.
Opaque starLang.
Definition OpenVar e := flat_map (fun l ⇒ match l with open a ⇒ [a] | _ ⇒ [] end) (Var e).
Definition balExpr a e := bindings e a ⊆ [ε;(0,true,0)].
Definition freshExpr a e := bindings e a ⊆ [ε].
Lemma balExpr_bindFin a e : is_binding_finite e → balExpr a e ↔ (∀ u, ⟦e⟧ u → a ⋄ u).
Lemma freshExpr_bindFin a e : is_binding_finite e → freshExpr a e ↔ (∀ u, ⟦e⟧ u → a #α u).
Definition balExprB a e := inclb (bindings e a) [ε;(0,true,0)].
Definition freshExprB a e := inclb (bindings e a) [ε].
Lemma balExprB_balExpr a e : balExprB a e = true ↔ balExpr a e.
Lemma freshExprB_freshExpr a e : freshExprB a e = true ↔ freshExpr a e.
Notation Regexp := (@regexp letter).
Lemma δ_inf_e_α e l : {|αKA, KA'|}⊢ ⟪ l ⟫ · δ l e =<= e.
Lemma Σ_bounded_α e L:
(∀ f, f ∈ L → {|αKA, KA'|}⊢ f =<= e) ↔ {|αKA, KA'|}⊢ Σ L =<= e.
Lemma δ_binFin a e : is_binding_finite e → is_binding_finite (δ a e).
Lemma δ_support e l : ⌊δ l e⌋ ⊆ ⌊ e ⌋.
Lemma 𝐇_support e f : f ∈ 𝐇 e → ⌊f⌋ ⊆ ⌊e⌋.
Transparent 𝐇.
Opaque 𝐇.
Lemma spines_support e e1 e2 : (e1,e2)∈ spines e → ⌊e1⌋++⌊e2⌋ ⊆ ⌊e⌋.
Lemma act_prod p e1 e2 : p ∙ (e1 · e2) = p∙ e1 · p ∙e2.
Lemma act_join p e1 e2 : p ∙ (e1 ∪ e2) = p∙ e1 ∪ p ∙e2.
Lemma act_star p e : p ∙ (e⋆) = (p∙ e)⋆.
Lemma In_OpenVar a u e : open a ∈ u → ⟦e⟧ u → a ∈ OpenVar e.
Transparent joinLang.
Remark cl_α_Σ L u : (cl_α ⟦Σ L⟧) u ↔ ∃ e, e ∈ L ∧ (cl_α ⟦e⟧) u.
Opaque joinLang.
Lemma balanced_alt a u : a ⋄ u ↔ 𝗙 a u ∈ [ε;(0,true,0)].
Lemma αfresh_alt a u : a #α u ↔ 𝗙 a u ∈ [ε].
Lemma perm_comm_pair a b (u:list letter) : [(a,b)] ∙ u = [(b,a)] ∙ u.
Lemma αKA_lang_inf e f : {|αKA,KA'|} ⊢ e =<= f → cl_α⟦e⟧ ≲ cl_α ⟦f⟧.
Global Instance αKA_KleeneAlgebra : KleeneAlgebra Regexp (ax_eq αKA KA') (ax_inf αKA KA').
Lemma Σ_map_equiv_α {A} f g (L : list A) :
(∀ e, e ∈ L → {|αKA, KA'|}⊢ f e == g e) →
{|αKA, KA'|} ⊢ Σ (map f L) == Σ (map g L).
Lemma δ_proper_αKA_not_open l :
(∀ a, l ≠ open a) →
Proper ((ax_eq αKA KA') ==> (ax_eq αKA KA')) (δ l).
Lemma δ_proper_αKA_not_open_inf l :
(∀ a, l ≠ open a) →
Proper ((ax_inf αKA KA') ==> (ax_inf αKA KA')) (δ l).
Lemma positive_αKA e f : {|αKA,KA'|} ⊢ e == f → {|αKA,KA'|} ⊢ positive e == positive f.
Lemma positive_αKA_inf e f : {|αKA,KA'|} ⊢ e =<= f → {|αKA,KA'|} ⊢ positive e =<= positive f.
Infix " =α " := (ax_eq αKA KA') (at level 80).
Infix " <=α " := (ax_inf αKA KA') (at level 80).
Lemma αKA_act p e f : e =α f → p ∙ e =α p ∙ f.
Lemma test0_αKA e f : e =α f → test0 e = test0 f.
Lemma ϵ_αKA e f : e =α f → ϵ e = ϵ f.
Lemma Σ_map_app {A} (f g : A → Regexp) L :
Σ (map f L) ∪ Σ (map g L) =α Σ (map (fun x ⇒ f x ∪ g x) L).
Lemma is_binding_finite_ax_eq e f :
e =α f → is_binding_finite e ↔ is_binding_finite f.
Lemma is_binding_finite_ax_inf e f : is_binding_finite f → e ≤α f → is_binding_finite e.
Lemma αKA_inf_act p e f : e ≤α f → p∙e ≤α p∙f.
End s.
Infix " =α " := (ax_eq αKA KA') (at level 80).
Infix " <=α " := (ax_inf αKA KA') (at level 80).
Require Import tools algebra language regexp aeq_facts alpha_regexp closed_languages binding_finite.
Require Import positive_regexp.
Section s.
Context {atom : Set}{𝐀 : Atom atom}.
Context {X : Set} {𝐗 : Alphabet 𝐀 X}.
Inductive αKA : relation regexp :=
| αKA_αα a b e : (∀ u, ⟦e⟧ u → a #α u ∧ b #α u) → αKA e ([(a,b)]∙e)
| αKA_KA e f : KA e f → αKA e f.
Hint Constructors αKA.
Lemma KA_αKA e f : {|KA,KA'|} ⊢ e == f → {|αKA,KA'|} ⊢ e == f.
Global Instance goodαKA : GoodEnoughAxiom αKA.
Global Instance verygoodαKA : VeryGoodAxioms αKA.
Lemma KA_αKA_inf e f : {|KA,KA'|} ⊢ e =<= f → {|αKA,KA'|} ⊢ e =<= f.
Lemma αKA_lang e f : {|αKA,KA'|} ⊢ e == f → cl_α⟦e⟧≃cl_α⟦f⟧.
Opaque prodLang.
Opaque joinLang.
Opaque starLang.
Definition OpenVar e := flat_map (fun l ⇒ match l with open a ⇒ [a] | _ ⇒ [] end) (Var e).
Definition balExpr a e := bindings e a ⊆ [ε;(0,true,0)].
Definition freshExpr a e := bindings e a ⊆ [ε].
Lemma balExpr_bindFin a e : is_binding_finite e → balExpr a e ↔ (∀ u, ⟦e⟧ u → a ⋄ u).
Lemma freshExpr_bindFin a e : is_binding_finite e → freshExpr a e ↔ (∀ u, ⟦e⟧ u → a #α u).
Definition balExprB a e := inclb (bindings e a) [ε;(0,true,0)].
Definition freshExprB a e := inclb (bindings e a) [ε].
Lemma balExprB_balExpr a e : balExprB a e = true ↔ balExpr a e.
Lemma freshExprB_freshExpr a e : freshExprB a e = true ↔ freshExpr a e.
Notation Regexp := (@regexp letter).
Lemma δ_inf_e_α e l : {|αKA, KA'|}⊢ ⟪ l ⟫ · δ l e =<= e.
Lemma Σ_bounded_α e L:
(∀ f, f ∈ L → {|αKA, KA'|}⊢ f =<= e) ↔ {|αKA, KA'|}⊢ Σ L =<= e.
Lemma δ_binFin a e : is_binding_finite e → is_binding_finite (δ a e).
Lemma δ_support e l : ⌊δ l e⌋ ⊆ ⌊ e ⌋.
Lemma 𝐇_support e f : f ∈ 𝐇 e → ⌊f⌋ ⊆ ⌊e⌋.
Transparent 𝐇.
Opaque 𝐇.
Lemma spines_support e e1 e2 : (e1,e2)∈ spines e → ⌊e1⌋++⌊e2⌋ ⊆ ⌊e⌋.
Lemma act_prod p e1 e2 : p ∙ (e1 · e2) = p∙ e1 · p ∙e2.
Lemma act_join p e1 e2 : p ∙ (e1 ∪ e2) = p∙ e1 ∪ p ∙e2.
Lemma act_star p e : p ∙ (e⋆) = (p∙ e)⋆.
Lemma In_OpenVar a u e : open a ∈ u → ⟦e⟧ u → a ∈ OpenVar e.
Transparent joinLang.
Remark cl_α_Σ L u : (cl_α ⟦Σ L⟧) u ↔ ∃ e, e ∈ L ∧ (cl_α ⟦e⟧) u.
Opaque joinLang.
Lemma balanced_alt a u : a ⋄ u ↔ 𝗙 a u ∈ [ε;(0,true,0)].
Lemma αfresh_alt a u : a #α u ↔ 𝗙 a u ∈ [ε].
Lemma perm_comm_pair a b (u:list letter) : [(a,b)] ∙ u = [(b,a)] ∙ u.
Lemma αKA_lang_inf e f : {|αKA,KA'|} ⊢ e =<= f → cl_α⟦e⟧ ≲ cl_α ⟦f⟧.
Global Instance αKA_KleeneAlgebra : KleeneAlgebra Regexp (ax_eq αKA KA') (ax_inf αKA KA').
Lemma Σ_map_equiv_α {A} f g (L : list A) :
(∀ e, e ∈ L → {|αKA, KA'|}⊢ f e == g e) →
{|αKA, KA'|} ⊢ Σ (map f L) == Σ (map g L).
Lemma δ_proper_αKA_not_open l :
(∀ a, l ≠ open a) →
Proper ((ax_eq αKA KA') ==> (ax_eq αKA KA')) (δ l).
Lemma δ_proper_αKA_not_open_inf l :
(∀ a, l ≠ open a) →
Proper ((ax_inf αKA KA') ==> (ax_inf αKA KA')) (δ l).
Lemma positive_αKA e f : {|αKA,KA'|} ⊢ e == f → {|αKA,KA'|} ⊢ positive e == positive f.
Lemma positive_αKA_inf e f : {|αKA,KA'|} ⊢ e =<= f → {|αKA,KA'|} ⊢ positive e =<= positive f.
Infix " =α " := (ax_eq αKA KA') (at level 80).
Infix " <=α " := (ax_inf αKA KA') (at level 80).
Lemma αKA_act p e f : e =α f → p ∙ e =α p ∙ f.
Lemma test0_αKA e f : e =α f → test0 e = test0 f.
Lemma ϵ_αKA e f : e =α f → ϵ e = ϵ f.
Lemma Σ_map_app {A} (f g : A → Regexp) L :
Σ (map f L) ∪ Σ (map g L) =α Σ (map (fun x ⇒ f x ∪ g x) L).
Lemma is_binding_finite_ax_eq e f :
e =α f → is_binding_finite e ↔ is_binding_finite f.
Lemma is_binding_finite_ax_inf e f : is_binding_finite f → e ≤α f → is_binding_finite e.
Lemma αKA_inf_act p e f : e ≤α f → p∙e ≤α p∙f.
End s.
Infix " =α " := (ax_eq αKA KA') (at level 80).
Infix " <=α " := (ax_inf αKA KA') (at level 80).