git.iko.soy/Idris-dev
on master help sign in
Tidy up accessibility proofs in views
3408098Edwin Brady
libs/base/Data/List/Views.idr+1−2
compare with master
unifiedsplit
@@ -70,8 +70,7 @@ splitRecFix xs srec with (split xs)
70||| Covering function for the `SplitRec` view
70||| Covering function for the `SplitRec` view
71export total
71export total
72splitRec : (xs : List a) -> SplitRec xs
72splitRec : (xs : List a) -> SplitRec xs
73−splitRec [] = SplitRecNil
74−splitRec (x :: xs) = accInd splitRecFix (x :: xs) (smallerAcc (x :: x :: xs) lteRefl)
73+splitRec xs = accInd splitRecFix xs (smallerAcc xs)
75
74
76||| View for traversing a list backwards
75||| View for traversing a list backwards
77public export
76public export
libs/base/Data/Nat/Views.idr+1−5
@@ -1,9 +1,5 @@
1module Data.Nat.Views
1module Data.Nat.Views
2
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−
7public export
3public export
8data Half : Nat -> Type where
4data Half : Nat -> Type where
9 HalfOdd : Half (S (n + n))
5 HalfOdd : Half (S (n + n))
@@ -34,5 +30,5 @@ halfRecFix (S k) hrec with (half k)
34
30
35export
31export
36halfRec : (n : Nat) -> HalfRec n
32halfRec : (n : Nat) -> HalfRec n
37−halfRec n = accInd halfRecFix n (ltAcc (S n) (LTESucc lteRefl))
33+halfRec n = accInd halfRecFix n (ltAccessible n)
38
34
libs/prelude/Prelude/WellFounded.idr+15−8
@@ -88,18 +88,25 @@ wfInd {rel} step x = accInd step x (wellFounded {rel} x)
88-- Some basic useful relations
88-- Some basic useful relations
89
89
90||| LT is a well-founded relation on numbers
90||| LT is a well-founded relation on numbers
91+ltAccessible : (n : Nat) -> Accessible LT n
92+ltAccessible n = Access (\v, prf => ltAccessible' {n'=v} n prf)
93+ where
91−ltAccessible : (m : Nat) -> LT n m -> Accessible LT n
94+ ltAccessible' : (m : Nat) -> LT n' m -> Accessible LT n'
92−ltAccessible Z x = absurd x
95+ ltAccessible' Z x = absurd x
93−ltAccessible (S k) (LTESucc x)
96+ ltAccessible' (S k) (LTESucc x)
94− = Access (\val, p => ltAccessible k (lteTransitive p x))
97+ = Access (\val, p => ltAccessible' k (lteTransitive p x))
95
98
96-- First list is smaller than the second
99-- First list is smaller than the second
97smaller : List a -> List a -> Type
100smaller : List a -> List a -> Type
98smaller xs ys = LT (length xs) (length ys)
101smaller xs ys = LT (length xs) (length ys)
99
102
100||| `smaller` is a well-founded relation on lists
103||| `smaller` is a well-founded relation on lists
104+smallerAcc : (xs : List a) -> Accessible WellFounded.smaller xs
105+smallerAcc xs = Access (\v, prf => smallerAcc' {xs'=v} xs prf)
106+ where
101−smallerAcc : (ys : List a) -> smaller xs ys -> Accessible smaller xs
107+ smallerAcc' : (ys : List a) -> smaller xs' ys -> Accessible smaller xs'
102−smallerAcc [] x = absurd x
108+ smallerAcc' [] x = absurd x
103−smallerAcc (y :: ys) (LTESucc x)
109+ smallerAcc' (y :: ys) (LTESucc x)
104− = Access (\val, p => smallerAcc ys (lteTransitive p x))
110+ = Access (\val, p => smallerAcc' ys (lteTransitive p x))
111+
105
112