列表平等 w/ `cong`
List Equality w/ `cong`
按照我的另一个 question, I tried to implement the actual exercise in 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
请说明。
如果您有两个值 u : c 和 v : c，以及一个函数 f : c -> d，那么如果您知道 u = v，它必须遵循 [=14] =]，简单地遵循引用透明度。
cong就是上述说法的证明。
在此特定用例中，您正在（通过统一）将 c 和 d 设置为 List a，u 为 xs，v 到 ys，f 到 (:) x，因为你想证明 xs = ys -> (:) x xs = (:) x ys。
按照我的另一个 question, I tried to implement the actual exercise in 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
请说明。
如果您有两个值 u : c 和 v : c，以及一个函数 f : c -> d，那么如果您知道 u = v，它必须遵循 [=14] =]，简单地遵循引用透明度。
cong就是上述说法的证明。
在此特定用例中，您正在（通过统一）将 c 和 d 设置为 List a，u 为 xs，v 到 ys，f 到 (:) x，因为你想证明 xs = ys -> (:) x xs = (:) x ys。