0 | ||| This module contains stuff that may use functions from `Data.List`.
 1 | ||| This separation is needed because `Data.List` uses `List1` type inside it,
 2 | ||| thus the core of `List1` must not import `Data.List`.
 3 | module Data.List1.Properties
 4 |
 5 | import Control.Function
 6 |
 7 | import public Data.Maybe
 8 | import Data.List
 9 | import Data.List1
10 |
11 | %default total
12 |
13 | export
14 | -- %deprecate -- deprecated in favor of Biinjective interface
15 | consInjective : (x ::: xs) === (y ::: ys) -> (x === y, xs === ys)
16 | consInjective Refl = (Refl, Refl)
17 |
18 | export
19 | Biinjective (:::) where
20 |   biinjective Refl = (Refl, Refl)
21 |
22 | export
23 | {x : a} -> Injective (x :::) where
24 |   injective Refl = Refl
25 |
26 | export
27 | {ys : List a} -> Injective (::: ys) where
28 |   injective Refl = Refl
29 |
30 | ||| Proof that the length of a List1 is the same as the length
31 | ||| of the List it represents.
32 | export
33 | listLength : (xs : List1 a) -> length xs = length (forget xs)
34 | listLength (head ::: tail) = Refl
35 |
36 | ------------------------------------------------------------------------
37 | -- Properties of append involving usual `List`'s append
38 |
39 | export
40 | appendlNilRightNeutral : (l : List1 a) -> l `appendl` [] = l
41 | appendlNilRightNeutral (_:::xs) = rewrite appendNilRightNeutral xs in Refl
42 |
43 | export
44 | lappendNilLeftNeutral : (l : List1 a) -> [] `lappend` l = l
45 | lappendNilLeftNeutral l = Refl
46 |
47 | export
48 | appendAssociative : (l, c, r : List1 a) -> l ++ (c ++ r) = (l ++ c) ++ r
49 | appendAssociative (l:::ls) (c:::cs) (r:::rs) = rewrite appendAssociative ls (c::cs) (r::rs) in Refl
50 |
51 | export
52 | toListAppendl : (xs : List1 a) -> (ys : List a) -> toList (xs `appendl` ys) = forget xs ++ ys
53 | toListAppendl (x:::xs) ys = Refl
54 |
55 | export
56 | toListLappend : (xs : List a) -> (ys : List1 a) -> toList (xs `lappend` ys) = xs ++ forget ys
57 | toListLappend []      ys = Refl
58 | toListLappend (x::xs) ys = Refl
59 |
60 | export
61 | toListAppend : (xs, ys : List1 a) -> toList (xs ++ ys) = toList xs ++ toList ys
62 | toListAppend (x:::xs) (y:::ys) = Refl
63 |
64 | export
65 | fromListAppend : (xs, ys : List a) -> fromList (xs ++ ys) = (fromList xs <+> fromList ys) @{Deep}
66 | fromListAppend [] ys with (fromList ys)
67 |   _ | Nothing  = Refl
68 |   _ | (Just _) = Refl
69 | fromListAppend (x::xs) ys with (fromList ys) proof prf
70 |   fromListAppend (x::xs) []      | Nothing         = rewrite appendNilRightNeutral xs in Refl
71 |   fromListAppend (x::xs) (y::ys) | (Just $ l:::ls) =
72 |     let (Refl, Refl) = biinjective $ injective prf in Refl
73 |