Question

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

如果你看一下standard library，有一个证明“两个列表是相等的，如果他们的头是相等的，他们的尾巴是相等的”。

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)

这将是有趣的，看看这些属性是否可以被证明也为最后一个项目在休息之前的一切。证明“两个列表是平等的，如果第一部分和最后一个项目是平等的”原来是很容易的

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?

1

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