0 | ||| Additional properties/lemmata of Nats involving order
  1 | module Data.Nat.Order.Properties
  2 |
  3 | import Syntax.PreorderReasoning.Generic
  4 | import Data.Nat
  5 | import Data.Bool.Decidable
  6 |
  7 |
  8 | %default total
  9 | export
 10 | LTESuccInjectiveMonotone : (m, n : Nat) -> Reflects (m `LTE` n) b -> Reflects (S m `LTE` S n) b
 11 | LTESuccInjectiveMonotone m n (RTrue      m_lte_n) = RTrue  $ LTESucc m_lte_n
 12 | LTESuccInjectiveMonotone m n (RFalse not_m_lte_n) = RFalse $ \case
 13 |                                                                LTESucc m_lte_n => not_m_lte_n m_lte_n
 14 |
 15 | export
 16 | lteReflection : (a, b : Nat) -> Reflects (a `LTE` b) (a `lte` b)
 17 | lteReflection 0 b = RTrue LTEZero
 18 | lteReflection (S k) 0 = RFalse $ \sk_lte_z => absurd sk_lte_z
 19 | lteReflection (S a) (S b) = LTESuccInjectiveMonotone a b (lteReflection a b)
 20 |
 21 | export
 22 | ltReflection : (a, b : Nat) -> Reflects (a `LT` b) (a `lt` b)
 23 | ltReflection a = lteReflection (S a)
 24 |
 25 | -- For example:
 26 | export
 27 | lteIsLTE : (a, b : Nat) -> a `lte` b = True -> a `LTE` b
 28 | lteIsLTE  a b prf = invert (replace {p = Reflects (a `LTE` b)} prf (lteReflection a b))
 29 |
 30 | export
 31 | ltIsLT : (a, b : Nat) -> a `lt` b = True -> a `LT` b
 32 | ltIsLT  a = lteIsLTE (S a)
 33 |
 34 | export
 35 | notlteIsNotLTE : (a, b : Nat) -> a `lte` b = False -> Not (a `LTE` b)
 36 | notlteIsNotLTE a b prf = invert (replace {p = Reflects (a `LTE` b)} prf (lteReflection a b))
 37 |
 38 | export
 39 | notltIsNotLT : (a, b : Nat) -> a `lt` b = False -> Not (a `LT` b)
 40 | notltIsNotLT a = notlteIsNotLTE (S a)
 41 |
 42 |
 43 | export
 44 | notlteIsLT : (a, b : Nat) -> a `lte` b = False -> b `LT` a
 45 | notlteIsLT a b prf = notLTImpliesGTE $
 46 |                        \prf' =>
 47 |                          (invert $ replace {p = Reflects (S a `LTE` S b)} prf
 48 |                                  $ lteReflection (S a) (S b)) prf'
 49 |
 50 | export
 51 | notltIsGTE : (a, b : Nat) -> (a `lt` b) === False -> a `GTE` b
 52 | notltIsGTE a b p = notLTImpliesGTE (notlteIsNotLTE (S a) b p)
 53 |
 54 |
 55 | -- The converse to lteIsLTE:
 56 | export
 57 | LteIslte : (a, b : Nat) -> a `LTE` b -> a `lte` b = True
 58 | LteIslte  a b a_lt_b = reflect (lteReflection a b) a_lt_b
 59 |
 60 | -- The converse to lteIsLTE with negation
 61 | export
 62 | notLteIsnotlte : (a, b : Nat) -> Not (a `LTE` b) -> a `lte` b = False
 63 | notLteIsnotlte a b not_a_lte_b = reflect (lteReflection a b) not_a_lte_b
 64 |
 65 | -- The converse to lteIsLTE:
 66 | export
 67 | GTIsnotlte : (a, b : Nat) -> b `LT` a -> a `lte` b = False
 68 | GTIsnotlte a b prf =
 69 |   notLteIsnotlte a b $ \contra =>
 70 |     succNotLTEpred $ transitive prf contra
 71 |
 72 | ||| Subtracting a number gives a smaller number
 73 | export
 74 | minusLTE : (a,b : Nat) -> (b `minus` a) `LTE` b
 75 | minusLTE a      0    = LTEZero
 76 | minusLTE 0     (S _) = reflexive
 77 | minusLTE (S a) (S b) =
 78 |   transitive
 79 |     (minusLTE a b)
 80 |     (lteSuccRight reflexive)
 81 |
 82 | ||| Subtracting a positive number gives a strictly smaller number
 83 | export
 84 | minusPosLT : (a,b : Nat) -> 0 `LT` a -> a `LTE` b -> (b `minus` a) `LT` b
 85 | minusPosLT 0     b     z_lt_z           a_lte_b impossible
 86 | minusPosLT (S a) 0     z_lt_sa          a_lte_b impossible
 87 | minusPosLT (S a) (S b) z_lt_sa          a_lte_b = LTESucc (minusLTE a b)
 88 |
 89 | -- This is the opposite of the convention in `Data.Nat`, but 'monotone on the left' means the below
 90 | export
 91 | multLteMonotoneRight : (l, a, b : Nat) -> a `LTE` b -> l*a `LTE` l*b
 92 | multLteMonotoneRight  0    a b _ = LTEZero
 93 | multLteMonotoneRight (S k) a b a_lte_b = CalcWith {leq = LTE} $
 94 |   |~ (1 + k) * a
 95 |   ~~ a +  k*a    ...(Refl)
 96 |   <~ b +  k*a    ...(plusLteMonotoneRight (k*a) a b a_lte_b)
 97 |   <~ b +  k*b    ...(plusLteMonotoneLeft  b (k*a) (k*b) $
 98 |                      multLteMonotoneRight k    a     b   a_lte_b)
 99 |   ~~ (1 + k) * b ...(Refl)
100 |
101 | export
102 | multLteMonotoneLeft : (a, b, r : Nat) -> a `LTE` b -> a*r `LTE` b*r
103 | multLteMonotoneLeft a b r a_lt_b =
104 |   rewrite multCommutative a r in
105 |   rewrite multCommutative b r in
106 |   multLteMonotoneRight r a b a_lt_b
107 |
108 | export
109 | lteNotLtEq : (a, b : Nat) -> LTE a b -> Not (LT a b) -> a = b
110 | lteNotLtEq a b a_lte_b not_n_lte_n =
111 |   let b_lte_a = notLTImpliesGTE not_n_lte_n
112 |   in antisymmetric a_lte_b b_lte_a
113 |
114 | -- Try succ left element LTE. Returns LT if successful, otherwise proof of equality a and b
115 | export
116 | decomposeLte : (a, b : Nat) -> LTE a b -> Either (LT a b) (a = b)
117 | decomposeLte a b a_lte_b with (isLT a b)
118 |   decomposeLte a b a_lte_b | Yes a_lt_b = Left a_lt_b
119 |   decomposeLte a b a_lte_b | No not_a_lt_b = Right $ lteNotLtEq a b a_lte_b not_a_lt_b
120 |