git.iko.soy/Idris-dev
on master help sign in
Add Data.Nat.Views to base

Also a couple of useful well-founded relations in Prelude.WellFounded, which we use in making views

commitd7b7e25a57dd4e6e7dfee4390871d9da9f8b242a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 10 Apr 2016, 15:11 (11 years ago) parent4079f54
6 files changed+75−23
compare with master
unifiedsplit
idris.cabal+1 libs/base/Data/List/Views.idr−23 libs/base/Data/Nat/Views.idr+38 libs/base/base.ipkg+1 libs/prelude/Prelude/Nat.idr+13 libs/prelude/Prelude/WellFounded.idr+22
idris.cabal+1
@@ -113,6 +113,7 @@ Extra-source-files:
113113 libs/base/Control/*.idr
114114 libs/base/Control/Monad/*.idr
115115 libs/base/Data/*.idr
116+ libs/base/Data/Nat/*.idr
116117 libs/base/Data/List/*.idr
117118 libs/base/Data/Vect/*.idr
118119 libs/base/Debug/*.idr
libs/base/Data/List/Views.idr−23
@@ -2,29 +2,6 @@ module Data.List.Views
22
33import Data.List
44
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−
285lengthSuc : (xs : List a) -> (y : a) -> (ys : List a) ->
296 length (xs ++ (y :: ys)) = S (length (xs ++ ys))
307lengthSuc [] _ _ = 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,
1818 Data.Complex,
1919 Data.Erased, Data.List, Data.List.Views,
2020 Data.List.Quantifiers,
21+ Data.Nat.Views,
2122 Data.So, Data.String,
2223
2324 Control.Isomorphism,
libs/prelude/Prelude/Nat.idr+13
@@ -141,6 +141,19 @@ lteSuccRight : LTE n m -> LTE n (S m)
141141lteSuccRight LTEZero = LTEZero
142142lteSuccRight (LTESucc x) = LTESucc (lteSuccRight x)
143143
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+
144157
145158||| Boolean test than one Nat is less than or equal to another
146159total lte : Nat -> Nat -> Bool
libs/prelude/Prelude/WellFounded.idr+22
@@ -5,6 +5,10 @@
55||| other metric of size.
66module Prelude.WellFounded
77
8+import Prelude.Nat
9+import Prelude.List
10+import Prelude.Uninhabited
11+
812%default total
913%access public export
1014
@@ -81,3 +85,21 @@ wfInd : WellFounded rel => {P : a -> Type} ->
8185 (x : a) -> P x
8286wfInd {rel} step x = accInd step x (wellFounded {rel} x)
8387
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+