在 Idris REPL 中试验 cong

Question

TL;DR：我想要一两个在 Idris REPL 中使用 cong 的示例，以帮助我更好地理解它。

泛型相等类型的概念定义如下：

data (=) : a -> b -> Type where
  Refl : x = x

当我第一次遇到这个时，我对语法很困惑。 （我一直认为 = 是一个运算符而不是一个类型。）但是在 REPL 中玩弄它有助于我理解。例如，我们可以声明类型来表示假等式：

λ> 2 + 2 = 5
4 = 5 : Type
λ> 2 = "wombat"
2 = "wombat" : Type

但是，= 的唯一构造函数是 Refl，我们只能在两个参数相等时使用它。

λΠ> the (4 = 4) Refl
Refl : 4 = 4
λΠ> the (4 = 5) Refl
... type mismatch

所以现在我试图通过在 REPL 中进行实验来理解 cong。 函数cong 证明如果两个值相等，应用 对他们的功能产生相同的结果。我找到了定义。

  cong : {f : t -> u} -> (a = b) -> f a = f b
  cong Refl = Refl

所以，例如，如果我定义...

λ> :let twoEqTwo = the (2 = 2) Refl
defined

...然后我希望能够证明两边都加 1 会导致另一个相等。

λΠ> :let ty = (S 2 = S 2)
defined
λΠ> the ty (cong twoEqTwo)
    ...type mismatch

谁能给我看一两个在 REPL 中使用 cong 的例子吗？

Answer 1

2s 的类型错误。它们在twoEqTwo 中默认为Integer 类型，因为它们没有其他约束。看，一个不受约束的2：

idris> 2
2 : Integer

然而，在ty，你说S 2。 S 强制整个事情在 Nat 中工作：

idris> S 2
3 : Nat

让twoEqTwo 也可以在Nat 中工作：

idris> :let twoEqTwo = the (the Nat 2 = 2) Refl
idris> the (S 2 = S 2) twoEqTwo
Refl : 3 = 3

请注意，如果您让它看到整个表达式，类型推断可以自行解决：

idris> the (S 2 = S 2) (cong (the (2 = 2) Refl))
Refl : 3 = 3