Case Study: Regular Expressions

A propriedade Ev fornece um exemplo simples para ilustrar definições indutivas e as técnicas básicas para raciocinar sobre elas, mas não é muito empolgante - afinal, é equivalente às duas definições não indutivas de paridade que já vimos, e não parece oferecer nenhum benefício concreto sobre elas. Para dar uma melhor noção do poder das definições indutivas, vamos mostrar como usá-las para modelar um conceito clássico da ciência da computação: expressões regulares.

Expressões regulares são uma linguagem simples para descrever strings, definidas da seguinte forma:

type Regexp (t: Type) {
    emptyset                              
    emptystr                              
    chr   (h: t)                          
    app   (st1: Regexp t) (st2: Regexp t) 
    union (st1: Regexp t) (st2: Regexp t)
    star  (st1: Regexp t)                 
  }

Observe que essa definição é polimórfica: expressões regulares em Reg_exp t descrevem strings com caracteres extraídos de t - ou seja, listas de elementos de t.

(Nós nos afastamos um pouco da prática padrão ao não exigir que o tipo t seja finito. Isso resulta em uma teoria um pouco diferente de expressões regulares, mas a diferença não é significativa para nossos propósitos.)

Conectamos expressões regulares e strings por meio das seguintes regras, que definem quando uma expressão regular corresponde a alguma string:

• A expressão EmptySet não corresponde a nenhuma string. • A expressão EmptyStr corresponde à string vazia []. • A expressão Chr x corresponde à string de um caractere [x]. • Se re1 corresponde a s1 e re2 corresponde a s2, então (App re1 re2) corresponde a (App s1 s2). • Se pelo menos uma das expressões re1 e re2 corresponder a s, então Union re1 re2 corresponde a s. • Finalmente, se podemos escrever alguma string s como a concatenação de uma sequência de strings s = (App s_1 (App... s_k...)), e a expressão re corresponde a cada uma das strings s_i, então Star re corresponde a s.

Como caso especial, a sequência de strings pode estar vazia, então Star re sempre corresponde à string vazia [] independentemente de qual seja re.

Podemos facilmente traduzir essa definição informal em uma definição de dados da seguinte forma:

type Expmatch <t> ~(xs: Data.List t) (r: Regexp t) {
mempty              : Expmatch t []   Regexp.emptystr 
mchar (x: t)        : Expmatch t [x] (Regexp.chr x)
mapp 
  <s1: Data.List t>
  <s2: Data.List t>
  <re1: Regexp t>
  <re2: Regexp t>
  (e1: Expmatch t s1 re1)
  (e2: Expmatch t s2 re2)
  : Expmatch t (Data.List.concat t s1 s2) (Regexp.app re1 re2)
munionl <s1: Data.List t> (re1: Regexp t) (re2: Regexp t)
  (e1: Expmatch t s1 re1)
  : Expmatch t s1 (Regexp.union re1 re2)
munionr (re1: Regexp t) <s2: Data.List t> (re2: Regexp t)
  (e1: Expmatch t s2 re2)
  : Expmatch t s2 (Regexp.union re1 re2)
mstarz (r: Regexp t) : Expmatch t [] (Regexp.star r)  
mstarapp 
  <s1: Data.List t> 
  <s2: Data.List t>
  <r1: Regexp t>
  (e1: Expmatch s1 r1)
  (e2: Expmatch s2 (Regexp.star r1))
  : Expmatch t (Data.List.concat t s1 s2) (Regexp.star r1)
}

Vamos ilustrar essas regras com alguns exemplos.

Regexp_ex1 : Expmatch [1] (Regexp.chr 1)
Regexp_ex1 = Expmatch.mchar 1 

Regexp_ex2 : Expmatch [1, 2] (Regexp.app (Regexp.chr 1) (Regexp.chr 2))
Regexp_ex2 = Expmatch.mapp [1] (Regexp.chr 1) (Expmatch.mchar 1) [2] (Regexp.chr 2) (Expmatch.mchar 2)

Usando correspondência de padrões, também podemos mostrar que certas strings não correspondem a uma expressão regular:

Regexp_ex3 : Not (Expmatch [1, 2] (Regexp.chr 1))
Regexp_ex3 = Empty.absurd _

Podemos definir funções auxiliares para ajudar a escrever expressões regulares. A função reg_exp_of_list constrói uma expressão regular que corresponde exatamente à lista que recebe como argumento:

Regexp_of_list <t> (xs: List t)        : Regexp t
Regexp_of_list t List.nil              = Regexp.emptystr
Regexp_of_list t (List.cons xs.h xs.t) = Regexp.app (Regexp.chr xs.h) (Regexp_of_list t xs.t)

Regexp_ex4 : Expmatch [1, 2, 3] (Regexp_of_list [1, 2, 3])
Regexp_ex4 = 
  (Expmatch.mapp 
    [1] 
    (Regexp.chr 1) 
    (Expmatch.mchar 1) 
    [2, 3] 
    (Regexp_of_list [2, 3])
    (Expmatch.mapp
      [2]
      (Regexp.chr 2)
      (Expmatch.mchar 2) 
      [3]
      (Regexp_of_list [3])
      (Expmatch.mapp
        [3]
        (Regexp.chr 3)
        (Expmatch.mchar 3)
        []
        (Regexp_of_list [])
        (Expmatch.mempty)
      )
    )
  )

Também podemos provar fatos gerais sobre Exp_match. Por exemplo, o seguinte lema mostra que toda string s que corresponde a re também corresponde a Star re.

Mstar1 <t> <s: List t> <re: Regexp t> (e: Expmatch s re) : Expmatch s (Regexp.star re)  
Mstar1 t s re e = 
  let msz = Expmatch.mstarz re
  let mss = Expmatch.mstarapp s [] re e msz
  let lst = List_concat s
  let rwt = Equal.rewrite lst (x => (Expmatch t x (Regexp.star re))) mss
  rwt

(Obsere o uso de appendNilRightNeutral*** para alterar o objetivo do teorema para exatamente a mesma forma esperada por MStarApp.)

Exp_match_ex1

Os seguintes lemas mostram que as regras de correspondência informais fornecidas no início do capítulo podem ser obtidas a partir da definição indutiva formal.

  Munion 
  <t> 
  <s: List t> 
  <re1:  Regexp t> 
  <re2:  Regexp t> 
  (p: Pair (Expmatch s re1) (Expmatch s re2))
  : Expmatch s (Regexp.union re1 re2)
Munion t s re1 re2 (Pair.new fst snd) = 
  Expmatch.munionl t s [] re1 re2

O próximo lema é declarado em termos da função fold do capítulo Poly: Se ss: List (List t) representa uma sequência de strings s1, ..., sn, então fold (++) ss [] é o resultado da concatenação de todas elas.

Fold <x> <y> (f: x -> y -> y) (l: Data.List x) (b: y) : y
Fold x y f Data.List.nil b = b
Fold x y f (Data.List.cons xs.h xs.t) b = f xs.h (Fold f xs.t b) 

MStar_ <t>
  (ss : Data.List (Data.List t))
  (re : Regexp t)
  (construct_match : (s : Data.List t) -> (i : In s ss) -> Expmatch s re)
  : Expmatch (Concats ss) (Regexp.star re)
MStar_ ss re construct_match = ?

Reg_exp_of_list

Prove que reg_exp_of_list satisfaz a seguinte especificação:

Reg_exp_of_list_spec <t> (s1: Data.List t) (s2: Data.List t) : Iff (Expmatch s1 (Regexp_of_list s2)) (Prop.Equal s1 s2)
Reg_exp_of_list_spec s1 s2 = ?

Como a definição de Exp_match tem uma estrutura recursiva, é de se esperar que as provas envolvendo expressões regulares frequentemente exijam indução com base nas evidências. Por exemplo, suponha que quiséssemos provar o seguinte resultado intuitivo: se uma expressão regular re corresponde a alguma string s, então todos os elementos de s devem ocorrer em algum lugar de re. Para enunciar este teorema, primeiro definimos uma função re_chars que lista todos os caracteres que ocorrem em uma expressão regular:

Re_chars <t> (re: Regexp t) : Data.List t
Re_chars t Regexp.emptyset  = []
Re_chars t Regexp.emptystr  = []
Re_chars t (Regexp.chr x)   = [x]
Re_chars t (Regexp.app r0 r1) = Data.List.concat (Re_chars r0) (Re_chars r1)
Re_chars t (Regexp.union r0 r1) = Data.List.concat (Re_chars r0) (Re_chars r1)
Re_chars t (Regexp.star r0) = Re_chars r0

Re_star <t> (re: Regexp t) : Prop.Equal (Re_chars (Regexp.star re)) (Re_chars re)
Re_star e re = Prop.Equal.refl

Podemos então formular nosso teorema da seguinte forma:

Destruct <a> (x: a) (lx: Data.List a) (ly: Data.List a) (i: In x (Data.List.concat a lx ly)) : (Data.Either (In x lx) (In x ly))
Destruct a x lx ly i =  
  let Data.Pair.new fst snd = (In_app_iff x lx ly) 
  let f = (fst :: (_) -> (_)) i 
  f

Construct <a> (x: a) (lx: Regexp a) (ly: Regexp a) (e: Data.Either (In x (Re_chars lx)) (In x (Re_chars ly))) : In x (Data.List.concat (Re_chars lx) (Re_chars ly))
Construct a x lx ly e = (Data.Pair.snd ( In_app_iff x (Re_chars lx) (Re_chars ly)) :: (_) -> (_)) e

In_re_match <a> (x: a) (re: Regexp a) (s: Data.List a) (e: Expmatch s re) (i: In x s) : In x (Re_chars re)
In_re_match a x (Regexp.emptyset) Data.List.nil e i = i
In_re_match a x (Regexp.emptyset) (Data.List.cons head tail) e i = Data.Empty.absurd _ //todo
In_re_match a x (Regexp.emptystr) (Data.List.nil) Expmatch.mempty i = i
In_re_match a x (Regexp.chr u s)  (Data.List.cons t re (Data.List.nil _)) (Expmatch.mchar c) i = 
  let e0 = Prop.Equal.refl :: Prop.Equal c re
  let e1 = Prop.Equal.refl :: Prop.Equal s c
  let chn = Prop.Equal.chain e1 e0
  let rrt = Prop.Equal.rewrite (Prop.Equal.mirror chn) (y => (Data.Either (Prop.Equal _ x y) _)) i 
  rrt
In_re_match a x (Regexp.app t z y) (Data.List.concat u l1 l2) e i = 
  let e0 = Prop.Equal.refl :: Prop.Equal u a
  let l3 = l1 :: Data.List a
  let l4 = l2 :: Data.List a
  let e1 = Prop.Equal.refl :: Prop.Equal l1 l3
  let e2 = Prop.Equal.refl :: Prop.Equal l2 l4
  let e3 = Prop.Equal.refl :: Prop.Equal  (Data.List.concat u l1 l2) (Data.List.concat a l3 l4) 
  let i = i :: (In a x (Data.List.concat u l1 l2))
  let rrt = Prop.Equal.rewrite e3 ((k: (Data.List a))=> (In a x k)) i 
  let des = Destruct x l3 l4 rrt
  des
In_re_match a x re Data.List.nil (Expmatch.mstarz z) i = Data.Empty.absurd _ //todo

Re_not_empty

Escreva uma função recursiva re_not_empty que testa se uma expressão regular corresponde a alguma string. Prove que sua função está correta.

Re_not_empty <t> (re: Regexp t)   : Data.Bool
Re_not_empty t re = ?

Re_not_empty_correct <t> <re: Regexp t> 
: Equivalence (Data.Sigma (Data.List t) (s => Expmatch s re)) (Prop.Equal (Re_not_empty re) Data.Bool.true)
Re_not_empty_correct t re = ?

The remember Tactic

Reescrever a seção, o casamento de padrões dependentes resolve tudo isso.

Uma característica potencialmente confusa da tática de indução é que ela permite facilmente que você tente configurar uma indução sobre um termo que não é suficientemente geral. O efeito disso é perder informações (assim como destruct pode fazer) e deixá-lo incapaz de concluir a prova. Aqui está um exemplo:

Star_app  <a> (re: Regexp a) (s1: Data.List a) (s2: Data.List a) (exp0: Expmatch a s1 (Regexp.star re)) (exp1: Expmatch a s2 (Regexp.star re)) 
: (Expmatch (Data.List.concat s1 s2) (Regexp.star re))
Star_app a re (Data.List.nil _) s2 (Expmatch.mstarz e) exp1 = exp1
Star_app a re s1 s2 (Expmatch.mstarapp t r s r1 m ms) exp1 = 
  let e0 = Prop.Equal.refl :: Prop.Equal r1 re
  let e1 = Prop.Equal.refl :: Prop.Equal (Data.List.concat r s) s1
  let ind = Expmatch.mstarapp m (Star_app r1 s s2 ms exp1)
  let rrt = Prop.Equal.rewrite e0 (x => (Expmatch _ _ (Regexp.star _ x))) ind
  let aux = App_assoc r s s2
  let rrt = Prop.Equal.rewrite aux (x => (Expmatch _ (x) (_))) rrt
  let rrt = Prop.Equal.rewrite e1 (x => (Expmatch t (Data.List.concat _ x s2) (Regexp.star t re))) rrt
  rrt

Exp_match_ex2

MStar2 <t> (re: Regexp t) (s: Data.List t) (ss: Data.List (Data.List t)) (exp: Expmatch s (Regexp.star re)) 
: (Data.Pair (Prop.Equal s (Fold (x => y => Data.List.concat x y ) ss [])) ((s2: Data.List t) -> (In s2 ss) -> (Expmatch s2 re)))

O lema MStar'' abaixo (junto com o seu inverso, o exercício MStar' acima), mostra que a nossa definição de Exp_match para Star é equivalente àquela informalmente dada anteriormente.

pumping

Um dos primeiros teoremas realmente interessantes na teoria das expressões regulares é o chamado lema do bombeamento, que afirma, informalmente, que qualquer string suficientemente longa s que corresponde a uma expressão regular re pode ser "bombeada" repetindo alguma seção do meio de s um número arbitrário de vezes para produzir uma nova string também correspondente a re.

Para começar, precisamos definir o que significa "suficientemente longa". Uma vez que estamos trabalhando em uma lógica construtiva, na verdade precisamos ser capazes de calcular, para cada expressão regular re, o comprimento mínimo para as strings s garantirem a "bombeabilidade".

pumping_constant :

Em seguida, é útil definir uma função auxiliar que repete uma string (anexa a si mesma) um certo número de vezes.

napp :

Agora, o próprio lema do bombeamento afirma que, se s => re e se o comprimento de s for pelo menos a constante de bombeamento de re, então s pode ser dividida em três substrings s1 ++ s2 ++ s3 de tal forma que s2 pode ser repetida qualquer número de vezes e o resultado, quando combinado com s1 e s3, ainda corresponderá a re. Como s2 também está garantida a não ser a string vazia, isso nos dá uma maneira (construtiva!) de gerar strings correspondentes a re que são tão longas quanto desejarmos.

pumping :

Para agilizar a prova (que você deve preencher), a tática omega, que é habilitada pelo Require a seguir, é útil em vários lugares para completar automaticamente argumentos tediosos de baixo nível envolvendo igualdades ou desigualdades sobre números naturais. Voltaremos à tática omega em um capítulo posterior, mas sinta-se à vontade para experimentá-la agora, se quiser. O primeiro caso da indução dá um exemplo de como ela é usada.

pumping m le = ?pumping_rhs