7454bb2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Clean up splitAt

Use a with-block to dodge #4001. Realize the simplifications this makes in proofs.

commit7454bb21f798d98c4d0e5185b9e268e65b5b852b authorhowtonotwin <rasheeqhere@gmail.com> dateSun 8 Jul 2018, 13:47 (8 years ago) parent5ed7efb

3 files changed+27−36

compare with master

unifiedsplit

libs/base/Data/Vect.idr+6−9 libs/contrib/Control/Isomorphism/Vect.idr+10−13 libs/prelude/Prelude/List.idr+11−14

libs/base/Data/Vect.idr+6−9

@@ -464,9 +464,8 @@ delete = deleteBy (==)

464464||| @ xs the `Vect` to split in two

465465splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)

466466splitAt Z xs = ([], xs)

467−splitAt (S k) (x :: xs) =

468− let (tk, dr) = splitAt k xs

469− in (x :: tk, dr)

467+splitAt (S k) (x :: xs) with (splitAt k xs)

468+ | (tk, dr) = (x :: tk, dr)

470469

471470partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))

472471partition p [] = ((_ ** []), (_ ** []))

@@ -641,12 +640,10 @@ dropTakeTakeDrop (S n) m (_ :: xs) (_ :: ys) prf = dropTakeTakeDrop n m xs ys (v

641640splitAtTakeDrop : (n : Nat) -> (xs : Vect (n + m) a) -> splitAt n xs = (take n xs, drop n xs)

642641splitAtTakeDrop Z xs = Refl

643642splitAtTakeDrop (S k) (x :: xs) with (splitAt k xs) proof p

644− | (tk, dr) =

645− let rec = sym $ trans p $ splitAtTakeDrop k xs

646− tkp = cong {f=fst} rec

647− drp = cong {f=snd} rec

648− in replace {P = \tk' => (x :: tk', dr) = (x :: take k xs, drop k xs)} tkp $

649− replace {P = \dr' => (x :: take k xs, dr') = (x :: take k xs, drop k xs) } drp Refl

643+ | (tk, dr) = let prf = trans p (splitAtTakeDrop k xs)

644+ in aux (cong {f=(x ::) . fst} prf) (cong {f=snd} prf)

645+ where aux : {a, b : Type} -> {w, x : a} -> {y, z : b} -> w = x -> y = z -> (w, y) = (x, z)

646+ aux Refl Refl = Refl

650647

651648zipWithIsLiftA2 : (f : a -> b -> c) -> (as : Vect n a) -> (bs : Vect n b) -> zipWith f as bs = [| f as bs |]

652649zipWithIsLiftA2 _ [] [] = Refl

libs/contrib/Control/Isomorphism/Vect.idr+10−13

@@ -29,7 +29,7 @@ splitPair {n} {m} = MkIso (splitAt n) (uncurry (++)) toFrom fromTo

2929 where pairify : q = w -> e = r -> (q, e) = (w, r)

3030 pairify Refl Refl = Refl

3131 toFrom (ns, ms) = trans (splitAtTakeDrop n (ns ++ ms)) $ pairify (takePrefix ns ms) (dropPrefix ns ms)

32− fromTo xs = rewrite splitAtTakeDrop {m=m} n xs in takeDropConcat n xs

32+ fromTo xs = rewrite splitAtTakeDrop {m} n xs in takeDropConcat n xs

3333

3434||| An `Iso` based on `zip` and `unzip`.

3535zipped : Iso (Vect n a, Vect n b) (Vect n (a, b))

@@ -68,7 +68,8 @@ transposition {a} = MkIso transpose transpose prf prf

6868||| This is the inverse of `concat`.

6969unconcat : Vect (n * m) a -> Vect n (Vect m a)

7070unconcat {n = Z} [] = []

71−unconcat {n = S k} {m} xs = let (xs', xss) = splitAt m xs in xs' :: unconcat xss

71+unconcat {n = S k} {m} xs with (splitAt m xs)

72+ | (xs', xss) = xs' :: unconcat xss

7273||| An `Iso` based on `unconcat` and `concat`.

7374|||

7475||| ```idris example

@@ -76,21 +77,17 @@ unconcat {n = S k} {m} xs = let (xs', xss) = splitAt m xs in xs' :: unconcat xss

7677||| ```

7778rectangular : Iso (Vect (n * m) a) (Vect n (Vect m a))

7879rectangular = MkIso unconcat concat toFrom fromTo

79−-- TODO: Clean up after #4001 is fixed

8080 where toFrom : (xss : Vect i (Vect o a)) -> unconcat (concat xss) = xss

8181 toFrom {i = Z} [] = Refl

82− toFrom {i = S k} {o} (xs :: xss) with (splitAt o (xs ++ concat xss)) proof p

83− | (tk, dr) = let sATK = sym $ trans p $ splitAtTakeDrop o (xs ++ concat xss)

84− tkp = trans (sym $ takePrefix xs $ concat xss) $ cong {f=fst} sATK

85− drp = trans (sym $ toFrom xss) $ cong {f=unconcat} $ trans (sym $ dropPrefix xs $ concat xss) $ cong {f=snd} sATK

86− in replace {P = \dr' => tk :: dr' = xs :: xss} drp $ replace {P = \tk' => tk' :: xss = xs :: xss} tkp Refl

82+ toFrom {i = S i} {o} (xs :: xss) = rewrite splitAtTakeDrop o {m = i * o} (xs ++ concat xss) in

83+ rewrite takePrefix xs (concat xss) in

84+ rewrite dropPrefix xs (concat xss) in

85+ cong (toFrom xss)

8786 fromTo : (xs : Vect (i * o) a) -> concat (unconcat xs) = xs

8887 fromTo {i = Z} [] = Refl

89− fromTo {i = S k} {o} xs with (splitAt o xs) proof p

90− | (tk, dr) = let sATK = sym $ trans p $ splitAtTakeDrop o xs

91− tkp = cong {f=fst} sATK

92− drp = trans (cong {f=snd} sATK) $ sym $ fromTo dr

93− in replace {P = \dr' => tk ++ dr' = xs} drp $ replace {P = \tk' => tk' ++ drop o xs = xs } tkp $ takeDropConcat o xs

88+ fromTo {i = S i} {o} xs = rewrite splitAtTakeDrop o {m = i * o} xs in

89+ rewrite fromTo {i} {o} (drop o xs) in

90+ takeDropConcat o xs

9491

9592-- Not an Iso because (=) is not extensional, but it works in spirit

9693||| Go through all possible inputs and tabulate the outputs in a `Vect`.

libs/prelude/Prelude/List.idr+11−14

@@ -685,20 +685,8 @@ split p xs =

685685splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)

686686splitAt Z xs = ([], xs)

687687splitAt (S k) [] = ([], [])

688−splitAt (S k) (x :: xs) =

689− let (tk, dr) = splitAt k xs

690− in (x :: tk, dr)

691−

692−splitAtTakeDrop : (n : Nat) -> (xs : List a) -> splitAt n xs = (take n xs, drop n xs)

693−splitAtTakeDrop Z xs = Refl

694−splitAtTakeDrop (S k) [] = Refl

695−splitAtTakeDrop (S k) (x::xs) with (splitAt k xs) proof p

696− | (tk, dr) =

697− let rec = sym $ trans p $ splitAtTakeDrop k xs

698− tkp = cong {f=fst} rec

699− drp = cong {f=snd} rec

700− in replace {P = \tk' => (x::tk', dr) = (x::take k xs, drop k xs)} tkp $

701− replace {P = \dr' => (x::take k xs, dr') = (x::take k xs, drop k xs) } drp Refl

688+splitAt (S k) (x :: xs) with (splitAt k xs)

689+ | (tk, dr) = (x :: tk, dr)

702690

703691||| The partition function takes a predicate a list and returns the pair of

704692||| lists of elements which do and do not satisfy the predicate, respectively;

@@ -948,3 +936,12 @@ foldlAsFoldr f z t = foldr (flip (.) . flip f) id t z

948936foldlMatchesFoldr : (f : b -> a -> b) -> (q : b) -> (xs : List a) -> foldl f q xs = foldlAsFoldr f q xs

949937foldlMatchesFoldr f q [] = Refl

950938foldlMatchesFoldr f q (x :: xs) = foldlMatchesFoldr f (f q x) xs

939+

940+splitAtTakeDrop : (n : Nat) -> (xs : List a) -> splitAt n xs = (take n xs, drop n xs)

941+splitAtTakeDrop Z xs = Refl

942+splitAtTakeDrop (S k) [] = Refl

943+splitAtTakeDrop (S k) (x :: xs) with (splitAt k xs) proof p

944+ | (tk, dr) = let prf = trans p (splitAtTakeDrop k xs)

945+ in aux (cong {f=(x ::) . fst} prf) (cong {f=snd} prf)

946+ where aux : {a, b : Type} -> {w, x : a} -> {y, z : b} -> w = x -> y = z -> (w, y) = (x, z)

947+ aux Refl Refl = Refl