git.iko.soy/Idris-dev
on master help sign in
Added CmpNat view and fixed type of take/drop
b7b8013Edwin Brady
libs/prelude/Prelude/Nat.idr+18
compare with master
unifiedsplit
@@ -312,6 +312,24 @@ lcm _ Z = Z
312lcm Z _ = Z
312lcm Z _ = Z
313lcm x y = divNat (x * y) (gcd x y)
313lcm x y = divNat (x * y) (gcd x y)
314
314
315+
316+--------------------------------------------------------------------------------
317+-- An informative comparison view
318+--------------------------------------------------------------------------------
319+data CmpNat : Nat -> Nat -> Type where
320+ cmpLT : (y : _) -> CmpNat x (x + S y)
321+ cmpEQ : CmpNat x x
322+ cmpGT : (x : _) -> CmpNat (y + S x) y
323+
324+total cmp : (x, y : Nat) -> CmpNat x y
325+cmp Z Z = cmpEQ
326+cmp Z (S k) = cmpLT _
327+cmp (S k) Z = cmpGT _
328+cmp (S x) (S y) with (cmp x y)
329+ cmp (S x) (S (x + (S k))) | cmpLT k = cmpLT k
330+ cmp (S x) (S x) | cmpEQ = cmpEQ
331+ cmp (S (y + (S k))) (S y) | cmpGT k = cmpGT k
332+
315--------------------------------------------------------------------------------
333--------------------------------------------------------------------------------
316-- Properties
334-- Properties
317--------------------------------------------------------------------------------
335--------------------------------------------------------------------------------
libs/prelude/Prelude/Vect.idr+7−15
@@ -100,17 +100,15 @@ updateAt (fS k) f (x::xs) = x :: updateAt k f xs
100
100
101||| Get the first m elements of a Vect
101||| Get the first m elements of a Vect
102||| @ m the number of elements to take
102||| @ m the number of elements to take
103−take : {n : Nat} -> (m : Fin (S n)) -> Vect n a -> Vect (cast m) a
103+take : (n : Nat) -> Vect (n + m) a -> Vect n a
104−take (fS k) [] = FinZElim k
104+take Z xs = []
105−take fZ _ = []
106−take (fS k) (x::xs) = x :: take k xs
105+take (S k) (x :: xs) = x :: take k xs
107
106
108||| Remove the first m elements of a Vect
107||| Remove the first m elements of a Vect
109||| @ m the number of elements to remove
108||| @ m the number of elements to remove
110−drop : (m : Fin (S n)) -> Vect n a -> Vect (n - cast m) a
109+drop : (n : Nat) -> Vect (n + m) a -> Vect m a
111−drop (fS k) [] = FinZElim k
110+drop Z xs = xs
112−drop fZ xs ?= xs
113−drop (fS k) (x::xs) = drop k xs
111+drop (S k) (x :: xs) = drop k xs
114
112
115--------------------------------------------------------------------------------
113--------------------------------------------------------------------------------
116-- Transformations
114-- Transformations
@@ -407,7 +405,7 @@ nub = nubBy (==)
407||| It is equivalent to (take n xs, drop n xs)
405||| It is equivalent to (take n xs, drop n xs)
408||| @ m the index to split at
406||| @ m the index to split at
409||| @ xs the Vect to split in two
407||| @ xs the Vect to split in two
410−splitAt : {n : Nat} -> (m : Fin (S n)) -> (xs : Vect n a) -> (Vect (cast m) a, Vect (n - cast m) a)
408+splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a)
411splitAt n xs = (take n xs, drop n xs)
409splitAt n xs = (take n xs, drop n xs)
412
410
413--------------------------------------------------------------------------------
411--------------------------------------------------------------------------------
@@ -489,12 +487,6 @@ vectAppendAssociative (x :: xs) ys zs =
489-- Proofs
487-- Proofs
490--------------------------------------------------------------------------------
488--------------------------------------------------------------------------------
491
489
492−Prelude.Vect.drop_lemma_1 = proof {
493− intros;
494− rewrite sym (minusZeroRight n);
495− trivial;
496−}
497−
498Prelude.Vect.reverse'_lemma_1 = proof {
490Prelude.Vect.reverse'_lemma_1 = proof {
499 intros;
491 intros;
500 rewrite prf;
492 rewrite prf;