packages feed

type-natural 0.6.0.0 → 0.6.1.0

raw patch · 3 files changed

+67/−14 lines, 3 filesdep ~equational-reasoning

Dependency ranges changed: equational-reasoning

Files

Data/Type/Natural/Class/Arithmetic.hs view
@@ -8,7 +8,7 @@         plusCong, plusCongR, plusCongL, succCong,         multCong, multCongL, multCongR,         minusCong, minusCongL, minusCongR,-        IsPeano(..), pattern Zero, pattern Succ+        IsPeano(..), pattern Zero, pattern Succ,        ) where import Data.Singletons.Decide import Data.Singletons.Prelude@@ -16,7 +16,6 @@ import Data.Type.Equality import Data.Void import Proof.Equational-import Proof.Propositional  type family Zero nat :: nat where   Zero nat = FromInteger 0@@ -131,6 +130,12 @@   induction     :: p (Zero nat) -> (forall n. Sing n -> p n -> p (S n)) -> Sing k -> p k   plusMinus :: Sing (n :: nat) -> Sing m -> n :+ m :- m :~: n +  plusMinus' :: Sing (n :: nat) -> Sing m -> n :+ m :- n :~: m+  plusMinus'  n m =+    start (n %:+ m %:- n)+      === m %:+ n %:- n   `because` minusCongL (plusComm n m) n+      === m               `because` plusMinus m n+   plusZeroL :: Sing n -> (Zero nat :+ n) :~: n   plusZeroL sn = idLProof (induction base step sn)     where@@ -383,7 +388,6 @@       === (sZero %:+ n) %:- n  `because` minusCongL (sym $ plusZeroL n) n       === sZero                `because` plusMinus sZero n -   multAssoc :: Sing (n :: nat) -> Sing m -> Sing l             -> (n :* m) :* l :~: n :* (m :* l)   multAssoc sn0 = assocProof $ induction base step sn0@@ -484,6 +488,13 @@   multEqSuccElimR n m l nmEsl =     multEqSuccElimL m n l (multComm m n `trans` nmEsl) +  minusZero :: Sing n -> n :- Zero nat :~: n+  minusZero n =+    start (n %:- sZero)+      === (n %:+ sZero) %:- sZero+             `because` minusCongL (sym $ plusZeroR n) sZero+      === n  `because` plusMinus n sZero+   multEqCancelR :: Sing (n :: nat) -> Sing m -> Sing l -> n :* Succ l :~: m :* Succ l -> n :~: m   multEqCancelR = proofMultEqCancelR . induction base step     where@@ -526,14 +537,6 @@   sPred' :: proxy n -> Sing (Succ n) -> Sing (n :: nat)   sPred' pxy sn = coerce (succInj $ succCong $ predSucc (sPred' pxy sn)) (sPred sn) -refute [t| 'LT :~: 'GT |]-refute [t| 'LT :~: 'EQ |]-refute [t| 'EQ :~: 'LT |]-refute [t| 'EQ :~: 'GT |]-refute [t| 'GT :~: 'LT |]-refute [t| 'GT :~: 'EQ |]-refute [t| 'True :~: 'False |]- pattern Zero :: forall nat (n :: nat). IsPeano nat => n ~ Zero nat => Sing n pattern Zero <- (zeroOrSucc -> IsZero) where   Zero = sZero@@ -541,3 +544,4 @@ pattern Succ :: forall nat (n :: nat). IsPeano nat => forall (n1 :: nat). n ~ Succ n1 => Sing n1 -> Sing n pattern Succ n <- (zeroOrSucc -> IsSucc n) where   Succ n = sSucc n+
Data/Type/Natural/Class/Order.hs view
@@ -5,7 +5,8 @@ module Data.Type.Natural.Class.Order        (PeanoOrder(..), DiffNat(..), LeqView(..),         FlipOrdering, sFlipOrdering, coerceLeqL, coerceLeqR,-        sLeqCongL, sLeqCongR, sLeqCong+        sLeqCongL, sLeqCongR, sLeqCong,+        (:-.), (%:-.), minPlusTruncMinus, truncMinusLeq        ) where import Data.Type.Natural.Class.Arithmetic @@ -657,3 +658,51 @@   lneqZeroAbsurd :: Sing n -> IsTrue (n :< Zero nat) -> Void   lneqZeroAbsurd n leq =     succLeqZeroAbsurd n (coerce (lneqSuccLeq n sZero) leq)++  minusPlus :: forall (n :: nat) m .PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue (m :<= n)+            -> n :- m :+ m :~: n+  minusPlus n m mLEQn =+    case leqWitness m n mLEQn of+      DiffNat _ k ->+        start (n %:- m %:+ m)+          =~= m %:+ k %:- m %:+ m+          === k %:+ m %:- m %:+ m  `because` plusCongL (minusCongL (plusComm m k) m) m+          === k %:+ m              `because` plusCongL (plusMinus k m) m+          === m %:+ k              `because` plusComm  k m+          =~= n++-- | Natural subtraction, truncated to zero if m > n.+type n :-. m = Subt n m (m :<= n)+type family Subt (n :: nat) (m :: nat) (b :: Bool) :: nat where+  Subt n          m 'True  = n :- m+  Subt (n :: nat) m 'False = Zero nat+infixl 6 :-.++(%:-.) :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> Sing (n :-. m)+n %:-. m =+  case m %:<= n of+    STrue -> n %:- m+    SFalse -> sZero++minPlusTruncMinus :: (PeanoOrder nat) => Sing (n :: nat) -> Sing (m :: nat)+                  -> Min n m :+ (n :-. m) :~: n+minPlusTruncMinus n m =+  case m %:<= n of+    STrue ->+      start (sMin n m %:+ (n %:-. m))+        === m %:+ (n %:-. m) `because` plusCongL (geqToMin n m Witness) (n %:-. m)+        =~= m %:+ (n %:- m)+        === (n %:- m) %:+ m  `because` plusComm m (n %:- m)+        === n                `because` minusPlus n m Witness+    SFalse ->+      start (sMin n m %:+ (n %:-. m))+        =~= sMin n m %:+ sZero+        === sMin n m  `because` plusZeroR (sMin n m)+        === n         `because` leqToMin n m (notLeqToLeq m n)++truncMinusLeq :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue (n :-. m :<= n)+truncMinusLeq n m =+  case m %:<= n of+    STrue  -> leqStep (n %:-. m) n m $ minusPlus n m Witness+    SFalse -> leqZero n+
type-natural.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                type-natural-version:             0.6.0.0+version:             0.6.1.0 synopsis:            Type-level natural and proofs of their properties. description:         Type-level natural numbers and proofs of their properties.                      .@@ -39,7 +39,7 @@                      , Data.Type.Natural.Core                      , Data.Type.Natural.Compat   build-depends:       base                      >= 4       && < 5-                     , equational-reasoning      == 0.4.*+                     , equational-reasoning      >= 0.4.1   && < 1                      , monomorphic               >= 0.0.3                      , template-haskell          >= 2.8     && < 3                      , constraints               >= 0.3     && < 0.9