added Store correctness proof by Russell O'Connor

ekmett committed Jan 5, 2011
1 parent 9c1e7a2 commit ac4e0c431a8e91c9a2f90574972f3328ed5f34b6
Showing with 107 additions and 3 deletions.
1. +3 −3 Control/Comonad/Trans/Store.hs
2. +7 −0 Setup.lhs
3. +1 −0 comonad-transformers.cabal
4. +96 −0 coq/Store.v
 @@ -10,9 +10,9 @@ -- -- The store (state-in-context/costate) comonad transformer is subject to the laws: -- --- x = put (get x) x --- y = get (put y x) --- put y x = put y (put z x) +-- > x = put (get x) x +-- > y = get (put y x) +-- > put y x = put y (put z x) -- -- Thanks go to Russell O'Connor and Daniel Peebles for their help formulating -- and proving the laws for this comonad transformer.
 @@ -0,0 +1,7 @@ +#!/usr/bin/runhaskell +> module Main (main) where + +> import Distribution.Simple + +> main :: IO () +> main = defaultMain
 @@ -12,6 +12,7 @@ copyright: Copyright (C) 2008-2011 Edward A. Kmett synopsis: Comonad transformers description: Comonad transformers build-type: Simple +extra-source-files: coq/Store.v library build-depends:
 @@ -0,0 +1,96 @@ +(* Proof StoreT forms a comonad -- Russell O'Connor *) + +Set Implict Arguments. +Unset Strict Implicit. + +Require Import FunctionalExtensionality. + +Record Comonad (w : Type -> Type) : Type := + { extract : forall a, w a -> a + ; extend : forall a b, (w a -> b) -> w a -> w b + ; law1 : forall a x, extend _ _ (extract a) x = x + ; law2 : forall a b f x, extract b (extend a _ f x) = f x + ; law3 : forall a b c f g x, extend b c f (extend a b g x) = extend a c (fun y => f (extend a b g y)) x + }. + +Section StoreT. + +Variables (s : Type) (w:Type -> Type). +Hypothesis wH : Comonad w. + +Definition map a b f x := extend _ wH a b (fun y => f (extract _ wH _ y)) x. + +Lemma map_extend : forall a b c f g x, map b c f (extend _ wH a b g x) = extend _ wH _ _ (fun y => f (g y)) x. +Proof. +intros a b c f g x. +unfold map. +rewrite law3. +apply equal_f. +apply f_equal. +extensionality y. +rewrite law2. +reflexivity. +Qed. + +Record StoreT (a:Type): Type := mkStoreT + {store : w (s -> a) + ;loc : s}. + +Definition extractST a (x:StoreT a) : a := + extract _ wH _ (store _ x) (loc _ x). + +Definition mapST a b (f:a -> b) (x:StoreT a) : StoreT b := + mkStoreT _ (map _ _ (fun g x => f (g x)) (store _ x)) (loc _ x). + +Definition duplicateST a (x:StoreT a) : StoreT (StoreT a) := + mkStoreT _ (extend _ wH _ _ (mkStoreT _) (store _ x)) (loc _ x). + +Let extendST := fun a b f x => mapST _ b f (duplicateST a x). + +Lemma law1ST : forall a x, extendST _ _ (extractST a) x = x. +Proof. +intros a [v b]. +unfold extractST, extendST, duplicateST, mapST. +simpl. +rewrite map_extend. +simpl. +replace (fun (y : w (s -> a)) (x : s) => extract w wH (s -> a) y x) + with (extract w wH (s -> a)). + rewrite law1. + reflexivity. +extensionality y. +extensionality x. +reflexivity. +Qed. + +Lemma law2ST : forall a b f x, extractST b (extendST a _ f x) = f x. +Proof. +intros a b f [v c]. +unfold extendST, mapST, extractST. +simpl. +rewrite map_extend. +rewrite law2. +reflexivity. +Qed. + +Lemma law3ST : forall a b c f g x, extendST b c f (extendST a b g x) = extendST a c (fun y => f (extendST a b g y)) x. +Proof. +intros a b c f g [v d]. +unfold extendST, mapST, extractST. +simpl. +repeat rewrite map_extend. +rewrite law3. +repeat (apply equal_f||apply f_equal). +extensionality y. +extensionality x. +rewrite map_extend. +reflexivity. +Qed. + +Definition StoreTComonad : Comonad StoreT := + Build_Comonad _ _ _ law1ST law2ST law3ST. + +End StoreT. + +Check StoreTComonad. +