列表相等 w/`cong`

Question

在我的另一个question 之后，我尝试在Type-Driven Development with Idris 中为same_cons 实施实际练习，以证明给定两个相等的列表，在每个列表前面添加相同的元素会导致两个相等的列表。

例子：

prove that 1 :: [1,2,3] == 1 :: [1,2,3]

所以我想出了以下编译代码：

sameS : {xs : List a} -> {ys : List a} -> (x: a) -> xs = ys -> x :: xs = x :: ys
sameS {xs} {ys} x prf = cong prf

same_cons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys
same_cons prf = sameS _ prf

我可以通过以下方式调用它：

> same_cons {x=5} {xs = [1,2,3]} {ys = [1,2,3]} Refl
Refl : [5, 1, 2, 3] = [5, 1, 2, 3]

关于cong函数，我的理解是它需要一个证明，即a = b，但我不明白它的第二个参数：f a。

> :t cong
cong : (a = b) -> f a = f b

请解释一下。

Answer 1

如果您有两个值u : c 和v : c，以及一个函数f : c -> d，那么如果您知道u = v，它必须遵循f u = f v，这只是从引用透明性开始。

cong是上述陈述的证明。

在这个特定的用例中，您正在（通过统一）将c 和d 设置为List a，将u 设置为xs，将v 设置为ys，并将f 设置为@ 987654335@，因为你想证明xs = ys -> (:) x xs = (:) x ys。