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

As said on twitter, this should be the implementation of gcjoin:

gcjoin l r = (MkGCounter ((value l) `max` (value r)))

Then implement something else like the following for what we call inflations:

increment : GCounter -> GCounter
increment = increment_by 1

increment_by : Int -> GCounter -> GCounter
increment_by amount counter = MkGCounter ((value counter) + amount)

@lenary - nice, thanks. The verified part is the bit that's giving me trouble.

*h> :p a

---------- Goal: ----------
{hole0} : (l : GCounter) ->
(c : GCounter) ->
(r : GCounter) ->
MkGCounter (plus (value l) (plus (value c) (value r))) =
MkGCounter (plus (plus (value l) (value c)) (value r))
-Main.a> intros
---------- Other goals: ----------
{hole2},{hole1},{hole0}
---------- Assumptions: ----------
l : GCounter
c : GCounter
r : GCounter
---------- Goal: ----------
{hole3} : MkGCounter (plus (value l)
(plus (value c) (value r))) =
MkGCounter (plus (plus (value l) (value c)) (value r))

Here's proofs for the two true ones:

Main.c = proof
  intros
  rewrite (plusCommutative (value l) (value r))
  trivial

Main.a = proof
  intros
  rewrite (sym (plusAssociative (value l) (value c) (value r)))
  trivial

And here's a cheat-sheet for the right one, arranged to be pedagogical rather than golfed. It shows a few different techniques, like proving in the prover or with pattern-matching, and using rewrite and cong.

module Main
import Prelude.Algebra

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)

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

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

gc1 : GCounter
gc1 = (MkGCounter 1)

gc2 : GCounter
gc2 = (MkGCounter 2)

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

instance JoinSemilattice GCounter where
  join = gcjoin

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

---------- Proofs ----------
Main.c = proof
  intros
  rewrite natMaxCommut (value l) (value r)
  trivial



Main.a = proof
  intros
  rewrite natMaxAssoc (value l) (value c) (value r)
  trivial

 <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