Last active
August 29, 2015 14:02
-
-
Save mrb/cae9ee1c37e3ce1c3e24 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
*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))