CODEWITHSUNDEEP
idristheorem-proving
fakedrake
fakedrake

Reputation: 6856

Idris simple proof with lists

I am trying to prove some simple things with idris but I am failing miserably. Here is my 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

The goal for ?list_append_eq_rhs_1 is (after a couple of intro's)

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

What I want to do is rewrite prf using the trivial theorems I have proved until it is exactly the goal but I don't know how to do that in idris.

Upvotes: 0

Views: 348

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15404

First of all, we need the fact that :: is injective:

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

Then we can use the above fact to prove list_append_eq by induction on l:

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)

Here is a more concise version suggested by @András Kovács, which achieves the same result without consInjective by using the standard cong (congruence) lemma

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

and the drop function:

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)

Upvotes: 4

Related Questions