0 | module Algebra.OrderedRing
  1 |
  2 | import Algebra.Solver.Ring
  3 | import Control.Relation.ReflexiveClosure
  4 | import Control.Relation.Trichotomy
  5 | import Syntax.PreorderReasoning.Generic
  6 |
  7 | %default total
  8 |
  9 | public export
 10 | record OrderedRing (a : Type) (lt : a -> a -> Type) (z,o : a) (p,m,sub : Op2 a) where
 11 |   constructor MkOR
 12 |   ring   : Ring a z o p m sub
 13 |   strict : Strict a lt
 14 |   add    : {u,v,w : a} -> lt u v -> lt (p u w) (p v w)
 15 |   mult   : {u,v,w : a} -> lt u v -> lt z w -> lt (m u w) (m v w)
 16 |
 17 | parameters {0 a : Type}
 18 |            {0 lt : a -> a -> Type}
 19 |            {0 z,o : a}
 20 |            {0 p,m,sub : Op2 a}
 21 |            (0 r : OrderedRing a lt z o p m sub)
 22 |
 23 |   ||| Adding a value on the right does not affect an inequality.
 24 |   export
 25 |   0 plusRight :  {u,v,w : a} -> lt u v -> lt (p u w) (p v w)
 26 |   plusRight prf = r.add prf
 27 |
 28 |   ||| Adding a value on the left does not affect an inequality.
 29 |   export
 30 |   0 plusLeft : {u,v,w : a} -> lt u v -> lt (p w u) (p w v)
 31 |   plusLeft {u} {v} {w} prf = CalcSmart {leq = lt} $
 32 |     |~ p w u
 33 |     ~~ p u w ... r.ring.plus.commutative
 34 |     <~ p v w ..> plusRight prf
 35 |     ~~ p w v ... r.ring.plus.commutative
 36 |
 37 |   ||| The result of adding a positive value is greater than
 38 |   ||| the original.
 39 |   export
 40 |   0 plusPosRight : {u,v : a} -> lt z v -> lt u (p u v)
 41 |   plusPosRight {u} {v} prf = CalcSmart {leq = lt} $
 42 |     |~ u
 43 |     ~~ p u z ..< r.ring.plus.rightNeutral
 44 |     <~ p u v ..> plusLeft prf
 45 |
 46 |   ||| The result of adding a positive value is greater than
 47 |   ||| the original.
 48 |   export
 49 |   0 plusPosLeft : {u,v : a} -> lt z v -> lt u (p v u)
 50 |   plusPosLeft {u} {v} prf = CalcSmart {leq = lt} $
 51 |     |~ u
 52 |     ~~ p z u ..< r.ring.plus.leftNeutral
 53 |     <~ p v u ..> plusRight prf
 54 |
 55 |   ||| The result of adding a non-negative value is not less than
 56 |   ||| the original.
 57 |   export
 58 |   0 plusNonNegRight :
 59 |        {u,v : a}
 60 |     -> ReflexiveClosure lt z u
 61 |     -> ReflexiveClosure lt v (p v u)
 62 |   plusNonNegRight (Rel l) = Rel $ plusPosRight l
 63 |   plusNonNegRight Refl    = fromEq (sym r.ring.plus.rightNeutral)
 64 |
 65 |   ||| The result of adding a non-negative value is not less than
 66 |   ||| the original.
 67 |   export
 68 |   0 plusNonNegLeft :
 69 |        {u,v : a}
 70 |     -> ReflexiveClosure lt z u
 71 |     -> ReflexiveClosure lt v (p u v)
 72 |   plusNonNegLeft (Rel l) = Rel $ plusPosLeft l
 73 |   plusNonNegLeft Refl    = fromEq (sym r.ring.plus.leftNeutral)
 74 |
 75 |   ||| The result of adding a negative value is less than
 76 |   ||| the original.
 77 |   export
 78 |   0 plusNegRight : {u,v : a} -> lt v z -> lt (p u v) u
 79 |   plusNegRight {u} {v} prf = CalcSmart {leq = lt} $
 80 |     |~ p u v
 81 |     <~ p u z ..> plusLeft prf
 82 |     ~~ u     ... r.ring.plus.rightNeutral
 83 |
 84 |   ||| The result of adding a negative value is less than
 85 |   ||| the original.
 86 |   export
 87 |   0 plusNegLeft : {u,v : a} -> lt v z -> lt (p v u) u
 88 |   plusNegLeft {u} {v} prf = CalcSmart {leq = lt} $
 89 |     |~ p v u
 90 |     <~ p z u ..> plusRight prf
 91 |     ~~ u     ... r.ring.plus.leftNeutral
 92 |
 93 |   ||| The result of adding a non-positive value is not greater than
 94 |   ||| the original.
 95 |   export
 96 |   0 plusNonPosRight :
 97 |        {u,v : a}
 98 |     -> ReflexiveClosure lt u z
 99 |     -> ReflexiveClosure lt (p v u) v
100 |   plusNonPosRight (Rel l) = Rel $ plusNegRight l
101 |   plusNonPosRight Refl    = fromEq r.ring.plus.rightNeutral
102 |
103 |   ||| The result of adding a non-positive value is not greater than
104 |   ||| the original.
105 |   export
106 |   0 plusNonPosLeft :
107 |        {u,v : a}
108 |     -> ReflexiveClosure lt u z
109 |     -> ReflexiveClosure lt (p u v) v
110 |   plusNonPosLeft (Rel l) = Rel $ plusNegLeft l
111 |   plusNonPosLeft Refl    = fromEq r.ring.plus.leftNeutral
112 |
113 |   ||| We can solve (in)equalities, where the same value has
114 |   ||| been added on both sides.
115 |   export
116 |   0 solvePlusRight : {u,v,w : a} -> lt (p u w) (p v w) -> lt u v
117 |   solvePlusRight {u} {v} {w} prf = CalcSmart {leq = lt} $
118 |     |~ u
119 |     ~~ p u z               ..< r.ring.plus.rightNeutral
120 |     ~~ p u (sub w w)       ..< cong (p u) r.ring.minusSelf
121 |     ~~ p u (p w (sub z w)) ... cong (p u) r.ring.minusIsPlusRight
122 |     ~~ p (p u w) (sub z w) ... r.ring.plus.associative
123 |     <~ p (p v w) (sub z w) ..> plusRight prf
124 |     ~~ p v (p w (sub z w)) ..< r.ring.plus.associative
125 |     ~~ p v (sub w w)       ..< cong (p v) r.ring.minusIsPlusRight
126 |     ~~ p v z               ... cong (p v) r.ring.minusSelf
127 |     ~~ v                   ... r.ring.plus.rightNeutral
128 |