cong.idr

module Main
 
import Prelude.Algebra

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

natMax : Nat -> Nat -> Nat
natMax Z m = m
natMax (S n) Z = S n
natMax (S n) (S m) = S (natMax n m)

natMaxAssoc : (l,c,r : Nat) -> natMax l (natMax c r) = natMax (natMax l c) r
natMaxAssoc Z c r = refl
natMaxAssoc (S k) Z r = refl
natMaxAssoc (S k) (S j) Z = refl
natMaxAssoc (S k) (S j) (S i) = rewrite natMaxAssoc k j i in refl

natMaxCommut : (l, r : Nat) -> natMax l r = natMax r l
natMaxCommut Z Z = refl
natMaxCommut Z (S k) = refl
natMaxCommut (S k) Z = refl
natMaxCommut (S k) (S j) = rewrite natMaxCommut k j in refl

natMaxIdempotent : (n : Nat) -> natMax n n = n
natMaxIdempotent Z = refl
natMaxIdempotent (S k) = cong (natMaxIdempotent k)

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

gc1 : GCounter
gc1 = (MkGCounter 1)

gc2 : GCounter
gc2 = (MkGCounter 2)

instance JoinSemilattice GCounter where
  join = gcjoin

counterIdempotent : (e : GCounter) -> MkGCounter (natMax (value e) (value e)) = e
counterIdempotent (MkGCounter val) = cong (natMaxIdempotent val)

counterCommutative : (l : GCounter) -> (r : GCounter) -> MkGCounter (natMax (value l) (value r)) =
                                      MkGCounter (natMax (value r) (value l))
counterCommutative l r = cong (natMaxCommut (value l) (value r))

counterAssociative : (l : GCounter) -> (c : GCounter) -> (r : GCounter) ->
                          MkGCounter (natMax (value l)
                                             (natMax (value c) (value r))) =
                          MkGCounter (natMax (natMax (value l) (value c))
                                             (value r))
counterAssociative l c r = cong (natMaxAssoc (value l) (value c) (value r))

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

gcounter.idr

module Main
 
import Prelude.Algebra

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

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

gc1 : GCounter
gc1 = (MkGCounter 1)

gc2 : GCounter
gc2 = (MkGCounter 2)

instance JoinSemilattice GCounter where
  join = gcjoin

instance VerifiedJoinSemilattice GCounter where
  joinSemilatticeJoinIsAssociative = ?a
  joinSemilatticeJoinIsCommutative = ?c
  joinSemilatticeJoinIsIdempotent  = ?i

-- *h> :t a
-- --------------------------------------
-- a : (l : GCounter) ->
--     (c : GCounter) ->
--     (r : GCounter) ->
--     MkGCounter (plus (value l) (plus (value c) (value r))) =
--     MkGCounter (plus (plus (value l) (value c)) (value r))
-- Metavariables: Main.i, Main.c, Main.a

 <christiansen> does it make sense?
11:05 AM <christiansen> the max function is defined to make it as easy as possible to prove those properties
11:06 AM <christiansen> the rewrite... in refl bits could all use cong as well
11:06 AM <christiansen> so you can try making it do that
11:07 AM <christiansen> also, try replacing the tactic scripts with normal defintions in the style of counterIdempotent
11:07 AM <lenary> ah right, so we can't just use maximum because it uses lte and everything gets hard
11:08 AM <mrb_bk> very interesting
11:08 AM <christiansen> dependent types are all about engineering coincidences that turn out in your favor
11:09 AM <christiansen> but the boolElim calls on the rhs of maximum will make it significantly less convenient to work with
11:11 AM <mrb_bk> christiansen: gotta study this
11:11 AM <mrb_bk> thanks a lot!
11:11 AM <christiansen> enjoy!
11:11 AM <christiansen> it's worth trying to repeat the proofs about natMax for maximum, and see where they get annoying