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

Cleanup.

parent e2f06519
......@@ -9,26 +9,32 @@ import DoubleExtensions.Predicates
|||
public export
total
plusZeroLeftNeutral : {x : Double} -> 0.0 + x = x
|||
public export
total
plusZeroRightNeutral : {x : Double} -> x + 0.0 = x
|||
public export
total
multZeroLeftZero : {x : Double} -> 0.0 * x = 0.0
|||
public export
total
multZeroRightZero : {x : Double} -> x * 0.0 = 0.0
|||
public export
total
minusSelfZero : {x : Double} -> x - x = 0.0
|||
public export
total
plusAssociative : (x : Double) -> (y : Double) -> (z : Double) ->
x + (y + z) = (x + y) + z
......@@ -37,35 +43,42 @@ plusAssociative : (x : Double) -> (y : Double) -> (z : Double) ->
||| LTE is reflexive
public export
total
reflexiveLTE : (x : Double) -> x `LTE` x
||| LTE is transitive
public export
total
transitiveLTE : (x, y, z : Double) -> x `LTE` y -> y `LTE` z -> x `LTE` z
||| LTE is monotone w.r.t. addition
public export
total
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
total
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
total
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
total
monotoneDivConstLTE : {a, b, c : Double} ->
a `LTE` b -> Positive c -> (a / c) `LTE` (b / c)
||| LTE is unique
public export
total
uniqueLTE : {x, y : Double} -> (p : x `LTE` y) -> (q : x `LTE` y) -> p = q
......@@ -73,6 +86,7 @@ uniqueLTE : {x, y : Double} -> (p : x `LTE` y) -> (q : x `LTE` y) -> p = q
||| LT is unique
public export
total
uniqueLT : {x, y : Double} -> (p : x `LT` y) -> (q : x `LT` y) -> p = q
......@@ -80,11 +94,13 @@ uniqueLT : {x, y : Double} -> (p : x `LT` y) -> (q : x `LT` y) -> p = q
||| Non-negative |Double|s are closed w.r.t. "subtraction"
public export
total
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
total
divPreservesNonNegativity : {x, y : Double} ->
NonNegative x -> NonNegative y -> NonNegative (x / y)
......@@ -93,21 +109,25 @@ divPreservesNonNegativity : {x, y : Double} ->
|||
public export
total
positivePlusAnyPositive : {x, y : Double} ->
Positive x -> NonNegative y -> Positive (x + y)
||| Positive |Double|s are closed w.r.t. division
public export
total
divPreservesPositivity : {x, y : Double} ->
Positive x -> Positive y -> Positive (x / y)
|||
public export
total
divPositiveSelfOne : {x : Double} -> Positive x -> x / x = 1.0
|||
public export
total
divZeroPositiveZero : {x : Double} -> Positive x -> 0.0 / x = 0.0
......@@ -115,10 +135,12 @@ divZeroPositiveZero : {x : Double} -> Positive x -> 0.0 / x = 0.0
|||
public export
total
gtLT : {x, y : Double} -> So (x > y) -> So (y < x)
|||
public export
total
notCompareEQ : {x, y : Double} -> Not (So (x == y)) -> Not (EQ = compare x y)
......
......@@ -23,11 +23,13 @@ data LTE : Double -> Double -> Type where
|||
public export
total
NonNegative : (x : Double) -> Type
NonNegative x = 0.0 `LTE` x
|||
public export
total
Positive : (x : Double) -> Type
Positive x = 0.0 `LT` x
......
......@@ -8,22 +8,28 @@ import Sigma.Operations
|||
public export
total
mkNonNegDouble : (x : Double) -> {auto prf : 0.0 `LTE` x} -> NonNegDouble
mkNonNegDouble x {prf} = MkSigma x prf
|||
public export
total
cast : (x : Double) -> {auto prf : 0.0 `LTE` x} -> NonNegDouble
cast x {prf} = mkNonNegDouble x {prf}
|||
public export
total
toDouble : NonNegDouble -> Double
toDouble = outl
|||
public export
total
fromDouble : (x : Double) -> NonNegative x -> NonNegDouble
fromDouble = MkSigma
......
......@@ -17,6 +17,7 @@ import Sigma.Sigma
||| Addition of positive double precision floating point numbers
public export
total
plus : NonNegDouble -> NonNegDouble -> NonNegDouble
plus (MkSigma x nnx) (MkSigma y nny) = MkSigma (x + y) (plusPreservesNonNegativity nnx nny)
......
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