在 Refl 中使用重写

Question

我正在使用 Idris 完成第 8 章类型驱动开发，我对重写如何与 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，从左侧重写但在第一次替换后停止并且不会替换所有plus m 0 与 m 的实例如我所料。

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

的左侧

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）。

在 Refl 中使用重写

using rewrite in Refl

idris