c4c03b6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #4505 from howtonotwin/feature/vect-isos

c4c03b6Niklas Larsson8 years ago

libs/base/Control/Isomorphism.idr+12−6

compare with master

unifiedsplit

@@ -8,12 +8,12 @@ import Control.Category

8%access public export

10||| An isomorphism between two types

11−data Iso : Type -> Type -> Type where

11+record Iso a b where

12+ constructor MkIso

12− MkIso : (to : a -> b) ->

13+ to : a -> b

13− (from : b -> a) ->

14+ from : b -> a

14− (toFrom : (y : b) -> to (from y) = y) ->

15+ toFrom : (y : b) -> to (from y) = y

15− (fromTo : (x : a) -> from (to x) = x) ->

16+ fromTo : (x : a) -> from (to x) = x

16− Iso a b

18-- Isomorphism properties

@@ -37,6 +37,12 @@ Category Iso where

37 id = isoRefl

38 (.) = flip isoTrans

40+Semigroup (Iso a a) where

41+ (<+>) = isoTrans

42+

43+Monoid (Iso a a) where

44+ neutral = isoRefl

45+

40||| Isomorphism is symmetric

46||| Isomorphism is symmetric

41isoSym : Iso a b -> Iso b a

47isoSym : Iso a b -> Iso b a

42isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom

48isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom

libs/base/Data/Vect.idr+117−19

@@ -293,7 +293,6 @@ mapMaybe f (x::xs) =

293 Just y => (S len ** y :: ys)

294 Nothing => ( len ** ys)

295

296−

297--------------------------------------------------------------------------------

296--------------------------------------------------------------------------------

298-- Folds

297-- Folds

299--------------------------------------------------------------------------------

298--------------------------------------------------------------------------------

@@ -321,6 +320,7 @@ foldr1 f (x::xs) = foldr f x xs

321||| Foldl without seeding the accumulator

320||| Foldl without seeding the accumulator

322foldl1 : (t -> t -> t) -> Vect (S n) t -> t

321foldl1 : (t -> t -> t) -> Vect (S n) t -> t

323foldl1 f (x::xs) = foldl f x xs

322foldl1 f (x::xs) = foldl f x xs

323+

324--------------------------------------------------------------------------------

325-- Scans

326--------------------------------------------------------------------------------

@@ -455,13 +455,17 @@ delete = deleteBy (==)

455-- Splitting and breaking lists

456--------------------------------------------------------------------------------

457

458−||| A tuple where the first element is a Vect of the n first elements and

458+||| A tuple where the first element is a `Vect` of the `n` first elements and

459−||| the second element is a Vect of the remaining elements of the original Vect

459+||| the second element is a `Vect` of the remaining elements of the original.

460−||| It is equivalent to (take n xs, drop n xs)

460+||| It is equivalent to `(take n xs, drop n xs)` (`splitAtTakeDrop`),

461+||| but is more efficient.

462+|||

461||| @ n the index to split at

463||| @ n the index to split at

462−||| @ xs the Vect to split in two

464+||| @ xs the `Vect` to split in two

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

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

464−splitAt n xs = (take n xs, drop n xs)

466+splitAt Z xs = ([], xs)

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

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

465

469

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

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

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

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

@@ -521,12 +525,14 @@ range : {len : Nat} -> Vect len (Fin len)

521range {len=Z} = []

525range {len=Z} = []

522range {len=S _} = FZ :: map FS range

526range {len=S _} = FZ :: map FS range

523

527

524−||| Transpose a Vect of Vects, turning rows into columns and vice versa.

528+||| Transpose a `Vect` of `Vect`s, turning rows into columns and vice versa.

529+|||

530+||| This is like zipping all the inner `Vect`s together and is equivalent to `traverse id` (`transposeTraverse`).

525|||

531|||

526||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.

532||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.

527−transpose : {n : Nat} -> Vect m (Vect n elem) -> Vect n (Vect m elem)

533+transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)

528−transpose [] = replicate _ []

534+transpose [] = replicate _ [] -- = [| [] |]

529−transpose (x :: xs) = zipWith (::) x (transpose xs)

535+transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]

530

536

531--------------------------------------------------------------------------------

537--------------------------------------------------------------------------------

532-- Applicative/Monad/Traversable

538-- Applicative/Monad/Traversable

@@ -534,7 +540,6 @@ transpose (x :: xs) = zipWith (::) x (transpose xs)

534

540

535implementation Applicative (Vect k) where

541implementation Applicative (Vect k) where

536 pure = replicate _

542 pure = replicate _

537−

538 fs <*> vs = zipWith apply fs vs

543 fs <*> vs = zipWith apply fs vs

539

544

540||| This monad is different from the List monad, (>>=)

545||| This monad is different from the List monad, (>>=)

@@ -543,8 +548,8 @@ implementation Monad (Vect len) where

543 m >>= f = diag (map f m)

548 m >>= f = diag (map f m)

544

549

545implementation Traversable (Vect n) where

550implementation Traversable (Vect n) where

546− traverse f [] = pure Vect.Nil

551+ traverse f [] = [| [] |]

547− traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]

552+ traverse f (x :: xs) = [| f x :: traverse f xs |]

548

553

549--------------------------------------------------------------------------------

554--------------------------------------------------------------------------------

550-- Show

555-- Show

@@ -553,13 +558,29 @@ implementation Traversable (Vect n) where

553implementation Show elem => Show (Vect len elem) where

558implementation Show elem => Show (Vect len elem) where

554 show = show . toList

559 show = show . toList

555

560

561+--------------------------------------------------------------------------------

562+-- Uninhabited

563+--------------------------------------------------------------------------------

564+

565+Uninhabited a => Uninhabited (Vect (S n) a) where

566+ uninhabited (x :: _) = uninhabited x

567+

556--------------------------------------------------------------------------------

568--------------------------------------------------------------------------------

557-- Properties

569-- Properties

558--------------------------------------------------------------------------------

570--------------------------------------------------------------------------------

559

571

572+vectMustBeNil : (xs : Vect Z a) -> xs = []

573+vectMustBeNil [] = Refl

574+

560vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys)

575vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys)

561vectConsCong x xs xs Refl = Refl

576vectConsCong x xs xs Refl = Refl

562

577

578+vectInjective1 : {xs : Vect n a} -> {ys : Vect m b} -> x :: xs ~=~ y :: ys -> x ~=~ y

579+vectInjective1 Refl = Refl

580+

581+vectInjective2 : {xs : Vect n a} -> {ys : Vect m b} -> x :: xs ~=~ y :: ys -> xs ~=~ ys

582+vectInjective2 Refl = Refl

583+

563vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs

584vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs

564vectNilRightNeutral [] = Refl

585vectNilRightNeutral [] = Refl

565vectNilRightNeutral (x :: xs) =

586vectNilRightNeutral (x :: xs) =

@@ -573,16 +594,93 @@ vectAppendAssociative [] y z = Refl

573vectAppendAssociative (x :: xs) ys zs =

594vectAppendAssociative (x :: xs) ys zs =

574 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)

595 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)

575

596

597+||| Adding a prefix and then taking the prefix gets the prefix. Or,

598+||| adding a suffix and then dropping the suffix does nothing.

599+takePrefix : (ns : Vect n a) -> (ms : Vect m a) -> take n (ns ++ ms) = ns

600+takePrefix [] _ = Refl

601+takePrefix (n :: ns) ms = cong $ takePrefix ns ms

602+

603+||| Adding a prefix and then dropping the prefix does nothing. Or,

604+||| adding a suffix and then taking the suffix gets the suffix.

605+dropPrefix : (ns : Vect n a) -> (ms : Vect m a) -> drop n (ns ++ ms) = ms

606+dropPrefix [] ms = Refl

607+dropPrefix (_ :: ns) ms = dropPrefix ns ms

608+

609+||| `take n . take (n + m) = take n`

610+takeTake : (n : Nat) -> (m : Nat) ->

611+ (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->

612+ xs ~=~ ys ->

613+ take n (take (n + m) xs) = take n ys

614+takeTake Z m _ _ _ = Refl

615+takeTake (S n) m (x :: xs) (y :: ys) prf = rewrite vectInjective1 prf in cong (takeTake n m xs ys (vectInjective2 prf))

616+

617+||| `drop (n + m) = drop m . drop n`

618+dropDrop : (n : Nat) -> (m : Nat) ->

619+ (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->

620+ xs ~=~ ys ->

621+ drop (n + m) xs = drop m (drop n ys)

622+dropDrop Z m xs xs Refl = Refl

623+dropDrop (S n) m (_ :: xs) (_ :: ys) prf = dropDrop n m xs ys (vectInjective2 prf)

624+

625+||| A `Vect` may be restored from its components.

626+takeDropConcat : (n : Nat) -> (xs : Vect (n + m) a) -> take n xs ++ drop n xs = xs

627+takeDropConcat Z xs = Refl

628+takeDropConcat (S n) (x :: xs) = cong $ takeDropConcat n xs

629+

630+||| `drop n . take (n + m) = take m . drop n`.

631+|||

632+||| Or: there are two ways to extract a subsequence.

633+dropTakeTakeDrop : (n : Nat) -> (m : Nat) ->

634+ (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->

635+ xs ~=~ ys ->

636+ drop n (take (n + m) xs) = take m (drop n ys)

637+dropTakeTakeDrop Z m xs xs Refl = Refl

638+dropTakeTakeDrop (S n) m (_ :: xs) (_ :: ys) prf = dropTakeTakeDrop n m xs ys (vectInjective2 prf)

639+

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

641+splitAtTakeDrop Z xs = Refl

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

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

647+

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

649+zipWithIsLiftA2 _ [] [] = Refl

650+zipWithIsLiftA2 f (a :: as) (b :: bs) = rewrite zipWithIsLiftA2 f as bs in Refl

651+zipWithIsLiftA3 : (f : a -> b -> c -> d) -> (as : Vect n a) -> (bs : Vect n b) -> (cs : Vect n c) -> zipWith3 f as bs cs = [| f as bs cs |]

652+zipWithIsLiftA3 _ [] [] [] = Refl

653+zipWithIsLiftA3 f (a :: as) (b :: bs) (c :: cs) = rewrite zipWithIsLiftA3 f as bs cs in Refl

654+

655+-- Note relationship to Applicative (Morphism (Fin n))

656+indexReplicate : (x : a) -> (n : Nat) -> (i : Fin n) -> index i (replicate n x) = x

657+indexReplicate x (S n) FZ = Refl

658+indexReplicate x (S n) (FS i) = indexReplicate x n i

659+indexZipWith : (f : a -> b -> c) -> (as : Vect n a) -> (bs : Vect n b) -> (i : Fin n) -> index i (zipWith f as bs) = f (index i as) (index i bs)

660+indexZipWith f (a :: _) (b :: _) FZ = Refl

661+indexZipWith f (_ :: as) (_ :: bs) (FS i) = indexZipWith f as bs i

662+indexTranspose : (x : Fin o) -> (y : Fin i) -> (xss : Vect o (Vect i a)) -> index y (index x xss) = index x (index y (transpose xss))

663+indexTranspose x y (xs :: xss) = rewrite prf in

664+ rewrite sym $ indexZipWith Vect.(::) xs (transpose xss) y in Refl

665+ where prf : index y (index x (xs :: xss)) = index x (index y xs :: index y (transpose xss))

666+ prf = case x of

667+ FZ => Refl

668+ FS k => indexTranspose k y xss

669+

670+transposeTraverse : (xss : Vect o (Vect i a)) -> transpose xss = traverse Basics.id xss

671+transposeTraverse [] = Refl

672+transposeTraverse (xs :: xss) = rewrite zipWithIsLiftA2 Vect.(::) xs (transpose xss) in cong (transposeTraverse xss)

673+

674+traverseIdCons : (xs : Vect o a) -> (xss : Vect o (Vect i a)) -> traverse Basics.id [| xs :: xss |] = xs :: traverse Basics.id xss

675+traverseIdCons [] [] = Refl

676+traverseIdCons (x :: xs) (ys :: xss) = rewrite traverseIdCons xs xss in Refl

677+transposeCons : (xs : Vect o a) -> (xss : Vect o (Vect i a)) -> transpose (zipWith (::) xs xss) = xs :: transpose xss

678+transposeCons xs xss = rewrite zipWithIsLiftA2 Vect.(::) xs xss in rewrite transposeTraverse (pure (::) <*> xs <*> xss) in rewrite transposeTraverse xss in traverseIdCons xs xss

679+

576--------------------------------------------------------------------------------

680--------------------------------------------------------------------------------

577-- DecEq

681-- DecEq

578--------------------------------------------------------------------------------

682--------------------------------------------------------------------------------

579

683

580−vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y

581−vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl

582−

583−vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys

584−vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl

585−

586implementation DecEq a => DecEq (Vect n a) where

684implementation DecEq a => DecEq (Vect n a) where

587 decEq [] [] = Yes Refl

685 decEq [] [] = Yes Refl

588 decEq (x :: xs) (y :: ys) with (decEq x y)

686 decEq (x :: xs) (y :: ys) with (decEq x y)

libs/contrib/Control/Algebra.idr+14

@@ -126,6 +126,20 @@ pow' : RingWithUnity a => a -> Nat -> a

126pow' _ Z = unity

127pow' x (S n) = x <.> pow' x n

128

129+-- TODO: This can be more efficient:

130+-- stimes 5 x = x <+> (x <+> (x <+> (x <+> x)))

131+-- = x <+> ((x <+> x) <+> (x <+> x))

132+-- = let y = x <+> x in x <+> (y <+> y)

133+-- 4 <+>s into 3 <+>

134+||| Combine `n` copies of a value with `<+>`

135+stimes : Semigroup a => (n : Nat) -> {auto prf : IsSucc n} -> a -> a

136+stimes (S Z) x = x

137+stimes (S (S k)) x = x <+> stimes (S k) x

138+

139+||| Like `stimes`, but accepting `Z` as argument.

140+mtimes : Monoid a => (n : Nat) -> a -> a

141+mtimes Z x = neutral

142+mtimes (S k) x = stimes (S k) x

129

143

130-- XXX todo:

144-- XXX todo:

131-- Structures where "abs" make sense.

145-- Structures where "abs" make sense.

libs/contrib/Control/Isomorphism/Extra.idrnew file+42

@@ -0,0 +1,42 @@

1+module Control.Isomorphism.Extra

3+import Control.Isomorphism

4+import Interfaces.Verified

6+%default total

7+%access public export

9+||| Form an `Iso` that is the identity for almost all inputs, except it will swap either of the arguments for the other.

10+||| It is the same function in both directions.

11+|||

12+||| @ l the value that will be turned into `r`

13+||| @ r the value that will be turned into `l`

14+swapped : DecEq a => (l : a) -> (r : a) -> Iso a a

15+swapped {a} l r = MkIso swap swap prf prf

16+ where swap : a -> a

17+ swap x = case decEq l x of { Yes _ => r; No _ => case decEq r x of { Yes _ => l; No _ => x } }

18+ prf : (x : a) -> swap (swap x) = x

19+ prf x with (decEq l x)

20+ | (Yes lex) with (decEq r x)

21+ | (Yes rex) with (decEq l r)

22+ | (Yes ler) = rex

23+ | (No lnr) = absurd $ lnr $ trans lex $ sym rex

24+ | (No rnx) with (decEq l r)

25+ | (Yes ler) = absurd $ rnx $ trans (sym ler) lex

26+ | (No lnr) with (decEq r r)

27+ | (Yes Refl) = lex

28+ | (No rnr) = absurd $ rnr Refl

29+ | (No lnx) with (decEq r x)

30+ | (Yes rex) with (decEq l l)

31+ | (Yes Refl) = rex

32+ | (No lnl) = absurd $ lnl Refl

33+ | (No rnx) with (decEq l x)

34+ | (Yes lex) = absurd $ lnx lex

35+ | (No lnx') with (decEq r x)

36+ | (Yes rex) = absurd $ rnx rex

37+ | (No rnx') = Refl

38+

39+mapIso : VerifiedFunctor f => Iso a b -> Iso (f a) (f b)

40+mapIso {f} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) (prf to from toFrom) (prf from to fromTo)

41+ where prf : {a : Type} -> {b : Type} -> (to : a -> b) -> (from : b -> a) -> (toFrom : (x : b) -> to (from x) = x) -> (x : f b) -> map to (map from x) = x

42+ prf to' from' toFrom' x = rewrite sym $ functorComposition x from' to' in functorIdentity (to' . from') toFrom' x

libs/contrib/Control/Isomorphism/Fin.idrnew file+54

@@ -0,0 +1,54 @@

1+module Control.Isomorphism.Fin

3+import Control.Isomorphism

4+import Data.Fin

6+%default total

7+%access public export

9+strengthenLeft : (i : Fin (S n)) -> (prf : strengthen i = Left x) -> i = Fin.last

10+strengthenLeft {n = Z} FZ Refl = Refl

11+strengthenLeft {n = S _} FZ Refl impossible

12+strengthenLeft {n = S k} (FS x) prf with (strengthen x) proof p

13+ | (Left l) = rewrite strengthenLeft x (sym p) in Refl

14+ | (Right r) = absurd $ leftNotRight $ sym prf

15+strengthenRight : (i : Fin (S n)) -> (prf : strengthen i = Right x) -> weaken x = i

16+strengthenRight {n = Z} FZ Refl impossible

17+strengthenRight {n = S _} FZ Refl = Refl

18+strengthenRight {n = S k} (FS x) prf with (strengthen x) proof p

19+ | (Left l) = absurd $ leftNotRight prf

20+ | (Right r) = rewrite rightInjective $ sym prf in rewrite strengthenRight x $ sym p in Refl

21+strengthenLast : (n : Nat) -> strengthen (last {n=n}) = Left last

22+strengthenLast Z = Refl

23+strengthenLast (S k) with (strengthen (last {n=k})) proof p

24+ | (Left l) = cong {f = Left . FS} $ leftInjective $ trans p $ strengthenLast k

25+ | (Right _) with (trans p (strengthenLast k))

26+ | Refl impossible

27+strengthenWeaken : (n : Fin k) -> strengthen (weaken n) = Right n

28+strengthenWeaken FZ = Refl

29+strengthenWeaken (FS n) with (strengthen (weaken n)) proof p

30+ | (Left _) with (trans p (strengthenWeaken n))

31+ | Refl impossible

32+ | (Right r) = cong {f = Right . FS} $ rightInjective $ trans p $ strengthenWeaken n

33+

34+||| Sends `FZ` to `last`, and `FS x` to `x`.

35+rotatedDown : Iso (Fin n) (Fin n)

36+rotatedDown = MkIso to from toFrom fromTo

37+ where to : Fin k -> Fin k

38+ to FZ = last

39+ to (FS x) = weaken x

40+ from : Fin k -> Fin k

41+ from {k = Z} _ impossible

42+ from {k = S k} j = either (const FZ) FS $ strengthen j

43+ toFrom : (j : Fin k) -> to (from j) = j

44+ toFrom {k = S Z} FZ = Refl

45+ toFrom {k = S (S k)} FZ = Refl

46+ toFrom {k = S (S k)} (FS i) with (strengthen i) proof p

47+ toFrom {k = S (S k)} (FS i) | (Left l) = rewrite strengthenLeft i (sym p) in Refl

48+ toFrom {k = S (S k)} (FS i) | (Right r) = rewrite strengthenRight i (sym p) in Refl

49+ fromTo : (j : Fin k) -> from (to j) = j

50+ fromTo {k = S k} FZ = rewrite strengthenLast k in Refl

51+ fromTo (FS x) = rewrite strengthenWeaken x in Refl

52+||| Sends `last` to `FZ` and every other `x` to `FS x`.

53+rotatedUp : Iso (Fin n) (Fin n)

54+rotatedUp = isoSym rotatedDown

libs/contrib/Control/Isomorphism/Vect.idrnew file+155

@@ -0,0 +1,155 @@

1+module Control.Isomorphism.Vect

3+import Control.Isomorphism

4+import Data.Vect

5+import Interfaces.Verified

7+%default total

8+%access public export

10+||| `Vect Z a` has only one value: `[]`.

11+nilUnit : Iso (Vect Z a) ()

12+nilUnit = MkIso (const ()) (const []) (\() => Refl) (\[] => Refl)

13+

14+||| A `Vect (S Z) a` is just an `a`.

15+oneIdentity : Iso (Vect (S Z) a) a

16+oneIdentity = MkIso to (\x => [x]) (\x => Refl) (\[x] => Refl)

17+ where to : Vect 1 a -> a

18+ to [x] = x

19+

20+||| Moves between `x :: xs` and `(x, xs)`.

21+consPair : Iso (Vect (S n) a) (a, Vect n a)

22+consPair = MkIso to (uncurry (::)) (\(x, xs) => Refl) (\(x :: xs) => Refl)

23+ where to : Vect (S n) a -> (a, Vect n a)

24+ to (x :: xs) = (x, xs)

25+

26+||| An `Iso` based on `splitAt` and `(++)`.

27+splitPair : Iso (Vect (n + m) a) (Vect n a, Vect m a)

28+splitPair {n} {m} = MkIso (splitAt n) (uncurry (++)) toFrom fromTo

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

30+ pairify Refl Refl = Refl

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

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

33+

34+||| An `Iso` based on `zip` and `unzip`.

35+zipped : Iso (Vect n a, Vect n b) (Vect n (a, b))

36+zipped = MkIso (uncurry zip) unzip toFrom (\(as, bs) => fromTo as bs)

37+ where toFrom : {n : Nat} -> (xs : Vect n (a, b)) -> uncurry Vect.zip (unzip xs) = xs

38+ toFrom [] = Refl

39+ toFrom ((a, b) :: xs) with (unzip xs) proof p

40+ | (as, bs) = cong $ trans (cong p) (toFrom xs)

41+ fromTo : {n : Nat} -> (as : Vect n a) -> (bs : Vect n b) -> unzip (zip as bs) = (as, bs)

42+ fromTo [] [] = Refl

43+ fromTo (a :: as) (b :: bs) = rewrite fromTo as bs in Refl

44+

45+||| An `Iso` based on `zip3` and `unzip3`.

46+zipped3 : Iso (Vect n a, Vect n b, Vect n c) (Vect n (a, b, c))

47+zipped3 = MkIso (uncurrry zip3) unzip3 toFrom (\(as, bs, cs) => fromTo as bs cs)

48+ where uncurrry : (w -> x -> y -> z) -> ((w, x, y) -> z)

49+ uncurrry w (x, y, z) = w x y z

50+ toFrom : {n : Nat} -> (xs : Vect n (a, b, c)) -> uncurrry Vect.zip3 (unzip3 xs) = xs

51+ toFrom [] = Refl

52+ toFrom ((a, b, c) :: xs) with (unzip3 xs) proof p

53+ | (as, bs, cs) = cong $ trans (cong p) (toFrom xs)

54+ fromTo : {n : Nat} -> (as : Vect n a) -> (bs : Vect n b) -> (cs : Vect n c) -> unzip3 (zip3 as bs cs) = (as, bs, cs)

55+ fromTo [] [] [] = Refl

56+ fromTo (a :: as) (b :: bs) (c :: cs) = rewrite fromTo as bs cs in Refl

57+

58+||| An `Iso` based on `transpose`.

59+transposition : Iso (Vect o (Vect i a)) (Vect i (Vect o a))

60+transposition {a} = MkIso transpose transpose prf prf

61+ where prf : {i : Nat} -> {o : Nat} -> (xss : Vect o (Vect i a)) -> transpose (transpose xss) = xss

62+ prf [] = vectMustBeNil $ transpose [| [] |]

63+ prf (xs :: xss) = rewrite transposeCons xs (transpose xss) in cong (prf xss)

64+

65+||| Split the `Vect` every `m` elements, making `n` `Vect m a`s.

66+||| The result is rectangular and has the same order as the original.

67+|||

68+||| This is the inverse of `concat`.

69+unconcat : Vect (n * m) a -> Vect n (Vect m a)

70+unconcat {n = Z} [] = []

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

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

73+||| An `Iso` based on `unconcat` and `concat`.

74+|||

75+||| ```idris example

76+||| from rectangular [[1,2,3],[4,5,6]]

77+||| ```

78+rectangular : Iso (Vect (n * m) a) (Vect n (Vect m a))

79+rectangular = MkIso unconcat concat toFrom fromTo

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

81+ toFrom {i = Z} [] = 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)

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

87+ fromTo {i = Z} [] = Refl

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

91+

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

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

94+|||

95+||| Or: turn a function from indices to values into a `Vect`.

96+||| Or: the inverse of `index`.

97+unindex : (Fin n -> a) -> Vect n a

98+unindex {n = Z} _ = []

99+unindex {n = S k} f = f FZ :: unindex (f . FS)

100+

101+||| Indexing into the table of outputs of `f` is like calling `f` itself.

102+indexUnindex : (i : Fin n) -> (f : Fin n -> a) -> index i (unindex f) = f i

103+indexUnindex FZ _ = Refl

104+indexUnindex (FS k) f = rewrite indexUnindex k (f . FS) in Refl

105+||| Given a function `f`, a `Vect` `xs`, and a proof that calling `f` gives the same result as indexing into `xs`,

106+||| prove that `xs` is the table of outputs of `f`.

107+unindexIndex' : (xs : Vect n a) -> (f : Fin n -> a) -> ((i : Fin n) -> f i = index i xs) -> unindex f = xs

108+unindexIndex' [] _ _ = Refl

109+unindexIndex' (x :: xs) f prf = rewrite prf FZ in rewrite unindexIndex' xs (f . FS) (\i => rewrite prf $ FS i in Refl) in Refl

110+||| If `f` and `g` are extensionally equal (equal outputs for all inputs), then `unindex f = unindex g`.

111+congExtUnindex : (f : Fin n -> a) -> (g : Fin n -> a) -> ((i : Fin n) -> f i = g i) -> unindex f = unindex g

112+congExtUnindex f g p = unindexIndex' (unindex g) f $ \i => trans (p i) $ sym $ indexUnindex i g

113+||| Functions with the same tables are the same themselves.

114+injExtUnindex : (f : Fin n -> a) -> (g : Fin n -> a) -> unindex f = unindex g -> ((i : Fin n) -> f i = g i)

115+injExtUnindex f g p i = rewrite sym $ indexUnindex i f in rewrite sym $ indexUnindex i g in cong p

116+||| A simpler version of `unindexIndex'` which only proves that `unindex` is the inverse of `index`.

117+unindexIndex : (xs : Vect n a) -> unindex (\i => index i xs) = xs

118+unindexIndex xs = unindexIndex' xs (\i => index i xs) (\i => Refl)

119+

120+||| Given a function that computes an index in the input from the index in the output, produce a `Vect o` of elements from the input.

121+|||

122+||| This is the map function of the functor `\i => Vect i a` from `\i, o => Fin o -> Fin i` to `\i, o => Vect i a -> Vect o a`.

123+fromIndices : (Fin o -> Fin i) -> Vect i a -> Vect o a

124+fromIndices f xs = unindex (flip index xs . f)

125+indexFromIndices : (f : Fin o -> Fin i) -> (xs : Vect i a) -> (n : Fin o) -> index n (fromIndices f xs) = index (f n) xs

126+indexFromIndices f xs n = indexUnindex n (\i => index (f i) xs)

127+fromIndicesFromIndices : (to : Fin n -> Fin n) -> (from : Fin n -> Fin n) -> (fromTo : (i : Fin n) -> from (to i) = i) -> (xs : Vect n a) -> fromIndices to (fromIndices from xs) = xs

128+fromIndicesFromIndices to from fromTo xs = unindexIndex' xs (\x => index (to x) (unindex (\x' => index (from x') xs))) $ \i =>

129+ rewrite indexUnindex (to i) (\x' => index (from x') xs) in rewrite fromTo i in Refl

130+

131+||| Given a permutation of the indices, provide an `Iso` that can permute a `Vect n` the "same" way. More precisely,

132+||| if the index `i` is sent to `j`, then the element at index `i` ends up at index `j` (`indexPermuted`). An

133+||| `Iso (Fin n) (Fin n)` represents a permutation of the integers `[0, n)` because it ensures that no elements

134+||| are "lost" or "duplicated".

135+|||

136+||| Note this has the *opposite* behavior to `fromIndices`. This function is more "visceral"; it can be imagined

137+||| as shuffling a `Vect` in the same way `map (to permutation)` shuffles `range`. Or, in more categorical terms,

138+||| `fromIndices` represents a contravariant functor from the category `\i, o => Fin i -> Fin o` to `\i, o => Vect i a -> Vect o a`,

139+||| and `permuted` represents that functor restricted to isomorphisms and made covariant with `isoSym`.

140+|||

141+||| ```idris example

142+||| to (permuted (stimes 2 rotatedDown)) [1, 2, 3, 4, 5] == [3, 4, 5, 1, 2]

143+||| to (permuted (swapped 3 0)) [1, 2, 3, 4, 5] == [4, 2, 3, 1, 5]

144+||| ```

145+|||

146+||| @ permutation an `Iso` representing the transformation on the indices

147+permuted : (permutation : Iso (Fin n) (Fin n)) -> Iso (Vect n a) (Vect n a)

148+-- [to, from => f from, f to] is not a typo

149+-- fromIndices needs a function outputIdx => inputIdx, so to "align" the "motion" of the Fins with the elements, to uses from and from uses to.

150+permuted (MkIso toI fromI toFromI fromToI) = MkIso (fromIndices fromI) (fromIndices toI) (fromIndicesFromIndices fromI toI toFromI) (fromIndicesFromIndices toI fromI fromToI)

151+permutedSym : (permutation : Iso (Fin n) (Fin n)) -> permuted (isoSym permutation) = isoSym (permuted permutation)

152+permutedSym (MkIso to from toFrom fromTo) = Refl

153+indexPermuted : (permutation : Iso (Fin n) (Fin n)) -> (i : Fin n) -> (xs : Vect n a) -> index i xs = index (to permutation i) (to (permuted permutation) xs)

154+indexPermuted (MkIso to from toFrom fromTo) i xs = replace {P = \xs' => index i xs' = index (to i) (fromIndices from xs) } (fromIndicesFromIndices to from fromTo xs) $

155+ rewrite indexFromIndices to (fromIndices from xs) i in Refl

libs/contrib/Interfaces/Verified.idr+46−20

@@ -4,8 +4,10 @@ import Control.Algebra

4import Control.Algebra.Lattice

5import Control.Algebra.NumericImplementations

6import Control.Algebra.VectorSpace

7+import Data.Vect

7import Data.ZZ

8import Data.ZZ

10+%default total

9%access public export

11%access public export

11-- Due to these being basically unused and difficult to implement,

13-- Due to these being basically unused and difficult to implement,

@@ -16,17 +18,26 @@ import Data.ZZ

16-- and Monoid).

18-- and Monoid).

18interface Functor f => VerifiedFunctor (f : Type -> Type) where

20interface Functor f => VerifiedFunctor (f : Type -> Type) where

19− functorIdentity : {a : Type} -> (x : f a) -> map Basics.id x = Basics.id x

21+ functorIdentity : {a : Type} -> (g : a -> a) -> ((v : a) -> g v = v) -> (x : f a) -> map g x = x

20 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->

22 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->

21 (g1 : a -> b) -> (g2 : b -> c) ->

23 (g1 : a -> b) -> (g2 : b -> c) ->

22 map (g2 . g1) x = (map g2 . map g1) x

24 map (g2 . g1) x = (map g2 . map g1) x

26+functorIdentity' : VerifiedFunctor f => (x : f a) -> map Basics.id x = x

27+functorIdentity' {f} = functorIdentity {f} id (\x => Refl)

28+

24VerifiedFunctor Maybe where

29VerifiedFunctor Maybe where

25− functorIdentity Nothing = Refl

30+ functorIdentity _ _ Nothing = Refl

26− functorIdentity (Just x) = Refl

31+ functorIdentity g p (Just x) = rewrite p x in Refl

27 functorComposition Nothing g1 g2 = Refl

32 functorComposition Nothing g1 g2 = Refl

28 functorComposition (Just x) g1 g2 = Refl

33 functorComposition (Just x) g1 g2 = Refl

35+VerifiedFunctor (Vect n) where

36+ functorIdentity _ _ [] = Refl

37+ functorIdentity g p (x :: xs) = rewrite p x in cong (functorIdentity g p xs)

38+ functorComposition [] _ _ = Refl

39+ functorComposition (x :: xs) f g = rewrite functorComposition xs f g in Refl

40+

30interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where

41interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where

31 applicativeMap : (x : f a) -> (g : a -> b) ->

42 applicativeMap : (x : f a) -> (g : a -> b) ->

32 map g x = pure g <*> x

43 map g x = pure g <*> x

@@ -38,6 +49,21 @@ interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type ->

38 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->

49 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->

39 g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g

50 g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g

52+VerifiedApplicative (Vect n) where

53+ applicativeMap [] f = Refl

54+ applicativeMap (x :: xs) f = rewrite applicativeMap xs f in Refl

55+ applicativeIdentity xs = rewrite sym $ applicativeMap xs id in functorIdentity' xs

56+ applicativeComposition [] [] [] = Refl

57+ applicativeComposition (x :: xs) (f :: fs) (g :: gs) = rewrite applicativeComposition xs fs gs in Refl

58+ applicativeHomomorphism = prf

59+ where prf : with Vect ((x : a) -> (f : a -> b) -> zipWith Basics.apply (replicate m f) (replicate m x) = replicate m (f x))

60+ prf {m = Z} x f = Refl

61+ prf {m = S k} x f = rewrite prf {m = k} x f in Refl

62+ applicativeInterchange = prf

63+ 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)

64+ prf {m = Z} x [] = Refl

65+ prf {m = S k} x (f :: fs) = rewrite prf x fs in Refl

66+

41VerifiedApplicative Maybe where

67VerifiedApplicative Maybe where

42 applicativeMap Nothing g = Refl

68 applicativeMap Nothing g = Refl

43 applicativeMap (Just x) g = Refl

69 applicativeMap (Just x) g = Refl

@@ -77,7 +103,7 @@ VerifiedMonad Maybe where

77 monadAssociativity (Just x) f g = Refl

103 monadAssociativity (Just x) f g = Refl

104

79interface Semigroup a => VerifiedSemigroup a where

105interface Semigroup a => VerifiedSemigroup a where

80− total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r

106+ semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r

107

82implementation VerifiedSemigroup (List a) where

108implementation VerifiedSemigroup (List a) where

83 semigroupOpIsAssociative = appendAssociative

109 semigroupOpIsAssociative = appendAssociative

@@ -95,8 +121,8 @@ implementation VerifiedSemigroup (List a) where

95 semigroupOpIsAssociative = multAssociativeZ

121 semigroupOpIsAssociative = multAssociativeZ

122

97interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where

123interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where

98− total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l

124+ monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l

99− total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r

125+ monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r

100

126

101[PlusNatMonoidV] VerifiedMonoid Nat using PlusNatSemiV, PlusNatMonoid where

127[PlusNatMonoidV] VerifiedMonoid Nat using PlusNatSemiV, PlusNatMonoid where

102 monoidNeutralIsNeutralL = plusZeroRightNeutral

128 monoidNeutralIsNeutralL = plusZeroRightNeutral

@@ -119,8 +145,8 @@ implementation VerifiedMonoid (List a) where

119 monoidNeutralIsNeutralR xs = Refl

145 monoidNeutralIsNeutralR xs = Refl

120

146

121interface (VerifiedMonoid a, Group a) => VerifiedGroup a where

147interface (VerifiedMonoid a, Group a) => VerifiedGroup a where

122− total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral

148+ groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral

123− total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral

149+ groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral

124

150

125VerifiedGroup ZZ using PlusZZMonoidV where

151VerifiedGroup ZZ using PlusZZMonoidV where

126 groupInverseIsInverseL k = rewrite sym $ multCommutativeZ (NegS 0) k in

152 groupInverseIsInverseL k = rewrite sym $ multCommutativeZ (NegS 0) k in

@@ -133,15 +159,15 @@ VerifiedGroup ZZ using PlusZZMonoidV where

133 plusNegateInverseRZ k

159 plusNegateInverseRZ k

134

160

135interface (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where

161interface (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where

136− total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l

162+ abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l

137

163

138VerifiedAbelianGroup ZZ where

164VerifiedAbelianGroup ZZ where

139 abelianGroupOpIsCommutative = plusCommutativeZ

165 abelianGroupOpIsCommutative = plusCommutativeZ

140

166

141interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

167interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

142− total ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r

168+ ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r

143− total ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)

169+ ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)

144− total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)

170+ ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)

145

171

146VerifiedRing ZZ where

172VerifiedRing ZZ where

147 ringOpIsAssociative = multAssociativeZ

173 ringOpIsAssociative = multAssociativeZ

@@ -149,19 +175,19 @@ VerifiedRing ZZ where

149 ringOpIsDistributiveR = multDistributesOverPlusLeftZ

175 ringOpIsDistributiveR = multDistributesOverPlusLeftZ

150

176

151interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where

177interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where

152− total ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l

178+ ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l

153− total ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r

179+ ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r

154

180

155VerifiedRingWithUnity ZZ where

181VerifiedRingWithUnity ZZ where

156 ringWithUnityIsUnityL = multOneRightNeutralZ

182 ringWithUnityIsUnityL = multOneRightNeutralZ

157 ringWithUnityIsUnityR = multOneLeftNeutralZ

183 ringWithUnityIsUnityR = multOneLeftNeutralZ

158

184

159interface JoinSemilattice a => VerifiedJoinSemilattice a where

185interface JoinSemilattice a => VerifiedJoinSemilattice a where

160− total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r

186+ joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r

161− total joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l

187+ joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l

162− total joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e

188+ joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e

163

189

164interface MeetSemilattice a => VerifiedMeetSemilattice a where

190interface MeetSemilattice a => VerifiedMeetSemilattice a where

165− total meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r

191+ meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r

166− total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l

192+ meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l

167− total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e

193+ meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e

libs/contrib/contrib.ipkg+5

@@ -12,7 +12,12 @@ modules = CFFI

12 , Control.Algebra.VectorSpace

14 , Control.Delayed

15+

16+ , Control.Isomorphism.Extra

17+ , Control.Isomorphism.Fin

15 , Control.Isomorphism.Primitives

18 , Control.Isomorphism.Primitives

19+ , Control.Isomorphism.Vect

20+

16 , Control.Monad.Syntax

21 , Control.Monad.Syntax

17 , Control.Partial

22 , Control.Partial

18 , Control.Pipeline

23 , Control.Pipeline

libs/prelude/Prelude/Algebra.idr−2

@@ -18,7 +18,6 @@ infixl 6 <+>

18interface Semigroup ty where

19 (<+>) : ty -> ty -> ty

21−

22||| Sets equipped with a single binary operation that is associative, along with

21||| Sets equipped with a single binary operation that is associative, along with

23||| a neutral element for that binary operation. Must satisfy the following

22||| a neutral element for that binary operation. Must satisfy the following

24||| laws:

23||| laws:

@@ -30,4 +29,3 @@ interface Semigroup ty where

30||| forall a, neutral <+> a == a

29||| forall a, neutral <+> a == a

31interface Semigroup ty => Monoid ty where

30interface Semigroup ty => Monoid ty where

32 neutral : ty

31 neutral : ty

33−

libs/prelude/Prelude/List.idr+19−5

@@ -675,13 +675,18 @@ split p xs =

675 (chunk, []) => [chunk]

676 (chunk, (c :: rest)) => chunk :: split p (assert_smaller xs rest)

677

678−||| A tuple where the first element is a List of the n first elements and

678+||| A tuple where the first element is a `List` of the `n` first elements and

679−||| the second element is a List of the remaining elements of the list

679+||| the second element is a `List` of the remaining elements of the original.

680−||| It is equivalent to (take n xs, drop n xs)

680+||| It is equivalent to `(take n xs, drop n xs)` (`splitAtTakeDrop`),

681+||| but is more efficient.

682+|||

681||| @ n the index to split at

683||| @ n the index to split at

682−||| @ xs the list to split in two

684+||| @ xs the `List` to split in two

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

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

684−splitAt n xs = (take n xs, drop n xs)

686+splitAt Z xs = ([], xs)

687+splitAt (S k) [] = ([], [])

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

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

685

690

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

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

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

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

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

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

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

932foldlMatchesFoldr f q [] = Refl

937foldlMatchesFoldr f q [] = Refl

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

938foldlMatchesFoldr 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

test/disambig002/disambig002.idr−5

@@ -19,11 +19,6 @@ Unique0 = Unique

19Unique1 : (t0 -> Type) -> Type

20Unique1 {t0} t1 = (v : t0) -> Unique0 (t1 v)

22−namespace Iso

23−

24− from : {A, B : Type} -> Iso A B -> (B -> A)

25− from (MkIso to from toFrom fromTo) = from

26−

27namespace Fin

22namespace Fin

29 ||| 'Tail' of a finite function

24 ||| 'Tail' of a finite function