regex - 正则表达式中 Kleene 星幂等性的形式化

Question

我正在尝试在 Agda 中形式化正则表达式 (RE) 的某些属性。我一直坚持 Kleene 星操作的幂等性证明。

我已经证明了这一点

xs <-[[ (e *) * ]] -> xs <-[[ e * ]]

即如果字符串 xs 是 RE (e *) * 的语言，那么它应该是 e *。我的问题是如何证明对方？ (lemmaKleeneIdem 中的漏洞)

xs <-[[ e * ]] -> xs <-[[ (e *) * ]]

这是我的形式化的一部分:

open import Data.List as List
open import Data.List.Properties
open List-solver renaming (nil to :[] ; _⊕_ to _:++_; _⊜_ to _:==_)
open import Data.Product renaming (_×_ to _*_)

open import Relation.Binary
open import Relation.Binary.PropositionalEquality renaming (_≡_ to _==_)
open import Relation.Nullary renaming (¬_ to not)

module Test {Token : Set}(eqTokenDec : Decidable {A = Token} _==_)  where

  infixr 5 _+_
  infixr 6 _o_
  infixl 7 _*

  data RegExp : Set where
    Emp : RegExp
    Eps : RegExp
    #_  : (a : Token) -> RegExp
    _o_ : (e e' : RegExp) -> RegExp
    _+_ : (e e' : RegExp) -> RegExp
    _*  : (e : RegExp) -> RegExp

  -- regular expression membership

  infix 3 _<-[[_]]
  infixr 6 _*_<=_
  infixr 6 _<+_ _+>_

  data _<-[[_]] : List Token -> RegExp -> Set where
    Eps    : List.[] <-[[ Eps ]]                       -- epsilon: empty string
    #_     : (a : Token) -> List.[ a ] <-[[ # a ]]     -- single token
    _*_<=_ : {xs ys zs : List Token}{e e' : RegExp}    -- concatenation of two REs
         (pr : xs <-[[ e ]])(pr' : ys <-[[ e' ]])
         (eq : zs == xs ++ ys) -> zs <-[[ e o e' ]]
    _<+_   : {xs : List Token}{e : RegExp}(e' : RegExp)  -- choice left
         -> (pr : xs <-[[ e ]]) -> xs <-[[ e + e' ]]           
    _+>_   : {xs : List Token}{e' : RegExp}(e : RegExp)   -- choice right
         -> (pr : xs <-[[ e' ]]) -> xs <-[[ e + e' ]]
    _*     : {xs : List Token}{e : RegExp} ->             -- Kleene star
         xs <-[[ Eps + e o e * ]]      ->
         xs <-[[ e * ]]


  -- regular expression equivalence

  infix 4 _:=:_

  _:=:_ : forall (e e' : RegExp) -> Set
  e :=: e' = forall (xs : List Token) -> (((pr : xs <-[[ e ]]) -> (xs <-[[ e' ]])) *
                                      ((pr : xs <-[[ e' ]]) -> (xs <-[[ e ]])))

  subsetLemma : forall {xs} e -> xs <-[[ e ]] -> xs <-[[ e * ]]
  subsetLemma {xs = xs} e pr = (_ +> pr * ((_ <+ Eps) *) <= solve 1 (\ xs -> xs :== xs :++ :[]) refl xs) *

  lemmaKleeneIdem : (e : RegExp) -> e * :=: (e *) *
  lemmaKleeneIdem e xs = subsetLemma (e *) , ?

任何关于我应该如何继续完成此证明的提示将不胜感激。

Answer 1

只是分享解决方案:

  lemmaKleeneIdem : (e : RegExp) -> e * :=: (e *) *
  lemmaKleeneIdem e xs = subsetLemma (e *) , subsetLemma' e
                     where
                       mem : forall {xs e} -> xs <-[[ e ]] -> List _
                       mem {xs = xs} _ = xs

                       assoc1 : forall {A : Set}(xs ys zs : List A) -> (xs ++ ys) ++ zs == xs ++ (ys ++ zs)
                       assoc1 = solve 3 (\ xs ys zs -> (xs :++ ys) :++ zs :== xs :++ (ys :++ zs)) refl

                       lem' : forall {xs ys zs} e -> zs == xs ++ ys -> xs <-[[ e ]]  -> ys <-[[ e * ]] -> zs <-[[ e * ]]
                       lem' e refl pr pr' = (_ +> pr * pr' <= refl) *

                       lem : forall {xs ys zs} e -> zs == xs ++ ys -> xs <-[[ e * ]] -> ys <-[[ e * ]] -> zs <-[[ e * ]]
                       lem e refl ((.(e o e *) <+ Eps) *)    q = q
                       lem e eq ((.Eps +> p * p₁ <= refl) *) q rewrite assoc1 (mem p) (mem p₁) (mem q)
                           = lem' e eq p (lem e refl p₁ q)

                       subsetLemma' : forall {xs} e -> xs <-[[ e * * ]] -> xs <-[[ e * ]]
                       subsetLemma' e ((.(e * o e * *) <+ pr) *)   = ((e o e *) <+ pr) *
                       subsetLemma' e ((.Eps +> pr * pr₁ <= eq) *) = lem e eq pr (subsetLemma' e pr₁)

                       subsetLemma : forall {xs} e -> xs <-[[ e ]] -> xs <-[[ e * ]]
                       subsetLemma {xs = xs} e pr = (_ +> pr * ((_ <+ Eps) *) <= solve 1 (\ xs -> xs :== xs :++ :[]) refl xs) *