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

Adding infrastructure to specify non-negative intervals of real numbers.

parent c0c9c1c1
module Bool.Properties
public export
total
trueNotFalse : True = False -> Void
trueNotFalse Refl impossible
module DoubleExtensions.Postulates
-- import Data.So
import Data.So
import DoubleExtensions.Predicates
......@@ -49,78 +49,79 @@ public export
monotonePlusLTE : {a, b, c, d : Double} ->
a `LTE` b -> c `LTE` d -> (a + c) `LTE` (b + d)
||| LTE is monotone w.r.t. multiplication
public export
monotoneMultLTE : {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"
public export
monotoneMinusConstLTE : {a, b, c : Double} ->
a `LTE` b -> (a - c) `LTE` (b - c)
> ||| 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"
public export
monotoneDivConstLTE : {a, b, c : Double} ->
a `LTE` b -> Positive c -> (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
public export
uniqueLTE : {x, y : Double} -> (p : x `LTE` y) -> (q : x `LTE` y) -> p = q
> ||| LTE is unique
> postulate
> uniqueLTE : {x, y : Double} -> (p : x `LTE` y) -> (q : x `LTE` y) -> p = q
-- |LT|:
* |LT|:
||| LT is unique
public export
uniqueLT : {x, y : Double} -> (p : x `LT` y) -> (q : x `LT` y) -> p = q
> ||| 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 precision floating point numbers:
||| Non-negative |Double|s are closed w.r.t. "subtraction"
public export
minusPreservesNonNegativity : {x, y : Double} ->
NonNegative x -> NonNegative y -> y `LTE` x -> NonNegative (x - y)
> ||| 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
public export
divPreservesNonNegativity : {x, y : Double} ->
NonNegative x -> NonNegative y -> 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:
* Positive double precision floating point numbers:
|||
public export
positivePlusAnyPositive : {x, y : Double} ->
Positive x -> NonNegative y -> Positive (x + y)
> |||
> postulate
> positivePlusAnyPositive : {x, y : Double} ->
> Positive x -> NonNegative y -> Positive (x + y)
||| Positive |Double|s are closed w.r.t. division
public export
divPreservesPositivity : {x, y : Double} ->
Positive x -> Positive y -> Positive (x / y)
|||
public export
divPositiveSelfOne : {x : Double} -> Positive x -> x / x = 1.0
> ||| 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
|||
public export
divZeroPositiveZero : {x : Double} -> Positive x -> 0.0 / x = 0.0
> |||
> postulate
> divZeroPositiveZero : {x : Double} -> Positive x -> 0.0 / x = 0.0
-- Ord methods:
|||
public export
gtLT : {x, y : Double} -> So (x > y) -> So (y < x)
* Ord methods:
|||
public export
notCompareEQ : {x, y : Double} -> Not (So (x == y)) -> Not (EQ = compare x y)
> |||
> 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 DoubleExtensions.Properties
-- import Data.So
import Data.So
-- import Double.Predicates
import Math.Interfaces
import DoubleExtensions.Predicates
import So.Properties
-- import Double.Postulates
-- import Double.Operations
-- import So.Properties
-- import Ordering.Properties
-- import Rel.TotalPreorder
-- import So.Properties
import Interfaces.Math
-- Implementations
implementation Math Double where
exp = Prelude.Doubles.exp
sin = Prelude.Doubles.sin
cos = Prelude.Doubles.cos
exp = Prelude.exp
sin = Prelude.sin
cos = Prelude.cos
-- Decidability of EQ
|||
public export
total
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)
-}
> |||
> 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
* Properties of Ord methods
|||
public export
total
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)
-}
> |||
> 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
......
module So.Properties
import Data.So
import Decidable.Equality
-- import Decidable.Predicates
-- import Unique.Predicates
import Bool.Properties
import Unique.Predicates
-- Introduction and elimination rules
{-
> |||
> soIntro : (b : Bool) -> b = True -> So b
> soIntro True Refl = Oh
> soIntro False contra = void (trueNotFalse (sym contra))
> |||
> soElim : (b : Bool) -> So b -> b = True
> soElim True Oh = Refl
> soElim False Oh impossible
** Or
> |||
> soOrIntro1 : (b1 : Bool) -> (b2 : Bool) -> So b1 -> So (b1 || b2)
> soOrIntro1 True _ Oh = Oh
> |||
> soOrIntro2 : (b1 : Bool) -> (b2 : Bool) -> So b2 -> So (b1 || b2)
> soOrIntro2 True True Oh = Oh
> soOrIntro2 False True Oh = Oh
> |||
> soOrElim : (b1 : Bool) -> (b2 : Bool) -> So (b1 || b2) -> Either (So b1) (So b2)
> soOrElim True True Oh = Left Oh
> soOrElim True False Oh = Left Oh
> soOrElim False True Oh = Right Oh
> soOrElim False False Oh impossible
> |||
> soOrElim1 : (b1 : Bool) -> (b2 : Bool) -> So (b1 || b2) -> So (not b1) -> So b2
> soOrElim1 True True Oh Oh impossible
> soOrElim1 True False Oh Oh impossible
> soOrElim1 False True Oh Oh = Oh
> soOrElim1 False False Oh Oh impossible
> |||
> soOrElim2 : (b1 : Bool) -> (b2 : Bool) -> So (b1 || b2) -> So (not b2) -> So b1
> soOrElim2 True True Oh Oh impossible
> soOrElim2 True False Oh Oh = Oh
> soOrElim2 False True Oh Oh impossible
> soOrElim2 False False Oh Oh impossible
** And
> |||
> soAndElim1 : (b1 : Bool) -> (b2 : Bool) -> So (b1 && b2) -> So b1
> soAndElim1 True True Oh = Oh
> soAndElim1 True False Oh impossible
> soAndElim1 False True Oh impossible
> soAndElim1 False False Oh impossible
> |||
> soAndElim2 : (b1 : Bool) -> (b2 : Bool) -> So (b1 && b2) -> So b2
> soAndElim2 True True Oh = Oh
> soAndElim2 True False Oh impossible
> soAndElim2 False True Oh impossible
> soAndElim2 False False Oh impossible
|||
public export
total
soIntro : (b : Bool) -> b = True -> So b
soIntro True Refl = Oh
soIntro False contra = void (trueNotFalse (sym contra))
|||
public export
total
soElim : (b : Bool) -> So b -> b = True
soElim True Oh = Refl
soElim False Oh impossible
---- Or
|||
public export
total
soOrIntro1 : (b1 : Bool) -> (b2 : Bool) -> So b1 -> So (b1 || b2)
soOrIntro1 True _ Oh = Oh
|||
public export
total
soOrIntro2 : (b1 : Bool) -> (b2 : Bool) -> So b2 -> So (b1 || b2)
soOrIntro2 True True Oh = Oh
soOrIntro2 False True Oh = Oh
|||
public export
total
soOrElim : (b1 : Bool) -> (b2 : Bool) -> So (b1 || b2) -> Either (So b1) (So b2)
soOrElim True True Oh = Left Oh
soOrElim True False Oh = Left Oh
soOrElim False True Oh = Right Oh
soOrElim False False Oh impossible
|||
public export
total
soOrElim1 : (b1 : Bool) -> (b2 : Bool) -> So (b1 || b2) -> So (not b1) -> So b2
soOrElim1 True True Oh Oh impossible
soOrElim1 True False Oh Oh impossible
soOrElim1 False True Oh Oh = Oh
soOrElim1 False False Oh Oh impossible
|||
public export
total
soOrElim2 : (b1 : Bool) -> (b2 : Bool) -> So (b1 || b2) -> So (not b2) -> So b1
soOrElim2 True True Oh Oh impossible
soOrElim2 True False Oh Oh = Oh
soOrElim2 False True Oh Oh impossible
soOrElim2 False False Oh Oh impossible
---- And
|||
public export
total
soAndElim1 : (b1 : Bool) -> (b2 : Bool) -> So (b1 && b2) -> So b1
soAndElim1 True True Oh = Oh
soAndElim1 True False Oh impossible
soAndElim1 False True Oh impossible
soAndElim1 False False Oh impossible
|||
public export
total
soAndElim2 : (b1 : Bool) -> (b2 : Bool) -> So (b1 && b2) -> So b2
soAndElim2 True True Oh = Oh
soAndElim2 True False Oh impossible
soAndElim2 False True Oh impossible
soAndElim2 False False Oh impossible
-- Counter factuals
|||
public export
total
contra : {b : Bool} -> b = False -> So b -> Void
contra {b} p q = trueNotFalse (trans (sym (soElim b q)) p)
-- Decidability
||| Lifted Booleans are decidable
public export
total
decSo : (b : Bool) -> Dec (So b)
decSo True = Yes Oh
decSo False = No (\ oh => absurd oh)
||| Lifted Boolean functions are decidable
public export
total
dec1So : {A : Type} -> (p : A -> Bool) -> ((a : A) -> Dec (So (p a)))
dec1So p a = decSo (p a)
-- Uniqueness
||| Lifted Booleans are unique
public export
total
uniqueSo : (b : Bool) -> Unique (So b)
uniqueSo True Oh Oh = Refl
uniqueSo False Oh Oh impossible
||| Lifted Boolean functions are unique
public export
total
unique1So : {A : Type} -> (p : A -> Bool) -> ((a : A) -> Unique (So (p a)))
unique1So p a = uniqueSo (p a)
* Counter factuals
> |||
> contra : {b : Bool} -> b = False -> So b -> Void
> contra {b} p q = trueNotFalse (trans (sym (soElim b q)) p)
* Decidability
> ||| Lifted Booleans are decidable
> decSo : (b : Bool) -> Dec (So b)
> decSo True = Yes Oh
> decSo False = No (\ oh => absurd oh)
> ||| Lifted Boolean functions are decidable
> dec1So : {A : Type} -> (p : A -> Bool) -> Dec1 (\ a => So (p a))
> dec1So p a = decSo (p a)
* Uniqueness
> ||| Lifted Booleans are unique
> uniqueSo : (b : Bool) -> Unique (So b)
> uniqueSo True Oh Oh = Refl
> uniqueSo False Oh Oh impossible
> ||| Lifted Boolean functions are unique
> unique1So : {A : Type} -> (p : A -> Bool) -> Unique1 (\ a => So (p a))
> unique1So p a = uniqueSo (p a)
{-
---}
......@@ -18,7 +18,7 @@ toVectFun {n = Z} _ = Nil
toVectFun {n = S m} f = (f FZ) :: (toVectFun (tail f))
N : Nat
N = 8
N = 100
xs : Vect (S N) Nat
xs = toVectFun {n = S N} finToNat
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment