Added components for the implementation of 'next'.

FastSimpleProb/BasicOperations.lidr

+> module FastSimpleProb.BasicOperations
+
+> import Data.List
+> import Data.So
+> import Syntax.PreorderReasoning
+
+> import FastSimpleProb.SimpleProb
+> import Double.Predicates
+> import NonNegDouble.NonNegDouble
+> import NonNegDouble.Constants
+> import NonNegDouble.BasicOperations
+> import NonNegDouble.Operations
+> import NonNegDouble.Properties
+> import NonNegDouble.Postulates
+> import List.Operations
+> import List.Properties
+> import Fun.Operations
+> import Pairs.Operations
+
+> %default total
+> %access public export
+> %auto_implicits off
+
+
+> using implementation NumNonNegDouble
+>   |||
+>   mkSimpleProb : {A : Type} -> 
+>                  (aps : List (A, NonNegDouble)) -> 
+>                  {auto prf : Positive (toDouble (sumMapSnd aps))} ->
+>                  SimpleProb A
+>   mkSimpleProb aps {prf} = MkSimpleProb aps prf
+
+
+> |||
+> toList : {A : Type} -> SimpleProb A -> List (A, NonNegDouble)
+> toList (MkSimpleProb aps _) = aps
+
+
+> |||
+> support : {A : Type} -> SimpleProb A -> List A
+> support = (map fst) . toList
+
+
+> using implementation NumNonNegDouble
+>   |||
+>   rescale : {A : Type} -> 
+>             (p : NonNegDouble) -> Positive (toDouble p) -> SimpleProb A -> SimpleProb A
+>   rescale {A} p pp (MkSimpleProb aps psum) = MkSimpleProb aps' psum' where
+>     aps'  : List (A, NonNegDouble)
+>     aps'  = mapIdRightMult (aps, p)
+>     psum' : Positive (toDouble (sumMapSnd aps'))
+>     psum' = mapIdRightMultPreservesPositivity aps psum p pp
+
+
+> using implementation NumNonNegDouble
+>   using implementation FractionalNonNegDouble
+>     |||
+>     normalize : {A : Type} -> 
+>                 SimpleProb A -> SimpleProb A
+>     normalize (MkSimpleProb aps psum) = 
+>       let p  : NonNegDouble
+>              = one / (sumMapSnd aps) in
+>       let pp : Positive (toDouble p)
+>              = divPreservesPositivity positiveOne psum in 
+>       rescale p pp (MkSimpleProb aps psum) 
+
+
+> |||
+> weights : {A : Type} -> SimpleProb A -> List NonNegDouble
+> weights = (map snd) . toList
+
+
+> using implementation NumNonNegDouble
+>   ||| 'weight sp a' is the weight of 'a' according to 'sp'
+>   weight : {A : Type} -> (Eq A) => SimpleProb A -> A -> NonNegDouble
+>   weight sp a = foldr f (fromInteger 0) (toList sp) where
+>     f : (A, NonNegDouble) -> NonNegDouble -> NonNegDouble
+>     f (a', w') w = if (a == a') then w + w' else w
+
+
+> using implementation FractionalNonNegDouble
+>   ||| 'prob sp a' is the probability of 'a' according to 'sp'
+>   prob : {A : Type} -> (Eq A) => SimpleProb A -> A -> NonNegDouble
+>   prob sp a = (weight sp a) / (sum (weights sp))
+
+> {-
+> ||| 'prob sp a' is the probability of 'a' according to 'sp'
+> prob : {A : Type} -> (Eq A) => SimpleProb A -> A -> Double
+> prob sp a = fst pq / snd pq where
+>   f : (A, Double) -> (Double, Double) -> (Double, Double)
+>   f (a', p') (p, q) = if (a == a') then (p + p', q + p') else (p, q + p')
+>   pq : (Double, Double)
+>   pq = foldr f (0.0, 0.0) (toList sp)
+> -}
+
+
+> using implementation NumNonNegDouble
+>   ||| Make a SimpleProb in which all elements of a list have the same 
+>   ||| probablility. If the list has no duplicates, this results in a
+>   ||| uniform probability distribution
+>   mkFlatSimpleProb : {A : Type} -> (as : List A) -> List.Operations.NonEmpty as -> SimpleProb A
+>   mkFlatSimpleProb      Nil              prf = absurd prf
+>   mkFlatSimpleProb {A} (a :: Nil)        _   = MkSimpleProb [(a, one)] positiveOne
+>   mkFlatSimpleProb {A} (a :: (a' :: as)) _   = MkSimpleProb aps prf where
+>     ps' : SimpleProb A
+>     ps' = assert_total (mkFlatSimpleProb (a' :: as) ())
+>     aps : List (A, NonNegDouble)
+>     aps = (a, one) :: (toList ps')
+>     prf : Positive (toDouble (sumMapSnd aps))
+>     prf = sumMapSndConsLemma1 a 1.0 positiveOne (MkLTE Oh) (toList ps')
+
+
+> using implementation NumNonNegDouble
+>   using implementation EqNonNegDouble
+>     |||
+>     trim : {A : Type} -> (Eq A) => 
+>            SimpleProb A -> SimpleProb A
+>     trim {A} (MkSimpleProb aps psum) = MkSimpleProb aps' psum' where
+>       aps'  : List (A, NonNegDouble)
+>       aps'  = discardBySndZeroEq aps
+>       psum' : Positive (toDouble (sumMapSnd aps'))
+>       psum' = replace {P = \ X => Positive (toDouble X)} (sym (discardBySndZeroLemmaEq aps)) psum
+
+
+> using implementation ShowNonNegDouble
+>   ||| 
+>   showlong : {A : Type} -> Show A => SimpleProb A -> String
+>   showlong sp = showlong (toList sp) 
+
+
+> {-
+
+> ---}    
+
+
+
+

NonNegDouble/Postulates.lidr

+> module NonNegDouble.Postulates
+
+> import NonNegDouble.Properties
+> import Double.Predicates
+> import Double.Properties
+> import NonNegDouble.NonNegDouble
+> import NonNegDouble.BasicOperations
+> import NonNegDouble.Operations
+> import NonNegDouble.Properties
+> import List.Operations
+
+
+> %default total
+> %access public export
+
+
+* Properties of sums of products:
+
+> using implementation NumNonNegDouble
+>   |||
+>   postulate 
+>   mapIdRightMultPreservesPositivity : 
+>     {A : Type} ->
+>     (axs : List (A, NonNegDouble)) -> 
+>     Positive (toDouble (sumMapSnd axs)) ->
+>     (y : NonNegDouble) -> 
+>     Positive (toDouble y) ->
+>     Positive (toDouble (sumMapSnd (mapIdRightMult (axs, y))))
+
+
+> using implementation NumNonNegDouble
+>   ||| 
+>   postulate 
+>   sumMapSndConsLemma1 : 
+>     {A : Type} ->
+>     (a : A) ->
+>     (x : Double) ->
+>     (px : Positive x) ->
+>     (nnx : NonNegative x) ->
+>     (axs : List (A, NonNegDouble)) -> 
+>     Positive (toDouble (sumMapSnd ((a, Element x nnx) :: axs)))
+
+
+> using implementation NumNonNegDouble
+>   |||
+>   postulate 
+>   mvMultLemma : {A, B : Type} ->
+>                 (axs : List (A, NonNegDouble)) -> 
+>                 Positive (toDouble (sumMapSnd axs)) -> 
+>                 (f : A -> List (B, NonNegDouble)) -> 
+>                 ((a : A) -> Positive (toDouble (sumMapSnd (f a)))) ->
+>                 Positive (toDouble (sumMapSnd (mvMult axs f)))
+
+
+> {-
+
+> ---}
+ 
+ 
+ 
+ 

Num/Refinements.lidr

+> module Num.Refinements
+
+
+> %default total
+
+> %access public export
+
+
+> |||
+> interface (Num t) => NumPlusZeroNeutral t where
+>   plusZeroLeftNeutral  : (x : t) -> 0 + x = x
+>   plusZeroRightNeutral : (x : t) -> x + 0 = x
+
+
+> |||
+> interface (NumPlusZeroNeutral t) => NumPlusAssociative t where
+> -- interface (Num t) => NumPlusAssociative t where
+>   plusAssociative : (x, y, z : t) -> x + (y + z) = (x + y) + z
+
+
+> |||
+> interface (NumPlusAssociative t) => NumMultZeroOne t where
+> -- interface (Num t) => NumMultZeroOne t where
+>   multZeroRightZero   : (x : t) -> x * 0 = 0
+>   multZeroLeftZero    : (x : t) -> 0 * x = 0
+>   multOneRightNeutral : (x : t) -> x * 1 = x
+>   multOneLeftNeutral  : (x : t) -> 1 * x = x
+
+
+> |||
+> interface (NumMultZeroOne t) => NumMultDistributesOverPlus t where
+> -- interface (Num t) => NumMultDistributesOverPlus t where
+>   multDistributesOverPlusRight : (x, y, z : t) -> x * (y + z) = (x * y) + (x * z)
+>   multDistributesOverPlusLeft  : (x, y, z : t) -> (x + y) * z = (x * z) + (y * z)

Unit/Properties.lidr

+> module Unit.Properties
+
+
+> import Data.Fin
+> import Control.Isomorphism
+
+> import Finite.Predicates
+> import Sigma.Sigma
+> import Pairs.Operations
+> import Basic.Predicates
+
+
+> %default total
+
+> %access public export
+
+
+> ||| Mapping |Unit|s to |Fin|s
+> toFin : Unit -> Fin (S Z)
+> toFin MkUnit = FZ
+> -- %freeze toFin
+
+
+> ||| Mapping |Fin (S Z)|s to |Unit|s
+> fromFin : Fin (S Z) -> Unit
+> fromFin  FZ = MkUnit
+> fromFin (FS k) = absurd k
+> -- %freeze fromFin
+
+
+> ||| |toFin| is the left-inverse of |fromFin|
+> toFinFromFinLemma : (k : Fin (S Z)) -> toFin (fromFin k) = k
+> toFinFromFinLemma FZ = Refl
+> toFinFromFinLemma (FS k) = absurd k
+> %freeze toFinFromFinLemma
+
+
+> ||| |fromFin| is the left-inverse of |toFin|
+> fromFinToFinLemma : (e : Unit) -> fromFin (toFin e) = e
+> fromFinToFinLemma MkUnit = Refl
+> %freeze fromFinToFinLemma
+
+
+> ||| Unit is not empty
+> notEmptyUnit : Not (Empty Unit)
+> notEmptyUnit contra = contra ()
+
+
+> ||| Unit is finite
+> finiteUnit : Finite Unit
+> finiteUnit = MkSigma (S Z) iso where
+>   iso : Iso Unit (Fin (S Z))
+>   iso = MkIso toFin fromFin toFinFromFinLemma fromFinToFinLemma
+
+
+> ||| Unit is decidable
+> decidableUnit : Dec Unit
+> decidableUnit = Yes MkUnit
+
+
+> {-
+
+> ---}

VeriFunctor/VeriFunctor.lidr

+> module VeriFunctor.VeriFunctor
+
+> import Fun.Predicates
+
+> %default total
+> %access public export
+> %auto_implicits off
+
+> interface Functor F => VeriFunctor (F : Type -> Type) where
+> 
+>   mapPresId    : {A : Type} -> ExtEq {A = F A} (map id) id
+>   
+>   mapPresComp  : {A, B, C : Type} -> (f : A -> B) -> (g : B -> C) -> 
+>                  ExtEq {A = F A} (map (g . f)) (map g . map f)
+>                 
+>   mapPresExtEq : {A, B : Type} -> (f, g : A -> B) -> 
+>                  ExtEq f g -> ExtEq {A = F A} (map f) (map g)
+
+> {-
+
+> ---}
+

VeriMonad/VeriMonad.lidr

+> module VeriMonad.VeriMonad
+
+> import Syntax.PreorderReasoning
+
+> import Fun.Predicates
+> import VeriFunctor.VeriFunctor
+
+> %default total
+> %access public export
+> %auto_implicits off
+
+> infixl 1 >>=
+
+
+A Monad is an endo-functor M on a category ℂ together with two natural
+transformations η and μ such that
+
+       η (M X)             M (η X)
+  M X ---------> M (M X) <--------- M X 
+                    |
+                    |
+                    | μ X
+                    |
+                    |
+                   M X
+
+   (4)  (μ X) . (η (M X)) = id
+
+   (5)  (μ X) . (M (η X)) = id
+
+and
+
+                  M (μ X)
+     M (M (M X)) ---------> M (M X)
+          |                  |
+          |                  |
+  μ (M X) |                  | μ X
+          |                  |
+          |                  |
+       M (M X) -----------> M X
+                  μ X
+
+  (6)  (μ X) . (M (μ X)) = (μ X) . (μ (M X))
+
+The naturality conditions for η and μ can be expressed as
+
+  (2)  (M f) . (η X) = (η Y) . f --- (map f) . ret = ret . f
+
+and
+
+  (3)  (M f) . (μ X) = (μ (M X)) . (M (M f)) --- (map f) . join = join . (map (map f))
+
+In Idris, η and μ are called |pure| and |join|, respectively 
+
+  pure : {M : Type -> Type} -> {X : Type} -> Monad M => X -> M X 
+
+  join : {M : Type -> Type} -> {X : Type} -> Monad M => M (M X) -> M X 
+
+The Idris |Monad| interface from "Prelude/Monad.idr" provides default
+implementations of bind (|>>=|) and |join| that fulfill the
+specification
+
+  (1)  >>= f = join . map f 
+
+and the conditions (1-6) can be expressed through a |VeriMonad|
+refinement of |VeriFunctor| and of |Monad|:
+
+> ||| 
+> interface (VeriFunctor M, Monad M) => VeriMonad (M : Type -> Type) where
+> 
+>   bindJoinMapSpec : {A, B : Type} -> (f : A -> M B) -> ExtEq (>>= f) (join . map f)
+>
+>   pureNatTrans    : {A, B : Type} -> (f : A -> B) -> ExtEq {B = M B} (map f . pure) (pure . f)
+> 
+>   joinNatTrans    : {A, B : Type} -> (f : A -> B) -> ExtEq {A = M (M A)} (map f . join) (join . map (map f))              
+>
+>   triangleLeft    : {A : Type} -> ExtEq {A = M A} (join . pure) id
+>
+>   triangleRight   : {A : Type} -> ExtEq {A = M A} (join . map pure) id         
+>
+>   square          : {A : Type} -> ExtEq {A = M (M (M A))} (join . map join) (join . join)         
+
+For a |VeriMonad|, one can show that |>>=| preserves extensional equality
+
+> ||| ∀ f, ∀ g, (∀ a, f a = g a) => (∀ ma, map f ma = map g ma)
+> bindPresExtEq : {M : Type -> Type} -> {A, B : Type} -> (VeriMonad M) => 
+>                 (f, g : A -> M B) -> ExtEq f g -> ExtEq (>>= f) (>>= g) 
+>                 
+> bindPresExtEq f g eeqfg ma = ( ma >>= f ) 
+>                            ={ bindJoinMapSpec f ma }=
+>                              ( join (map f ma) )
+>                            ={ cong (mapPresExtEq f g eeqfg ma) }=
+>                              ( join (map g ma) )   
+>                            ={ sym (bindJoinMapSpec g ma) }=
+>                              ( ma >>= g ) 
+>                            QED
+
+, the monadic laws
+
+> ||| ∀ f, ∀ a,  (pure a) >>= f = f a
+> leftIdentity : {M : Type -> Type} -> {A, B : Type} -> (VeriMonad M) => 
+>                (f : A -> M B) -> ExtEq (\ a => (pure a) >>= f) f
+>                
+> leftIdentity f a = ( (pure a) >>= f )
+>                  ={ bindJoinMapSpec f (pure a) }=
+>                    ( join (map f (pure a)) )
+>                  ={ cong {f = join} (pureNatTrans f a) }=
+>                    ( join (pure (f a)) )
+>                  ={ triangleLeft (f a) }=
+>                    ( f a )
+>                  QED
+
+
+> ||| ∀ ma,  ma >>= pure = ma
+> rightIdentity : {M : Type -> Type} -> {A : Type} -> (VeriMonad M) => 
+>                 ExtEq {A = M A} (>>= pure) id
+>                 
+> rightIdentity ma = ( ma >>= pure )
+>                  ={ bindJoinMapSpec pure ma }=
+>                    ( join (map pure ma) )
+>                  ={ triangleRight ma }=
+>                    ( ma )
+>                  QED            
+
+
+> ||| ∀ f, ∀ g, ∀ ma,  (ma >>= f) >>= g = ma >>= (\ a => (f a) >>= g)
+> associativity : {M : Type -> Type} -> {A, B, C : Type} -> (VeriMonad M) => 
+>                 (f : A -> M B) -> (g : B -> M C) -> 
+>                 ExtEq (\ ma => (ma >>= f) >>= g) (>>= (\ x => (f x) >>= g))
+>                 
+> associativity f g ma = ( (ma >>= f) >>= g )
+>                      ={ bindJoinMapSpec g (ma >>= f) }=
+>                        ( join (map g (ma >>= f)) )
+>                      ={ cong {f = \ X => join (map g X)} (bindJoinMapSpec f ma) }=
+>                        ( join (map g (join (map f ma))) )
+>                      ={ cong (joinNatTrans g (map f ma)) }=
+>                        ( join (join (map (map g) (map f ma))) )
+>                      ={ sym (square (map (map g) (map f ma))) }=
+>                        ( join (map join (map (map g) (map f ma))) )
+>                      ={ Refl }=
+>                        ( join (map join ((map (map g) . (map f)) ma)) )
+>                      ={ cong {f = \ X => join (map join X)} (sym (mapPresComp f (map g) ma)) }=
+>                        ( join (map join (map ((map g) . f) ma)) )
+>                      ={ Refl }=
+>                        ( join (((map join) . (map ((map g) . f))) ma) )
+>                      ={ cong (sym (mapPresComp ((map g) . f) join ma)) }=
+>                        ( join (map (join . ((map g) . f)) ma) ) 
+>                      ={ Refl }=
+>                        ( join (map (\ a => join (map g (f a))) ma) ) 
+>                      ={ cong (mapPresExtEq (\ a => join (map g (f a))) 
+>                                            (\ a => (f a) >>= g)
+>                                            (\ a => sym (bindJoinMapSpec g (f a))) 
+>                                            ma) }=
+>                        ( join (map (\ a => (f a) >>= g) ma) )
+>                      ={ sym (bindJoinMapSpec (\ a => (f a) >>= g) ma) }=
+>                        ( ma >>= (\ a => (f a) >>= g) )
+>                      QED
+
+and some more generic results that turn out to be very usful in
+applications, see for instance
+"IdrisLibs/TimeDiscreteDynamicalSystems/Monadic.lidr":
+
+> ||| ∀ f, ∀ g, ∀ ma,  map f (join (map g ma)) = join (map (map f . g) ma)
+> mapJoinLemma : {M : Type -> Type} -> {A, B, C : Type} -> (VeriMonad M) => 
+>                (f : B -> C) -> (g : A -> M B) -> 
+>                ExtEq {A = M A} {B = M C} (map f . (join . map g)) (join . map (map f . g))
+>
+> mapJoinLemma f g ma = ( map f (join (map g ma)) )
+>                     ={ joinNatTrans f (map g ma) }=
+>                       ( join (map (map f) (map g ma)) )
+>                     ={ Refl }=
+>                       ( join ((map (map f) . (map g)) ma) )
+>                     ={ cong (sym (mapPresComp g (map f) ma)) }=
+>                       ( join (map (map f . g) ma) )
+>                     QED
+
+
+> ||| ∀ f, ∀ g, ∀ ma,  map f (ma >>= g) = ma >>= map f . g
+> mapBindLemma : {M : Type -> Type} -> {A, B, C : Type} -> (VeriMonad M) => 
+>                (f : B -> C) -> (g : A -> M B) -> 
+>                ExtEq {A = M A} (\ ma => map f (ma >>= g)) (>>= map f . g)
+>
+> mapBindLemma f g ma = ( map f (ma >>= g) )
+>                     ={ cong (bindJoinMapSpec g ma) }=
+>                       ( map f (join (map g ma)) )
+>                     ={ mapJoinLemma f g ma }=
+>                       ( join (map (map f . g) ma) ) 
+>                     ={ sym (bindJoinMapSpec (map f . g) ma) }=
+>                       ( ma >>= map f . g )
+>                     QED
+
+> ||| ∀ f, ∀ g, ∀ ma, join (map (map f . g) ma  =  ma >>= map f . g 
+> mapJoinMapBindLemma : {M : Type -> Type} -> {A, B, C : Type} -> (VeriMonad M) => 
+>                       (f : B -> C) -> (g : A -> M B) -> 
+>                       ExtEq (join . map (map f . g)) (>>= map f . g)
+> mapJoinMapBindLemma f g ma = ( join (map (map f . g) ma) )
+>                                ={ sym (mapJoinLemma f g ma) }=
+>                              ( map f (join (map g ma)) )
+>                                ={ cong (sym (bindJoinMapSpec g ma)) }=
+>                              ( map f (ma >>= g) )
+>                                ={ mapBindLemma f g ma }=
+>                              ( ma >>= map f . g )
+>                                QED
+
+
+> {-               
+                                                
+> ---}
+
+ 

Void/Properties.lidr

+> module Void.Properties
+
+
+> import Data.Fin
+> import Control.Isomorphism
+
+> import Finite.Predicates
+> import Sigma.Sigma
+
+
+> %default total
+
+> %access public export
+
+
+> ||| Mapping |Void|s to |Fin|s
+> toFin : Void -> Fin Z
+> toFin = void
+> %freeze toFin
+
+
+> ||| Mapping |Fin Z|s to |Void|s
+> fromFin : Fin Z -> Void
+> fromFin k = absurd k
+> %freeze fromFin 
+
+
+> ||| |toFin| is the left-inverse of |fromFin|
+> toFinFromFinLemma : (k : Fin Z) -> toFin (fromFin k) = k
+> toFinFromFinLemma k = absurd k
+> %freeze toFinFromFinLemma
+
+
+> ||| |fromFin| is the left-inverse of |toFin|
+> fromFinToFinLemma : (e : Void) -> fromFin (toFin e) = e
+> fromFinToFinLemma e = void e
+> %freeze fromFinToFinLemma
+
+
+> ||| Void is finite
+> finiteVoid : Finite Void
+> finiteVoid = MkSigma Z iso where
+>   iso : Iso Void (Fin Z)
+>   iso = MkIso toFin fromFin toFinFromFinLemma fromFinToFinLemma
+
+
+> ||| Void is decidable
+> decidableVoid : Dec Void
+> decidableVoid = No void
+
+
+> {-
+
+> ---}