type-natural 1.1.0.0 → 1.1.0.1
raw patch · 4 files changed
+596/−297 lines, 4 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- Data.Type.Natural.Lemma.Order: notLeqToLeq :: (n <=? m) ~ 'False => SNat n -> SNat m -> IsTrue (m <=? n)
+ Data.Type.Natural.Lemma.Order: notLeqToLeq :: forall n m. (n <=? m) ~ 'False => SNat n -> SNat m -> IsTrue (m <=? n)
Files
- src/Data/Type/Natural/Core.hs +2/−2
- src/Data/Type/Natural/Lemma/Order.hs +39/−225
- tests/Data/Type/Natural/Lemma/OrderSpec.hs +476/−0
- type-natural.cabal +79/−70
src/Data/Type/Natural/Core.hs view
@@ -19,6 +19,7 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE NoStarIsType #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} module Data.Type.Natural.Core@@ -73,7 +74,6 @@ import GHC.TypeNats import Math.NumberTheory.Logarithms (naturalLog2) import Numeric.Natural (Natural)-import Proof.Propositional (Empty) import Type.Reflection (Typeable) import Unsafe.Coerce (unsafeCoerce) @@ -132,7 +132,7 @@ equalAbsurdFromBool :: (x === y) ~ 'False => x :~: y -> a-equalAbsurdFromBool = \case+equalAbsurdFromBool = \case {} type family a === b where a === a = 'True
src/Data/Type/Natural/Lemma/Order.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE DataKinds #-}+{-# LANGUAGE CPP #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE ExplicitForAll #-} {-# LANGUAGE ExplicitNamespaces #-}@@ -157,7 +158,6 @@ start, sym, trans,- withRefl, (===), (=~=), )@@ -267,8 +267,6 @@ newtype LeqWitPf n = LeqWitPf {leqWitPf :: forall m. SNat m -> IsTrue (n <=? m) -> DiffNat n m} -newtype LeqStepPf n = LeqStepPf {leqStepPf :: forall m l. SNat m -> SNat l -> n + l :~: m -> IsTrue (n <=? m)}- succDiffNat :: SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m) succDiffNat _ _ (DiffNat n m) = gcastWith (plusSuccL n m) $ DiffNat (sSucc n) m @@ -302,16 +300,6 @@ sLeqCongR :: SNat a -> b :~: c -> (a <= b) :~: (a <= c) sLeqCongR _ Refl = Refl -newtype LTSucc n = LTSucc {proofLTSucc :: CmpNat n (Succ n) :~: 'LT}--newtype CmpSuccStepR n = CmpSuccStepR- { proofCmpSuccStepR ::- forall m.- SNat m ->- CmpNat n m :~: 'LT ->- CmpNat n (Succ m) :~: 'LT- }- newtype LeqViewRefl n = LeqViewRefl {proofLeqViewRefl :: LeqView n n} leqToCmp ::@@ -355,25 +343,7 @@ leqNeqToLT a b aLEQb aNEQb = either (absurd . aNEQb) id $ leqToCmp a b aLEQb succLeqToLT :: SNat a -> SNat b -> IsTrue (S a <=? b) -> CmpNat a b :~: 'LT-succLeqToLT a b saLEQb =- case leqWitness (sSucc a) b saLEQb of- DiffNat _ k ->- let aLEQb =- leqStep a b (sSucc k) $- start (a %+ sSucc k)- === sSucc (a %+ k) `because` plusSuccR a k- === sSucc a %+ k `because` sym (plusSuccL a k)- =~= b- aNEQb aeqb =- succNonCyclic k $- plusEqCancelL a (sSucc k) sZero $- start (a %+ sSucc k)- === sSucc (a %+ k) `because` plusSuccR a k- === sSucc a %+ k `because` sym (plusSuccL a k)- =~= b- === a `because` sym aeqb- === a %+ sZero `because` sym (plusZeroR a)- in leqNeqToLT a b aLEQb aNEQb+succLeqToLT _ _ Witness = Refl ltToLeq :: SNat a ->@@ -387,11 +357,7 @@ SNat b -> CmpNat a b :~: 'GT -> IsTrue (b <=? a)-gtToLeq n m nGTm =- ltToLeq m n $- start (sCmpNat m n) === sFlipOrdering (sCmpNat n m) `because` sym (flipCmpNat n m)- === sFlipOrdering SGT `because` congFlipOrdering nGTm- =~= SLT+gtToLeq _ _ Refl = Witness congFlipOrdering :: a :~: b -> FlipOrdering a :~: FlipOrdering b@@ -402,27 +368,17 @@ SNat b -> CmpNat a b :~: 'LT -> IsTrue (Succ a <=? b)-ltToSuccLeq n m nLTm =- leqNeqToSuccLeq n m (ltToLeq n m nLTm) (ltToNeq n m nLTm)+ltToSuccLeq _ _ Refl = Witness cmpZero :: SNat a -> CmpNat 0 (Succ a) :~: 'LT-cmpZero sn =- leqToLT sZero (sSucc sn) $- leqStep (sSucc sZero) (sSucc sn) sn $- start (sSucc sZero %+ sn)- === sSucc (sZero %+ sn) `because` plusSuccL sZero sn- === sSucc sn `because` succCong (plusZeroL sn)+cmpZero _ = Refl leqToGT :: SNat a -> SNat b -> IsTrue (Succ b <=? a) -> CmpNat a b :~: 'GT-leqToGT a b sbLEQa =- start (sCmpNat a b)- === sFlipOrdering (sCmpNat b a) `because` sym (flipCmpNat b a)- === sFlipOrdering SLT `because` congFlipOrdering (leqToLT b a sbLEQa)- =~= SGT+leqToGT _ _ Witness = Refl cmpZero' :: SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT) cmpZero' n =@@ -449,57 +405,13 @@ === SLT `because` cmp0nLT ltRightPredSucc :: SNat a -> SNat b -> CmpNat a b :~: 'LT -> b :~: Succ (Pred b)-ltRightPredSucc a b aLTb =- case zeroOrSucc b of- IsZero -> absurd $ zeroNoLT a aLTb- IsSucc b' ->- sym $- start (sSucc (sPred b))- =~= sSucc (sPred (sSucc b'))- === sSucc b' `because` succCong (predSucc b')- =~= b+ltRightPredSucc _ _ Refl = Refl cmpSucc :: SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)-cmpSucc n m =- case sCmpNat n m of- SEQ ->- let nEQm = eqToRefl n m Refl- in sym $ eqlCmpEQ (sSucc n) (sSucc m) $ succCong nEQm- SLT -> case leqWitness (sSucc n) m $ ltToSuccLeq n m Refl of- DiffNat _ k ->- sym $- succLeqToLT (sSucc n) (sSucc m) $- leqStep (sSucc (sSucc n)) (sSucc m) k $- start (sSucc (sSucc n) %+ k)- === sSucc (sSucc n %+ k) `because` plusSuccL (sSucc n) k- =~= sSucc m- SGT -> case leqWitness (sSucc m) n $ ltToSuccLeq m n (sym $ flipCmpNat n m) of- DiffNat _ k ->- let pf =- ( succLeqToLT (sSucc m) (sSucc n) $- leqStep (sSucc (sSucc m)) (sSucc n) k $- start (sSucc (sSucc m) %+ k)- === sSucc (sSucc m %+ k) `because` plusSuccL (sSucc m) k- =~= sSucc n- )- in start (sCmpNat n m)- =~= SGT- =~= sFlipOrdering SLT- === sFlipOrdering (sCmpNat (sSucc m) (sSucc n)) `because` congFlipOrdering (sym pf)- === sCmpNat (sSucc n) (sSucc m) `because` flipCmpNat (sSucc m) (sSucc n)+cmpSucc _ _ = Refl ltSucc :: SNat a -> CmpNat a (Succ a) :~: 'LT-ltSucc = proofLTSucc . induction base step- where- base :: LTSucc 0- base = LTSucc $ cmpZero (sZero :: SNat 0)-- step :: SNat n -> LTSucc n -> LTSucc (Succ n)- step n (LTSucc ih) =- LTSucc $- start (sCmpNat (sSucc n) (sSucc (sSucc n)))- === sCmpNat n (sSucc n) `because` sym (cmpSucc n (sSucc n))- === SLT `because` ih+ltSucc _ = Refl cmpSuccStepR :: forall n m.@@ -507,21 +419,7 @@ SNat m -> CmpNat n m :~: 'LT -> CmpNat n (Succ m) :~: 'LT-cmpSuccStepR = \sn -> proofCmpSuccStepR (induction base step sn) @m- where- base :: CmpSuccStepR 0- base = CmpSuccStepR $ \m _ -> cmpZero m-- step :: SNat x -> CmpSuccStepR x -> CmpSuccStepR (Succ x)- step n (CmpSuccStepR ih) = CmpSuccStepR $ \m snltm ->- case zeroOrSucc m of- IsZero -> absurd $ zeroNoLT (sSucc n) snltm- IsSucc m' ->- let nLTm' = trans (cmpSucc n m') snltm- in start (sCmpNat (sSucc n) (sSucc m))- =~= sCmpNat (sSucc n) (sSucc (sSucc m'))- === sCmpNat n (sSucc m') `because` sym (cmpSucc n (sSucc m'))- === SLT `because` ih m' nLTm'+cmpSuccStepR _ _ Refl = Refl ltSuccLToLT :: SNat n ->@@ -541,14 +439,7 @@ SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT-leqToLT n m snLEQm =- case leqToCmp (sSucc n) m snLEQm of- Left eql ->- withRefl eql $- start (sCmpNat n m)- =~= sCmpNat n (sSucc n)- === SLT `because` ltSucc n- Right nLTm -> ltSuccLToLT n m nLTm+leqToLT _ _ Witness = Refl leqZero :: SNat n -> IsTrue (0 <=? n) leqZero _ = Witness@@ -589,25 +480,14 @@ step :: SNat x -> LeqWitPf x -> LeqWitPf (Succ x) step (n :: SNat x) (LeqWitPf ih) = LeqWitPf $ \m snLEQm -> case viewLeq (sSucc n) m snLEQm of+#if !MIN_VERSION_ghc(9,2,0) LeqZero _ -> absurd $ succNonCyclic n Refl+#endif LeqSucc (_ :: SNat n') pm nLEQpm -> succDiffNat n pm $ ih pm $ coerceLeqL (succInj Refl :: n' :~: x) pm nLEQpm leqStep :: forall n m l. SNat n -> SNat m -> SNat l -> n + l :~: m -> IsTrue (n <=? m)-leqStep sn = leqStepPf (induction base step sn) @m @l- where- base :: LeqStepPf 0- base = LeqStepPf $ \k _ _ -> leqZero k-- step :: forall k. SNat k -> LeqStepPf k -> LeqStepPf (Succ k)- step n (LeqStepPf ih) =- LeqStepPf $ \k l snPlEqk ->- let kEQspk =- start k- === sSucc n %+ l `because` sym snPlEqk- === sSucc (n %+ l) `because` plusSuccL n l- pk = n %+ l- in coerceLeqR (sSucc n) (sym kEQspk) $ leqSucc n pk $ ih pk l Refl+leqStep _ _ _ Refl = Witness leqNeqToSuccLeq :: SNat n -> SNat m -> IsTrue (n <=? m) -> (n :~: m -> Void) -> IsTrue (Succ n <=? m) leqNeqToSuccLeq n m nLEQm nNEQm =@@ -623,47 +503,22 @@ =~= m leqRefl :: SNat n -> IsTrue (n <=? n)-leqRefl sn = leqStep sn sn sZero (plusZeroR sn)+leqRefl _ = Witness leqSuccStepR :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)-leqSuccStepR n m nLEQm =- case leqWitness n m nLEQm of- DiffNat _ k ->- leqStep n (sSucc m) (sSucc k) $- start (n %+ sSucc k) === sSucc (n %+ k) `because` plusSuccR n k =~= sSucc m+leqSuccStepR _ _ Witness = Witness leqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m)-leqSuccStepL n m snLEQm =- leqTrans n (sSucc n) m (leqSuccStepR n n $ leqRefl n) snLEQm+leqSuccStepL _ _ Witness = Witness leqReflexive :: SNat n -> SNat m -> n :~: m -> IsTrue (n <=? m)-leqReflexive n _ Refl = leqRefl n+leqReflexive _ _ Refl = Witness leqTrans :: SNat n -> SNat m -> SNat l -> IsTrue (n <=? m) -> IsTrue (m <=? l) -> IsTrue (n <=? l)-leqTrans n m k nLEm mLEk =- case leqWitness n m nLEm of- DiffNat _ mMn -> case leqWitness m k mLEk of- DiffNat _ kMn -> leqStep n k (mMn %+ kMn) (sym $ plusAssoc n mMn kMn)+leqTrans _ _ _ Witness Witness = Witness leqAntisymm :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m-leqAntisymm n m nLEm mLEn =- case (leqWitness n m nLEm, leqWitness m n mLEn) of- (DiffNat _ mMn, DiffNat _ nMm) ->- let pEQ0 =- plusEqCancelL n (mMn %+ nMm) sZero $- start (n %+ (mMn %+ nMm))- === (n %+ mMn) %+ nMm- `because` sym (plusAssoc n mMn nMm)- =~= m %+ nMm- =~= n- === n %+ sZero- `because` sym (plusZeroR n)- nMmEQ0 = plusEqZeroL mMn nMm pEQ0- in sym $- start m- =~= n %+ mMn- === n %+ sZero `because` plusCongR n nMmEQ0- === n `because` plusZeroR n+leqAntisymm _ _ Witness Witness = Refl plusMonotone :: SNat n ->@@ -673,31 +528,10 @@ IsTrue (n <=? m) -> IsTrue (l <=? k) -> IsTrue ((n + l) <=? (m + k))-plusMonotone n m l k nLEm lLEk =- case (leqWitness n m nLEm, leqWitness l k lLEk) of- (DiffNat _ mMINn, DiffNat _ kMINl) ->- let r = mMINn %+ kMINl- in leqStep (n %+ l) (m %+ k) r $- start (n %+ l %+ r)- === n %+ (l %+ r)- `because` plusAssoc n l r- =~= n %+ (l %+ (mMINn %+ kMINl))- === n %+ (l %+ (kMINl %+ mMINn))- `because` plusCongR n (plusCongR l (plusComm mMINn kMINl))- === n %+ ((l %+ kMINl) %+ mMINn)- `because` plusCongR n (sym $ plusAssoc l kMINl mMINn)- =~= n %+ (k %+ mMINn)- === n %+ (mMINn %+ k)- `because` plusCongR n (plusComm k mMINn)- === n %+ mMINn %+ k- `because` sym (plusAssoc n mMINn k)- =~= m %+ k+plusMonotone _ _ _ _ Witness Witness = Witness leqZeroElim :: SNat n -> IsTrue (n <=? 0) -> n :~: 0-leqZeroElim n nLE0 =- case viewLeq n sZero nLE0 of- LeqZero _ -> Refl- LeqSucc _ pZ _ -> absurd $ succNonCyclic pZ Refl+leqZeroElim _ Witness = Refl plusMonotoneL :: SNat n ->@@ -705,7 +539,7 @@ SNat l -> IsTrue (n <=? m) -> IsTrue ((n + l) <=? (m + l))-plusMonotoneL n m l leq = plusMonotone n m l l leq (leqRefl l)+plusMonotoneL _ _ _ Witness = Witness plusMonotoneR :: SNat n ->@@ -713,13 +547,13 @@ SNat l -> IsTrue (m <=? l) -> IsTrue ((n + m) <=? (n + l))-plusMonotoneR n m l leq = plusMonotone n n m l (leqRefl n) leq+plusMonotoneR _ _ _ Witness = Witness plusLeqL :: SNat n -> SNat m -> IsTrue (n <=? (n + m))-plusLeqL n m = leqStep n (n %+ m) m Refl+plusLeqL _ _ = Witness plusLeqR :: SNat n -> SNat m -> IsTrue (m <=? (n + m))-plusLeqR n m = leqStep m (n %+ m) n $ plusComm m n+plusLeqR _ _ = Witness plusCancelLeqR :: SNat n ->@@ -727,17 +561,7 @@ SNat l -> IsTrue ((n + l) <=? (m + l)) -> IsTrue (n <=? m)-plusCancelLeqR n m l nlLEQml =- case leqWitness (n %+ l) (m %+ l) nlLEQml of- DiffNat _ k ->- let pf =- plusEqCancelR (n %+ k) m l $- start ((n %+ k) %+ l)- === n %+ (k %+ l) `because` plusAssoc n k l- === n %+ (l %+ k) `because` plusCongR n (plusComm k l)- === n %+ l %+ k `because` sym (plusAssoc n l k)- =~= m %+ l- in leqStep n m k pf+plusCancelLeqR _ _ _ Witness = Witness plusCancelLeqL :: SNat n ->@@ -745,20 +569,14 @@ SNat l -> IsTrue ((n + m) <=? (n + l)) -> IsTrue (m <=? l)-plusCancelLeqL n m l nmLEQnl =- plusCancelLeqR m l n $- coerceLeqL (plusComm n m) (l %+ n) $- coerceLeqR (n %+ m) (plusComm n l) nmLEQnl+plusCancelLeqL _ _ _ Witness = Witness succLeqZeroAbsurd :: SNat n -> IsTrue (S n <=? 0) -> Void succLeqZeroAbsurd n leq = succNonCyclic n (leqZeroElim (sSucc n) leq) succLeqZeroAbsurd' :: SNat n -> (S n <=? 0) :~: 'False-succLeqZeroAbsurd' n =- case sSucc n %<=? sZero of- STrue -> absurd $ succLeqZeroAbsurd n Witness- SFalse -> Refl+succLeqZeroAbsurd' _ = Refl succLeqAbsurd :: SNat n -> IsTrue (S n <=? n) -> Void succLeqAbsurd n snLEQn =@@ -768,17 +586,10 @@ === SEQ `because` eqlCmpEQ n n Refl succLeqAbsurd' :: SNat n -> (S n <=? n) :~: 'False-succLeqAbsurd' n =- case sSucc n %<=? n of- STrue -> absurd $ succLeqAbsurd n Witness- SFalse -> Refl+succLeqAbsurd' _ = Refl -notLeqToLeq :: ((n <=? m) ~ 'False) => SNat n -> SNat m -> IsTrue (m <=? n)-notLeqToLeq n m =- case sCmpNat n m of- SLT -> eliminate $ ltToLeq n m Refl- SEQ -> eliminate $ leqReflexive n m $ eqToRefl n m Refl- SGT -> gtToLeq n m Refl+notLeqToLeq :: forall n m. ((n <=? m) ~ 'False) => SNat n -> SNat m -> IsTrue (m <=? n)+notLeqToLeq _ _ = Witness leqSucc' :: SNat n -> SNat m -> (n <=? m) :~: (Succ n <=? Succ m) leqSucc' _ _ = Refl@@ -841,12 +652,15 @@ SFalse -> lLEQm leqToMax :: SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m-leqToMax n m nLEQm =- leqAntisymm (sMax n m) m (maxLeast m n m nLEQm (leqRefl m)) (maxLeqR n m)+leqToMax n m Witness =+ case n %>=? m of+ STrue -> Refl+ SFalse -> Refl geqToMax :: SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n-geqToMax n m mLEQn =- leqAntisymm (sMax n m) n (maxLeast n n m (leqRefl n) mLEQn) (maxLeqL n m)+geqToMax n m Witness =+ case n %>=? m of+ STrue -> Refl maxComm :: SNat n -> SNat m -> Max n m :~: Max m n maxComm n m =
+ tests/Data/Type/Natural/Lemma/OrderSpec.hs view
@@ -0,0 +1,476 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# OPTIONS_GHC -Wno-orphans #-}++module Data.Type.Natural.Lemma.OrderSpec where++import Control.Exception (SomeException (..), evaluate, try)+import Data.Functor ((<&>))+import Data.List (isInfixOf, isPrefixOf)+import Data.Type.Natural+import Data.Type.Natural.Lemma.Order+import Data.Void (Void)+import Proof.Propositional (IsTrue (Witness))+import Shared ()+import Test.Tasty (TestTree, testGroup)+import Test.Tasty.HUnit+import Test.Tasty.QuickCheck+import Type.Reflection+import Unsafe.Coerce (unsafeCoerce)++someNat' :: NonNegative Integer -> SomeSNat+someNat' = toSomeSNat . fromInteger . getNonNegative++data SomeLeqNat where+ MkSomeLeqNat :: n <= m => SNat n -> SNat m -> SomeLeqNat++data SomeLtNat where+ MkSomeLtNat ::+ CmpNat n m ~ 'LT =>+ SNat n ->+ SNat m ->+ SomeLtNat++data SomeLneqNat where+ MkSomeLneqNat ::+ n < m =>+ SNat n ->+ SNat m ->+ SomeLneqNat++data SomeGtNat where+ MkSomeGtNat ::+ CmpNat n m ~ 'GT =>+ SNat n ->+ SNat m ->+ SomeGtNat++deriving instance Show SomeLeqNat++deriving instance Show SomeLtNat++deriving instance Show SomeLneqNat++deriving instance Show SomeGtNat++instance Arbitrary SomeLeqNat where+ arbitrary = do+ SomeSNat n <- someNat' <$> arbitrary+ SomeSNat m <- someNat' <$> arbitrary+ case n %<=? m of+ STrue -> pure $ MkSomeLeqNat n m+ SFalse ->+ case m %<=? n of+ STrue -> pure $ MkSomeLeqNat m n+ SFalse -> error "Impossible!"++instance Arbitrary SomeLtNat where+ arbitrary = do+ MkSomeLeqNat (n :: SNat n) (m :: SNat m) <- arbitrary+ let m' = Succ m+ case sCmpNat n m' of+ SLT -> pure $ MkSomeLtNat n m'+ _ -> error "impossible"++instance Arbitrary SomeLneqNat where+ arbitrary = do+ MkSomeLtNat (n :: SNat n) (m :: SNat m) <- arbitrary+ let m' = Succ m+ case n %<? m' of+ STrue -> pure $ MkSomeLneqNat n m'+ _ -> error "impossible"++instance Arbitrary SomeGtNat where+ arbitrary = do+ MkSomeLeqNat (n :: SNat n) (m :: SNat m) <- arbitrary+ let m' = Succ m+ case sCmpNat m' n of+ SGT -> pure $ MkSomeGtNat m' n+ _ -> error "impossible"++data SomeLeqView where+ MkSomeLeqView :: LeqView n m -> SomeLeqView++instance Show SomeLeqView where+ showsPrec d (MkSomeLeqView (LeqZero n)) =+ showParen (d > 10) $+ showString "LeqZero "+ . showsPrec 11 n+ showsPrec d (MkSomeLeqView (LeqSucc n m w)) =+ showParen (d > 10) $+ showString "LeqSucc "+ . showsPrec 11 n+ . showChar ' '+ . showsPrec 11 m+ . showChar ' '+ . showsPrec 11 w++instance Arbitrary SomeLeqView where+ arbitrary = sized $ \n ->+ if n <= 0+ then+ arbitrary <&> \case+ SomeSNat sn -> MkSomeLeqView (LeqZero sn)+ else+ arbitrary <&> \case+ MkSomeLeqNat sn sm -> MkSomeLeqView $ LeqSucc sn sm Witness++givesImpossibleVoid :: Void -> Property+givesImpossibleVoid contradiction = ioProperty $ do+ eith <- try @SomeException $ evaluate contradiction+ case eith of+ Left someE -> do+ pure $+ property $+ "Impossible" `isPrefixOf` show someE+ || "Non-exhaustive" `isInfixOf` show someE+ Right {} -> pure $ property False++test_Lemmas :: TestTree+test_Lemmas =+ testGroup+ "Lemmas"+ [ testProperty @(SomeLeqNat -> Property) "coerceLeqL terminates" $ \(MkSomeLeqNat (_ :: SNat n) sm) -> totalWitness $ coerceLeqL (Refl :: n :~: n) sm Witness+ , testProperty @(SomeLeqNat -> Property) "coerceLeqR terminates" $ \(MkSomeLeqNat sn (_ :: SNat m)) -> totalWitness $ coerceLeqR sn (Refl :: m :~: m) Witness+ , testProperty @(SomeSNat -> SomeSNat -> Property) "sLeqCong terminates" $+ \(SomeSNat (_ :: SNat n)) (SomeSNat (_ :: SNat m)) ->+ totalRefl $ sLeqCong (Refl @n) (Refl @m)+ , testProperty @(SomeSNat -> SomeSNat -> Property) "succDiffNat terminates and gives the correct value" $+ \(SomeSNat sn) (SomeSNat sm) ->+ case succDiffNat sn (sn %+ sm) (DiffNat sn sm) of+ DiffNat sns sms ->+ toNatural (sns %+ sms)+ === toNatural sn + toNatural sm + 1+ , testProperty @(SomeSNat -> SomeSNat -> Property)+ "compareCongR terminates"+ $ \(SomeSNat a) (SomeSNat (_ :: SNat b)) ->+ totalRefl $ compareCongR a (Refl @b)+ , testProperty @(SomeLeqNat -> Property)+ "leqToCmp works properly"+ $ \case+ MkSomeLeqNat a b ->+ case leqToCmp a b Witness of+ Left Refl -> toNatural a === toNatural b+ Right Refl ->+ property $ toNatural a < toNatural b+ , testProperty @(SomeSNat -> Property)+ "eqlCmpEQ terminates"+ $ \(SomeSNat n) ->+ totalRefl $ eqlCmpEQ n n Refl+ , testProperty @(SomeSNat -> Property)+ "eqToRefl terminates"+ $ \(SomeSNat n) ->+ totalRefl $ eqToRefl n n Refl+ , testProperty @(SomeSNat -> SomeSNat -> Property)+ "flipCmpNat terminates"+ $ \(SomeSNat n) (SomeSNat m) ->+ totalRefl $ flipCmpNat n m+ , testProperty @(SomeSNat -> Property)+ "ltToNeq works as expected"+ $ \(SomeSNat n) ->+ givesImpossibleVoid $+ ltToNeq n n (unsafeCoerce $ Refl @()) Refl+ , testProperty @(SomeLeqNat -> Property)+ "leqNeqToLT terminates"+ $ \(MkSomeLeqNat n m) ->+ case n %~ m of+ Equal -> discard+ NonEqual ->+ totalRefl $ leqNeqToLT n m Witness (\case {})+ , testProperty @(SomeLeqNat -> Property)+ "succLeqToLT terminates"+ $ \(MkSomeLeqNat n' m) ->+ case n' of+ Succ n ->+ totalRefl $ succLeqToLT n m Witness+ _ -> discard+ , testProperty @(SomeLtNat -> Property)+ "ltToLeq terminates"+ $ \(MkSomeLtNat n m) ->+ totalWitness $ ltToLeq n m Refl+ , testProperty @(SomeGtNat -> Property)+ "gtToLeq terminates"+ $ \(MkSomeGtNat n m) ->+ totalWitness $ gtToLeq n m Refl+ , testCase "congFlipOrdering" $ do+ Refl <- evaluate (congFlipOrdering (Refl @( 'LT)))+ Refl <- evaluate (congFlipOrdering (Refl @( 'GT)))+ Refl <- evaluate (congFlipOrdering (Refl @( 'EQ)))+ pure ()+ , testProperty @(SomeLtNat -> Property) "ltToSuccLeq terminates" $ \(MkSomeLtNat n m) ->+ totalWitness $ ltToSuccLeq n m Refl+ , testProperty @(SomeSNat -> Property) "cmpZero terminates" $ \(SomeSNat n) ->+ totalRefl $ cmpZero n+ , testProperty @(SomeLeqNat -> Property) "leqToGT terminates" $ \(MkSomeLeqNat b0 a) ->+ case b0 of+ Succ b ->+ totalRefl $ leqToGT a b Witness+ Zero -> discard+ , testProperty @(SomeSNat -> Property) "cmpZero' works as expected" $ \(SomeSNat n) ->+ case n of+ Zero -> cmpZero' n === Left Refl+ Succ {} -> case cmpZero' n of+ Right Refl -> property True+ l -> counterexample ("Left Refl expected, but got: " <> show l) False+ , testProperty @(SomeSNat -> Property)+ "zeroNoLT works as expected"+ $ \(SomeSNat n) ->+ givesImpossibleVoid $ zeroNoLT n (unsafeCoerce $ Refl @())+ , testProperty @(SomeLtNat -> Property) "ltRightPredSucc terminates" $ \(MkSomeLtNat a b) ->+ totalRefl $ ltRightPredSucc a b Refl+ , testProperty @(SomeSNat -> SomeSNat -> Property) "cmpSucc terminates" $ \(SomeSNat a) (SomeSNat b) ->+ totalRefl $ cmpSucc a b+ , testProperty @(SomeSNat -> Property) "ltSucc terminates" $ \(SomeSNat a) ->+ totalRefl $ ltSucc a+ , testProperty @(SomeLtNat -> Property) "cmpSuccStepR terminates" $ \(MkSomeLtNat a b) ->+ totalRefl $ cmpSuccStepR a b Refl+ , testProperty @(SomeLtNat -> Property) "ltSuccLToLT terminates" $ \(MkSomeLtNat a0 b) ->+ case a0 of+ Succ a -> totalRefl $ ltSuccLToLT a b Refl+ Zero -> discard+ , testProperty @(SomeLeqNat -> Property) "leqToLT terminates" $ \(MkSomeLeqNat a0 b) ->+ case a0 of+ Succ a -> totalRefl $ leqToLT a b Witness+ Zero -> discard+ , testProperty @(SomeSNat -> Property) "leqZero terminates" $ \(SomeSNat n) ->+ totalWitness $ leqZero n+ , testProperty @(SomeLeqNat -> Property) "leqSucc terminates" $ \(MkSomeLeqNat n m) ->+ totalWitness $ leqSucc n m Witness+ , testProperty @(SomeLeqView -> Property) "fromLeqView terminates" $ \(MkSomeLeqView lview) ->+ totalWitness $ fromLeqView lview+ , testProperty @(SomeSNat -> Property) "leqViewRefl works properly" $ \(SomeSNat sn) ->+ case leqViewRefl sn of+ LeqZero sn' ->+ toNatural sn' === toNatural sn .&&. toNatural sn' === 0+ LeqSucc sn' sm' Witness ->+ toNatural sn' === toNatural sm'+ .&&. toNatural sn' + 1 === toNatural sn+ , testProperty @(SomeLeqNat -> Property) "viewLeq works properly" $ \(MkSomeLeqNat sn sm) ->+ case viewLeq sn sm Witness of+ LeqZero sm' ->+ toNatural sn === 0 .&&. toNatural sm === toNatural sm'+ LeqSucc sn' sm' Witness ->+ toNatural sn' + 1 === toNatural sn+ .&&. toNatural sm' + 1 === toNatural sm+ .&&. toNatural sn' <= toNatural sm'+ , testProperty @(SomeLeqNat -> Property) "leqWitness gives the difference as a witness" $+ \(MkSomeLeqNat sn sm) ->+ case leqWitness sn sm Witness of+ DiffNat sn' delta ->+ toNatural sn === toNatural sn'+ .&&. toNatural sn' + toNatural delta === toNatural sm+ , testProperty @(SomeSNat -> SomeSNat -> Property)+ "leqStep terminates"+ $ \(SomeSNat n) (SomeSNat l) ->+ let m = n %+ l+ in totalWitness $ leqStep n m l Refl+ , testProperty @(SomeLeqNat -> Property) "leqNeqToSuccLeq terminates" $+ \(MkSomeLeqNat n m) ->+ case n %~ m of+ Equal -> discard+ NonEqual ->+ totalWitness $ leqNeqToSuccLeq n m Witness (\case {})+ , testProperty @(SomeSNat -> Property) "leqRefl terminates" $+ \(SomeSNat n) ->+ totalWitness $ leqRefl n+ , testProperty @(SomeLeqNat -> Property) "leqSuccStepR and leqSuccStepL terminates" $+ \(MkSomeLeqNat n m) ->+ totalWitness (leqSuccStepR n m Witness)+ .&&. case n of+ Succ n' ->+ label "leqSuccStepL tested" $+ totalWitness (leqSuccStepL n' m Witness)+ _ -> property True+ , testProperty @(SomeSNat -> Property) "leqReflexive terminates" $+ \(SomeSNat n) ->+ totalWitness $ leqReflexive n n Refl+ , testProperty @(SomeLeqNat -> SomeSNat -> Property) "leqTrans terminates" $+ \(MkSomeLeqNat (n :: SNat n) (m :: SNat m)) (SomeSNat (l0 :: SNat lMinsM)) ->+ let l = m %+ l0+ in case m %<=? l of+ STrue ->+ totalWitness $+ leqTrans n m l Witness (Witness :: IsTrue (m <=? (m + lMinsM)))+ SFalse -> error "impossible"+ , testProperty @(SomeSNat -> Property) "leqAntisymm terminates" $+ \(SomeSNat n) ->+ totalRefl $ leqAntisymm n n Witness Witness+ , testProperty @(SomeLeqNat -> SomeLeqNat -> Property) "plusMonotone terminates" $+ \(MkSomeLeqNat n m) (MkSomeLeqNat l k) ->+ totalWitness $ plusMonotone n m l k Witness Witness+ , testCase "leqZeroElim terminates" $+ leqZeroElim (sNat @0) Witness @?= Refl+ , testProperty @(SomeLeqNat -> SomeSNat -> Property) "plusMonotoneL terminates" $+ \(MkSomeLeqNat n m) (SomeSNat l) ->+ totalWitness $ plusMonotoneL n m l Witness+ , testProperty @(SomeLeqNat -> SomeSNat -> Property) "plusMonotoneR terminates" $+ \(MkSomeLeqNat n m) (SomeSNat l) ->+ totalWitness $ plusMonotoneR l n m Witness+ , testProperty @(SomeSNat -> SomeSNat -> Property) "plusLeqL terminates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalWitness $ plusLeqL n m+ , testProperty @(SomeSNat -> SomeSNat -> Property) "plusLeqR terminates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalWitness $ plusLeqR n m+ , testProperty @(SomeLeqNat -> SomeSNat -> Property) "plusCancelLeqL terminates" $+ \(MkSomeLeqNat (m :: SNat m) (l :: SNat l)) (SomeSNat n) ->+ totalWitness $+ plusCancelLeqR+ n+ m+ l+ (unsafeCoerce (Witness :: IsTrue (m <=? l)))+ , testProperty @(SomeLeqNat -> SomeSNat -> Property) "plusCancelLeqR terminates" $+ \(MkSomeLeqNat (n :: SNat n) (m :: SNat m)) (SomeSNat l) ->+ totalWitness $+ plusCancelLeqR+ n+ m+ l+ (unsafeCoerce (Witness :: IsTrue (n <=? m)))+ , testProperty @(SomeSNat -> Property) "succLeqZeroAbsurd works properly" $ \(SomeSNat n) ->+ givesImpossibleVoid $ succLeqZeroAbsurd n (unsafeCoerce Witness)+ , testProperty @(SomeSNat -> Property) "succLeqZeroAbsurd' works properly" $ \(SomeSNat n) ->+ totalRefl $ succLeqZeroAbsurd' n+ , testProperty @(SomeSNat -> Property) "succLeqAbsurd works properly" $ \(SomeSNat n) ->+ givesImpossibleVoid $ succLeqAbsurd n (unsafeCoerce Witness)+ , testProperty @(SomeSNat -> Property) "succLeqAbsurd' works properly" $ \(SomeSNat n) ->+ totalRefl $ succLeqAbsurd' n+ , testProperty @(SomeGtNat -> Property)+ "notLeqToLeq terminates"+ $ \(MkSomeGtNat n m) ->+ case n %<=? m of+ STrue -> error "impossible!"+ SFalse ->+ totalWitness $ notLeqToLeq n m+ , testProperty+ @(SomeSNat -> SomeSNat -> Property)+ "leqSucc' terminates"+ $ \(SomeSNat n) (SomeSNat m) ->+ totalRefl $ leqSucc' n m+ , testProperty @(SomeLeqNat -> Property) "leqToMin terminates" $+ \(MkSomeLeqNat n m) ->+ totalRefl $ leqToMin n m Witness+ , testProperty @(SomeLeqNat -> Property) "geqToMin terminates" $+ \(MkSomeLeqNat n m) ->+ totalRefl $ geqToMin m n Witness+ , testProperty @(SomeSNat -> SomeSNat -> Property) "minComm terminates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalRefl $ minComm n m+ , testProperty @(SomeSNat -> SomeSNat -> Property) "minLeqL terminates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalWitness $ minLeqL n m+ , testProperty @(SomeSNat -> SomeSNat -> Property) "minLeqR terminates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalWitness $ minLeqR n m+ , testProperty @(SomeLeqNat -> SomeSNat -> Property) "minLargest terminates" $+ \(MkSomeLeqNat l n) (SomeSNat lm) ->+ let m = l %+ lm+ in totalWitness $+ minLargest l n m Witness (unsafeCoerce Witness)+ , testProperty @(SomeLeqNat -> Property) "leqToMax termaxates" $+ \(MkSomeLeqNat n m) ->+ totalRefl $ leqToMax n m Witness+ , testProperty @(SomeLeqNat -> Property) "geqToMax termaxates" $+ \(MkSomeLeqNat n m) ->+ totalRefl $ geqToMax m n Witness+ , testProperty @(SomeSNat -> SomeSNat -> Property) "maxComm termaxates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalRefl $ maxComm n m+ , testProperty @(SomeSNat -> SomeSNat -> Property) "maxLeqL termaxates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalWitness $ maxLeqL n m+ , testProperty @(SomeSNat -> SomeSNat -> Property) "maxLeqR termaxates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalWitness $ maxLeqR n m+ , testProperty @(SomeLeqNat -> Property) "maxLeast termaxates" $+ \(MkSomeLeqNat n l) ->+ forAll (elements [0 .. toNatural l]) $ \m0 ->+ case toSomeSNat m0 of+ SomeSNat m ->+ totalWitness $+ maxLeast l n m Witness (unsafeCoerce Witness)+ , testProperty @(SomeSNat -> SomeSNat -> Property) "lneqSuccLeq terminates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalRefl $ lneqSuccLeq n m+ , testProperty @(SomeSNat -> SomeSNat -> Property) "lneqReversed terminates" $+ \(SomeSNat n) (SomeSNat m) ->+ totalRefl $ lneqReversed n m+ , testProperty @(SomeLneqNat -> Property) "lneqToLT terminates" $+ \(MkSomeLneqNat n m) ->+ totalRefl $ lneqToLT n m Witness+ , testProperty @(SomeLtNat -> Property) "ltToLneq terminates" $+ \(MkSomeLtNat n m) ->+ totalWitness $ ltToLneq n m Refl+ , testProperty @(SomeSNat -> Property) "lneqZero terminates" $+ \(SomeSNat n) -> totalWitness $ lneqZero n+ , testProperty @(SomeSNat -> Property) "lneqSucc terminates" $+ \(SomeSNat n) -> totalWitness $ lneqSucc n+ , testProperty @(SomeSNat -> SomeSNat -> Property) "succLneqSucc terminates" $+ \(SomeSNat n) (SomeSNat m) -> totalRefl $ succLneqSucc n m+ , testProperty @(SomeLneqNat -> Property) "lneqRightPredSucc terminates" $+ \(MkSomeLneqNat n m) ->+ totalRefl $ lneqRightPredSucc n m Witness+ , testProperty @(SomeLneqNat -> Property) "lneqSuccStepL and lneqSuccStepR works properly" $+ \(MkSomeLneqNat n m) ->+ conjoin+ [ totalWitness (lneqSuccStepR n m Witness)+ , case n of+ Succ n' ->+ label "lneqSuccStepL checked" $+ totalWitness (lneqSuccStepL n' m Witness)+ Zero -> property True+ ]+ , testProperty @(SomeLneqNat -> SomeLneqNat -> Property)+ "plusStrictMonotone terminates"+ $ \(MkSomeLneqNat n m) (MkSomeLneqNat l k) ->+ totalWitness $+ plusStrictMonotone n m l k Witness Witness+ , testProperty @(SomeSNat -> Property) "maxZeroL terminates" $+ \(SomeSNat n) -> totalRefl $ maxZeroL n+ , testProperty @(SomeSNat -> Property) "maxZeroR terminates" $+ \(SomeSNat n) -> totalRefl $ maxZeroR n+ , testProperty @(SomeSNat -> Property) "minZeroL terminates" $+ \(SomeSNat n) -> totalRefl $ minZeroL n+ , testProperty @(SomeSNat -> Property) "minZeroR terminates" $+ \(SomeSNat n) -> totalRefl $ minZeroR n+ , testProperty @(SomeLeqNat -> Property) "minusSucc terminates" $+ \(MkSomeLeqNat m n) ->+ totalRefl $ minusSucc n m Witness+ , testProperty @(SomeSNat -> Property) "lneqZeroAbsurd is absurd" $+ \(SomeSNat n) ->+ givesImpossibleVoid $+ lneqZeroAbsurd n $ unsafeCoerce Witness+ , testProperty @(SomeLeqNat -> Property)+ "minusPlus terminates"+ $ \(MkSomeLeqNat m n) ->+ totalRefl $+ minusPlus n m Witness+ , testProperty @(SomeSNat -> SomeSNat -> Property)+ "minPlusTruncMinus terminates"+ $ \(SomeSNat n) (SomeSNat m) ->+ totalRefl $ minPlusTruncMinus n m+ , testProperty @(SomeSNat -> SomeSNat -> Property)+ "truncMinusLeq terminates"+ $ \(SomeSNat n) (SomeSNat m) ->+ totalWitness $ truncMinusLeq n m+ ]++totalWitness :: IsTrue p -> Property+totalWitness w =+ counterexample "Witness is not totalRefl!" $+ within+ 10000+ ( (case w of Witness -> True :: Bool) ::+ Bool+ )++totalRefl :: a :~: b -> Property+totalRefl = total
type-natural.cabal view
@@ -1,96 +1,105 @@ cabal-version: >=1.10 name: type-natural-version: 1.1.0.0+version: 1.1.0.1 license: BSD3 license-file: LICENSE copyright: (C) Hiromi ISHII 2013-2014 maintainer: konn.jinro_at_gmail.com author: Hiromi ISHII-tested-with:- ghc ==8.4.3 ghc ==8.6.5 ghc ==8.8.3 ghc ==8.10.3-+tested-with: GHC ==8.6.5 || ==8.8.4 || ==8.10.7 || ==9.0.1 || ==9.2.1 homepage: https://github.com/konn/type-natural synopsis: Type-level natural and proofs of their properties. description:- Type-level natural numbers and proofs of their properties.- .- Version 0.6+ supports __GHC 8+ only__.- .- __Use 0.5.* with ~ GHC 7.10.3__.+ Type-level natural numbers and proofs of their properties.+ .+ Version 0.6+ supports __GHC 8+ only__.+ .+ __Use 0.5.* with ~ GHC 7.10.3__. category: Math build-type: Simple source-repository head- type: git- location: git://github.com/konn/type-natural.git+ type: git+ location: git://github.com/konn/type-natural.git library- exposed-modules:- Data.Type.Natural- Data.Type.Ordinal- Data.Type.Ordinal.Builtin- Data.Type.Natural.Builtin- Data.Type.Natural.Lemma.Arithmetic- Data.Type.Natural.Lemma.Order- Data.Type.Natural.Presburger.MinMaxSolver+ exposed-modules:+ Data.Type.Natural+ Data.Type.Natural.Builtin+ Data.Type.Natural.Lemma.Arithmetic+ Data.Type.Natural.Lemma.Order+ Data.Type.Natural.Presburger.MinMaxSolver+ Data.Type.Ordinal+ Data.Type.Ordinal.Builtin - hs-source-dirs: src- other-modules:- Data.Type.Natural.Core- Data.Type.Natural.Utils- Data.Type.Natural.Lemma.Presburger+ hs-source-dirs: src+ other-modules:+ Data.Type.Natural.Core+ Data.Type.Natural.Lemma.Presburger+ Data.Type.Natural.Utils - default-language: Haskell2010- default-extensions:- DataKinds PolyKinds ConstraintKinds GADTs ScopedTypeVariables- TemplateHaskell TypeFamilies TypeOperators MultiParamTypeClasses- UndecidableInstances FlexibleContexts FlexibleInstances+ default-language: Haskell2010+ default-extensions:+ ConstraintKinds+ DataKinds+ FlexibleContexts+ FlexibleInstances+ GADTs+ MultiParamTypeClasses+ PolyKinds+ ScopedTypeVariables+ TemplateHaskell+ TypeFamilies+ TypeOperators+ UndecidableInstances - ghc-options: -Wall -O2 -fno-warn-orphans- build-depends:- base ==4.*,- ghc,- equational-reasoning >=0.4.1.1,- template-haskell >=2.8,- constraints >=0.3,- ghc-typelits-natnormalise >=0.4,- ghc-typelits-presburger >=0.5.1,- ghc-typelits-knownnat -any,- integer-logarithms -any+ ghc-options: -Wall -O2 -fno-warn-orphans+ build-depends:+ base >=4 && <5+ , constraints >=0.3+ , equational-reasoning >=0.4.1.1+ , ghc+ , ghc-typelits-knownnat+ , ghc-typelits-natnormalise >=0.4+ , ghc-typelits-presburger >=0.5.1+ , integer-logarithms+ , template-haskell >=2.8 - if impl(ghc >=8.0.0)- ghc-options: -Wno-redundant-constraints+ if impl(ghc >=8.0.0)+ ghc-options: -Wno-redundant-constraints - if impl(ghc >=8.6)- default-extensions: NoStarIsType+ if impl(ghc >=8.6)+ default-extensions: NoStarIsType test-suite type-natural-test- type: exitcode-stdio-1.0- main-is: test.hs- build-tools: tasty-discover -any- hs-source-dirs: tests- default-language: Haskell2010- other-modules:- Shared- Data.Type.NaturalSpec- Data.Type.NaturalSpec.TH- Data.Type.Natural.Presburger.MinMaxSolverSpec- Data.Type.Natural.Presburger.Cases- Data.Type.OrdinalSpec+ type: exitcode-stdio-1.0+ main-is: test.hs+ build-tools: tasty-discover -any+ hs-source-dirs: tests+ default-language: Haskell2010+ ghc-options: -Wall+ other-modules:+ Data.Type.Natural.Lemma.OrderSpec+ Data.Type.Natural.Presburger.Cases+ Data.Type.Natural.Presburger.MinMaxSolverSpec+ Data.Type.NaturalSpec+ Data.Type.NaturalSpec.TH+ Data.Type.OrdinalSpec+ Shared - build-depends:- tasty -any,- QuickCheck -any,- tasty-quickcheck -any,- quickcheck-instances -any,- integer-logarithms -any,- tasty-hunit -any,- tasty-discover -any,- template-haskell -any,- base -any,- type-natural -any,- equational-reasoning -any+ build-depends:+ base+ , equational-reasoning+ , integer-logarithms+ , QuickCheck+ , quickcheck-instances+ , tasty+ , tasty-discover+ , tasty-hunit+ , tasty-quickcheck+ , template-haskell+ , type-natural - if impl(ghc >=8.6)- default-extensions: NoStarIsType+ if impl(ghc >=8.6)+ default-extensions: NoStarIsType