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)))))

$ idris counter.idr
     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 0.9.13.1
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help

Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Type checking ./counter.idr
counter.idr:16:19:
When elaborating right hand side of counterIdempotent:
When elaborating an application of function Prelude.Basics.cong:
        No such variable maximumIdempotent
counter.idr:28:20:
When elaborating right hand side of counterAssociative:
When elaborating an application of function Prelude.Basics.cong:
        No such variable maximumAssociative
counter.idr:45:9:When elaborating right hand side of sucMaxR:
Can't unify
        S (boolElim (lte l (S l)) (Delay (S l)) (Delay l)) = S (S l)
with
        boolElim (lte l (S l)) (Delay (S (S l))) (Delay (S l)) = S (S l)

Specifically:
        Can't unify
                S (boolElim (lte l (S l)) (Delay (S l)) (Delay l))
        with
                boolElim (lte l (S l)) (Delay (S (S l))) (Delay (S l))
Metavariables: Main.sucMaxR, Main.counterAssociative, Main.counterIdempotent

What am I missing?

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