リストを使ってイドリス簡単な証明

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の目標は

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

私がやりたいことは、それが正確になるまで私が証明している些細な定理を使ってprfを書き換えるです（intro'秒のカップルの後）であります目標は、私は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ásKovácsによって提案されたより簡潔なバージョンは、標準 congを使用して consInjectiveなしで同じ結果を達成します（co ngruence）補題

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)