git.iko.soy/Idris-dev
on master help sign in
Add Data.Nat.Views to base
d7b7e25Edwin Brady
idris.cabal+1
compare with master
unifiedsplit
@@ -113,6 +113,7 @@ Extra-source-files:
113 libs/base/Control/*.idr
113 libs/base/Control/*.idr
114 libs/base/Control/Monad/*.idr
114 libs/base/Control/Monad/*.idr
115 libs/base/Data/*.idr
115 libs/base/Data/*.idr
116+ libs/base/Data/Nat/*.idr
116 libs/base/Data/List/*.idr
117 libs/base/Data/List/*.idr
117 libs/base/Data/Vect/*.idr
118 libs/base/Data/Vect/*.idr
118 libs/base/Debug/*.idr
119 libs/base/Debug/*.idr
libs/base/Data/List/Views.idr−23
@@ -2,29 +2,6 @@ module Data.List.Views
2
2
3import Data.List
3import Data.List
4
4
5−-- First list is smaller than the second
6−smaller : List a -> List a -> Type
7−smaller xs ys = LT (length xs) (length ys)
8−
9−-- Some proofs to help us out with recursion later
10−ltS : LTE (S x) y -> LTE x y
11−ltS (LTESucc x) = lteSuccRight x
12−
13−total
14−ltTrans : LTE n m -> LTE m p -> LTE n p
15−ltTrans LTEZero y = LTEZero
16−ltTrans (LTESucc x) (LTESucc y) = LTESucc (ltTrans x y)
17−
18−ltZimpossible : (x : smaller xs []) -> Accessible smaller xs
19−ltZimpossible LTEZero impossible
20−ltZimpossible (LTESucc _) impossible
21−
22−total
23−smallerAcc : (ys : List a) -> smaller xs ys -> Accessible smaller xs
24−smallerAcc [] x = ltZimpossible x
25−smallerAcc (y :: ys) (LTESucc x)
26− = Access (\val, p => smallerAcc ys (ltTrans p x))
27−
28lengthSuc : (xs : List a) -> (y : a) -> (ys : List a) ->
5lengthSuc : (xs : List a) -> (y : a) -> (ys : List a) ->
29 length (xs ++ (y :: ys)) = S (length (xs ++ ys))
6 length (xs ++ (y :: ys)) = S (length (xs ++ ys))
30lengthSuc [] _ _ = Refl
7lengthSuc [] _ _ = Refl
libs/base/Data/Nat/Views.idrnew file+38
@@ -0,0 +1,38 @@
1+module Data.Nat.Views
2+
3+ltAcc : (m : Nat) -> LT n m -> Accessible LT n
4+ltAcc Z x = absurd x
5+ltAcc (S k) (LTESucc x) = Access (\val, p => ltAcc k (lteTransitive p x))
6+
7+public export
8+data Half : Nat -> Type where
9+ HalfOdd : Half (S (n + n))
10+ HalfEven : Half (n + n)
11+
12+public export
13+data HalfRec : Nat -> Type where
14+ HalfRecZ : HalfRec 0
15+ HalfRecEven : Lazy (HalfRec n) -> HalfRec (n + n)
16+ HalfRecOdd : Lazy (HalfRec n) -> HalfRec (S (n + n))
17+
18+export
19+half : (n : Nat) -> Half n
20+half Z = HalfEven {n=0}
21+half (S k) with (half k)
22+ half (S (S (n + n))) | HalfOdd = rewrite plusSuccRightSucc (S n) n in
23+ HalfEven {n=S n}
24+ half (S (n + n)) | HalfEven = HalfOdd
25+
26+halfRecFix : (n : Nat) -> ((m : Nat) -> LT m n -> HalfRec m) -> HalfRec n
27+halfRecFix Z hrec = HalfRecZ
28+halfRecFix (S k) hrec with (half k)
29+ halfRecFix (S (S (n + n))) hrec | HalfOdd
30+ = rewrite plusSuccRightSucc (S n) n in
31+ HalfRecEven (hrec (S n) (LTESucc (LTESucc (lteAddRight _))))
32+ halfRecFix (S (n + n)) hrec | HalfEven
33+ = HalfRecOdd (hrec n (LTESucc (lteAddRight _)))
34+
35+export
36+halfRec : (n : Nat) -> HalfRec n
37+halfRec n = accInd halfRecFix n (ltAcc (S n) (LTESucc lteRefl))
38+
libs/base/base.ipkg+1
@@ -18,6 +18,7 @@ modules = System,
18 Data.Complex,
18 Data.Complex,
19 Data.Erased, Data.List, Data.List.Views,
19 Data.Erased, Data.List, Data.List.Views,
20 Data.List.Quantifiers,
20 Data.List.Quantifiers,
21+ Data.Nat.Views,
21 Data.So, Data.String,
22 Data.So, Data.String,
22
23
23 Control.Isomorphism,
24 Control.Isomorphism,
libs/prelude/Prelude/Nat.idr+13
@@ -141,6 +141,19 @@ lteSuccRight : LTE n m -> LTE n (S m)
141lteSuccRight LTEZero = LTEZero
141lteSuccRight LTEZero = LTEZero
142lteSuccRight (LTESucc x) = LTESucc (lteSuccRight x)
142lteSuccRight (LTESucc x) = LTESucc (lteSuccRight x)
143
143
144+||| n + 1 < m implies n < m
145+lteSuccLeft : LTE (S n) m -> LTE n m
146+lteSuccLeft (LTESucc x) = lteSuccRight x
147+
148+||| `LTE` is transitive
149+lteTransitive : LTE n m -> LTE m p -> LTE n p
150+lteTransitive LTEZero y = LTEZero
151+lteTransitive (LTESucc x) (LTESucc y) = LTESucc (lteTransitive x y)
152+
153+lteAddRight : (n : Nat) -> LTE n (plus n m)
154+lteAddRight Z = LTEZero
155+lteAddRight (S k) = LTESucc (lteAddRight k)
156+
144
157
145||| Boolean test than one Nat is less than or equal to another
158||| Boolean test than one Nat is less than or equal to another
146total lte : Nat -> Nat -> Bool
159total lte : Nat -> Nat -> Bool
libs/prelude/Prelude/WellFounded.idr+22
@@ -5,6 +5,10 @@
5||| other metric of size.
5||| other metric of size.
6module Prelude.WellFounded
6module Prelude.WellFounded
7
7
8+import Prelude.Nat
9+import Prelude.List
10+import Prelude.Uninhabited
11+
8%default total
12%default total
9%access public export
13%access public export
10
14
@@ -81,3 +85,21 @@ wfInd : WellFounded rel => {P : a -> Type} ->
81 (x : a) -> P x
85 (x : a) -> P x
82wfInd {rel} step x = accInd step x (wellFounded {rel} x)
86wfInd {rel} step x = accInd step x (wellFounded {rel} x)
83
87
88+-- Some basic useful relations
89+
90+||| LT is a well-founded relation on numbers
91+ltAccessible : (m : Nat) -> LT n m -> Accessible LT n
92+ltAccessible Z x = absurd x
93+ltAccessible (S k) (LTESucc x)
94+ = Access (\val, p => ltAccessible k (lteTransitive p x))
95+
96+-- First list is smaller than the second
97+smaller : List a -> List a -> Type
98+smaller xs ys = LT (length xs) (length ys)
99+
100+||| `smaller` is a well-founded relation on lists
101+smallerAcc : (ys : List a) -> smaller xs ys -> Accessible smaller xs
102+smallerAcc [] x = absurd x
103+smallerAcc (y :: ys) (LTESucc x)
104+ = Access (\val, p => smallerAcc ys (lteTransitive p x))
105+