git.iko.soy/Idris-dev
on master help sign in
Add more Vect proofs
a6f9820howtonotwin
libs/base/Data/Vect.idr+46
compare with master
unifiedsplit
@@ -104,12 +104,36 @@ take : (n : Nat) -> Vect (n + m) elem -> Vect n elem
104take Z xs = []
104take Z xs = []
105take (S k) (x :: xs) = x :: take k xs
105take (S k) (x :: xs) = x :: take k xs
106
106
107+takeTake : (n : Nat) -> (m : Nat) -> (xs : Vect (n + m + l) a) -> take n (take (n + m) xs) = take n {m = m + l} (rewrite plusAssociative n m l in xs)
108+takeTake Z m xs = Refl
109+takeTake {l} (S k) m (x :: xs) = rewrite aux (plusAssociative k m l) x xs in cong { f = (x ::) } $ takeTake k m xs
110+ where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
111+ (x : a) -> (xs : Vect m a) ->
112+ rewrite__impl (\rep => Vect rep a) (rewrite__impl (\rep => S rep = S m) prf Refl) (x :: xs) = x :: rewrite__impl (\rep => Vect rep a) prf xs
113+ aux Refl x xs = Refl
114+
107||| Remove the first n elements of a Vect
115||| Remove the first n elements of a Vect
108||| @ n the number of elements to remove
116||| @ n the number of elements to remove
109drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
117drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
110drop Z xs = xs
118drop Z xs = xs
111drop (S k) (x :: xs) = drop k xs
119drop (S k) (x :: xs) = drop k xs
112
120
121+dropDrop : (n : Nat) -> (m : Nat) -> (xs : Vect (m + n + l) a) -> drop n (drop m {m = n + l} (rewrite plusAssociative m n l in xs)) = drop (m + n) xs
122+dropDrop n Z xs = Refl
123+dropDrop {l} n (S k) (x :: xs) = rewrite aux (plusAssociative k n l) x xs in dropDrop n k xs
124+ where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
125+ (x : a) -> (xs : Vect m a) ->
126+ rewrite__impl (\rep => Vect rep a) (rewrite__impl (\rep => S rep = S m) prf Refl) (x :: xs) = x :: rewrite__impl (\rep => Vect rep a) prf xs
127+ aux Refl x xs = Refl
128+
129+takeDropDropTake : (n : Nat) -> (m : Nat) -> (xs : Vect (m + n + l) a) -> take n (drop m {m = n + l} (rewrite plusAssociative m n l in xs)) = drop m (take (m + n) xs)
130+takeDropDropTake n Z xs = Refl
131+takeDropDropTake {l} n (S k) (x :: xs) = rewrite aux (plusAssociative k n l) x xs in takeDropDropTake n k xs
132+ where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
133+ (x : a) -> (xs : Vect m a) ->
134+ rewrite__impl (\rep => Vect rep a) (rewrite__impl (\rep => S rep = S m) prf Refl) (x :: xs) = x :: rewrite__impl (\rep => Vect rep a) prf xs
135+ aux Refl x xs = Refl
136+
113||| Take the longest prefix of a Vect such that all elements satisfy some
137||| Take the longest prefix of a Vect such that all elements satisfy some
114||| Boolean predicate.
138||| Boolean predicate.
115|||
139|||
@@ -188,6 +212,18 @@ fromList l =
188(++) [] ys = ys
212(++) [] ys = ys
189(++) (x::xs) ys = x :: xs ++ ys
213(++) (x::xs) ys = x :: xs ++ ys
190
214
215+takePrefix : (ns : Vect n a) -> (ms : Vect m a) -> take n (ns ++ ms) = ns
216+takePrefix [] _ = Refl
217+takePrefix (n :: ns) ms = cong $ takePrefix ns ms
218+
219+dropPrefix : (ns : Vect n a) -> (ms : Vect m a) -> drop n (ns ++ ms) = ms
220+dropPrefix [] ms = Refl
221+dropPrefix (_ :: ns) ms = dropPrefix ns ms
222+
223+takeDropConcat : (n : Nat) -> (xs : Vect (n + m) a) -> take n xs ++ drop n xs = xs
224+takeDropConcat Z xs = Refl
225+takeDropConcat (S k) (x :: xs) = cong $ takeDropConcat k xs
226+
191||| Repeate some value some number of times.
227||| Repeate some value some number of times.
192|||
228|||
193||| @ len the number of times to repeat it
229||| @ len the number of times to repeat it
@@ -567,6 +603,13 @@ implementation Traversable (Vect n) where
567implementation Show elem => Show (Vect len elem) where
603implementation Show elem => Show (Vect len elem) where
568 show = show . toList
604 show = show . toList
569
605
606+--------------------------------------------------------------------------------
607+-- Uninhabited
608+--------------------------------------------------------------------------------
609+
610+Uninhabited a => Uninhabited (Vect (S n) a) where
611+ uninhabited (x :: _) = uninhabited x
612+
570--------------------------------------------------------------------------------
613--------------------------------------------------------------------------------
571-- Properties
614-- Properties
572--------------------------------------------------------------------------------
615--------------------------------------------------------------------------------
@@ -574,6 +617,9 @@ implementation Show elem => Show (Vect len elem) where
574vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys)
617vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys)
575vectConsCong x xs xs Refl = Refl
618vectConsCong x xs xs Refl = Refl
576
619
620+vectMustBeNil : (xs : Vect Z a) -> xs = []
621+vectMustBeNil [] = Refl
622+
577vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
623vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
578vectNilRightNeutral [] = Refl
624vectNilRightNeutral [] = Refl
579vectNilRightNeutral (x :: xs) =
625vectNilRightNeutral (x :: xs) =
libs/contrib/Interfaces/Verified.idr+23
@@ -4,8 +4,10 @@ import Control.Algebra
4import Control.Algebra.Lattice
4import Control.Algebra.Lattice
5import Control.Algebra.NumericImplementations
5import Control.Algebra.NumericImplementations
6import Control.Algebra.VectorSpace
6import Control.Algebra.VectorSpace
7+import Data.Vect
7import Data.ZZ
8import Data.ZZ
8
9
10+%default total
9%access public export
11%access public export
10
12
11-- Due to these being basically unused and difficult to implement,
13-- Due to these being basically unused and difficult to implement,
@@ -27,6 +29,12 @@ VerifiedFunctor Maybe where
27 functorComposition Nothing g1 g2 = Refl
29 functorComposition Nothing g1 g2 = Refl
28 functorComposition (Just x) g1 g2 = Refl
30 functorComposition (Just x) g1 g2 = Refl
29
31
32+VerifiedFunctor (Vect n) where
33+ functorIdentity [] = Refl
34+ functorIdentity (x :: xs) = rewrite functorIdentity xs in Refl
35+ functorComposition [] _ _ = Refl
36+ functorComposition (x :: xs) f g = rewrite functorComposition xs f g in Refl
37+
30interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
38interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
31 applicativeMap : (x : f a) -> (g : a -> b) ->
39 applicativeMap : (x : f a) -> (g : a -> b) ->
32 map g x = pure g <*> x
40 map g x = pure g <*> x
@@ -38,6 +46,21 @@ interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type ->
38 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
46 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
39 g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g
47 g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g
40
48
49+VerifiedApplicative (Vect n) where
50+ applicativeMap [] f = Refl
51+ applicativeMap (x :: xs) f = rewrite applicativeMap xs f in Refl
52+ applicativeIdentity xs = rewrite sym $ applicativeMap xs id in functorIdentity xs
53+ applicativeComposition [] [] [] = Refl
54+ applicativeComposition (x :: xs) (f :: fs) (g :: gs) = rewrite applicativeComposition xs fs gs in Refl
55+ applicativeHomomorphism = prf
56+ where prf : with Vect ((x : a) -> (f : a -> b) -> zipWith Basics.apply (replicate m f) (replicate m x) = replicate m (f x))
57+ prf {m = Z} x f = Refl
58+ prf {m = S k} x f = rewrite prf {m = k} x f in Refl
59+ applicativeInterchange = prf
60+ where prf : with Vect ((x : a) -> (f : Vect m (a -> b)) -> zipWith Basics.apply f (replicate m x) = zipWith Basics.apply (replicate m (\f' => f' x)) f)
61+ prf {m = Z} x [] = Refl
62+ prf {m = S k} x (f :: fs) = rewrite prf x fs in Refl
63+
41VerifiedApplicative Maybe where
64VerifiedApplicative Maybe where
42 applicativeMap Nothing g = Refl
65 applicativeMap Nothing g = Refl
43 applicativeMap (Just x) g = Refl
66 applicativeMap (Just x) g = Refl