0 | module Data.List.Equalities
  1 |
  2 | import Control.Function
  3 | import Syntax.PreorderReasoning
  4 |
  5 | import Data.List
  6 | import Data.List.Reverse
  7 |
  8 | %default total
  9 |
 10 | ||| A list constructed using snoc cannot be empty.
 11 | export
 12 | snocNonEmpty : {x : a} -> {xs : List a} -> Not (xs ++ [x] = [])
 13 | snocNonEmpty {xs = []} prf = uninhabited prf
 14 | snocNonEmpty {xs = y :: ys} prf = uninhabited prf
 15 |
 16 | ||| Proof that snoc'ed list is not empty in terms of `NonEmpty`.
 17 | export %hint
 18 | SnocNonEmpty : (xs : List a) -> (x : a) -> NonEmpty (xs `snoc` x)
 19 | SnocNonEmpty []     _ = IsNonEmpty
 20 | SnocNonEmpty (_::_) _ = IsNonEmpty
 21 |
 22 | ||| Two lists are equal, if their heads are equal and their tails are equal.
 23 | export
 24 | consCong2 : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
 25 |             x = y -> xs = ys -> x :: xs = y :: ys
 26 | consCong2 Refl Refl = Refl
 27 |
 28 | ||| Equal non-empty lists should result in equal components after destructuring 'snoc'.
 29 | export
 30 | snocInjective : {x : a} -> {xs : List a} -> {y : a} -> {ys : List a} ->
 31 |             (xs `snoc` x) = (ys `snoc` y) -> (xs = ys, x = y)
 32 | snocInjective {xs = []} {ys = []} Refl = (Refl, Refl)
 33 | snocInjective {xs = []} {ys = z :: zs} prf =
 34 |   let nilIsSnoc = snd $ consInjective {xs = []} {ys = zs ++ [y]} prf
 35 |    in void $ snocNonEmpty (sym nilIsSnoc)
 36 | snocInjective {xs = z :: xs} {ys = []} prf =
 37 |   let snocIsNil = snd $ consInjective {x = z} {xs = xs ++ [x]} {ys = []} prf
 38 |    in void $ snocNonEmpty snocIsNil
 39 | snocInjective {xs = w :: xs} {ys = z :: ys} prf =
 40 |   let (wEqualsZ, xsSnocXEqualsYsSnocY) = biinjective prf
 41 |       (xsEqualsYS, xEqualsY) = snocInjective xsSnocXEqualsYsSnocY
 42 |    in (consCong2 wEqualsZ xsEqualsYS, xEqualsY)
 43 |
 44 | ||| Appending pairwise equal lists gives equal lists
 45 | export
 46 | appendCong2 : {x1 : List a} -> {x2 : List a} ->
 47 |               {y1 : List b} -> {y2 : List b} ->
 48 |               x1 = y1 -> x2 = y2 -> x1 ++ x2 = y1 ++ y2
 49 | appendCong2 {x1=[]} {y1=(_ :: _)} Refl _ impossible
 50 | appendCong2 {x1=(_ :: _)} {y1=[]} Refl _ impossible
 51 | appendCong2 {x1=[]} {y1=[]} _ eq2 = eq2
 52 | appendCong2 {x1=(_ :: _)} {y1=(_ :: _)} eq1 eq2 =
 53 |   let (hdEqual, tlEqual) = consInjective eq1
 54 |    in consCong2 hdEqual (appendCong2 tlEqual eq2)
 55 |
 56 | ||| List.map is distributive over appending.
 57 | export
 58 | mapDistributesOverAppend
 59 |   : (f : a -> b)
 60 |   -> (xs : List a)
 61 |   -> (ys : List a)
 62 |   -> map f (xs ++ ys) = map f xs ++ map f ys
 63 | mapDistributesOverAppend _ [] _ = Refl
 64 | mapDistributesOverAppend f (x :: xs) ys =
 65 |   cong (f x ::) $ mapDistributesOverAppend f xs ys
 66 |
 67 | ||| List.length is distributive over appending.
 68 | export
 69 | lengthDistributesOverAppend
 70 |   : (xs, ys : List a)
 71 |   -> length (xs ++ ys) = length xs + length ys
 72 | lengthDistributesOverAppend [] ys = Refl
 73 | lengthDistributesOverAppend (x :: xs) ys =
 74 |   cong S $ lengthDistributesOverAppend xs ys
 75 |
 76 | ||| Length of a snoc'd list is the same as Succ of length list.
 77 | export
 78 | lengthSnoc : (x : _) -> (xs : List a) -> length (snoc xs x) = S (length xs)
 79 | lengthSnoc x [] = Refl
 80 | lengthSnoc x (_ :: xs) = cong S (lengthSnoc x xs)
 81 |
 82 | ||| Appending the same list at left is injective.
 83 | export
 84 | appendSameLeftInjective : (xs, ys, zs : List a) -> zs ++ xs = zs ++ ys -> xs = ys
 85 | appendSameLeftInjective xs ys []      = id
 86 | appendSameLeftInjective xs ys (_::zs) = appendSameLeftInjective xs ys zs . snd . biinjective
 87 |
 88 | ||| Appending the same list at right is injective.
 89 | export
 90 | appendSameRightInjective : (xs, ys, zs : List a) -> xs ++ zs = ys ++ zs -> xs = ys
 91 | appendSameRightInjective xs ys [] = rewrite appendNilRightNeutral xs in
 92 |                                     rewrite appendNilRightNeutral ys in
 93 |                                     id
 94 | appendSameRightInjective xs ys (z::zs) = rewrite appendAssociative xs [z] zs in
 95 |                                          rewrite appendAssociative ys [z] zs in
 96 |                                          fst . snocInjective . appendSameRightInjective (xs ++ [z]) (ys ++ [z]) zs
 97 |
 98 | export
 99 | {zs : List a} -> Injective (zs ++) where
100 |   injective = appendSameLeftInjective _ _ zs
101 |
102 | export
103 | {zs : List a} -> Injective (++ zs) where
104 |   injective = appendSameRightInjective _ _ zs
105 |
106 | ||| List cannot be equal to itself prepended with some non-empty list.
107 | export
108 | appendNonEmptyLeftNotEq : (zs, xs : List a) -> NonEmpty xs => Not (zs = xs ++ zs)
109 | appendNonEmptyLeftNotEq []      (_::_)  Refl impossible
110 | appendNonEmptyLeftNotEq (z::zs) (_::xs) prf
111 |   = appendNonEmptyLeftNotEq zs (xs ++ [z]) @{SnocNonEmpty xs z}
112 |   $ rewrite sym $ appendAssociative xs [z] zs in snd $ biinjective prf
113 |
114 | ||| List cannot be equal to itself appended with some non-empty list.
115 | export
116 | appendNonEmptyRightNotEq : (zs, xs : List a) -> NonEmpty xs => Not (zs = zs ++ xs)
117 | appendNonEmptyRightNotEq []      (_::_)  Refl impossible
118 | appendNonEmptyRightNotEq (_::zs) (x::xs) prf = appendNonEmptyRightNotEq zs (x::xs) $ snd $ biinjective prf
119 |
120 | listBindOntoPrf : (xs: List a)
121 |                 -> (f: a -> List b)
122 |                 -> (zs, ys: List b)
123 |                 -> listBindOnto f (reverse zs ++ reverse ys) xs = ys ++ listBindOnto f (reverse zs) xs
124 | listBindOntoPrf [] f zs ys =
125 |   Calc $
126 |     |~  reverse (reverse zs ++ reverse ys)
127 |     ~~  reverse (reverse (ys ++ zs)) ... cong reverse (revAppend ys zs)
128 |     ~~  ys ++ zs ... reverseInvolutive _
129 |     ~~  ys ++ reverse (reverse zs) ... cong (ys ++) (sym $ reverseInvolutive _)
130 | listBindOntoPrf (x::xs) f zs ys =
131 |   Calc $
132 |     |~ listBindOnto f (reverseOnto (reverse zs ++ reverse ys) (f x)) xs
133 |     ~~ listBindOnto f (reverse (f x) ++ reverse zs ++ reverse ys) xs
134 |                           ... cong  (\n => listBindOnto f n xs)
135 |                                     (reverseOntoSpec _ _)
136 |     ~~ listBindOnto f ((reverse (f x) ++ reverse zs) ++ reverse ys) xs
137 |                           ... cong  (\n => listBindOnto f n xs)
138 |                                     (appendAssociative _ _ _)
139 |     ~~ listBindOnto f (reverse (zs ++ f x) ++ reverse ys) xs
140 |                           ... cong  (\n => listBindOnto f (n ++ reverse ys) xs)
141 |                                     (revAppend _ _)
142 |     ~~ ys ++ listBindOnto f (reverse (zs ++ f x)) xs ... listBindOntoPrf _ _ _ _
143 |     ~~ ys ++ listBindOnto f (reverse (f x) ++ reverse zs) xs
144 |                           ... cong  (\n => ys ++ listBindOnto f n xs)
145 |                                     (sym $ revAppend _ _)
146 |     ~~ ys ++ listBindOnto f (reverseOnto (reverse zs) (f x)) xs
147 |                           ... cong  (\n => ys ++ listBindOnto f n xs)
148 |                                     (sym $ reverseOntoSpec _ _)
149 |
150 | ||| Proof of correspondence between list bind and concatenation.
151 | export
152 | bindConcatPrf : (xs: List a)
153 |               -> (x: a)
154 |               -> (f: a -> List b)
155 |               -> ((x::xs >>= f) = (f x) ++ (xs >>= f))
156 | bindConcatPrf xs x f =
157 |   Calc $
158 |     |~ listBindOnto f ([] ++ reverse (f x)) xs
159 |     ~~ listBindOnto f (reverse [] ++ reverse (f x)) xs
160 |                           ... cong  (\n => listBindOnto f (n ++ reverse (f x)) xs)
161 |                                     (sym reverseNil)
162 |     ~~ f x ++ listBindOnto f [] xs ... listBindOntoPrf xs f [] (f x)
163 |