
   0 | module Algebra.SizeChange
   1 | 
   2 | import Algebra.Semiring
   3 | 
   4 | import Libraries.Text.PrettyPrint.Prettyprinter
   5 | 
   6 | public export
   7 | data SizeChange = Smaller | Same | Unknown
   8 | 
   9 | export
  10 | Semigroup SizeChange where
  11 |   -- Same is a neutral
  12 |   Unknown <+> _ = Unknown
  13 |   Same <+> c = c
  14 |   _ <+> Unknown = Unknown
  15 |   Smaller <+> _ = Smaller
  16 | 
  17 | export
  18 | Monoid SizeChange where
  19 |   neutral = Same
  20 | 
  21 | export
  22 | Show SizeChange where
  23 |   show Smaller = "Smaller"
  24 |   show Same = "Same"
  25 |   show Unknown = "Unknown"
  26 | 
  27 | export
  28 | Eq SizeChange where
  29 |   Smaller == Smaller = True
  30 |   Same == Same = True
  31 |   Unknown == Unknown = True
  32 |   _ == _ = False
  33 | 
  34 | -- information order
  35 | export
  36 | Ord SizeChange where
  37 |   compare Unknown Unknown = EQ
  38 |   compare Unknown _ = LT
  39 |   compare _ Unknown = GT
  40 |   compare Same Same = EQ
  41 |   compare Same _ = LT
  42 |   compare _ Same = GT
  43 |   compare Smaller Smaller = EQ
  44 | 
  45 |   max Unknown y = y
  46 |   max Same Unknown = Same
  47 |   max Same y = y
  48 |   max Smaller y = Smaller -- holds definitionally!
  49 | 
  50 | export
  51 | Semiring SizeChange where
  52 |   (|*|) = (<+>)
  53 |   timesNeutral = neutral
  54 |   (|+|) = max
  55 |   plusNeutral = Unknown
  56 | 
  57 | -- semiring laws
  58 | scPlusNeutralLeft : (a : SizeChange) -> Unknown |+| a = a
  59 | scPlusNeutralLeft a = Refl
  60 | 
  61 | scPlusNeutralRight : (a : SizeChange) -> a |+| Unknown = a
  62 | scPlusNeutralRight Smaller = Refl
  63 | scPlusNeutralRight Same = Refl
  64 | scPlusNeutralRight Unknown = Refl
  65 | 
  66 | partial
  67 | scPlusCommutative : (a, b : SizeChange) -> a |+| b = b |+| a
  68 | scPlusCommutative Unknown b = sym (scPlusNeutralRight b)
  69 | scPlusCommutative b Unknown = scPlusNeutralRight b
  70 | scPlusCommutative Smaller Smaller = Refl
  71 | scPlusCommutative Same Smaller = Refl
  72 | scPlusCommutative Smaller Same = Refl
  73 | scPlusCommutative Same Same = Refl
  74 | 
  75 | scPlusAssoc : (a, b, c : SizeChange) -> (a |+| b) |+| c = a |+| (b |+| c)
  76 | scPlusAssoc Smaller b c = Refl
  77 | scPlusAssoc Same Smaller c = Refl
  78 | scPlusAssoc Same Same Smaller = Refl
  79 | scPlusAssoc Same Same Same = Refl
  80 | scPlusAssoc Same Same Unknown = Refl
  81 | scPlusAssoc Same Unknown c = Refl
  82 | scPlusAssoc Unknown b c = Refl
  83 | 
  84 | scMultNeutralLeft : (a : SizeChange) -> Same |*| a = a
  85 | scMultNeutralLeft a = Refl
  86 | 
  87 | scMultNeutralRight : (a : SizeChange) -> a |*| Same = a
  88 | scMultNeutralRight Smaller = Refl
  89 | scMultNeutralRight Same = Refl
  90 | scMultNeutralRight Unknown = Refl
  91 | 
  92 | scMultZeroLeft : (a : SizeChange) -> Unknown |*| a = Unknown
  93 | scMultZeroLeft a = Refl
  94 | 
  95 | scMultZeroRight : (a : SizeChange) -> a |*| Unknown = Unknown
  96 | scMultZeroRight Smaller = Refl
  97 | scMultZeroRight Same = Refl
  98 | scMultZeroRight Unknown = Refl
  99 | 
 100 | scMultAssociative : (a, b, c : SizeChange) -> a |*| (b |*| c) = (a |*| b) |*| c
 101 | scMultAssociative Smaller Smaller Smaller = Refl
 102 | scMultAssociative Same b c = Refl
 103 | scMultAssociative a Same c =
 104 |   rewrite scMultNeutralRight a in
 105 |   Refl
 106 | scMultAssociative a b Same =
 107 |   rewrite scMultNeutralRight b in
 108 |   rewrite scMultNeutralRight (a |*| b) in
 109 |   Refl
 110 | scMultAssociative Unknown b c = Refl
 111 | scMultAssociative a Unknown c =
 112 |   rewrite scMultZeroRight a in
 113 |   Refl
 114 | scMultAssociative a b Unknown =
 115 |   rewrite scMultZeroRight b in
 116 |   rewrite scMultZeroRight a in
 117 |   rewrite scMultZeroRight (a |*| b) in
 118 |   Refl
 119 | 
 120 | scMultCommutative : (a, b : SizeChange) -> a |*| b = b |*| a
 121 | scMultCommutative Smaller Smaller = Refl
 122 | scMultCommutative b Same =
 123 |   rewrite scMultNeutralRight b in
 124 |   Refl
 125 | scMultCommutative Smaller Unknown = Refl
 126 | scMultCommutative Same b =
 127 |   rewrite scMultNeutralRight b in
 128 |   Refl
 129 | scMultCommutative Unknown b =
 130 |  rewrite scMultZeroRight b in
 131 |  Refl
 132 | 
 133 | scPlusIdempotent : (a : SizeChange) -> a |+| a = a
 134 | scPlusIdempotent Smaller = Refl
 135 | scPlusIdempotent Same = Refl
 136 | scPlusIdempotent Unknown = Refl
 137 | 
 138 | scMultPlusDist : (a, b, c : SizeChange) -> a |*| (b |+| c) = (a |*| b) |+| (a |*| c)
 139 | scMultPlusDist Unknown b c = Refl
 140 | scMultPlusDist a Unknown c =
 141 |   rewrite scMultZeroRight a in
 142 |   Refl
 143 | scMultPlusDist a b Unknown =
 144 |   rewrite scPlusNeutralRight b in
 145 |   rewrite scMultZeroRight a in
 146 |   rewrite scPlusNeutralRight (a |*| b) in
 147 |   Refl
 148 | scMultPlusDist Same b c = Refl
 149 | scMultPlusDist a Same Same =
 150 |   rewrite scMultNeutralRight a in
 151 |   rewrite scPlusIdempotent a in
 152 |   Refl
 153 | scMultPlusDist Smaller Same Smaller = Refl
 154 | scMultPlusDist Smaller Smaller Same = Refl
 155 | scMultPlusDist Smaller Smaller Smaller = Refl
 156 | 
 157 | export
 158 | Pretty Void SizeChange where
 159 |   pretty Smaller = pretty "<"
 160 |   pretty Same = pretty "="
 161 |   pretty Unknown = neutral
 162 |