0 | ||| This contains additional proofs on natural number.
 1 | module Data.Nat.BSExtra
 2 |
 3 | import public Data.Array.Index
 4 |
 5 | %default total
 6 |
 7 | export
 8 | 0 ltPlusRight : {k,m,n : Nat} -> LT m n -> LT (k + m) (k + n)
 9 | ltPlusRight {k = 0}   x = x
10 | ltPlusRight {k = S _} x = LTESucc $ ltPlusRight x
11 |
12 | export
13 | 0 ltePlusSuccRight : {k,m,n : Nat} -> LTE (k + S m) n -> LTE (S $ k + m) n
14 | ltePlusSuccRight p = rewrite plusSuccRightSucc k m in p
15 |
16 | export
17 | 0 ltePlusRight : (o : Nat) -> LTE m n -> LTE (o + m) (o + n)
18 | ltePlusRight 0     lt = lt
19 | ltePlusRight (S k) lt = LTESucc $ ltePlusRight k lt
20 |
21 | export
22 | 0 ltPlusSuccRight' : (k : Nat) -> LTE (k + S m) n -> LT m n
23 | ltPlusSuccRight' 0     p           = p
24 | ltPlusSuccRight' (S x) (LTESucc p) =
25 |   lteSuccRight $ ltPlusSuccRight' x p
26 |
27 | export
28 | 0 plusMinus' : (m,n : Nat) -> LTE m n -> (n `minus` m) + m === n
29 | plusMinus' m n lt = trans (plusCommutative (n `minus` m) m) (plusMinus m n lt)
30 |
31 | export
32 | 0 lteAddLeft : (x : Nat) -> LTE m n -> LTE m (x + n)
33 | lteAddLeft 0 y = y
34 | lteAddLeft (S k) y = lteSuccRight $ lteAddLeft k y
35 |
36 | export
37 | 0 lteAddRight : (x : Nat) -> LTE m n -> LTE m (n + x)
38 | lteAddRight x lt = rewrite plusCommutative n x in lteAddLeft x lt
39 |
40 | export
41 | 0 concatLemma1 : {0 k,m,n : Nat} -> LTE (k + m) (k + (m+n))
42 | concatLemma1 = rewrite plusAssociative k m n in lteAddRight _
43 |
44 | export
45 | 0 concatLemma2 : {0 l,k,m,n : Nat} -> l+(k+m) === n -> (l+k)+m === n
46 | concatLemma2 p1 = trans (sym $ plusAssociative l k m) p1
47 |
48 | export
49 | 0 lteMinus : (n : Nat) -> LTE (S (minus n 0)) (S n)
50 | lteMinus n = rewrite minusZeroRight n in reflexive
51 |
52 | export
53 | 0 minusLT : (m,n : Nat) -> (lt : LT m n) -> LT (minus n (S m)) n
54 | minusLT 0     (S l) lt           = lteMinus l
55 | minusLT (S k) (S l) (LTESucc lt) =
56 |   let lt' := minusLT k l lt in lteSuccRight lt'
57 | minusLT Z     Z     lt impossible
58 |