counter.idr

module Main
 
import Prelude.Algebra

record GCounter : Type where
  MkGCounter : (value : Nat) -> GCounter

gcjoin : GCounter -> GCounter -> GCounter
gcjoin l r = (MkGCounter (maximum (value l) (value r)))

gcincrement : GCounter -> GCounter
gcincrement g = (MkGCounter (1 + (value g)))

counterIdempotent : (e : GCounter) -> 
                          MkGCounter (maximum (value e) (value e)) = e
counterIdempotent (MkGCounter val) = cong (maximumIdempotent val)

counterCommutative : (l : GCounter) -> (r : GCounter) -> 
                          MkGCounter (maximum (value l) (value r)) =
                          MkGCounter (maximum (value r) (value l))
counterCommutative l r = cong (maximumCommutative (value l) (value r))

counterAssociative : (l : GCounter) -> (c : GCounter) -> (r : GCounter) ->
                          MkGCounter (maximum (value l)
                                              (maximum (value c) (value r))) =
                          MkGCounter (maximum (maximum (value l) (value c))
                                              (value r))
counterAssociative l c r = cong (maximumAssociative (value l) (value c) (value r))

class VerifiedJoinSemilattice a => CRDTCounter a where
  val : a -> Nat
  incr : a -> a
  total incrInflates : (l : a) -> (join l (incr l)) = (incr l)

instance JoinSemilattice GCounter where
  join = gcjoin

instance VerifiedJoinSemilattice GCounter where
  joinSemilatticeJoinIsAssociative = counterAssociative
  joinSemilatticeJoinIsCommutative = counterCommutative
  joinSemilatticeJoinIsIdempotent  = counterIdempotent

total sucMaxR : (l : Nat) -> maximum l (S l) = (S l)
sucMaxR Z = refl
sucMaxR (S l) = cong (sucMaxR l)

gcIncrInflates : (l : GCounter) ->
                    MkGCounter (maximum (value l) (S (value l))) =
                    MkGCounter (S (value l))
gcIncrInflates l = cong (sucMaxR (value l))

instance CRDTCounter GCounter where
  val = value
  incr = gcincrement
  incrInflates = gcIncrInflates

main : IO ()
main = do
  putStrLn (show (value (join (MkGCounter 111) (incr (MkGCounter 8)))))

@seancribbs Try these - https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Nat.idr#L634-L649