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

Adding components needed for the responsibility manuscript.

parent be8971ff
> module Basic.Properties
> import Basic.Predicates
> import Basic.Operations
> %default total
> %access public export
* Properties of |Empty|:
> emptyPairFst : {A, B : Type} -> Empty A -> Empty (A, B)
> emptyPairFst contra = contra . fst
> emptyPairSnd : {A, B : Type} -> Empty B -> Empty (A, B)
> emptyPairSnd contra = contra . snd
> notEmptyPair : {A, B : Type} -> Not (Empty A) -> Not (Empty B) -> Not (Empty (A, B))
> notEmptyPair contraFst contraSnd contra = contraFst (contraSnd . (curry contra))
> -- curry contra : A -> B -> Void
> -- contraSnd . (curry contra) : A -> Void
> -- contraFst (contraSnd . (curry contra)) : Void
* Replace properties:
> |||
> replaceLemma : {a : _} -> {x : _} -> {y : _} -> {P : a -> Type} ->
> (prf : x = y) -> (px : P x) -> replace prf px = px
> replaceLemma Refl px = Refl
> |||
> replaceLemma2 : {A : Type} -> {P : A -> Type} -> {Q : (a : A) -> P a -> Type} ->
> {a1 : A} -> {a2 : A} ->
> (f : (a : A) -> (pa : P a) -> Q a pa) ->
> (prf : a1 = a2) ->
> (pa2 : P a2) ->
> f a1 (replace (sym prf) pa2) = f a2 pa2
> replaceLemma2 f Refl pa2 = Refl
module BoundedNat.Operations
import Data.Nat
import Data.Vect
import Sigma.Sigma
import BoundedNat.BoundedNat
|||
idx : {n : Nat} -> Vect n alpha -> Blt n -> alpha
idx {n = Z} Nil b impossible -- = void (ltZ_bot (getProof b))
-- idx {n = S m} (a :: as) (Z ** _) = a
-- idx {n = S m} (a :: as) (S k ** q) = idx {n = m} as (k ** lemma5 q)
> module Double.Operations
> import Data.So
> import Data.Fin
> import Double.Predicates
> import So.Properties
> %default total
> %access public export
> |||
> fromNat : (n : Nat) -> Double
> fromNat Z = 0.0
> fromNat (S m) = 1.0 + (fromNat m)
> |||
> fromFin : {n : Nat} -> Fin n -> Double
> fromFin = fromNat . finToNat
> |||
> mkLinear : Double -> Double -> Double -> Double
> mkLinear a b x = a + b * x
> mkLinearStep : (x1 : Double) -> (x2 : Double) -> Positive (x2 - x1) ->
> (y1 : Double) -> (y2 : Double) ->
> Double -> Double
> mkLinearStep x1 x2 px2mx1 y1 y2 x with (decSo (x < x1))
> | Yes _ = y1
> | No _ with (decSo (x1 <= x && x <= x2))
> | Yes _ = y1 * (1.0 - alpha) + y2 * alpha where
> alpha : Double
> alpha = (x - x1) / (x2 - x1)
> | No _ = y2
> module Double.Postulates
> import Data.So
> import Double.Predicates
> %default total
> %access public export
> %auto_implicits on
* Arithmetic
> |||
> postulate
> plusZeroLeftNeutral : {x : Double} -> 0.0 + x = x
> |||
> postulate
> plusZeroRightNeutral : {x : Double} -> x + 0.0 = x
> |||
> postulate
> multZeroLeftZero : {x : Double} -> 0.0 * x = 0.0
> |||
> postulate
> multZeroRightZero : {x : Double} -> x * 0.0 = 0.0
> |||
> postulate
> minusSelfZero : {x : Double} -> x - x = 0.0
> |||
> postulate
> plusAssociative : (x : Double) -> (y : Double) -> (z : Double) ->
> x + (y + z) = (x + y) + z
* |LTE|:
> ||| LTE is reflexive
> postulate
> reflexiveLTE : (x : Double) -> x `LTE` x
> ||| LTE is transitive
> postulate
> transitiveLTE : (x, y, z : Double) -> x `LTE` y -> y `LTE` z -> x `LTE` z
> ||| LTE is monotone w.r.t. addition
> postulate
> monotonePlusLTE : {a, b, c, d : Double} ->
> a `LTE` b -> c `LTE` d -> a + c `LTE` b + d
> ||| LTE is monotone w.r.t. multiplication
> postulate
> monotoneMultLTE : {a, b, c, d : Double} ->
> a `LTE` b -> c `LTE` d -> a * c `LTE` b * d
> ||| LTE is monotone w.r.t. "subtraction of a const"
> postulate
> monotoneMinusConstLTE : {a, b, c : Double} ->
> a `LTE` b -> a - c `LTE` b - c
> ||| LTE is monotone w.r.t. "division by a const"
> postulate
> monotoneDivConstLTE : {a, b, c : Double} ->
> a `LTE` b -> Positive c -> a / c `LTE` b / c
> ||| LTE is unique
> postulate
> uniqueLTE : {x, y : Double} -> (p : x `LTE` y) -> (q : x `LTE` y) -> p = q
* |LT|:
> ||| LT is unique
> postulate
> uniqueLT : {x, y : Double} -> (p : x `LT` y) -> (q : x `LT` y) -> p = q
* Non-negative double precision floating point numbers:
> ||| Non-negative |Double|s are closed w.r.t. "subtraction"
> postulate
> minusPreservesNonNegativity : {x, y : Double} ->
> NonNegative x -> NonNegative y -> y `LTE` x -> NonNegative (x - y)
> ||| Non-negative |Double|s are closed w.r.t. division
> postulate
> divPreservesNonNegativity : {x, y : Double} ->
> NonNegative x -> NonNegative y -> NonNegative (x / y)
* Positive double precision floating point numbers:
> |||
> postulate
> positivePlusAnyPositive : {x, y : Double} ->
> Positive x -> NonNegative y -> Positive (x + y)
> ||| Positive |Double|s are closed w.r.t. division
> postulate
> divPreservesPositivity : {x, y : Double} ->
> Positive x -> Positive y -> Positive (x / y)
> |||
> postulate
> divPositiveSelfOne : {x : Double} -> Positive x -> x / x = 1.0
> |||
> postulate
> divZeroPositiveZero : {x : Double} -> Positive x -> 0.0 / x = 0.0
* Ord methods:
> |||
> postulate
> gtLT : {x, y : Double} -> So (x > y) -> So (y < x)
> postulate
> notCompareEQ : {x, y : Double} -> Not (So (x == y)) -> Not (EQ = compare x y)
> module Double.Predicates
> import Data.So
> %default total
> %access public export
> %auto_implicits on
* EQ
> |||
> data EQ : Double -> Double -> Type where
> MkEQ : {x : Double} -> {y : Double} -> So (x == y) -> EQ x y
* LT
> |||
> data LT : Double -> Double -> Type where
> MkLT : {x : Double} -> {y : Double} -> So (x < y) -> LT x y
* LTE
> |||
> data LTE : Double -> Double -> Type where
> MkLTE : {x : Double} -> {y : Double} -> So (x <= y) -> LTE x y
* Non-negative, positive
> -- |||
> -- data NonNegative : Double -> Type where
> -- MkNonNegative : {x : Double} -> So (0.0 <= x) -> NonNegative x
> -- |||
> -- data Positive : Double -> Type where
> -- MkPositive : {x : Double} -> So (0.0 < x) -> Positive x
> |||
> NonNegative : (x : Double) -> Type
> NonNegative x = 0.0 `LTE` x
> |||
> Positive : (x : Double) -> Type
> Positive x = 0.0 `LT` x
> module Double.Properties
> import Data.So
> import Double.Predicates
> import Double.Postulates
> import Double.Operations
> import So.Properties
> import Ordering.Properties
> import Rel.TotalPreorder
> import So.Properties
> import Interfaces.Math
> %default total
> %access public export
> %auto_implicits on
* Implementations
> implementation Math Double where
> exp = Prelude.Doubles.exp
> sin = Prelude.Doubles.sin
> cos = Prelude.Doubles.cos
* Decidability of EQ
> |||
> decEQ : (x : Double) -> (y : Double) -> Dec (x `EQ` y)
> decEQ x y with (decSo (x == y))
> | Yes p = Yes (MkEQ p)
> | No contra = No (\ (MkEQ p) => contra p)
* Properties of Ord methods
> |||
> LTinLTE : {x, y : Double} -> So (x < y) -> So (x <= y)
> LTinLTE {x} {y} prf = soOrIntro1 (x < y) (x == y) prf
> -- LTinLTE : {x, y : Double} -> x `LT` y -> x `LTE` y
> -- LTinLTE {x} {y} (MkLT prf) = MkLTE (soOrIntro1 (x < y) (x == y) prf)
> |||
> EQinLTE : {x, y : Double} -> So (x == y) -> So (x <= y)
> EQinLTE {x} {y} prf = soOrIntro2 (x < y) (x == y) prf
> |||
> compareLT : {x, y : Double} -> LT = compare x y -> So (x < y)
> compareLT {x} {y} p with (compare x y)
> compareLT {x} {y} _ | LT = Oh
> compareLT {x} {y} p | EQ = absurd p
> compareLT {x} {y} p | GT = absurd p
> compareEQ : {x, y : Double} -> EQ = compare x y -> So (x == y)
> compareEQ {x} {y} p with (compare x y) proof prf
> | LT = absurd p
> | EQ with (decSo (x == y))
> | (Yes q) = q
> | (No c) = void (notCompareEQ c prf)
> | GT = absurd p
> compareEQ' : {x, y : Double} -> So (x == y) -> compare x y = EQ
> compareEQ' {x} {y} p with (x == y) proof q
> | True = Refl
> | False = absurd p
> |||
> compareGT : {x, y : Double} -> GT = compare x y -> So (x > y)
> compareGT {x} {y} p with (compare x y)
> compareGT {x} {y} p | LT = absurd p
> compareGT {x} {y} p | EQ = absurd p
> compareGT {x} {y} _ | GT = Oh
* LT, LTE:
> ||| LTE is total
> totalLTE : (x, y : Double) -> Either (x `LTE` y) (y `LTE` x)
> totalLTE x y with (compare x y) proof prf
> | LT = Left (MkLTE (LTinLTE (compareLT prf)))
> | EQ = Left (MkLTE (EQinLTE (compareEQ prf)))
> | GT = Right (MkLTE (LTinLTE (gtLT (compareGT prf))))
> ||| LTE is a total preorder
> totalPreorderLTE : TotalPreorder Double.Predicates.LTE
> totalPreorderLTE = MkTotalPreorder LTE reflexiveLTE transitiveLTE totalLTE
> ||| LT is decidable
> decLT : (x : Double) -> (y : Double) -> Dec (x `LT` y)
> decLT x y with (decSo (x < y))
> | Yes prf = Yes (MkLT prf)
> | No contra = No (\ (MkLT prf) => void (contra prf))
> ||| LTE is decidable
> decLTE : (x : Double) -> (y : Double) -> Dec (x `LTE` y)
> decLTE x y with (decSo (x <= y))
> | Yes prf = Yes (MkLTE prf)
> | No contra = No (\ (MkLTE prf) => void (contra prf))
> |||
> minusLTELemma : (x : Double) -> (y : Double) ->
> x `LTE` y -> 0.0 `LTE` y - x
> minusLTELemma x y xLTEy = s2 where
> s1 : x - x `LTE` y - x
> s1 = monotoneMinusConstLTE xLTEy
> s2 : 0.0 `LTE` y - x
> s2 = replace {P = \ X => X `LTE` y - x} (minusSelfZero) s1
> |||
> divLTELemma : (x : Double) -> (y : Double) -> x `LTE` y ->
> Positive y -> x / y `LTE` 1.0
> divLTELemma x y xLTEy py = s2 where
> s1 : x / y `LTE` y / y
> s1 = monotoneDivConstLTE xLTEy py
> s2 : x / y `LTE` 1.0
> s2 = replace {P = \ X => x / y `LTE` X} (divPositiveSelfOne py) s1
> |||
> divNonNegativePositiveNonNegative : (x : Double) -> (y : Double) ->
> 0.0 `LTE` x -> Positive y ->
> 0.0 `LTE` x / y
> divNonNegativePositiveNonNegative x y zLTEx py = s2 where
> s1 : 0.0 / y `LTE` x / y
> s1 = monotoneDivConstLTE zLTEx py
> s2 : 0.0 `LTE` x / y
> s2 = replace {P = \ X => X `LTE` x / y} (divZeroPositiveZero py) s1
> ||| |sum| is monotone
> monotoneSum : {A : Type} ->
> (f : A -> Double) -> (g : A -> Double) ->
> (p : (a : A) -> f a `LTE` g a) ->
> (as : List A) ->
> sum (map f as) `LTE` sum (map g as)
> monotoneSum f g p Nil = reflexiveLTE 0.0
> monotoneSum f g p (a :: as) =
> monotonePlusLTE {a = f a} {b = g a} {c = sum (map f as)} {d = sum (map g as)} (p a) (monotoneSum f g p as)
* Non-negative double precision floating point numbers:
> ||| Non-negative |Double|s are closed w.r.t. sum
> plusPreservesNonNegativity : {x, y : Double} ->
> NonNegative x -> NonNegative y -> NonNegative (x + y)
> plusPreservesNonNegativity {x} {y} zeroLTEx zeroLTEy = s2 where
> s1 : 0.0 + 0.0 `LTE` x + y
> s1 = monotonePlusLTE {a = 0.0} {b = x} {c = 0.0} {d = y} zeroLTEx zeroLTEy
> s2 : 0.0 `LTE` x + y
> s2 = replace {P = \ X => X `LTE` x + y} plusZeroLeftNeutral s1
> ||| Non-negative |Double|s are closed w.r.t. multiplication
> multPreservesNonNegativity : {x, y : Double} ->
> NonNegative x -> NonNegative y -> NonNegative (x * y)
> multPreservesNonNegativity {x} {y} zeroLTEx zeroLTEy = s2 where
> s1 : 0.0 * 0.0 `LTE` x * y
> s1 = monotoneMultLTE {a = 0.0} {b = x} {c = 0.0} {d = y} zeroLTEx zeroLTEy
> s2 : 0.0 `LTE` x * y
> s2 = replace {P = \ X => X `LTE` x * y} (multZeroLeftZero {x = 0.0}) s1
* Positive double precision floating point numbers:
> |||
> positiveImpliesNonNegative : {x : Double} -> Positive x -> NonNegative x
> positiveImpliesNonNegative (MkLT prf) = MkLTE (LTinLTE prf)
* Properties of constants:
> ||| one is not zero
> notOneEqZero : Not (1.0 = 0.0)
> notOneEqZero Refl impossible
> ||| zero is not positive
> notPositiveZero : Not (Positive 0.0)
> notPositiveZero (MkLT prf) = contra Refl prf
* Properties of |fromNat|
> |||
> fromNatNonNegative : {n : Nat} -> NonNegative (fromNat n)
> fromNatNonNegative {n = Z} = MkLTE Oh
> fromNatNonNegative {n = S m} = plusPreservesNonNegativity (MkLTE Oh) fromNatNonNegative
> |||
> fromSuccPositive : {n : Nat} -> Positive (fromNat (S n))
> fromSuccPositive {n} = positivePlusAnyPositive (MkLT Oh) fromNatNonNegative
* Convexity
> |||
> convexLemma1 : (x1 : Double) -> (x2 : Double) -> Positive (x2 - x1) ->
> (x : Double) -> (q : x1 `LTE` x) ->
> 0.0 `LTE` (x - x1) / (x2 - x1)
> convexLemma1 x1 x2 px2mx1 x x1LTEx =
> divNonNegativePositiveNonNegative (x - x1) (x2 - x1) s1 px2mx1 where
> s1 : 0.0 `LTE` (x - x1)
> s1 = minusLTELemma x1 x x1LTEx
> |||
> convexLemma2 : (x1 : Double) -> (x2 : Double) -> Positive (x2 - x1) ->
> (x : Double) -> (q : x `LTE` x2) ->
> (x - x1) / (x2 - x1) `LTE` 1.0
> convexLemma2 x1 x2 px2mx1 x q = divLTELemma (x - x1) (x2 - x1) s1 px2mx1 where
> s1 : (x - x1) `LTE` (x2 - x1)
> s1 = monotoneMinusConstLTE q
> |||
> convexLemma : (x1 : Double) -> (x2 : Double) -> (alpha : Double) ->
> NonNegative x1 -> NonNegative x2 ->
> 0.0 `LTE` alpha -> alpha `LTE` 1.0 ->
> NonNegative (x1 * (1.0 - alpha) + x2 * alpha)
> convexLemma x1 x2 alpha nnx1 nnx2 (MkLTE p1) (MkLTE p2) = s4 where
> s1 : NonNegative alpha
> s1 = MkLTE p1
> s2 : alpha - alpha `LTE` 1.0 - alpha
> s2 = monotoneMinusConstLTE (MkLTE p2)
> s3 : NonNegative (1.0 - alpha)
> s3 = replace {P = \ X => X `LTE` 1.0 - alpha} minusSelfZero s2
> s4 : NonNegative (x1 * (1.0 - alpha) + x2 * alpha)
> s4 = plusPreservesNonNegativity {x = x1 * (1.0 - alpha)} {y = x2 * alpha}
> (multPreservesNonNegativity nnx1 s3)
> (multPreservesNonNegativity nnx2 s1)
* Properties of |mkLinearStepLemma|:
> |||
> mkLinearStepLemma : (x1 : Double) -> (x2 : Double) -> Positive (x2 - x1) ->
> (y1 : Double) -> (y2 : Double) ->
> NonNegative y1 -> NonNegative y2 ->
> (x : Double) -> NonNegative (mkLinearStep x1 x2 prf y1 y2 x)
> mkLinearStepLemma x1 x2 px2mx1 y1 y2 nny1 nny2 x with (decSo (x < x1))
> | Yes _ = nny1
> | No _ with (decSo (x1 <= x && x <= x2))
> | Yes prf = s3 where
> alpha : Double
> alpha = (x - x1) / (x2 - x1)
> s1 : 0.0 `LTE` alpha
> s1 = convexLemma1 x1 x2 px2mx1 x (MkLTE (soAndElim1 (x1 <= x) (x <= x2) prf))
> s2 : alpha `LTE` 1.0
> s2 = convexLemma2 x1 x2 px2mx1 x (MkLTE (soAndElim2 (x1 <= x) (x <= x2) prf))
> s3 : NonNegative (y1 * (1.0 - alpha) + y2 * alpha)
> s3 = convexLemma y1 y2 alpha nny1 nny2 s1 s2
> | No _ = nny2
> {-
> ---}
> module FastSimpleProb.SimpleProb
> import Data.So
> import Double.Predicates
> import NonNegDouble.NonNegDouble
> import NonNegDouble.BasicOperations
> import NonNegDouble.Properties
> import List.Operations
> %default total
> %access public export
> %auto_implicits off
> using implementation NumNonNegDouble
> |||
> data SimpleProb : Type -> Type where
> MkSimpleProb : {A : Type} ->
> (aps : List (A, NonNegDouble)) ->
> Positive (toDouble (sumMapSnd aps)) ->
> SimpleProb A
...@@ -22,9 +22,7 @@ ...@@ -22,9 +22,7 @@
> import Tuple.Properties > import Tuple.Properties
> %default total > %default total
> %access public export > %access public export
......
> module Interfaces.Math
> %default total
> %access public export
> %auto_implicits off
> interface (Num ty) => Math ty where
> exp : ty -> ty
> sin : ty -> ty
> cos : ty -> ty
> module List.Operations
> import Data.List
> import Data.List.Quantifiers
> import Syntax.PreorderReasoning
> import Sigma.Sigma
> import Fun.Operations
> -- import NumRefinements
> import Rel.TotalPreorder
> import Rel.TotalPreorderOperations
> import List.Predicates
> %default total
> %access public export
> %auto_implicits on
* |List| is a functor:
> ||| fmap
> fmap : {A, B : Type} -> (A -> B) -> List A -> List B
> fmap = map
* |List| is a monad:
> ||| ret
> ret : {A : Type} -> A -> List A
> ret = pure
> ||| bind
> bind : {A, B : Type} -> List A -> (A -> List B) -> List B
> bind = (>>=)
* |List| is a container monad:
> |||
> NonEmpty : {A : Type} -> List A -> Type
> NonEmpty Nil = Void
> NonEmpty (a :: as) = Unit
> idThere : {A : Type} ->
> (a : A) -> (as : List A) ->
> Sigma A (\ x => x `Elem` as) -> Sigma A (\ x => x `Elem` (a :: as))
> idThere a as (MkSigma x p) = MkSigma x (There p)
> ||| Tagging
> tagElem : {A : Type} -> (as : List A) -> List (Sigma A (\ a => a `Elem` as))
> tagElem Nil = Nil
> tagElem {A} (x :: xs) = (MkSigma x Here) :: (map (idThere x xs) (tagElem xs))
* Membership
> elem : {A : Type} -> (DecEq A) => A -> List A -> Bool
> elem x xs with (isElem x xs)
> | (Yes _) = True
> | (No _) = False
* Show
> implementation Show (Elem a as) where
> show = show' where
> show' : {A : Type} -> {a : A} -> {as : List A} -> Elem a as -> String
> show' Here = "Here"
> show' (There p) = "There" ++ show' p
> showlong : Show a => List a -> String
> showlong xs = " [" ++ show' "" xs ++ "]" where
> show' acc [] = acc