Commit adabb546 authored by Nicola Botta's avatar Nicola Botta
Browse files

Adding components needed for Responsibility section of the responsibility paper.

parent f1c63eac
> module Basic.Predicates
> import Control.Isomorphism
> %default total
> %access public export
> %auto_implicits off
......@@ -7,3 +9,6 @@
> Empty : Type -> Type
> Empty A = A -> Void
> Singleton : Type -> Type
> Singleton A = Iso A Unit
> module FastSimpleProb.BasicProperties
> import Data.List
> import FastSimpleProb.SimpleProb
> import FastSimpleProb.BasicOperations
> import Double.Predicates
> import List.Operations
> import NonNegDouble.NonNegDouble
> import NonNegDouble.BasicOperations
> import NonNegDouble.Properties
> import List.Operations
> import List.Properties
> %default total
> %access public export
> %auto_implicits on
* Properties of |toList|:
> using implementation NumNonNegDouble
> |||
> toListLemma : {A : Type} -> (sp : SimpleProb A) -> Positive (toDouble (sumMapSnd (toList sp)))
> toListLemma (MkSimpleProb _ prf) = prf
* Properties of weights:
> using implementation NumNonNegDouble
> |||
> positiveWeights : {A : Type} -> (sp : SimpleProb A) -> Positive (toDouble (sum (weights sp)))
> positiveWeights = toListLemma
> |||
> lengthSupportWeightsLemma : {A : Type} ->
> (sp : SimpleProb A) ->
> length (support sp) = length (weights sp)
> lengthSupportWeightsLemma sp = lengthLemma (toList sp) fst snd
* Implementations:
> using implementation ShowNonNegDouble
> ||| SimpleProb is an implementation of Show
> implementation Show a => Show (SimpleProb a) where
> show sp = show (toList sp)
> {-
> ---}
> module FastSimpleProb.Functor
> import FastSimpleProb.SimpleProb
> import FastSimpleProb.MonadicOperations
> %default total
> %access public export
> %auto_implicits on
> ||| |SimpleProb| is a functor:
> implementation Functor SimpleProb where
> map = fmap
> {-
> ---}
> module FastSimpleProb.Measures
> import FastSimpleProb.SimpleProb
> import FastSimpleProb.BasicOperations
> import FastSimpleProb.MonadicOperations
> import FastSimpleProb.MonadicPostulates
> import FastSimpleProb.MonadicProperties
> import Double.Predicates
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Predicates
> import NonNegDouble.BasicOperations
> import NonNegDouble.Operations
> import NonNegDouble.Properties
> import NonNegDouble.Measures
> import NonNegDouble.LTEProperties
> import List.Operations
> import List.Properties
> import Fun.Operations
> import Rel.TotalPreorder
> import Pairs.Operations
> %default total
> %access public export
> %auto_implicits off
* Measures
> ||| Worst
> worst : SimpleProb NonNegDouble -> NonNegDouble
> worst sp = List.Operations.min totalPreorderLTE xs ne where
> xs : List NonNegDouble
> xs = map fst (toList sp)
> ne : List.Operations.NonEmpty xs
> ne = mapPreservesNonEmpty fst (toList sp) (nonEmptyLemma1 sp)
> using implementation NumNonNegDouble
> ||| Sum
> sum : SimpleProb NonNegDouble -> NonNegDouble
> sum = Prelude.Foldable.sum . (map (uncurry (*))) . toList
> ||| Expected value
> expectedValue : SimpleProb NonNegDouble -> NonNegDouble
> expectedValue = sum . normalize
> {-
> ---}
> module FastSimpleProb.MonadicOperations
> import Data.List
> import Data.List.Quantifiers
> import Data.So
> import FastSimpleProb.SimpleProb
> import FastSimpleProb.BasicOperations
> import FastSimpleProb.BasicProperties
> import Double.Predicates
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Postulates
> import NonNegDouble.Constants
> import NonNegDouble.BasicOperations
> import NonNegDouble.Operations
> import NonNegDouble.Properties
> import List.Operations
> import List.Properties
> import Fun.Operations
> import Sigma.Sigma
> %default total
> %access public export
> %auto_implicits off
* |SimpleProb| is a functor:
> using implementation NumNonNegDouble
> |||
> fmap : {A, B : Type} -> (A -> B) -> SimpleProb A -> SimpleProb B
> fmap f (MkSimpleProb aps psum) = MkSimpleProb aps' psum' where
> aps' : List (B, NonNegDouble)
> aps' = map (cross f id) aps
> psum' : Positive (toDouble (sumMapSnd aps'))
> psum' = replace {P = \ X => Positive (toDouble X)} s2 psum where
> s1 : map snd (map (cross f id) aps) = map snd aps
> s1 = mapSndMapCrossAnyIdLemma f aps
> s2 : sumMapSnd aps = sumMapSnd aps'
> s2 = cong {f = sum} (sym s1)
* |SimpleProb| is a monad:
> |||
> ret : {A : Type} -> A -> SimpleProb A
> ret a = MkSimpleProb [(a, one)] positiveOne
> using implementation NumNonNegDouble
> |||
> bind : {A, B : Type} -> SimpleProb A -> (A -> SimpleProb B) -> SimpleProb B
> bind {A} {B} (MkSimpleProb aps psum) f = normalize (MkSimpleProb bps' psum') where
> f' : A -> List (B, NonNegDouble)
> f' a = toList (normalize (f a))
> psums' : (a : A) -> Positive (toDouble (sumMapSnd (f' a)))
> psums' a = toListLemma (normalize (f a))
> bps' : List (B, NonNegDouble)
> bps' = mvMult aps f'
> psum' : Positive (toDouble (sumMapSnd bps'))
> psum' = mvMultLemma aps psum f' psums'
> using implementation NumNonNegDouble
> |||
> naivebind : {A, B : Type} -> SimpleProb A -> (A -> SimpleProb B) -> SimpleProb B
> {-
> naivebind {A} {B} (MkSimpleProb aps psum) f = MkSimpleProb bps' psum' where
> f' : A -> List (B, NonNegDouble)
> f' a = toList (f a)
> psums' : (a : A) -> Positive (toDouble (sumMapSnd (f' a)))
> psums' a = toListLemma (f a)
> bps' : List (B, NonNegDouble)
> bps' = mvMult aps f'
> psum' : Positive (toDouble (sumMapSnd bps'))
> psum' = mvMultLemma aps psum f' psums'
> -}
> naivebind {A} {B} (MkSimpleProb aps psum) f =
> let f' : (A -> List (B, NonNegDouble))
> = toList . f in
> let psums' : ((a : A) -> Positive (toDouble (sumMapSnd (f' a))))
> = (\ a => toListLemma (f a)) in
> let bps' : List (B, NonNegDouble)
> = mvMult aps f' in
> let psum' : Positive (toDouble (sumMapSnd bps'))
> = mvMultLemma aps psum f' psums' in
> MkSimpleProb bps' psum'
* |SimpleProb| is a container monad:
> |||
> Elem : {A : Type} -> A -> SimpleProb A -> Type
> Elem a sp = Elem a (support sp)
> |||
> NonEmpty : {A : Type} -> SimpleProb A -> Type
> NonEmpty sp = List.Operations.NonEmpty (support sp)
> |||
> All : {A : Type} -> (P : A -> Type) -> SimpleProb A -> Type
> All P sp = All P (support sp)
> using implementation NumNonNegDouble
> ||| Tagging
> tagElem : {A : Type} -> (sp : SimpleProb A) -> SimpleProb (Sigma A (\ a => a `Elem` sp))
> tagElem sp = MkSimpleProb aps' psum' where
> ssp : List A
> ssp = support sp
> wsp : List NonNegDouble
> wsp = weights sp
> as' : List (Sigma A (\ a => a `Elem` sp))
> as' = List.Operations.tagElem ssp
> aps' : List (Sigma A (\ a => a `Elem` sp), NonNegDouble)
> aps' = zip as' wsp
> psum' : Positive (toDouble (sumMapSnd aps'))
> psum' = s9 where
> s1 : sumMapSnd aps' = sum (snd (unzip aps'))
> s1 = sumMapSndUnzipLemma aps'
> s2 : length as' = length ssp
> s2 = tagElemPreservesLength ssp
> s3 : length ssp = length wsp
> s3 = lengthSupportWeightsLemma sp
> s4 : length as' = length wsp
> s4 = trans s2 s3
> s5 : unzip (zip as' wsp) = (as', wsp)
> s5 = unzipZipLemma as' wsp s4
> s6 : snd (unzip aps') = wsp
> s6 = cong {f = snd} s5
> s7 : Positive (toDouble (sum wsp))
> s7 = positiveWeights sp
> s8 : Positive (toDouble (sum (snd (unzip aps'))))
> s8 = replace {P = \ X => Positive (toDouble (sum X))} (sym s6) s7
> s9 : Positive (toDouble (sumMapSnd aps'))
> s9 = replace {P = \ X => Positive (toDouble X)} (sym s1) s8
> {-
> ---}
> module FastSimpleProb.MonadicPostulates
> import FastSimpleProb.SimpleProb
> import FastSimpleProb.BasicOperations
> import FastSimpleProb.MonadicOperations
> import FastSimpleProb.Functor
> import Double.Predicates
> import NonNegDouble.NonNegDouble
> import NonNegDouble.BasicOperations
> import Functor.Predicates
> %default total
> %access public export
> %auto_implicits off
* On |fmap| and |rescale|:
> postulate
> fmapRescaleLemma : {A : Type} ->
> (f : A -> NonNegDouble) ->
> (p : NonNegDouble) -> (pp : Positive (toDouble p)) ->
> (sp : SimpleProb A) ->
> rescale p pp (fmap f sp) = fmap f (rescale p pp sp)
> postulate
> naturalRescale : (p : NonNegDouble) -> (pp : Positive (toDouble p)) ->
> Natural (rescale p pp)
* On |fmap| and |normalize|:
> postulate
> fmapNormalizeLemma : {A, B : Type} ->
> (f : A -> B) ->
> (sp : SimpleProb A) ->
> normalize (fmap f sp) = fmap f (normalize sp)
> postulate
> naturalNormalize : Natural normalize
> module FastSimpleProb.MonadicProperties
> import Data.List
> import Data.List.Quantifiers
> import Syntax.PreorderReasoning
> import FastSimpleProb.SimpleProb
> import FastSimpleProb.BasicOperations
> import FastSimpleProb.BasicProperties
> import FastSimpleProb.MonadicOperations
> import FastSimpleProb.MonadicPostulates
> import FastSimpleProb.Predicates
> import FastSimpleProb.Functor
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Postulates
> import NonNegDouble.Constants
> import NonNegDouble.BasicOperations
> import NonNegDouble.Operations
> import NonNegDouble.Properties
> import Double.Predicates
> import Num.Refinements
> import Num.Properties
> import Fun.Operations
> import List.Operations
> import List.Properties
> import Unique.Predicates
> import Finite.Predicates
> import Sigma.Sigma
> import Pairs.Operations
> import Functor.Predicates
> %default total
> %access public export
> -- %access export
> %auto_implicits off
* Monadic properties of |support|, |normalize|:
> |||
> supportRetLemma : {A : Type} ->
> (a : A) -> support (ret a) = ret a
> supportRetLemma a = ( support (ret a) )
> ={ Refl }=
> ( map fst (toList (ret a)) )
> ={ Refl }=
> ( map fst (toList (MkSimpleProb [(a, one)] positiveOne)) )
> ={ Refl }=
> ( map fst [(a, one)] )
> ={ Refl }=
> ( [a] )
> ={ Refl }=
> ( ret a )
> QED
> ||| |normalize| is a natural transformation
> normalizeNatural : Natural {F = SimpleProb} {G = SimpleProb} normalize
> normalizeNatural = fmapNormalizeLemma
* |SimpleProb| is a container monad:
> |||
> elemNonEmptySpec0 : {A : Type} ->
> (a : A) -> (sp : SimpleProb A) -> a `Elem` sp -> NonEmpty sp
> elemNonEmptySpec0 {A} a sp aesp = List.Properties.elemNonEmptySpec0 a (support sp) aesp
> |||
> elemNonEmptySpec1 : {A : Type} ->
> (sp : SimpleProb A) -> NonEmpty sp -> Sigma A (\ a => a `Elem` sp)
> elemNonEmptySpec1 {A} sp nesp = List.Properties.elemNonEmptySpec1 (support sp) nesp
> |||
> containerMonadSpec1 : {A : Type} -> {a : A} -> a `FastSimpleProb.MonadicOperations.Elem` (ret a)
> containerMonadSpec1 {A} {a} = s3 where
> s1 : a `Data.List.Elem` (List.Operations.ret a)
> s1 = List.Properties.containerMonadSpec1
> s2 : a `Data.List.Elem` (support (FastSimpleProb.MonadicOperations.ret a))
> s2 = replace {P = \ X => a `Data.List.Elem` X} (sym (supportRetLemma a)) s1
> s3 : a `FastSimpleProb.MonadicOperations.Elem` (ret a)
> s3 = s2
> |||
> containerMonadSpec3 : {A : Type} -> {P : A -> Type} ->
> (a : A) -> (sp : SimpleProb A) ->
> All P sp -> a `Elem` sp -> P a
> containerMonadSpec3 {A} {P} a sp allp elemp = List.Properties.containerMonadSpec3 a (support sp) allp elemp
* Specific container monad properties
> |||
> uniqueAllLemma : {A : Type} -> {P : A -> Type} ->
> Unique1 P -> (sp : SimpleProb A) -> Unique (All P sp)
> uniqueAllLemma u1P sp = List.Properties.uniqueAllLemma u1P (support sp)
> |||
> finiteAll : {A : Type} -> {P : A -> Type} ->
> Finite1 P -> (sp : SimpleProb A) -> Finite (All P sp)
> finiteAll f1P sp = List.Properties.finiteAll f1P (support sp)
> ||| All is decidable
> decidableAll : {A : Type} -> {P : A -> Type} ->
> (dec : (a : A) -> Dec (P a)) -> (sp : SimpleProb A) -> Dec (All P sp)
> decidableAll dec sp = List.Properties.decidableAll dec (support sp)
> ||| NotEmpty is finite
> finiteNonEmpty : {A : Type} -> (sp : SimpleProb A) -> Finite (FastSimpleProb.MonadicOperations.NonEmpty sp)
> finiteNonEmpty sp = List.Properties.finiteNonEmpty (support sp)
> ||| NotEmpty is decidable
> decidableNonEmpty : {A : Type} -> (sp : SimpleProb A) -> Dec (FastSimpleProb.MonadicOperations.NonEmpty sp)
> decidableNonEmpty sp = List.Properties.decidableNonEmpty (support sp)
* |SimpleProb|s are never empty
> using implementation NumNonNegDouble
> |||
> nonEmptyLemma1 : {A : Type} -> (sp : SimpleProb A) -> List.Operations.NonEmpty (toList sp)
> nonEmptyLemma1 {A} (MkSimpleProb Nil psum) = s4 where
> s1 : sumMapSnd {A = A} {B = NonNegDouble} Nil = zero
> s1 = sumMapSndNilLemma {A = A} {B = NonNegDouble}
> s2 : Positive (toDouble (sumMapSnd {A = A} {B = NonNegDouble} Nil))
> s2 = psum
> s3 : Positive (toDouble zero)
> s3 = replace {P = \ X => Positive (toDouble X)} s1 s2
> s4 : List.Operations.NonEmpty {A = (A, NonNegDouble)} (toList (MkSimpleProb Nil psum))
> s4 = notPositiveZero s3
> nonEmptyLemma1 (MkSimpleProb (ap :: aps) psum) = ()
> |||
> nonEmptyLemma : {A : Type} -> (sp : SimpleProb A) -> NonEmpty sp
> nonEmptyLemma {A} sp = s4 where
> s1 : List.Operations.NonEmpty (toList sp)
> s1 = nonEmptyLemma1 sp
> s2 : List.Operations.NonEmpty (map fst (toList sp))
> s2 = mapPreservesNonEmpty fst (toList sp) s1
> s3 : List.Operations.NonEmpty (support sp)
> s3 = s2
> s4 : NonEmpty sp
> s4 = s3
* Properies of |fmap| and |toList|
> using implementation NumNonNegDouble
> |||
> toListFmapLemma : {A, B : Type} ->
> (f : A -> B) -> (sp : SimpleProb A) ->
> toList (fmap f sp) = fmap (cross f id) (toList sp)
> toListFmapLemma f (MkSimpleProb aps psum) =
> ( toList (fmap f (MkSimpleProb aps psum)) )
> ={ Refl }=
> ( toList (MkSimpleProb
> (fmap (cross f id) aps)
> (replace {P = \ X => Positive (toDouble X)} (cong {f = sum} (sym (mapSndMapCrossAnyIdLemma f aps))) psum)) )
> ={ Refl }=
> ( fmap (cross f id) aps )
> ={ Refl }=
> ( fmap (cross f id) (toList (MkSimpleProb aps psum)) )
> QED
> {-
> ---}
> module FastSimpleProb.Predicates
> import FastSimpleProb.SimpleProb
> import FastSimpleProb.MonadicOperations
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Predicates
> import Functor.Predicates
> %default total
> %access public export
> %auto_implicits off
> {-
> ||| Monotonicity of |SimpleProb| measures
> Monotone : (SimpleProb NonNegDouble -> NonNegDouble) -> Type
> Monotone meas = {A : Type} ->
> (f : A -> NonNegDouble) -> (g : A -> NonNegDouble) ->
> (p : (a : A) -> f a `LTE` g a) -> (sp : SimpleProb A) ->
> meas (fmap f sp) `LTE` meas (fmap g sp)
> Monotone = Functor.Predicates.Monotone {B = NonNegDouble} {C = NonNegDouble} {F = SimpleProb} LTE LTE
> -}
> module Functor.Predicates
> %default total
> %access public export
> %auto_implicits off
* Naturality
> ||| What it means for a transformation to be natural
> Natural : {F, G : Type -> Type} ->
> (Functor F) => (Functor G) =>
> (t : {A : Type} -> F A -> G A) ->
> Type
>
> Natural {F} {G} t = {A, B : Type} ->
> (f : A -> B) ->
> (x : F A) ->
> t (map f x) = map f (t x)
> {-
> ||| What it means for a transformation to be natural
> Natural : {F, G : Type -> Type} ->
> (Functor F) => (Functor G) =>
> (t : (A : Type) -> F A -> G A) ->
> Type
>
> Natural {F} {G} t = {A, B : Type} ->
> (f : A -> B) ->
> (x : F A) ->
> t B (map f x) = map f (t A x)
> -}
* Monotonicity
> ||| What it means for a measure to be monotone
> Monotone : {B, C : Type} -> {F : Type -> Type} -> (Functor F) =>
> (LTE_B : B -> B -> Type) ->
> (LTE_C : C -> C -> Type) ->
> (measure : F B -> C) ->
> Type
>
> Monotone {B} {C} {F} LTE_B LTE_C measure =
> {A : Type} ->
> (f : A -> B) ->
> (g : A -> B) ->
> (p : (a : A) -> f a `LTE_B` g a) ->
> (x : F A) ->
> measure (map f x) `LTE_C` measure (map g x)
> {-
> ---}
> module Matrix.Matrix
> import Data.Vect
> %default total
> %access public export
> Matrix : (m : Nat) -> (n : Nat) -> Type -> Type
> Matrix m n t = Vect m (Vect n t)
> module Matrix.Operations
> import Data.Fin
> import Data.Vect
> import Matrix.Matrix
> %default total
> %access public export
> %auto_implicits on
> row : (Fin m) -> Matrix m n t -> Vect n t
> row k xss = index k xss
> toVect : Matrix m n t -> Vect (m * n) t
> toVect = concat
> module NonNegDouble.Measures
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Constants
> import NonNegDouble.Operations
> import NonNegDouble.Properties
> %default total
> %access public export
> %auto_implicits off
> using implementation FractionalNonNegDouble
> |||
> average : List NonNegDouble -> NonNegDouble
> average xs = (sum xs) * ( one / fromNat (length xs))
> {-
> ---}
......@@ -16,6 +16,8 @@
> LTE x y = LTE (toDouble x) (toDouble y)
> ||| Proofs that `x` is equal to `y`
> EQ : (x, y : NonNegDouble) -> Type
> EQ x y = EQ (toDouble x) (toDouble y)
> module Num.Operations
> import Dat