------------------------------------------------------------------------
-- The Agda standard library
--
-- Regular expressions: core properties (only require a Preorder)
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary.Bundles using (Preorder)

module Text.Regex.Properties.Core {a e r} (P : Preorder a e r) where

open import Level using (_⊔_)

open import Data.Bool.Base using (Bool)
open import Data.List.Base as List using (List; []; _∷_; _++_)

open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.Product.Base using (_×_; _,_)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)

open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Unary using (Pred)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

open Preorder P using (_≈_) renaming (Carrier to A; _∼_ to _≤_)
open import Text.Regex.Base P

open import Data.List.Relation.Ternary.Appending.Propositional.Properties {A = A}
  using (++[]⁻¹; []++⁻¹; conicalˡ; conicalʳ)

------------------------------------------------------------------------
-- Views

is-∅ : ∀ (e : Exp) → Dec (e ≡ ∅)
is-∅ ε          = no (λ ())
is-∅ [ [] ]     = yes refl
is-∅ [ r ∷ rs ] = no (λ ())
is-∅ [^ rs ]    = no (λ ())
is-∅ (e ∣ f)    = no (λ ())
is-∅ (e ∙ f)    = no (λ ())
is-∅ (e ⋆)      = no (λ ())

is-ε : ∀ (e : Exp) → Dec (e ≡ ε)
is-ε ε       = yes refl
is-ε [ rs ]  = no (λ ())
is-ε [^ rs ] = no (λ ())
is-ε (e ∣ f) = no (λ ())
is-ε (e ∙ f) = no (λ ())
is-ε (e ⋆)   = no (λ ())

------------------------------------------------------------------------
-- Inversion lemmas

∉∅ : ∀ {xs} → xs ∉ ∅
∉∅ [ () ]

∈ε⋆-inv : ∀ {w} → w ∈ (ε ⋆) → w ∈ ε
∈ε⋆-inv (star (sum (inj₁ ε))) = ε
∈ε⋆-inv (star (sum (inj₂ (prod eq ε p)))) rewrite []++⁻¹ eq = ∈ε⋆-inv p

∈∅⋆-inv : ∀ {w} → w ∈ (∅ ⋆) → w ∈ ε
∈∅⋆-inv (star (sum (inj₁ ε))) = ε
∈∅⋆-inv (star (sum (inj₂ (prod eq p q)))) = contradiction p ∉∅

∈ε∙e-inv : ∀ {w e} → w ∈ (ε ∙ e) → w ∈ e
∈ε∙e-inv (prod eq ε p) rewrite []++⁻¹ eq = p

∈e∙ε-inv : ∀ {w e} → w ∈ (e ∙ ε) → w ∈ e
∈e∙ε-inv (prod eq p ε) rewrite ++[]⁻¹ eq = p

[]∈e∙f-inv : ∀ {e f} → [] ∈ (e ∙ f) → [] ∈ e × [] ∈ f
[]∈e∙f-inv (prod eq p q) rewrite conicalˡ eq | conicalʳ eq = p , q