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，我会收到 "repeated variables" 错误。

除了 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.

这里有一个类似的示例。

Agda：模式匹配相等变量？

Agda: pattern matching equal variables?

types

functional-programming

agda

dependent-type