在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替换它。

我的问题是这个解决方案重写qazxsw poi作为qazxsw poi练习的一部分，答案是：

plusCommutative

我遇到这条线路有问题：

myPlusCommutes

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

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

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

接下来，重写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

到=的变化，从左边重写但在第一次替换后停止，而不是像我预期的那样用plus m 0 = plus m 0替换m = plus m 0的所有实例。

最终，这是我的问题，为什么重写会以这种方式表现。重写相等类型是不同的，在那些情况下重写只替换在plus m 0的左侧？

Answer 1

要了解这里发生了什么，我们需要考虑m是多态的这一事实：

=

这意味着伊德里斯试图使用来自背景的信息将类型归因于Refl这一术语。例如。

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

的Refl有Refl型。伊德里斯本可以选择myPlusCommutes Z m = Refl输出类型的LHS，并试图将plus m 0 = plus m 0类型归因于myPlusCommutes。你也可以像这样指定m = m表达式：Refl。

现在，x就你目前的目标而言，即Refl {x = m}用你的目标中的RHS替换rewrite的LHS的所有出现，而不是在某些可能的rewrite Eq类型中。

让我举一个使用一系列重写来说明我的意思的愚蠢的例子：

Eq

• 我们从目标Refl开始，然后
• 第1行使用相关性定律将目标转换为

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

• 第2行将当前目标n = (n + Z) + Z（在定义上等于n = n + (Z + Z)）变成n = n + Z
• 第3行提供了当前目标的证明术语（如果我们想要更明确，我们可以用n = n + (Z + Z)代替n = n）。