types - Agda:模式匹配相等变量？

Question

作为一种学习经验，我正在尝试根据 this paper 中提出的方法，在 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，则会出现“重复变量”错误。

除了 ConcatMatch 构造函数外，没有办法为 (r1 · r2) 构造匹配项。

我的问题:

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

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 的缘故):

The presence of ‘green slime’ — defined functions in the return types of constructors — is a danger sign.

这是一个类似的说明性 question .