Idris einfacher Beweis mit Listen

Question

Ich versuche, einige einfache Dinge mit Idris zu beweisen, aber ich versage kläglich. Hier ist mein Code

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 

Das Ziel für ?list_append_eq_rhs_1 ist (nach ein paar intro' s)

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

Was ich tun möchte, ist prf umschreiben die trivialen Sätze mit ich bewiesen haben, bis es genau ist Das Ziel, aber ich weiß nicht, wie ich das in Idris machen soll.

Answer 1

Zunächst einmal müssen wir die Tatsache, dass :: injektiv:

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

Dann können wir die obige Tatsache verwenden list_append_eq auf l durch Induktion beweisen:

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) 

---

Hier eine prägnantere Version von @ András Kovács, die das gleiche Ergebnis ohne consInjective unter Verwendung des Standards cong (co ngruence) Lemma

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

und die drop Funktion:

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)