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
Raw
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
Raw
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
@david-christiansen
Copy link

david-christiansen commented Jun 25, 2014

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

@mrb
Copy link
Author

mrb commented Jun 25, 2014 

 <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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment