Skip to content

Instantly share code, notes, and snippets.

@mrb

mrb/cong.idr

Last active August 29, 2015 14:02
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save mrb/cae9ee1c37e3ce1c3e24 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save mrb/cae9ee1c37e3ce1c3e24 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. mrb revised this gist Jun 25, 2014. 1 changed file with 58 additions and 0 deletions.
    58 changes: 58 additions & 0 deletions cong.idr
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,58 @@
    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
  2. mrb revised this gist Jun 25, 2014. 1 changed file with 11 additions and 2 deletions.
    13 changes: 11 additions & 2 deletions gcounter.idr
    View file
    Original file line number Diff line number Diff line change
    @@ -3,7 +3,7 @@ module Main
    import Prelude.Algebra

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

    gcjoin : GCounter -> GCounter -> GCounter
    gcjoin l r = (MkGCounter ((value l) + (value r)))
    @@ -16,8 +16,17 @@ 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
  3. mrb revised this gist Jun 25, 2014. 1 changed file with 6 additions and 1 deletion.
    7 changes: 6 additions & 1 deletion gcounter.idr
    View file
    Original file line number Diff line number Diff line change
    @@ -15,4 +15,9 @@ gc2 : GCounter
    gc2 = (MkGCounter 2)

    instance JoinSemilattice GCounter where
    join = gcjoin
    join = gcjoin

    instance VerifiedJoinSemilattice GCounter where
    joinSemilatticeJoinIsAssociative = ?a
    joinSemilatticeJoinIsCommutative = ?c
    joinSemilatticeJoinIsIdempotent = ?i
  4. mrb created this gist Jun 25, 2014.
    18 changes: 18 additions & 0 deletions gcounter.idr
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,18 @@
    module Main

    import Prelude.Algebra

    record GCounter : Type where
    MkGCounter : (value : Int) -> 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