7

我正在尝试为 Setoids（具有等价关系的类型）建模 Agda 风格的等式推理证明。我的设置如下：

infix 1 :=:

interface Equality a where
  (:=:)  : a -> a -> Type

interface Equality a => VerifiedEquality a where  
  eqRefl : {x : a} -> x :=: x
  eqSym  : {x, y : a} -> x :=: y -> y :=: x
  eqTran : {x, y, z : a} -> x :=: y -> y :=: z -> x :=: z

使用这样的接口，我可以 Syntax.PreorderReasoning对 Idris 库中的一些等式推理组合器进行建模。

syntax [expr] "QED" = qed expr 
syntax [from] "={" [prf] "}=" [to] = step from prf to

namespace EqReasoning
  using (a : Type, x : a, y : a, z : a)
    qed : VerifiedEquality a => (x : a) -> x :=: x
    qed x = eqRefl {x = x}

    step : VerifiedEquality a => (x : a) -> x :=: y -> (y :=: z) -> x :=: z
    step x prf prf1 = eqTran {x = x} prf prf1

与 Idris 库的主要区别只是将命题等式及其相关函数替换为使用VerifiedEquality接口中的函数。

到目前为止，一切都很好。但是当我尝试使用这样的组合器时，我遇到了我认为与接口解析有关的问题。由于代码是我正在研究的矩阵库的一部分，因此我将其相关部分发布在以下要点中。

错误发生在以下证明中

zeroMatAddRight : ( VerifiedSemiring s
                  , VerifiedEquality s ) =>
                  {r, c : Shape} ->
                  (m : M s r c)  -> 
                  (m :+: (zeroMat r c)) :=: m
zeroMatAddRight {r = r}{c = c} m 
    = m :+: (zeroMat r c)
         ={ addMatComm {r = r}{c = c} m (zeroMat r c) }=
      (zeroMat r c) :+: m
         ={ zeroMatAddLeft {r = r}{c = c} m }=
      m
      QED

返回以下错误消息：

 When checking right hand side of zeroMatAddRight with expected type
         m :+: (zeroMat r c) :=: m

 Can't find implementation for Semiring a

 Possible cause:
         ./Data/Matrix/Operations/Addition.idr:112:11-118:1:When checking an application of function Algebra.Equality.EqReasoning.step:
                 Type mismatch between
                         m :=: m (Type of qed m)
                 and
                         y :=: z (Expected type)

至少在我看来，这个错误似乎与与语法扩展不能很好交互的接口解析有关。

我的经验是，这种奇怪的错误可以通过显式传递隐式参数来解决。问题是这样的解决方案会破坏等式推理组合证明的“可读性”。

有没有办法解决这个问题？重现此错误的相关部分可在先前链接的gist中找到。

4

0 回答 0