idris 中列表的简单等式证明（证明 xs ++ [x] = ys ++ [y] -> x = y -> xs = ys）

Question

我正在学习 idris 并且对证明列表的属性非常感兴趣。

如果你看一下 standard library，可以证明 "Two lists are equal, if their heads are equal and their tails are equal."

consCong2 : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
x = y -> xs = ys -> x :: xs = y :: ys
consCong2 Refl Refl = Refl

我们也可以证明另一个方向

consCong2' : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
x::xs = y::ys -> x = y -> xs = ys
consCong2' Refl Refl = Refl

或者更明确地说，我们可以把方程两边的头都放下来得到证明。

consCong2' : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
x::xs = y::ys -> x = y -> xs = ys
consCong2' prf_cons Refl = (cong {f = drop 1} prf_cons)

看看这些属性是否也可以证明其余的最后一项以及之前的所有内容，这将很有趣。证明 "Two lists are equal, if the first part and the very last item are equal" 结果非常容易

consCong2' : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
x = y -> xs = ys -> xs ++ [x] = ys ++ [y]
consCong2' Refl Refl = Refl

但是另一个方向没有通过类型检查：

consCong2' : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
xs ++ [x] = ys ++ [y] -> x = y -> xs = ys
consCong2' Refl Refl = Refl

因为

Type mismatch between
                         ys ++ [x]
                 and
                         xs ++ [x]

显然，因为如果xs ++ [x] = ys ++ [y]在推导中排在第一位，idris不可能统一双方。

所以我们需要做的就是告诉 idris 在等式两边应用 init，就像我们之前对 drop 1 所做的一样。这失败了，因为 init 需要证明列表是非空的，这在此处不能以某种方式隐式推断。所以为此我写了一个辅助函数，它明确定义了 (a ++ [x]) = a.

dropOneRight :  (xs : List a) -> List a
dropOneRight xs with (snocList xs)
  dropOneRight [] | Empty = []
  dropOneRight (a ++ [x]) | Snoc rec = a

consCong2' : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
xs ++ [x] = ys ++ [y] -> x = y -> xs = ys
consCong2' prf_cons Refl = cong {f = dropOneRight} prf_cons

但这会产生

Type mismatch between
                 dropOneRight (ys ++ [x])
         and
                 ys

我花了一些时间在其他方法上，使用 snocList 进行案例分割，但没有取得显着进展。我不明白如何向 idris 展示 dropOneRight (ys ++ [x]) = ys。我如何证明 xs ++ [x] = ys ++ [y] -> x = y -> xs = ys？

Answer 1

我想 snocList 方法会很棘手；至少使用遵循定义的简单证明策略。为了证明ys = dropOneRight (ys ++ [x])统一snocList (ys ++ [x])和参数会出问题，大致是：

prf' : (ys : List a) -> (x : a) -> ys = dropOneRight (ys ++ [x])
prf' ys x with (snocList (ys ++ [x]))
    ...
    prf' ?? x | Snoc rec = ?hole

如果你允许 dropOneRight 更简单，那就更直接了：

dropOneRight : (xs : List a) -> List a
dropOneRight [] = []
dropOneRight [x] = []
dropOneRight (x :: y :: xs) = x :: dropOneRight (y :: xs)

dropPrf : (ys : List a) -> (x : a) -> ys = dropOneRight (ys ++ [x])
dropPrf [] z = Refl
dropPrf [x] z = Refl
dropPrf (x :: y :: xs) z = cong $ dropPrf (y::xs) z

consCong2' : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
             xs ++ [x] = ys ++ [y] -> x = y -> xs = ys
consCong2' {xs} {ys} {x} prf_cons Refl = 
  rewrite dropPrf ys x in rewrite dropPrf xs x in
  cong prf_cons

idris 中列表的简单等式证明（证明 xs ++ [x] = ys ++ [y] -> x = y -> xs = ys）

Simple equality proofs on lists in idris (prooving xs ++ [x] = ys ++ [y] -> x = y -> xs = ys)

idris

dependent-type

theorem-proving