RIS.positive_regexp: regular expressions that do not contain the empty word.

Set Implicit Arguments.

Require Import tools algebra language regexp systems.

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

  Notation Regexp := (@regexp X).

  Fixpoint positive e : Regexp :=
    match e with
    | e_zero | e_un ⇒ zero
    | ⟪x⟫ ⇒ ⟪x⟫
    | e_add e f ⇒ positive e ∪ positive f
    | e_prod e f ⇒ positive e · f ∪ e · positive f
    | e_star e ⇒ positive e · e ⋆
    end.

  Lemma positive_lang e u : ⟦positive e⟧ u ↔ ⟦e⟧ u ∧ u ≠ [].

  Lemma positive_KA e f : e=KA f → positive e =KA positive f.

  Lemma positive_KA_inf e f : e≤KA f → positive e ≤KA positive f.

  Lemma positive_inf e : positive e ≤KA e.

  Lemma positive_star e : positive e ⋆ =KA e ⋆.

End s.