regexp.lang.world: Languages on Worlds and Thickening



Overview

  • world B: Worlds over the boolean symbols type B
  • consistent Ws xs: The sequence of worlds Ws is consistent with the string xs
  • thicken L Given a language L : lang B thicken it to the language on worlds. The thickening operation has many natural properties and preserve many language properties.

Worlds

Fix an finite type B as the alphabet. We often need to interpret letters x : B as proposition symbols. Under that interpretation, a world is nothing but a subset over B.

Definition world (B : finType) := {set B}.

Given a string over xs : B and a sequence Ws : seq (world B) of worlds over B. We say Ws is consistent with xs if they are of the same length and the letter xᵢ \in Wᵢ where xᵢ and Wᵢ are the elements at i-th position of xs and Ws respectively.

Module consistent.

  Fixpoint rel {B : finType} (Ws : seq (world B))(xs : seq B) : bool :=
  match Ws, xs with
  | V :: VS, y :: ys ⇒ (y \in V) && rel VS ys
  | [::], [::] ⇒ true
  | _ , _ ⇒ false
  end.

  Module left.

    Section Cxt.
      Context {B : finType}.
      Lemma nilE (xs : seq B) : rel [::] xs ↔ xs = [::].
        constructor.
        - by case: xs; rewrite //=.
        - by move ⇒ h; rewrite h.
      Qed.

      Lemma consP (W : world B) Ws xs
        : reflect (∃ y ys, xs = y :: ys ∧ y \in W ∧ rel Ws ys) (rel (W :: Ws) xs).

      Proof.
        apply/(iffP idP).
        - by case xs; rewrite //=; move ⇒ y ys; case /andP ⇒ h1 h2; ∃ y; ∃ ys.
        - case ⇒ y [ys [hxs [hy Hcons]]]; by rewrite hxs //=; by apply /andP.
      Qed.

    End Cxt.
  End left.

  Module right.

    Section Cxt.
      Context {B : finType}.

      Lemma nilE (Ws : seq (world B)) : rel Ws [::] ↔ Ws = [::].
        split.
        - by case: Ws; rewrite //=.
        - by move ⇒ h; rewrite h.
      Qed.

      Lemma consP {Ws : seq (world B)} {x} {xs}
        : reflect (∃ V Vs, Ws = V :: Vs ∧ x \in V ∧ rel Vs xs) (rel Ws (x :: xs)).
        apply/(iffP idP).
        - by case Ws; rewrite //=; move ⇒ V Vs; case /andP ⇒ h1 h2; ∃ V; ∃ Vs.
        - case ⇒ y [ys [hxs [hy Hcons]]]; by rewrite hxs //=; by apply /andP.
      Qed.

      Lemma singletonP Ws (x : B) : reflect (∃ W : {set B}, Ws = [:: W] ∧ x \in W) (rel Ws [:: x]).
        apply /(iffP idP).
        - case /consP ⇒ V [Vs [HWs [Hx]]].
          case/nilE ⇒ H; ∃ V; by rewrite HWs H.
        - case ⇒ V [HWs Hx]; by rewrite HWs /rel Hx.
      Qed.

      Lemma concat (xs1 : seq B) :
        ∀ Ws xs2, rel Ws (xs1 ++ xs2) → ∃ Ws1 Ws2, Ws = Ws1 ++ Ws2 ∧ rel Ws1 xs1 ∧ rel Ws2 xs2.
        elim xs1 ⇒ [| y ys IH].
        - move ⇒ Ws xs2; by rewrite //= ⇒ H; ∃ [::]; ∃ Ws.
        - move ⇒ Ws xs2; rewrite cat_cons.
          case /consP ⇒ V [Vs [Hws [Hx Hcons]]].
          set Hyp := (IH _ _ Hcons).
          case: Hyp ⇒ Ws1 [Ws2 [Hcat [Hcons1 Hcons2]]];
                      ∃ (V :: Ws1); ∃ Ws2; rewrite Hws Hcat -cat_cons //=; intuition.
      Qed.

    End Cxt.
  End right.

  Lemma concat {B : finType}{Ws1 : seq (world B)}
    : ∀ xs1, rel Ws1 xs1 → ∀ Ws2 xs2, rel Ws2 xs2 → rel (Ws1 ++ Ws2) (xs1 ++ xs2).
    elim: Ws1 ⇒ [| W Ws IH].
    - move ⇒ xs1. case /consistent.left.nilE ⇒ H; by rewrite H.
    - move ⇒ xs1. case /consistent.left.consP ⇒ x [xs [Hxs1 [HxW Hcons]]].
      move ⇒ Ws2 xs2 Hcons2; rewrite Hxs1 cat_cons //=; apply/andP; split.
      × done.
      × by apply IH.
  Qed.

End consistent.

Thickening

Using the consistency relation, any language L over B can be thickened to a language over B-worlds as follows

Section Thickening.

  Context {B : finType}.

  Definition thicken (L : lang B) : lang (world B) :=
    fun Ws ⇒ ∃ xs, consistent.rel Ws xs ∧ L xs.

  Lemma thicken_epsilon : thicken ε ≡ ε.
    move ⇒ Ws; rewrite /thicken //=; split.
    - case ⇒ xs [Hcons Heps]; move: Hcons; rewrite Heps.
      by move /consistent.right.nilE.
    - move ⇒ Heps; ∃ [::]; split; by rewrite ?Heps.
  Qed.

  Lemma thicken_singleton : ∀ x, thicken (singleton x) ≡ satisfy (fun A : world B ⇒ x \in A).
    move ⇒ x Ws; rewrite /thicken /singleton /satisfy; split.
    - case ⇒ xs [Hcons Hxs]. move: Hcons; rewrite Hxs.
      by case/consistent.right.singletonP ⇒ W [HWs Hx]; ∃ W.
    - case ⇒ W [HWs Hx]. by ∃ [:: x]; rewrite HWs //= andbT.
  Qed.

  Lemma thicken_alt {L1 L2 : lang B} : (thicken (L1 || L2) ≡ thicken L1 || thicken L2)%lan.
    move ⇒ Ws; rewrite /thicken /alt //=; split.
    - case ⇒ xs [Hcons [H|H]].
      × by left; ∃ xs.
      × by right; ∃ xs.
    - by case ⇒ H; case: H ⇒ [xs [Hcons H]]; ∃ xs; split; intuition.
  Qed.

  Lemma thicken_concat {L1 L2 : lang B} : (thicken (L1 ++ L2) ≡ thicken L1 ++ thicken L2)%lan.
  move ⇒ Ws; rewrite /thicken /concat; split.
  - case ⇒ xs [Hcons H].
    case: H ⇒ xs1 [xs2 [Hxs [HL1 HL2]]].
    move: Hcons; rewrite Hxs; case /consistent.right.concat ⇒ Ws1 [Ws2 [Hws [Hcons1 Hcons2]]]; ∃ Ws1; ∃ Ws2; intuition.
    × by ∃ xs1.
    × by ∃ xs2.
  - case ⇒ Ws1 [Ws2 [Hconcat [H1 H2]]].
    case: H1 ⇒ xs1 [Hcons1 HL1].
    case: H2 ⇒ xs2 [Hcons2 HL2].
    ∃ (xs1 ++ xs2); rewrite Hconcat; split.
    × by apply consistent.concat.
    × by ∃ xs1; ∃ xs2.
  Qed.

  Lemma thicken_pow {L : lang B} : ∀ n, (thicken (L ^ n) ≡ thicken L ^n)%lan.
    elim ⇒ [|n IH].
    - by rewrite thicken_epsilon.
    - by rewrite thicken_concat IH.
  Qed.

  Lemma thicken_many1 {L : lang B} : thicken (many1 L) ≡ many1 (thicken L)%lan.
    move ⇒ Ws; split.
    - set lhs := many1 (thicken L).
      rewrite /thicken; case ⇒ xs [Hcons HL].
      case: HL ⇒ n HLnp1.
      have Hyp : thicken (L^(n.+1))%lan Ws by rewrite /thicken; ∃ xs.
      ∃ n. by rewrite -(thicken_pow _ Ws).
    - case ⇒ n; rewrite -(thicken_pow _ Ws) /thicken.
      case ⇒ xs [Hcons HL]; ∃ xs; split.
      + done.
      + by ∃ n.
  Qed.
End Thickening.

Add Parametric Morphism (B : finType) : (@thicken B) with signature
    (@lang.eq.rel B) ==> (eq.rel) as thicken_morphism.
  move ⇒ L1 L2 H Ws.
  rewrite /thicken; split; case ⇒ xs [Hcon Hxs]; ∃ xs.
  - by rewrite -(H xs).
  - by rewrite (H xs).
Qed.