带有列表的 Idris 简单证明

Question

我试图用 idris 证明一些简单的事情，但我失败得很惨。这是我的代码

module MyReverse
%hide reverse
%default total

reverse : List a -> List a
reverse [] = []
reverse (x :: xs) = reverse xs ++ [x]

listEmptyAppend : (l : List a) -> [] ++ l = l
listEmptyAppend [] = Refl
listEmptyAppend (x :: xs) = Refl
listAppendEmpty : (l : List a) -> l ++ [] = l
listAppendEmpty [] = Refl
listAppendEmpty (x :: xs) = rewrite listAppendEmpty xs in Refl

list_append_eq : (l, l1, l2 : List a) -> l ++ l1 = l ++ l2 -> l1 = l2
list_append_eq l [] [] prf = Refl
list_append_eq l [] (x :: xs) prf = ?list_append_eq_rhs_1
list_append_eq l (x :: xs) [] prf = ?list_append_eq_rhs_2
list_append_eq l (x :: xs) (y :: ys) prf = ?list_append_eq_rhs_3

?list_append_eq_rhs_1 的目标是（在 intro' 秒后）

----------              Assumptions:              ----------
 a : Type
 l : List a
 x : a
 xs : List a
 prf : l ++ [] = l ++ x :: xs
----------                 Goal:                  ----------
{hole0} : [] = x :: xs

我想做的是使用我已经证明的平凡定理重写 prf 直到它正是目标，但我不知道如何在 idris 中做到这一点。

Answer 1

首先，我们需要::是单射的：

consInjective : {x : a} -> {l1, l2 : List a} -> x :: l1 = x :: l2 -> l1 = l2
consInjective Refl = Refl

那么我们可以用上面的事实通过对l的归纳来证明list_append_eq：

list_append_eq : (l, l1, l2 : List a) -> l ++ l1 = l ++ l2 -> l1 = l2
list_append_eq [] _ _ prf = prf
list_append_eq (x :: xs) l1 l2 prf =
  list_append_eq xs l1 l2 (consInjective prf)

这是@András Kovács 建议的更简洁的版本，它通过使用标准 cong（一致）引理

在没有 consInjective 的情况下实现相同的结果

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

和drop函数：

list_append_eq : (l, l1, l2 : List a) -> l ++ l1 = l ++ l2 -> l1 = l2
list_append_eq [] _ _ prf = prf
list_append_eq (x :: xs) l1 l2 prf =
  list_append_eq xs l1 l2 (cong {f = drop 1} prf)

带有列表的 Idris 简单证明

Idris simple proof with lists

theorem-proving

idris