
   0 | module Algebra.ZeroOneOmega
   1 | 
   2 | import Algebra.Semiring
   3 | import Algebra.Preorder
   4 | 
   5 | %default total
   6 | 
   7 | export
   8 | data ZeroOneOmega = Rig0 | Rig1 | RigW
   9 | 
  10 | %name ZeroOneOmega rig
  11 | 
  12 | export
  13 | Preorder ZeroOneOmega where
  14 |   Rig0 <=    _ = True
  15 |   Rig1 <= Rig1 = True
  16 |   _    <= RigW = True
  17 |   _    <=    _ = False
  18 |   preorderRefl {x = Rig0} = Refl
  19 |   preorderRefl {x = Rig1} = Refl
  20 |   preorderRefl {x = RigW} = Refl
  21 |   preorderTrans {x = Rig0} _ _ = Refl
  22 |   preorderTrans {x = Rig1} {y = Rig0} _ _ impossible
  23 |   preorderTrans {x = Rig1} {y = Rig1} _ yz = yz
  24 |   preorderTrans {x = Rig1} {y = RigW} {z = Rig0} _ _ impossible
  25 |   preorderTrans {x = Rig1} {y = RigW} {z = Rig1} _ _ = Refl
  26 |   preorderTrans {x = Rig1} {y = RigW} {z = RigW} _ _ = Refl
  27 |   preorderTrans {x = RigW} {y = Rig0} _ _ impossible
  28 |   preorderTrans {x = RigW} {y = Rig1} _ _ impossible
  29 |   preorderTrans {x = RigW} {y = RigW} _ yz = yz
  30 | 
  31 | public export
  32 | Eq ZeroOneOmega where
  33 |   (==) Rig0 Rig0 = True
  34 |   (==) Rig1 Rig1 = True
  35 |   (==) RigW RigW = True
  36 |   (==) _ _ = False
  37 | 
  38 | export
  39 | Show ZeroOneOmega where
  40 |   show Rig0 = "Rig0"
  41 |   show Rig1 = "Rig1"
  42 |   show RigW = "RigW"
  43 | 
  44 | export
  45 | rigPlus : ZeroOneOmega -> ZeroOneOmega -> ZeroOneOmega
  46 | rigPlus Rig0 a = a
  47 | rigPlus a Rig0 = a
  48 | rigPlus _ _ = RigW
  49 | 
  50 | export
  51 | rigMult : ZeroOneOmega -> ZeroOneOmega -> ZeroOneOmega
  52 | rigMult Rig0 _ = Rig0
  53 | rigMult _ Rig0 = Rig0
  54 | rigMult Rig1 a = a
  55 | rigMult a Rig1 = a
  56 | rigMult _ _ = RigW
  57 | 
  58 | 
  59 | public export
  60 | Semiring ZeroOneOmega where
  61 |   (|+|) = rigPlus
  62 |   (|*|) = rigMult
  63 |   plusNeutral = Rig0
  64 |   timesNeutral = Rig1
  65 | 
  66 | ||| The top value of a lattice
  67 | export
  68 | Top ZeroOneOmega where
  69 |   top = RigW
  70 |   topAbs {x = Rig0} = Refl
  71 |   topAbs {x = Rig1} = Refl
  72 |   topAbs {x = RigW} = Refl
  73 | 
  74 | ----------------------------------------
  75 | 
  76 | rigPlusAssociative : (x, y, z : ZeroOneOmega) ->
  77 |   rigPlus x (rigPlus y z) = rigPlus (rigPlus x y) z
  78 | rigPlusAssociative Rig0 _ _ = Refl
  79 | rigPlusAssociative Rig1 Rig0 _ = Refl
  80 | rigPlusAssociative Rig1 Rig1 Rig0 = Refl
  81 | rigPlusAssociative Rig1 Rig1 Rig1 = Refl
  82 | rigPlusAssociative Rig1 Rig1 RigW = Refl
  83 | rigPlusAssociative Rig1 RigW Rig0 = Refl
  84 | rigPlusAssociative Rig1 RigW Rig1 = Refl
  85 | rigPlusAssociative Rig1 RigW RigW = Refl
  86 | rigPlusAssociative RigW Rig0 _ = Refl
  87 | rigPlusAssociative RigW Rig1 Rig0 = Refl
  88 | rigPlusAssociative RigW Rig1 Rig1 = Refl
  89 | rigPlusAssociative RigW Rig1 RigW = Refl
  90 | rigPlusAssociative RigW RigW Rig0 = Refl
  91 | rigPlusAssociative RigW RigW Rig1 = Refl
  92 | rigPlusAssociative RigW RigW RigW = Refl
  93 | 
  94 | rigPlusCommutative : (x, y : ZeroOneOmega) ->
  95 |   rigPlus x y = rigPlus y x
  96 | rigPlusCommutative Rig0 Rig0 = Refl
  97 | rigPlusCommutative Rig0 Rig1 = Refl
  98 | rigPlusCommutative Rig0 RigW = Refl
  99 | rigPlusCommutative Rig1 Rig0 = Refl
 100 | rigPlusCommutative Rig1 Rig1 = Refl
 101 | rigPlusCommutative Rig1 RigW = Refl
 102 | rigPlusCommutative RigW Rig0 = Refl
 103 | rigPlusCommutative RigW Rig1 = Refl
 104 | rigPlusCommutative RigW RigW = Refl
 105 | 
 106 | rigMultAssociative : (x, y, z : ZeroOneOmega) ->
 107 |   rigMult x (rigMult y z) = rigMult (rigMult x y) z
 108 | rigMultAssociative Rig0 _ _ = Refl
 109 | rigMultAssociative Rig1 Rig0 _ = Refl
 110 | rigMultAssociative Rig1 Rig1 Rig0 = Refl
 111 | rigMultAssociative Rig1 Rig1 Rig1 = Refl
 112 | rigMultAssociative Rig1 Rig1 RigW = Refl
 113 | rigMultAssociative Rig1 RigW Rig0 = Refl
 114 | rigMultAssociative Rig1 RigW Rig1 = Refl
 115 | rigMultAssociative Rig1 RigW RigW = Refl
 116 | rigMultAssociative RigW Rig0 _ = Refl
 117 | rigMultAssociative RigW Rig1 Rig0 = Refl
 118 | rigMultAssociative RigW Rig1 Rig1 = Refl
 119 | rigMultAssociative RigW Rig1 RigW = Refl
 120 | rigMultAssociative RigW RigW Rig0 = Refl
 121 | rigMultAssociative RigW RigW Rig1 = Refl
 122 | rigMultAssociative RigW RigW RigW = Refl
 123 | 
 124 | rigMultCommutative : (x, y : ZeroOneOmega) ->
 125 |   rigMult x y = rigMult y x
 126 | rigMultCommutative Rig0 Rig0 = Refl
 127 | rigMultCommutative Rig0 Rig1 = Refl
 128 | rigMultCommutative Rig0 RigW = Refl
 129 | rigMultCommutative Rig1 Rig0 = Refl
 130 | rigMultCommutative Rig1 Rig1 = Refl
 131 | rigMultCommutative Rig1 RigW = Refl
 132 | rigMultCommutative RigW Rig0 = Refl
 133 | rigMultCommutative RigW Rig1 = Refl
 134 | rigMultCommutative RigW RigW = Refl
 135 |