Agda:模式匹配等变量？

Question

作为一种学习经验,我试图在Agda中使用延续传递方式实现经过验证的正则表达式匹配器,基于本文提出的方法.

我有一个像这样定义的正则表达式的类型:

data RE :  Set where
  ? : RE 
  ? : RE 
  Lit : Char -> RE 
  _+_ : RE -> RE -> RE
  _·_ :  RE -> RE -> RE
  _* : RE -> RE

还有一个类型,用于证明字符串与RE匹配,如下所示:

data REMatch : List Char -> RE -> Set where
  EmptyMatch : REMatch [] ?
  LitMatch : (c : Char) -> REMatch (c ? []) (Lit c)
  ...
  ConcatMatch : 
    (s1 : List Char) (s2 : List Char ) (r1 : RE) (r2 : RE)
    -> REMatch s1 r1
    -> REMatch s2 r2
    -> REMatch (s1 ++ s2) (r1 · r2)

我正在尝试为我的匹配器编写正确性证明,但是在我的模式匹配之前我遇到了类型错误,在我尝试获得证据之前:

accCorrect : 
  (r : RE) (s : List Char) (s1 : List Char) (s2 : List Char) (k : (List Char -> Bool)) 
  -> ( (s1 ++ s2) ? s)
  -> (REMatch s1 r)
  -> (k s2 ? true)
  -> (acc r s k ? true )
accCorrect ? [] [] [] k _ EmptyMatch kproof = kproof
accCorrect (r1 · r2) s s1 s2 k splitProof (ConcatMatch s1' s1'' r1' r2' subMatch1 subMatch2 ) kproof = ?

但是,这会产生以下错误:

r2' != r2 of type RE
when checking that the pattern
ConcatMatch s1' s1'' r1' r2' subMatch1 subMatch2 has type
REMatch s1 (r1 · r2)

但是,如果我更换下划线r2'用 r2,我得到一个"重复的变量"错误.

(r1 · r2)除了ConcatMatch构造函数之外,没有办法构造匹配项.

我的问题:

如何说服类型检查器r2和r2'相等,从模式匹配中？任何类型的参数都REMatch s1 (r1 · r2)必须ConcatMatch使用参数r1和构造函数构造r2,但是我不知道如何在模式匹配中证明这种情况.

Answer 1

这就是为什么Agda有点图案:

accCorrect : 
  (r : RE) (s : List Char) (s1 : List Char) (s2 : List Char) (k : (List Char -> Bool)) 
  -> ( (s1 ++ s2) ? s)
  -> (REMatch s1 r)
  -> (k s2 ? true)
  -> (acc r s k ? true )
accCorrect (.r1 · .r2) s ._ s2 k splitProof (ConcatMatch s1' s1'' r1 r2 subMatch1 subMatch2 ) kproof = {!!}
accCorrect _ _ _ = {!!}

即只是放在.应该被推断的表达式之前.或者您可以(并且应该)使用隐式参数:

accCorrect' : 
  {r : RE} (s : List Char) {s1 : List Char} (s2 : List Char) (k : (List Char -> Bool)) 
  -> ( (s1 ++ s2) ? s)
  -> (REMatch s1 r)
  -> (k s2 ? true)
  -> (acc r s k ? true )
accCorrect' s s2 k splitProof (ConcatMatch s1' s1'' r1 r2 subMatch1 subMatch2 ) kproof = {!!}
accCorrect' _ _ _ _ _ = {!!}

然而,你可能会遇到更复杂的问题,因为你触及了绿色粘液(术语是由于Conor McBride):

"绿泥" - 在构造函数的返回类型中定义的函数 - 的存在是一个危险的标志.

这是一个类似的说明性问题.