idris - 在 Refl 中使用重写

Question

我正在使用第 8 章使用 Idris 进行类型驱动开发，我对 rewrite 如何与 Refl 交互有疑问。

此代码作为重写如何作用于表达式的示例显示:

myReverse : Vect n elem -> Vect n elem
myReverse [] = []
myReverse {n = S k} (x :: xs)
    = let result = myReverse xs ++ [x] in
          rewrite plusCommutative 1 k in result

其中 plusCommutative 1 k 将查找 1 + k 的任何实例并将其替换为 k + 1。

我的问题是这个解决方案将 plusCommutative 重写为 myPlusCommutes 的一部分，答案是:

myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m = m + n
myPlusCommutes Z m = rewrite plusZeroRightNeutral m in Refl
myPlusCommutes (S k) m = rewrite myPlusCommutes k m in
                         rewrite plusSuccRightSucc m k in Refl

我遇到了这条线的问题:

myPlusCommutes Z m = rewrite plusZeroRightNeutral m in Refl

因为我可以通过在该行中单独使用 Refl 来理解:

myPlusCommutes Z m = Refl

我收到这个错误:

When checking right hand side of myPlusCommutes with expected type
        0 + m = m + 0

Type mismatch between
        plus m 0 = plus m 0 (Type of Refl)
and
        m = plus m 0 (Expected type)

Specifically:
        Type mismatch between
                plus m 0
        and
                m

首先，我没有意识到的一件事是 Refl 似乎在 = 的右侧工作，并从那个方向寻求反射。

接下来，似乎重写 Refl 会导致从 plus m 0 = plus m 0 变为 m = plus m 0，从左侧重写但停止在第一次替换之后，并没有像我预期的那样用 m 替换 plus m 0 的所有实例。

最后，这就是我的问题，为什么重写会以这种方式进行。对相等类型的重写是否不同，在那些情况下，重写仅替换 = 的左侧？

Answer 1

要了解这里发生的事情，我们需要考虑 Refl 是多态的这一事实:

λΠ> :set showimplicits
λΠ> :t Refl
Refl : {A : Type} -> {x : A} -> (=) {A = A} {B = A} x x

这意味着 Idris 正在尝试使用来自上下文的信息将类型归因于术语 Refl。例如。 myPlusCommutes Z m = Refl 中的 Refl 具有类型 plus m 0 = plus m 0。 Idris 可以选择 myPlusCommutes 输出类型的 LHS，并尝试将类型 m = m 归因于 Refl。您也可以像这样指定 x 表达式:Refl {x = m}。

现在，rewrite 针对您的当前目标 工作，即 rewrite Eq 替换所有出现的 Eq LHS 其 RHS 在您的目标中，而不是在某些可能的 Refl 类型中。

让我给你一个愚蠢的例子，使用一系列重写来说明我的意思:

foo : (n : Nat) -> n = (n + Z) + Z
foo n =
  rewrite sym $ plusAssociative n Z Z in   -- 1
  rewrite plusZeroRightNeutral n in        -- 2 
  Refl                                     -- 3

• 我们从目标n = (n + Z) + Z开始，然后
• 第 1 行使用结合律将目标变成 n = n + (Z + Z)，然后
• 第 2 行将当前目标 n = n + Z(定义上等于 n = n + (Z + Z))转换为 n = n
• 第 3 行为当前目标提供了证明项(如果我们想要更明确，我们可以用 Refl {x = n} 代替 Refl ).