Формализация звездной идемпотентности Клини в регулярных выражениях

Я пытаюсь формализовать некоторые свойства регулярных выражений (RE) в Agda. Я застрял на доказательстве идемпотентности звездной операции Клини.

Мне удалось это доказать

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 *) , ?

Мы будем очень признательны за любые советы о том, как мне приступить к завершению этого доказательства.


regex agda
person Rodrigo Ribeiro    schedule 19.12.2015    source источник
comment
Включите свой код в вопрос.   -  person Gilles 'SO- stop being evil'    schedule 19.12.2015
comment
Я голосую за то, чтобы закрыть этот вопрос как не по теме, потому что формальные регулярные выражения - это не то же самое, что регулярные выражения в программировании. Вероятно, это принадлежит math.stackexchange.com.   -  person Barmar    schedule 19.12.2015
comment
@ShafKhan Не используйте разметку кода для вещей, которые не являются кодом. И не меняйте американский английский на британский английский, это выбор автора.   -  person Gilles 'SO- stop being evil'    schedule 19.12.2015
comment
@Barmar: Вопрос в том, чтобы доказать это на Agda, языке программирования.   -  person Tikhon Jelvis    schedule 19.12.2015
comment
Хорошо, я отказался. Но вы должны размещать свой код здесь, а не в виде ссылки.   -  person Barmar    schedule 19.12.2015
comment
Понятия не имею, что я только что написал, но похоже, что это работает.   -  person user3237465    schedule 19.12.2015

Ответы (1)


arrow_upward
1
arrow_downward

Просто поделитесь решением:

  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) *
person Rodrigo Ribeiro    schedule 20.12.2015
comment
Будет лучше, если вы не только поделитесь решением, но и опишете, что в нем творится. - person user3237465; 21.12.2015