证明 `weaken` 不会改变数字的值

Question

假设我们想证明削弱Data.Fin 的上限不会改变数字的值。直观的表述方式是：

weakenEq : (num : Fin n) -> num = weaken num

现在让我们生成定义...等一下！让我们想一想那句话。 num 和 weaken num 有不同的类型。我们可以在这种情况下说明相等吗？

= 上的文档建议我们可以尝试，但我们可能想改用~=~。好吧，无论如何，让我们继续生成定义和大小写，结果

weakenEq : (num : Fin n) -> num = weaken num
weakenEq FZ = ?weakenEq_rhs_1
weakenEq (FS x) = ?weakenEq_rhs_2

weakenEq_rhs_1 洞中的目标是FZ = FZ，从价值的角度来看还是有道理的。所以我们乐观地用Refl替换了这个洞，但结果却失败了：

When checking right hand side of weakenEq with expected type
        FZ = weaken FZ

Unifying k and S k would lead to infinite value

一个有点神秘的错误消息，所以我们想知道这是否真的与类型不同有关。

无论如何，让我们再试一次，但现在用~=~ 而不是=。不幸的是，错误仍然相同。

那么，如何陈述和证明weaken x 不会改变x 的值？这样做真的有意义吗？如果这是一个更大的证明的一部分，我可能想用Vect n (Fin (S k)) 和Vect n (Fin (S k)) 在原始向量上获得rewrite 和weaken，我该怎么办？

Answer 1

如果你真的想证明Fin n的值在应用弱化函数后没有改变，你需要证明这些值的相等性：

weakenEq: (num: Fin n) -> finToNat num = finToNat $ weaken num
weakenEq FZ     = Refl
weakenEq (FS x) = cong $ weakenEq x

Answer 2

关于你的第二个问题/马库斯关于map (Data.Fin.finToNat) v = map (Data.Fin.finToNat . Data.Fin.weaken) v的评论：

vectorWeakenEq : (v: Vect n (Fin k)) -> 
                 map Fin.finToNat v = map (Fin.finToNat . Fin.weaken) v
vectorWeakenEq [] = Refl
vectorWeakenEq (x :: xs) =
  rewrite sym $ weakenEq x in
  cong {f=(::) (finToNat x)} (vectorWeakenEq xs)

要了解为什么num = weaken num 不起作用，我们来看一个反例：

getSize : Fin n -> Nat
getSize _ {n} = n

现在使用x : Fin n、getSize x = n != (n + 1) = getSize (weaken x)。仅依赖于构造函数的函数不会发生这种情况，例如finToNat。所以你必须约束自己并证明他们的行为是这样的。