type-natural 0.6.1.0 → 0.6.1.1
raw patch · 5 files changed
+53/−74 lines, 5 filesdep ~equational-reasoningPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: equational-reasoning
API changes (from Hackage documentation)
- Data.Type.Natural: (%:**) :: forall (t_aYH2 :: Nat) (t_aYH3 :: Nat). Sing t_aYH2 -> Sing t_aYH3 -> Sing (Apply (Apply (:**$) t_aYH2) t_aYH3 :: Nat)
+ Data.Type.Natural: (%:**) :: forall (t_aYIR :: Nat) (t_aYIS :: Nat). Sing t_aYIR -> Sing t_aYIS -> Sing (Apply (Apply (:**$) t_aYIR) t_aYIS :: Nat)
- Data.Type.Natural: class (SOrd nat, IsPeano nat) => PeanoOrder nat where ltToNeq a b aLTb aEQb = eliminate $ start SLT === sCompare a b `because` sym aLTb === SEQ `because` eqlCmpEQ a b aEQb leqNeqToLT a b aLEQb aNEQb = either (absurd . aNEQb) id $ leqToCmp a b aLEQb 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 } gtToLeq n m nGTm = ltToLeq m n $ start (sCompare m n) === sFlipOrdering (sCompare n m) `because` sym (flipCompare n m) === sFlipOrdering SGT `because` congFlipOrdering nGTm =~= SLT ltToSuccLeq n m nLTm = leqNeqToSuccLeq n m (ltToLeq n m nLTm) (ltToNeq n m nLTm) 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) leqToGT a b sbLEQa = start (sCompare a b) === sFlipOrdering (sCompare b a) `because` sym (flipCompare b a) === sFlipOrdering SLT `because` congFlipOrdering (leqToLT b a sbLEQa) =~= SGT cmpZero' n = case zeroOrSucc n of { IsZero -> Left $ eqlCmpEQ sZero n Refl IsSucc n' -> Right $ cmpZero n' } zeroNoLT n eql = case cmpZero' n of { Left cmp0nEQ -> eliminate $ start SGT =~= sFlipOrdering SLT === sFlipOrdering (sCompare n sZero) `because` congFlipOrdering (sym eql) === sCompare sZero n `because` flipCompare n sZero === SEQ `because` cmp0nEQ Right cmp0nLT -> eliminate $ start SGT =~= sFlipOrdering SLT === sFlipOrdering (sCompare n sZero) `because` congFlipOrdering (sym eql) === sCompare sZero n `because` flipCompare n sZero === SLT `because` cmp0nLT } 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 } cmpSucc n m = case sCompare 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 $ flipCompare 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 (sCompare n m) =~= SGT =~= sFlipOrdering SLT === sFlipOrdering (sCompare (sSucc m) (sSucc n)) `because` congFlipOrdering (sym pf) === sCompare (sSucc n) (sSucc m) `because` flipCompare (sSucc m) (sSucc n) } } ltSucc = proofLTSucc . induction base step where base :: LTSucc (Zero nat) base = LTSucc $ cmpZero (sZero :: Sing (Zero nat)) step :: Sing (n :: nat) -> LTSucc n -> LTSucc (Succ n) step n (LTSucc ih) = LTSucc $ start (sCompare (sSucc n) (sSucc (sSucc n))) === sCompare n (sSucc n) `because` sym (cmpSucc n (sSucc n)) === SLT `because` ih cmpSuccStepR = proofCmpSuccStepR . induction base step where base :: CmpSuccStepR (Zero nat) base = CmpSuccStepR $ \ m _ -> cmpZero m step :: Sing (n :: nat) -> CmpSuccStepR n -> CmpSuccStepR (Succ n) 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 (sCompare (sSucc n) (sSucc m)) =~= sCompare (sSucc n) (sSucc (sSucc m')) === sCompare n (sSucc m') `because` sym (cmpSucc n (sSucc m')) === SLT `because` ih m' nLTm' } ltSuccLToLT n m snLTm = case zeroOrSucc m of { IsZero -> absurd $ zeroNoLT (sSucc n) snLTm IsSucc m' -> let nLTm = cmpSucc n m' `trans` snLTm in start (sCompare n (sSucc m')) === SLT `because` cmpSuccStepR n m' nLTm } leqToLT n m snLEQm = case leqToCmp (sSucc n) m snLEQm of { Left Refl -> start (sCompare n m) =~= sCompare n (sSucc n) === SLT `because` ltSucc n Right nLTm -> ltSuccLToLT n m nLTm } leqZero sn = case zeroOrSucc sn of { IsZero -> leqRefl sn IsSucc pn -> ltToLeq sZero sn $ cmpZero pn } leqSucc n m nLEQm = case leqToCmp n m nLEQm of { Left Refl -> leqRefl (sSucc n) Right nLTm -> ltToLeq (sSucc n) (sSucc m) $ sym (cmpSucc n m) `trans` nLTm } fromLeqView (LeqZero n) = leqZero n fromLeqView (LeqSucc n m nLEQm) = leqSucc n m nLEQm leqViewRefl = proofLeqViewRefl . induction base step where base :: LeqViewRefl (Zero nat) base = LeqViewRefl $ LeqZero sZero step :: Sing (n :: nat) -> LeqViewRefl n -> LeqViewRefl (Succ n) step n (LeqViewRefl nLEQn) = LeqViewRefl $ LeqSucc n n (fromLeqView nLEQn) viewLeq n m nLEQm = case (zeroOrSucc n, leqToCmp n m nLEQm) of { (IsZero, _) -> LeqZero m (_, Left Refl) -> leqViewRefl n (IsSucc n', Right nLTm) -> let sm'EQm = ltRightPredSucc n m nLTm m' = sPred m n'LTm' = cmpSucc n' m' `trans` compareCongR n (sym sm'EQm) `trans` nLTm in coerce (sym sm'EQm) $ LeqSucc n' m' $ ltToLeq n' m' n'LTm' } leqWitness = leqWitPf . induction base step where base :: LeqWitPf (Zero nat) base = LeqWitPf $ \ sm _ -> coerce (plusZeroL sm) $ DiffNat sZero sm step :: Sing (n :: nat) -> LeqWitPf n -> LeqWitPf (Succ n) step (n :: Sing n) (LeqWitPf ih) = LeqWitPf $ \ m snLEQm -> case viewLeq (sSucc n) m snLEQm of { LeqZero _ -> absurd $ succNonCyclic n Refl LeqSucc (_ :: Sing n') pm nLEQpm -> succDiffNat n pm $ ih pm $ coerceLeqL (succInj Refl :: n' :~: n) pm nLEQpm } leqStep = leqStepPf . induction base step where base :: LeqStepPf (Zero nat) base = LeqStepPf $ \ k _ _ -> leqZero k step :: Sing (n :: nat) -> LeqStepPf n -> LeqStepPf (Succ n) 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 leqNeqToSuccLeq n m nLEQm nNEQm = case leqWitness n m nLEQm of { DiffNat _ k -> case zeroOrSucc k of { IsZero -> absurd $ nNEQm $ sym $ plusZeroR n IsSucc k' -> leqStep (sSucc n) m k' $ start (sSucc n %:+ k') === sSucc (n %:+ k') `because` plusSuccL n k' === n %:+ sSucc k' `because` sym (plusSuccR n k') =~= m } } leqRefl sn = leqStep sn sn sZero (plusZeroR sn) 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 } leqSuccStepL n m snLEQm = leqTrans n (sSucc n) m (leqSuccStepR n n $ leqRefl n) snLEQm leqReflexive n _ Refl = leqRefl n 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) } } 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 } 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 } leqZeroElim n nLE0 = case viewLeq n sZero nLE0 of { LeqZero _ -> Refl LeqSucc _ pZ _ -> absurd $ succNonCyclic pZ Refl } plusMonotoneL n m l leq = plusMonotone n m l l leq (leqRefl l) plusMonotoneR n m l leq = plusMonotone n n m l (leqRefl n) leq plusLeqL n m = leqStep n (n %:+ m) m Refl plusLeqR n m = leqStep m (n %:+ m) n $ plusComm m n 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 } plusCancelLeqL n m l nmLEQnl = plusCancelLeqR m l n $ coerceLeqL (plusComm n m) (l %:+ n) $ coerceLeqR (n %:+ m) (plusComm n l) nmLEQnl succLeqZeroAbsurd n leq = succNonCyclic n (leqZeroElim (sSucc n) leq) succLeqZeroAbsurd' n = case sSucc n %:<= sZero of { STrue -> absurd $ succLeqZeroAbsurd n Witness SFalse -> Refl } succLeqAbsurd n snLEQn = eliminate $ start SLT === sCompare n n `because` sym (succLeqToLT n n snLEQn) === SEQ `because` eqlCmpEQ n n Refl succLeqAbsurd' n = case sSucc n %:<= n of { STrue -> absurd $ succLeqAbsurd n Witness SFalse -> Refl } notLeqToLeq n m = case sCompare n m of { SLT -> eliminate $ ltToLeq n m Refl SEQ -> eliminate $ leqReflexive n m $ eqToRefl n m Refl SGT -> gtToLeq n m Refl } leqSucc' n m = case n %:<= m of { STrue -> case leqSucc n m Witness of { Witness -> Refl } SFalse -> case sSucc n %:<= sSucc m of { SFalse -> Refl STrue -> case viewLeq (sSucc n) (sSucc m) Witness of { LeqZero _ -> absurd $ succNonCyclic n Refl LeqSucc n' m' Witness -> eliminate $ start STrue =~= (n' %:<= m') === (n %:<= m) `because` sLeqCong (succInj' n' n Refl) (succInj' m' m Refl) =~= SFalse } } } leqToMin n m nLEQm = leqAntisymm (sMin n m) n (minLeqL n m) (minLargest n n m (leqRefl n) nLEQm) geqToMin n m mLEQn = leqAntisymm (sMin n m) m (minLeqR n m) (minLargest m n m mLEQn (leqRefl m)) minComm n m = case n %:<= m of { STrue -> start (sMin n m) === n `because` leqToMin n m Witness === sMin m n `because` sym (geqToMin m n Witness) SFalse -> start (sMin n m) === m `because` geqToMin n m (notLeqToLeq n m) === sMin m n `because` sym (leqToMin m n $ notLeqToLeq n m) } minLeqL n m = case n %:<= m of { STrue -> leqReflexive (sMin n m) n $ leqToMin n m Witness SFalse -> let mLEQn = notLeqToLeq n m in leqTrans (sMin n m) m n (leqReflexive (sMin n m) m (geqToMin n m mLEQn)) $ mLEQn } minLeqR n m = leqTrans (sMin n m) (sMin m n) m (leqReflexive (sMin n m) (sMin m n) $ minComm n m) (minLeqL m n) minLargest l n m lLEQn lLEQm = withSingI l $ withSingI n $ withSingI m $ withSingI (sMin n m) $ case n %:<= m of { STrue -> leqTrans l n (sMin n m) lLEQn $ leqReflexive sing sing $ sym $ leqToMin n m Witness SFalse -> let mLEQn = notLeqToLeq n m in leqTrans l m (sMin n m) lLEQm $ leqReflexive sing sing $ sym $ geqToMin n m mLEQn } leqToMax n m nLEQm = leqAntisymm (sMax n m) m (maxLeast m n m nLEQm (leqRefl m)) (maxLeqR n m) geqToMax n m mLEQn = leqAntisymm (sMax n m) n (maxLeast n n m (leqRefl n) mLEQn) (maxLeqL n m) maxComm n m = case n %:<= m of { STrue -> start (sMax n m) === m `because` leqToMax n m Witness === sMax m n `because` sym (geqToMax m n Witness) SFalse -> start (sMax n m) === n `because` geqToMax n m (notLeqToLeq n m) === sMax m n `because` sym (leqToMax m n $ notLeqToLeq n m) } maxLeqR n m = case n %:<= m of { STrue -> leqReflexive m (sMax n m) $ sym $ leqToMax n m Witness SFalse -> let mLEQn = notLeqToLeq n m in leqTrans m n (sMax n m) mLEQn (leqReflexive n (sMax n m) (sym $ geqToMax n m mLEQn)) } maxLeqL n m = leqTrans n (sMax m n) (sMax n m) (maxLeqR m n) (leqReflexive (sMax m n) (sMax n m) $ maxComm m n) maxLeast l n m lLEQn lLEQm = withSingI l $ withSingI n $ withSingI m $ withSingI (sMax n m) $ case n %:<= m of { STrue -> leqTrans (sMax n m) m l (leqReflexive sing sing $ leqToMax n m Witness) lLEQm SFalse -> let mLEQn = notLeqToLeq n m in leqTrans (sMax n m) n l (leqReflexive sing sing $ geqToMax n m mLEQn) lLEQn } lneqToLT n m nLNEm = succLeqToLT n m $ coerce (lneqSuccLeq n m) nLNEm ltToLneq n m nLTm = coerce (sym $ lneqSuccLeq n m) $ ltToSuccLeq n m nLTm lneqZero n = ltToLneq sZero (sSucc n) $ cmpZero n lneqSucc n = ltToLneq n (sSucc n) $ ltSucc n succLneqSucc n m = start (n %:< m) === (sSucc n %:<= m) `because` lneqSuccLeq n m === (sSucc (sSucc n) %:<= sSucc m) `because` leqSucc' (sSucc n) m === (sSucc n %:< sSucc m) `because` sym (lneqSuccLeq (sSucc n) (sSucc m)) lneqRightPredSucc n m nLNEQm = ltRightPredSucc n m $ lneqToLT n m nLNEQm lneqSuccStepL n m snLNEQm = coerce (sym $ lneqSuccLeq n m) $ leqSuccStepL (sSucc n) m $ coerce (lneqSuccLeq (sSucc n) m) snLNEQm lneqSuccStepR n m nLNEQm = coerce (sym $ lneqSuccLeq n (sSucc m)) $ leqSuccStepR (sSucc n) m $ coerce (lneqSuccLeq n m) nLNEQm plusStrictMonotone n m l k nLNm lLNk = coerce (sym $ lneqSuccLeq (n %:+ l) (m %:+ k)) $ flip coerceLeqL (m %:+ k) (plusSuccL n l) $ plusMonotone (sSucc n) m l k (coerce (lneqSuccLeq n m) nLNm) (leqTrans l (sSucc l) k (leqSuccStepR l l (leqRefl l)) $ coerce (lneqSuccLeq l k) lLNk) maxZeroL n = leqToMax sZero n (leqZero n) maxZeroR n = geqToMax n sZero (leqZero n) minZeroL n = leqToMin sZero n (leqZero n) minZeroR n = geqToMin n sZero (leqZero n) minusSucc n m mLEQn = case leqWitness m n mLEQn of { DiffNat _ k -> start (sSucc n %:- m) =~= sSucc (m %:+ k) %:- m === (m %:+ sSucc k) %:- m `because` minusCongL (sym $ plusSuccR m k) m === (sSucc k %:+ m) %:- m `because` minusCongL (plusComm m (sSucc k)) m === sSucc k `because` plusMinus (sSucc k) m === sSucc (k %:+ m %:- m) `because` succCong (sym $ plusMinus k m) === sSucc (m %:+ k %:- m) `because` succCong (minusCongL (plusComm k m) m) =~= sSucc (n %:- m) } lneqZeroAbsurd n leq = succLeqZeroAbsurd n (coerce (lneqSuccLeq n sZero) leq) 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 }
+ Data.Type.Natural: class (SOrd nat, IsPeano nat) => PeanoOrder nat where ltToNeq a b aLTb aEQb = eliminate $ start SLT === sCompare a b `because` sym aLTb === SEQ `because` eqlCmpEQ a b aEQb leqNeqToLT a b aLEQb aNEQb = either (absurd . aNEQb) id $ leqToCmp a b aLEQb 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 } gtToLeq n m nGTm = ltToLeq m n $ start (sCompare m n) === sFlipOrdering (sCompare n m) `because` sym (flipCompare n m) === sFlipOrdering SGT `because` congFlipOrdering nGTm =~= SLT ltToSuccLeq n m nLTm = leqNeqToSuccLeq n m (ltToLeq n m nLTm) (ltToNeq n m nLTm) 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) leqToGT a b sbLEQa = start (sCompare a b) === sFlipOrdering (sCompare b a) `because` sym (flipCompare b a) === sFlipOrdering SLT `because` congFlipOrdering (leqToLT b a sbLEQa) =~= SGT cmpZero' n = case zeroOrSucc n of { IsZero -> Left $ eqlCmpEQ sZero n Refl IsSucc n' -> Right $ cmpZero n' } zeroNoLT n eql = case cmpZero' n of { Left cmp0nEQ -> eliminate $ start SGT =~= sFlipOrdering SLT === sFlipOrdering (sCompare n sZero) `because` congFlipOrdering (sym eql) === sCompare sZero n `because` flipCompare n sZero === SEQ `because` cmp0nEQ Right cmp0nLT -> eliminate $ start SGT =~= sFlipOrdering SLT === sFlipOrdering (sCompare n sZero) `because` congFlipOrdering (sym eql) === sCompare sZero n `because` flipCompare n sZero === SLT `because` cmp0nLT } 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 } cmpSucc n m = case sCompare 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 $ flipCompare 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 (sCompare n m) =~= SGT =~= sFlipOrdering SLT === sFlipOrdering (sCompare (sSucc m) (sSucc n)) `because` congFlipOrdering (sym pf) === sCompare (sSucc n) (sSucc m) `because` flipCompare (sSucc m) (sSucc n) } } ltSucc = proofLTSucc . induction base step where base :: LTSucc (Zero nat) base = LTSucc $ cmpZero (sZero :: Sing (Zero nat)) step :: Sing (n :: nat) -> LTSucc n -> LTSucc (Succ n) step n (LTSucc ih) = LTSucc $ start (sCompare (sSucc n) (sSucc (sSucc n))) === sCompare n (sSucc n) `because` sym (cmpSucc n (sSucc n)) === SLT `because` ih cmpSuccStepR = proofCmpSuccStepR . induction base step where base :: CmpSuccStepR (Zero nat) base = CmpSuccStepR $ \ m _ -> cmpZero m step :: Sing (n :: nat) -> CmpSuccStepR n -> CmpSuccStepR (Succ n) 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 (sCompare (sSucc n) (sSucc m)) =~= sCompare (sSucc n) (sSucc (sSucc m')) === sCompare n (sSucc m') `because` sym (cmpSucc n (sSucc m')) === SLT `because` ih m' nLTm' } ltSuccLToLT n m snLTm = case zeroOrSucc m of { IsZero -> absurd $ zeroNoLT (sSucc n) snLTm IsSucc m' -> let nLTm = cmpSucc n m' `trans` snLTm in start (sCompare n (sSucc m')) === SLT `because` cmpSuccStepR n m' nLTm } leqToLT n m snLEQm = case leqToCmp (sSucc n) m snLEQm of { Left eql -> withRefl eql $ start (sCompare n m) =~= sCompare n (sSucc n) === SLT `because` ltSucc n Right nLTm -> ltSuccLToLT n m nLTm } leqZero sn = case zeroOrSucc sn of { IsZero -> leqRefl sn IsSucc pn -> ltToLeq sZero sn $ cmpZero pn } leqSucc n m nLEQm = case leqToCmp n m nLEQm of { Left eql -> withRefl eql $ leqRefl (sSucc n) Right nLTm -> ltToLeq (sSucc n) (sSucc m) $ sym (cmpSucc n m) `trans` nLTm } fromLeqView (LeqZero n) = leqZero n fromLeqView (LeqSucc n m nLEQm) = leqSucc n m nLEQm leqViewRefl = proofLeqViewRefl . induction base step where base :: LeqViewRefl (Zero nat) base = LeqViewRefl $ LeqZero sZero step :: Sing (n :: nat) -> LeqViewRefl n -> LeqViewRefl (Succ n) step n (LeqViewRefl nLEQn) = LeqViewRefl $ LeqSucc n n (fromLeqView nLEQn) viewLeq n m nLEQm = case (zeroOrSucc n, leqToCmp n m nLEQm) of { (IsZero, _) -> LeqZero m (_, Left Refl) -> leqViewRefl n (IsSucc n', Right nLTm) -> let sm'EQm = ltRightPredSucc n m nLTm m' = sPred m n'LTm' = cmpSucc n' m' `trans` compareCongR n (sym sm'EQm) `trans` nLTm in coerce (sym sm'EQm) $ LeqSucc n' m' $ ltToLeq n' m' n'LTm' } leqWitness = leqWitPf . induction base step where base :: LeqWitPf (Zero nat) base = LeqWitPf $ \ sm _ -> coerce (plusZeroL sm) $ DiffNat sZero sm step :: Sing (n :: nat) -> LeqWitPf n -> LeqWitPf (Succ n) step (n :: Sing n) (LeqWitPf ih) = LeqWitPf $ \ m snLEQm -> case viewLeq (sSucc n) m snLEQm of { LeqZero _ -> absurd $ succNonCyclic n Refl LeqSucc (_ :: Sing n') pm nLEQpm -> succDiffNat n pm $ ih pm $ coerceLeqL (succInj Refl :: n' :~: n) pm nLEQpm } leqStep = leqStepPf . induction base step where base :: LeqStepPf (Zero nat) base = LeqStepPf $ \ k _ _ -> leqZero k step :: Sing (n :: nat) -> LeqStepPf n -> LeqStepPf (Succ n) 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 leqNeqToSuccLeq n m nLEQm nNEQm = case leqWitness n m nLEQm of { DiffNat _ k -> case zeroOrSucc k of { IsZero -> absurd $ nNEQm $ sym $ plusZeroR n IsSucc k' -> leqStep (sSucc n) m k' $ start (sSucc n %:+ k') === sSucc (n %:+ k') `because` plusSuccL n k' === n %:+ sSucc k' `because` sym (plusSuccR n k') =~= m } } leqRefl sn = leqStep sn sn sZero (plusZeroR sn) 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 } leqSuccStepL n m snLEQm = leqTrans n (sSucc n) m (leqSuccStepR n n $ leqRefl n) snLEQm leqReflexive n _ Refl = leqRefl n 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) } } 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 } 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 } leqZeroElim n nLE0 = case viewLeq n sZero nLE0 of { LeqZero _ -> Refl LeqSucc _ pZ _ -> absurd $ succNonCyclic pZ Refl } plusMonotoneL n m l leq = plusMonotone n m l l leq (leqRefl l) plusMonotoneR n m l leq = plusMonotone n n m l (leqRefl n) leq plusLeqL n m = leqStep n (n %:+ m) m Refl plusLeqR n m = leqStep m (n %:+ m) n $ plusComm m n 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 } plusCancelLeqL n m l nmLEQnl = plusCancelLeqR m l n $ coerceLeqL (plusComm n m) (l %:+ n) $ coerceLeqR (n %:+ m) (plusComm n l) nmLEQnl succLeqZeroAbsurd n leq = succNonCyclic n (leqZeroElim (sSucc n) leq) succLeqZeroAbsurd' n = case sSucc n %:<= sZero of { STrue -> absurd $ succLeqZeroAbsurd n Witness SFalse -> Refl } succLeqAbsurd n snLEQn = eliminate $ start SLT === sCompare n n `because` sym (succLeqToLT n n snLEQn) === SEQ `because` eqlCmpEQ n n Refl succLeqAbsurd' n = case sSucc n %:<= n of { STrue -> absurd $ succLeqAbsurd n Witness SFalse -> Refl } notLeqToLeq n m = case sCompare n m of { SLT -> eliminate $ ltToLeq n m Refl SEQ -> eliminate $ leqReflexive n m $ eqToRefl n m Refl SGT -> gtToLeq n m Refl } leqSucc' n m = case n %:<= m of { STrue -> withWitness (leqSucc n m Witness) Refl SFalse -> case sSucc n %:<= sSucc m of { SFalse -> Refl STrue -> case viewLeq (sSucc n) (sSucc m) Witness of { LeqZero _ -> absurd $ succNonCyclic n Refl LeqSucc n' m' Witness -> eliminate $ start STrue =~= (n' %:<= m') === (n %:<= m) `because` sLeqCong (succInj' n' n Refl) (succInj' m' m Refl) =~= SFalse } } } leqToMin n m nLEQm = leqAntisymm (sMin n m) n (minLeqL n m) (minLargest n n m (leqRefl n) nLEQm) geqToMin n m mLEQn = leqAntisymm (sMin n m) m (minLeqR n m) (minLargest m n m mLEQn (leqRefl m)) minComm n m = case n %:<= m of { STrue -> start (sMin n m) === n `because` leqToMin n m Witness === sMin m n `because` sym (geqToMin m n Witness) SFalse -> start (sMin n m) === m `because` geqToMin n m (notLeqToLeq n m) === sMin m n `because` sym (leqToMin m n $ notLeqToLeq n m) } minLeqL n m = case n %:<= m of { STrue -> leqReflexive (sMin n m) n $ leqToMin n m Witness SFalse -> let mLEQn = notLeqToLeq n m in leqTrans (sMin n m) m n (leqReflexive (sMin n m) m (geqToMin n m mLEQn)) $ mLEQn } minLeqR n m = leqTrans (sMin n m) (sMin m n) m (leqReflexive (sMin n m) (sMin m n) $ minComm n m) (minLeqL m n) minLargest l n m lLEQn lLEQm = withSingI l $ withSingI n $ withSingI m $ withSingI (sMin n m) $ case n %:<= m of { STrue -> leqTrans l n (sMin n m) lLEQn $ leqReflexive sing sing $ sym $ leqToMin n m Witness SFalse -> let mLEQn = notLeqToLeq n m in leqTrans l m (sMin n m) lLEQm $ leqReflexive sing sing $ sym $ geqToMin n m mLEQn } leqToMax n m nLEQm = leqAntisymm (sMax n m) m (maxLeast m n m nLEQm (leqRefl m)) (maxLeqR n m) geqToMax n m mLEQn = leqAntisymm (sMax n m) n (maxLeast n n m (leqRefl n) mLEQn) (maxLeqL n m) maxComm n m = case n %:<= m of { STrue -> start (sMax n m) === m `because` leqToMax n m Witness === sMax m n `because` sym (geqToMax m n Witness) SFalse -> start (sMax n m) === n `because` geqToMax n m (notLeqToLeq n m) === sMax m n `because` sym (leqToMax m n $ notLeqToLeq n m) } maxLeqR n m = case n %:<= m of { STrue -> leqReflexive m (sMax n m) $ sym $ leqToMax n m Witness SFalse -> let mLEQn = notLeqToLeq n m in leqTrans m n (sMax n m) mLEQn (leqReflexive n (sMax n m) (sym $ geqToMax n m mLEQn)) } maxLeqL n m = leqTrans n (sMax m n) (sMax n m) (maxLeqR m n) (leqReflexive (sMax m n) (sMax n m) $ maxComm m n) maxLeast l n m lLEQn lLEQm = withSingI l $ withSingI n $ withSingI m $ withSingI (sMax n m) $ case n %:<= m of { STrue -> leqTrans (sMax n m) m l (leqReflexive sing sing $ leqToMax n m Witness) lLEQm SFalse -> let mLEQn = notLeqToLeq n m in leqTrans (sMax n m) n l (leqReflexive sing sing $ geqToMax n m mLEQn) lLEQn } lneqToLT n m nLNEm = succLeqToLT n m $ coerce (lneqSuccLeq n m) nLNEm ltToLneq n m nLTm = coerce (sym $ lneqSuccLeq n m) $ ltToSuccLeq n m nLTm lneqZero n = ltToLneq sZero (sSucc n) $ cmpZero n lneqSucc n = ltToLneq n (sSucc n) $ ltSucc n succLneqSucc n m = start (n %:< m) === (sSucc n %:<= m) `because` lneqSuccLeq n m === (sSucc (sSucc n) %:<= sSucc m) `because` leqSucc' (sSucc n) m === (sSucc n %:< sSucc m) `because` sym (lneqSuccLeq (sSucc n) (sSucc m)) lneqRightPredSucc n m nLNEQm = ltRightPredSucc n m $ lneqToLT n m nLNEQm lneqSuccStepL n m snLNEQm = coerce (sym $ lneqSuccLeq n m) $ leqSuccStepL (sSucc n) m $ coerce (lneqSuccLeq (sSucc n) m) snLNEQm lneqSuccStepR n m nLNEQm = coerce (sym $ lneqSuccLeq n (sSucc m)) $ leqSuccStepR (sSucc n) m $ coerce (lneqSuccLeq n m) nLNEQm plusStrictMonotone n m l k nLNm lLNk = coerce (sym $ lneqSuccLeq (n %:+ l) (m %:+ k)) $ flip coerceLeqL (m %:+ k) (plusSuccL n l) $ plusMonotone (sSucc n) m l k (coerce (lneqSuccLeq n m) nLNm) (leqTrans l (sSucc l) k (leqSuccStepR l l (leqRefl l)) $ coerce (lneqSuccLeq l k) lLNk) maxZeroL n = leqToMax sZero n (leqZero n) maxZeroR n = geqToMax n sZero (leqZero n) minZeroL n = leqToMin sZero n (leqZero n) minZeroR n = geqToMin n sZero (leqZero n) minusSucc n m mLEQn = case leqWitness m n mLEQn of { DiffNat _ k -> start (sSucc n %:- m) =~= sSucc (m %:+ k) %:- m === (m %:+ sSucc k) %:- m `because` minusCongL (sym $ plusSuccR m k) m === (sSucc k %:+ m) %:- m `because` minusCongL (plusComm m (sSucc k)) m === sSucc k `because` plusMinus (sSucc k) m === sSucc (k %:+ m %:- m) `because` succCong (sym $ plusMinus k m) === sSucc (m %:+ k %:- m) `because` succCong (minusCongL (plusComm k m) m) =~= sSucc (n %:- m) } lneqZeroAbsurd n leq = succLeqZeroAbsurd n (coerce (lneqSuccLeq n sZero) leq) 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 }
- Data.Type.Natural: data SSym0 (l_aVR8 :: TyFun Nat Nat)
+ Data.Type.Natural: data SSym0 (l_aVSX :: TyFun Nat Nat)
- Data.Type.Natural: type SSym1 (t_aVR7 :: Nat) = S t_aVR7
+ Data.Type.Natural: type SSym1 (t_aVSW :: Nat) = S t_aVSW
- Data.Type.Natural.Class.Order: class (SOrd nat, IsPeano nat) => PeanoOrder nat where ltToNeq a b aLTb aEQb = eliminate $ start SLT === sCompare a b `because` sym aLTb === SEQ `because` eqlCmpEQ a b aEQb leqNeqToLT a b aLEQb aNEQb = either (absurd . aNEQb) id $ leqToCmp a b aLEQb 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 } gtToLeq n m nGTm = ltToLeq m n $ start (sCompare m n) === sFlipOrdering (sCompare n m) `because` sym (flipCompare n m) === sFlipOrdering SGT `because` congFlipOrdering nGTm =~= SLT ltToSuccLeq n m nLTm = leqNeqToSuccLeq n m (ltToLeq n m nLTm) (ltToNeq n m nLTm) 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) leqToGT a b sbLEQa = start (sCompare a b) === sFlipOrdering (sCompare b a) `because` sym (flipCompare b a) === sFlipOrdering SLT `because` congFlipOrdering (leqToLT b a sbLEQa) =~= SGT cmpZero' n = case zeroOrSucc n of { IsZero -> Left $ eqlCmpEQ sZero n Refl IsSucc n' -> Right $ cmpZero n' } zeroNoLT n eql = case cmpZero' n of { Left cmp0nEQ -> eliminate $ start SGT =~= sFlipOrdering SLT === sFlipOrdering (sCompare n sZero) `because` congFlipOrdering (sym eql) === sCompare sZero n `because` flipCompare n sZero === SEQ `because` cmp0nEQ Right cmp0nLT -> eliminate $ start SGT =~= sFlipOrdering SLT === sFlipOrdering (sCompare n sZero) `because` congFlipOrdering (sym eql) === sCompare sZero n `because` flipCompare n sZero === SLT `because` cmp0nLT } 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 } cmpSucc n m = case sCompare 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 $ flipCompare 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 (sCompare n m) =~= SGT =~= sFlipOrdering SLT === sFlipOrdering (sCompare (sSucc m) (sSucc n)) `because` congFlipOrdering (sym pf) === sCompare (sSucc n) (sSucc m) `because` flipCompare (sSucc m) (sSucc n) } } ltSucc = proofLTSucc . induction base step where base :: LTSucc (Zero nat) base = LTSucc $ cmpZero (sZero :: Sing (Zero nat)) step :: Sing (n :: nat) -> LTSucc n -> LTSucc (Succ n) step n (LTSucc ih) = LTSucc $ start (sCompare (sSucc n) (sSucc (sSucc n))) === sCompare n (sSucc n) `because` sym (cmpSucc n (sSucc n)) === SLT `because` ih cmpSuccStepR = proofCmpSuccStepR . induction base step where base :: CmpSuccStepR (Zero nat) base = CmpSuccStepR $ \ m _ -> cmpZero m step :: Sing (n :: nat) -> CmpSuccStepR n -> CmpSuccStepR (Succ n) 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 (sCompare (sSucc n) (sSucc m)) =~= sCompare (sSucc n) (sSucc (sSucc m')) === sCompare n (sSucc m') `because` sym (cmpSucc n (sSucc m')) === SLT `because` ih m' nLTm' } ltSuccLToLT n m snLTm = case zeroOrSucc m of { IsZero -> absurd $ zeroNoLT (sSucc n) snLTm IsSucc m' -> let nLTm = cmpSucc n m' `trans` snLTm in start (sCompare n (sSucc m')) === SLT `because` cmpSuccStepR n m' nLTm } leqToLT n m snLEQm = case leqToCmp (sSucc n) m snLEQm of { Left Refl -> start (sCompare n m) =~= sCompare n (sSucc n) === SLT `because` ltSucc n Right nLTm -> ltSuccLToLT n m nLTm } leqZero sn = case zeroOrSucc sn of { IsZero -> leqRefl sn IsSucc pn -> ltToLeq sZero sn $ cmpZero pn } leqSucc n m nLEQm = case leqToCmp n m nLEQm of { Left Refl -> leqRefl (sSucc n) Right nLTm -> ltToLeq (sSucc n) (sSucc m) $ sym (cmpSucc n m) `trans` nLTm } fromLeqView (LeqZero n) = leqZero n fromLeqView (LeqSucc n m nLEQm) = leqSucc n m nLEQm leqViewRefl = proofLeqViewRefl . induction base step where base :: LeqViewRefl (Zero nat) base = LeqViewRefl $ LeqZero sZero step :: Sing (n :: nat) -> LeqViewRefl n -> LeqViewRefl (Succ n) step n (LeqViewRefl nLEQn) = LeqViewRefl $ LeqSucc n n (fromLeqView nLEQn) viewLeq n m nLEQm = case (zeroOrSucc n, leqToCmp n m nLEQm) of { (IsZero, _) -> LeqZero m (_, Left Refl) -> leqViewRefl n (IsSucc n', Right nLTm) -> let sm'EQm = ltRightPredSucc n m nLTm m' = sPred m n'LTm' = cmpSucc n' m' `trans` compareCongR n (sym sm'EQm) `trans` nLTm in coerce (sym sm'EQm) $ LeqSucc n' m' $ ltToLeq n' m' n'LTm' } leqWitness = leqWitPf . induction base step where base :: LeqWitPf (Zero nat) base = LeqWitPf $ \ sm _ -> coerce (plusZeroL sm) $ DiffNat sZero sm step :: Sing (n :: nat) -> LeqWitPf n -> LeqWitPf (Succ n) step (n :: Sing n) (LeqWitPf ih) = LeqWitPf $ \ m snLEQm -> case viewLeq (sSucc n) m snLEQm of { LeqZero _ -> absurd $ succNonCyclic n Refl LeqSucc (_ :: Sing n') pm nLEQpm -> succDiffNat n pm $ ih pm $ coerceLeqL (succInj Refl :: n' :~: n) pm nLEQpm } leqStep = leqStepPf . induction base step where base :: LeqStepPf (Zero nat) base = LeqStepPf $ \ k _ _ -> leqZero k step :: Sing (n :: nat) -> LeqStepPf n -> LeqStepPf (Succ n) 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 leqNeqToSuccLeq n m nLEQm nNEQm = case leqWitness n m nLEQm of { DiffNat _ k -> case zeroOrSucc k of { IsZero -> absurd $ nNEQm $ sym $ plusZeroR n IsSucc k' -> leqStep (sSucc n) m k' $ start (sSucc n %:+ k') === sSucc (n %:+ k') `because` plusSuccL n k' === n %:+ sSucc k' `because` sym (plusSuccR n k') =~= m } } leqRefl sn = leqStep sn sn sZero (plusZeroR sn) 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 } leqSuccStepL n m snLEQm = leqTrans n (sSucc n) m (leqSuccStepR n n $ leqRefl n) snLEQm leqReflexive n _ Refl = leqRefl n 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) } } 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 } 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 } leqZeroElim n nLE0 = case viewLeq n sZero nLE0 of { LeqZero _ -> Refl LeqSucc _ pZ _ -> absurd $ succNonCyclic pZ Refl } plusMonotoneL n m l leq = plusMonotone n m l l leq (leqRefl l) plusMonotoneR n m l leq = plusMonotone n n m l (leqRefl n) leq plusLeqL n m = leqStep n (n %:+ m) m Refl plusLeqR n m = leqStep m (n %:+ m) n $ plusComm m n 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 } plusCancelLeqL n m l nmLEQnl = plusCancelLeqR m l n $ coerceLeqL (plusComm n m) (l %:+ n) $ coerceLeqR (n %:+ m) (plusComm n l) nmLEQnl succLeqZeroAbsurd n leq = succNonCyclic n (leqZeroElim (sSucc n) leq) succLeqZeroAbsurd' n = case sSucc n %:<= sZero of { STrue -> absurd $ succLeqZeroAbsurd n Witness SFalse -> Refl } succLeqAbsurd n snLEQn = eliminate $ start SLT === sCompare n n `because` sym (succLeqToLT n n snLEQn) === SEQ `because` eqlCmpEQ n n Refl succLeqAbsurd' n = case sSucc n %:<= n of { STrue -> absurd $ succLeqAbsurd n Witness SFalse -> Refl } notLeqToLeq n m = case sCompare n m of { SLT -> eliminate $ ltToLeq n m Refl SEQ -> eliminate $ leqReflexive n m $ eqToRefl n m Refl SGT -> gtToLeq n m Refl } leqSucc' n m = case n %:<= m of { STrue -> case leqSucc n m Witness of { Witness -> Refl } SFalse -> case sSucc n %:<= sSucc m of { SFalse -> Refl STrue -> case viewLeq (sSucc n) (sSucc m) Witness of { LeqZero _ -> absurd $ succNonCyclic n Refl LeqSucc n' m' Witness -> eliminate $ start STrue =~= (n' %:<= m') === (n %:<= m) `because` sLeqCong (succInj' n' n Refl) (succInj' m' m Refl) =~= SFalse } } } leqToMin n m nLEQm = leqAntisymm (sMin n m) n (minLeqL n m) (minLargest n n m (leqRefl n) nLEQm) geqToMin n m mLEQn = leqAntisymm (sMin n m) m (minLeqR n m) (minLargest m n m mLEQn (leqRefl m)) minComm n m = case n %:<= m of { STrue -> start (sMin n m) === n `because` leqToMin n m Witness === sMin m n `because` sym (geqToMin m n Witness) SFalse -> start (sMin n m) === m `because` geqToMin n m (notLeqToLeq n m) === sMin m n `because` sym (leqToMin m n $ notLeqToLeq n m) } minLeqL n m = case n %:<= m of { STrue -> leqReflexive (sMin n m) n $ leqToMin n m Witness SFalse -> let mLEQn = notLeqToLeq n m in leqTrans (sMin n m) m n (leqReflexive (sMin n m) m (geqToMin n m mLEQn)) $ mLEQn } minLeqR n m = leqTrans (sMin n m) (sMin m n) m (leqReflexive (sMin n m) (sMin m n) $ minComm n m) (minLeqL m n) minLargest l n m lLEQn lLEQm = withSingI l $ withSingI n $ withSingI m $ withSingI (sMin n m) $ case n %:<= m of { STrue -> leqTrans l n (sMin n m) lLEQn $ leqReflexive sing sing $ sym $ leqToMin n m Witness SFalse -> let mLEQn = notLeqToLeq n m in leqTrans l m (sMin n m) lLEQm $ leqReflexive sing sing $ sym $ geqToMin n m mLEQn } leqToMax n m nLEQm = leqAntisymm (sMax n m) m (maxLeast m n m nLEQm (leqRefl m)) (maxLeqR n m) geqToMax n m mLEQn = leqAntisymm (sMax n m) n (maxLeast n n m (leqRefl n) mLEQn) (maxLeqL n m) maxComm n m = case n %:<= m of { STrue -> start (sMax n m) === m `because` leqToMax n m Witness === sMax m n `because` sym (geqToMax m n Witness) SFalse -> start (sMax n m) === n `because` geqToMax n m (notLeqToLeq n m) === sMax m n `because` sym (leqToMax m n $ notLeqToLeq n m) } maxLeqR n m = case n %:<= m of { STrue -> leqReflexive m (sMax n m) $ sym $ leqToMax n m Witness SFalse -> let mLEQn = notLeqToLeq n m in leqTrans m n (sMax n m) mLEQn (leqReflexive n (sMax n m) (sym $ geqToMax n m mLEQn)) } maxLeqL n m = leqTrans n (sMax m n) (sMax n m) (maxLeqR m n) (leqReflexive (sMax m n) (sMax n m) $ maxComm m n) maxLeast l n m lLEQn lLEQm = withSingI l $ withSingI n $ withSingI m $ withSingI (sMax n m) $ case n %:<= m of { STrue -> leqTrans (sMax n m) m l (leqReflexive sing sing $ leqToMax n m Witness) lLEQm SFalse -> let mLEQn = notLeqToLeq n m in leqTrans (sMax n m) n l (leqReflexive sing sing $ geqToMax n m mLEQn) lLEQn } lneqToLT n m nLNEm = succLeqToLT n m $ coerce (lneqSuccLeq n m) nLNEm ltToLneq n m nLTm = coerce (sym $ lneqSuccLeq n m) $ ltToSuccLeq n m nLTm lneqZero n = ltToLneq sZero (sSucc n) $ cmpZero n lneqSucc n = ltToLneq n (sSucc n) $ ltSucc n succLneqSucc n m = start (n %:< m) === (sSucc n %:<= m) `because` lneqSuccLeq n m === (sSucc (sSucc n) %:<= sSucc m) `because` leqSucc' (sSucc n) m === (sSucc n %:< sSucc m) `because` sym (lneqSuccLeq (sSucc n) (sSucc m)) lneqRightPredSucc n m nLNEQm = ltRightPredSucc n m $ lneqToLT n m nLNEQm lneqSuccStepL n m snLNEQm = coerce (sym $ lneqSuccLeq n m) $ leqSuccStepL (sSucc n) m $ coerce (lneqSuccLeq (sSucc n) m) snLNEQm lneqSuccStepR n m nLNEQm = coerce (sym $ lneqSuccLeq n (sSucc m)) $ leqSuccStepR (sSucc n) m $ coerce (lneqSuccLeq n m) nLNEQm plusStrictMonotone n m l k nLNm lLNk = coerce (sym $ lneqSuccLeq (n %:+ l) (m %:+ k)) $ flip coerceLeqL (m %:+ k) (plusSuccL n l) $ plusMonotone (sSucc n) m l k (coerce (lneqSuccLeq n m) nLNm) (leqTrans l (sSucc l) k (leqSuccStepR l l (leqRefl l)) $ coerce (lneqSuccLeq l k) lLNk) maxZeroL n = leqToMax sZero n (leqZero n) maxZeroR n = geqToMax n sZero (leqZero n) minZeroL n = leqToMin sZero n (leqZero n) minZeroR n = geqToMin n sZero (leqZero n) minusSucc n m mLEQn = case leqWitness m n mLEQn of { DiffNat _ k -> start (sSucc n %:- m) =~= sSucc (m %:+ k) %:- m === (m %:+ sSucc k) %:- m `because` minusCongL (sym $ plusSuccR m k) m === (sSucc k %:+ m) %:- m `because` minusCongL (plusComm m (sSucc k)) m === sSucc k `because` plusMinus (sSucc k) m === sSucc (k %:+ m %:- m) `because` succCong (sym $ plusMinus k m) === sSucc (m %:+ k %:- m) `because` succCong (minusCongL (plusComm k m) m) =~= sSucc (n %:- m) } lneqZeroAbsurd n leq = succLeqZeroAbsurd n (coerce (lneqSuccLeq n sZero) leq) 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 }
+ Data.Type.Natural.Class.Order: class (SOrd nat, IsPeano nat) => PeanoOrder nat where ltToNeq a b aLTb aEQb = eliminate $ start SLT === sCompare a b `because` sym aLTb === SEQ `because` eqlCmpEQ a b aEQb leqNeqToLT a b aLEQb aNEQb = either (absurd . aNEQb) id $ leqToCmp a b aLEQb 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 } gtToLeq n m nGTm = ltToLeq m n $ start (sCompare m n) === sFlipOrdering (sCompare n m) `because` sym (flipCompare n m) === sFlipOrdering SGT `because` congFlipOrdering nGTm =~= SLT ltToSuccLeq n m nLTm = leqNeqToSuccLeq n m (ltToLeq n m nLTm) (ltToNeq n m nLTm) 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) leqToGT a b sbLEQa = start (sCompare a b) === sFlipOrdering (sCompare b a) `because` sym (flipCompare b a) === sFlipOrdering SLT `because` congFlipOrdering (leqToLT b a sbLEQa) =~= SGT cmpZero' n = case zeroOrSucc n of { IsZero -> Left $ eqlCmpEQ sZero n Refl IsSucc n' -> Right $ cmpZero n' } zeroNoLT n eql = case cmpZero' n of { Left cmp0nEQ -> eliminate $ start SGT =~= sFlipOrdering SLT === sFlipOrdering (sCompare n sZero) `because` congFlipOrdering (sym eql) === sCompare sZero n `because` flipCompare n sZero === SEQ `because` cmp0nEQ Right cmp0nLT -> eliminate $ start SGT =~= sFlipOrdering SLT === sFlipOrdering (sCompare n sZero) `because` congFlipOrdering (sym eql) === sCompare sZero n `because` flipCompare n sZero === SLT `because` cmp0nLT } 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 } cmpSucc n m = case sCompare 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 $ flipCompare 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 (sCompare n m) =~= SGT =~= sFlipOrdering SLT === sFlipOrdering (sCompare (sSucc m) (sSucc n)) `because` congFlipOrdering (sym pf) === sCompare (sSucc n) (sSucc m) `because` flipCompare (sSucc m) (sSucc n) } } ltSucc = proofLTSucc . induction base step where base :: LTSucc (Zero nat) base = LTSucc $ cmpZero (sZero :: Sing (Zero nat)) step :: Sing (n :: nat) -> LTSucc n -> LTSucc (Succ n) step n (LTSucc ih) = LTSucc $ start (sCompare (sSucc n) (sSucc (sSucc n))) === sCompare n (sSucc n) `because` sym (cmpSucc n (sSucc n)) === SLT `because` ih cmpSuccStepR = proofCmpSuccStepR . induction base step where base :: CmpSuccStepR (Zero nat) base = CmpSuccStepR $ \ m _ -> cmpZero m step :: Sing (n :: nat) -> CmpSuccStepR n -> CmpSuccStepR (Succ n) 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 (sCompare (sSucc n) (sSucc m)) =~= sCompare (sSucc n) (sSucc (sSucc m')) === sCompare n (sSucc m') `because` sym (cmpSucc n (sSucc m')) === SLT `because` ih m' nLTm' } ltSuccLToLT n m snLTm = case zeroOrSucc m of { IsZero -> absurd $ zeroNoLT (sSucc n) snLTm IsSucc m' -> let nLTm = cmpSucc n m' `trans` snLTm in start (sCompare n (sSucc m')) === SLT `because` cmpSuccStepR n m' nLTm } leqToLT n m snLEQm = case leqToCmp (sSucc n) m snLEQm of { Left eql -> withRefl eql $ start (sCompare n m) =~= sCompare n (sSucc n) === SLT `because` ltSucc n Right nLTm -> ltSuccLToLT n m nLTm } leqZero sn = case zeroOrSucc sn of { IsZero -> leqRefl sn IsSucc pn -> ltToLeq sZero sn $ cmpZero pn } leqSucc n m nLEQm = case leqToCmp n m nLEQm of { Left eql -> withRefl eql $ leqRefl (sSucc n) Right nLTm -> ltToLeq (sSucc n) (sSucc m) $ sym (cmpSucc n m) `trans` nLTm } fromLeqView (LeqZero n) = leqZero n fromLeqView (LeqSucc n m nLEQm) = leqSucc n m nLEQm leqViewRefl = proofLeqViewRefl . induction base step where base :: LeqViewRefl (Zero nat) base = LeqViewRefl $ LeqZero sZero step :: Sing (n :: nat) -> LeqViewRefl n -> LeqViewRefl (Succ n) step n (LeqViewRefl nLEQn) = LeqViewRefl $ LeqSucc n n (fromLeqView nLEQn) viewLeq n m nLEQm = case (zeroOrSucc n, leqToCmp n m nLEQm) of { (IsZero, _) -> LeqZero m (_, Left Refl) -> leqViewRefl n (IsSucc n', Right nLTm) -> let sm'EQm = ltRightPredSucc n m nLTm m' = sPred m n'LTm' = cmpSucc n' m' `trans` compareCongR n (sym sm'EQm) `trans` nLTm in coerce (sym sm'EQm) $ LeqSucc n' m' $ ltToLeq n' m' n'LTm' } leqWitness = leqWitPf . induction base step where base :: LeqWitPf (Zero nat) base = LeqWitPf $ \ sm _ -> coerce (plusZeroL sm) $ DiffNat sZero sm step :: Sing (n :: nat) -> LeqWitPf n -> LeqWitPf (Succ n) step (n :: Sing n) (LeqWitPf ih) = LeqWitPf $ \ m snLEQm -> case viewLeq (sSucc n) m snLEQm of { LeqZero _ -> absurd $ succNonCyclic n Refl LeqSucc (_ :: Sing n') pm nLEQpm -> succDiffNat n pm $ ih pm $ coerceLeqL (succInj Refl :: n' :~: n) pm nLEQpm } leqStep = leqStepPf . induction base step where base :: LeqStepPf (Zero nat) base = LeqStepPf $ \ k _ _ -> leqZero k step :: Sing (n :: nat) -> LeqStepPf n -> LeqStepPf (Succ n) 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 leqNeqToSuccLeq n m nLEQm nNEQm = case leqWitness n m nLEQm of { DiffNat _ k -> case zeroOrSucc k of { IsZero -> absurd $ nNEQm $ sym $ plusZeroR n IsSucc k' -> leqStep (sSucc n) m k' $ start (sSucc n %:+ k') === sSucc (n %:+ k') `because` plusSuccL n k' === n %:+ sSucc k' `because` sym (plusSuccR n k') =~= m } } leqRefl sn = leqStep sn sn sZero (plusZeroR sn) 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 } leqSuccStepL n m snLEQm = leqTrans n (sSucc n) m (leqSuccStepR n n $ leqRefl n) snLEQm leqReflexive n _ Refl = leqRefl n 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) } } 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 } 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 } leqZeroElim n nLE0 = case viewLeq n sZero nLE0 of { LeqZero _ -> Refl LeqSucc _ pZ _ -> absurd $ succNonCyclic pZ Refl } plusMonotoneL n m l leq = plusMonotone n m l l leq (leqRefl l) plusMonotoneR n m l leq = plusMonotone n n m l (leqRefl n) leq plusLeqL n m = leqStep n (n %:+ m) m Refl plusLeqR n m = leqStep m (n %:+ m) n $ plusComm m n 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 } plusCancelLeqL n m l nmLEQnl = plusCancelLeqR m l n $ coerceLeqL (plusComm n m) (l %:+ n) $ coerceLeqR (n %:+ m) (plusComm n l) nmLEQnl succLeqZeroAbsurd n leq = succNonCyclic n (leqZeroElim (sSucc n) leq) succLeqZeroAbsurd' n = case sSucc n %:<= sZero of { STrue -> absurd $ succLeqZeroAbsurd n Witness SFalse -> Refl } succLeqAbsurd n snLEQn = eliminate $ start SLT === sCompare n n `because` sym (succLeqToLT n n snLEQn) === SEQ `because` eqlCmpEQ n n Refl succLeqAbsurd' n = case sSucc n %:<= n of { STrue -> absurd $ succLeqAbsurd n Witness SFalse -> Refl } notLeqToLeq n m = case sCompare n m of { SLT -> eliminate $ ltToLeq n m Refl SEQ -> eliminate $ leqReflexive n m $ eqToRefl n m Refl SGT -> gtToLeq n m Refl } leqSucc' n m = case n %:<= m of { STrue -> withWitness (leqSucc n m Witness) Refl SFalse -> case sSucc n %:<= sSucc m of { SFalse -> Refl STrue -> case viewLeq (sSucc n) (sSucc m) Witness of { LeqZero _ -> absurd $ succNonCyclic n Refl LeqSucc n' m' Witness -> eliminate $ start STrue =~= (n' %:<= m') === (n %:<= m) `because` sLeqCong (succInj' n' n Refl) (succInj' m' m Refl) =~= SFalse } } } leqToMin n m nLEQm = leqAntisymm (sMin n m) n (minLeqL n m) (minLargest n n m (leqRefl n) nLEQm) geqToMin n m mLEQn = leqAntisymm (sMin n m) m (minLeqR n m) (minLargest m n m mLEQn (leqRefl m)) minComm n m = case n %:<= m of { STrue -> start (sMin n m) === n `because` leqToMin n m Witness === sMin m n `because` sym (geqToMin m n Witness) SFalse -> start (sMin n m) === m `because` geqToMin n m (notLeqToLeq n m) === sMin m n `because` sym (leqToMin m n $ notLeqToLeq n m) } minLeqL n m = case n %:<= m of { STrue -> leqReflexive (sMin n m) n $ leqToMin n m Witness SFalse -> let mLEQn = notLeqToLeq n m in leqTrans (sMin n m) m n (leqReflexive (sMin n m) m (geqToMin n m mLEQn)) $ mLEQn } minLeqR n m = leqTrans (sMin n m) (sMin m n) m (leqReflexive (sMin n m) (sMin m n) $ minComm n m) (minLeqL m n) minLargest l n m lLEQn lLEQm = withSingI l $ withSingI n $ withSingI m $ withSingI (sMin n m) $ case n %:<= m of { STrue -> leqTrans l n (sMin n m) lLEQn $ leqReflexive sing sing $ sym $ leqToMin n m Witness SFalse -> let mLEQn = notLeqToLeq n m in leqTrans l m (sMin n m) lLEQm $ leqReflexive sing sing $ sym $ geqToMin n m mLEQn } leqToMax n m nLEQm = leqAntisymm (sMax n m) m (maxLeast m n m nLEQm (leqRefl m)) (maxLeqR n m) geqToMax n m mLEQn = leqAntisymm (sMax n m) n (maxLeast n n m (leqRefl n) mLEQn) (maxLeqL n m) maxComm n m = case n %:<= m of { STrue -> start (sMax n m) === m `because` leqToMax n m Witness === sMax m n `because` sym (geqToMax m n Witness) SFalse -> start (sMax n m) === n `because` geqToMax n m (notLeqToLeq n m) === sMax m n `because` sym (leqToMax m n $ notLeqToLeq n m) } maxLeqR n m = case n %:<= m of { STrue -> leqReflexive m (sMax n m) $ sym $ leqToMax n m Witness SFalse -> let mLEQn = notLeqToLeq n m in leqTrans m n (sMax n m) mLEQn (leqReflexive n (sMax n m) (sym $ geqToMax n m mLEQn)) } maxLeqL n m = leqTrans n (sMax m n) (sMax n m) (maxLeqR m n) (leqReflexive (sMax m n) (sMax n m) $ maxComm m n) maxLeast l n m lLEQn lLEQm = withSingI l $ withSingI n $ withSingI m $ withSingI (sMax n m) $ case n %:<= m of { STrue -> leqTrans (sMax n m) m l (leqReflexive sing sing $ leqToMax n m Witness) lLEQm SFalse -> let mLEQn = notLeqToLeq n m in leqTrans (sMax n m) n l (leqReflexive sing sing $ geqToMax n m mLEQn) lLEQn } lneqToLT n m nLNEm = succLeqToLT n m $ coerce (lneqSuccLeq n m) nLNEm ltToLneq n m nLTm = coerce (sym $ lneqSuccLeq n m) $ ltToSuccLeq n m nLTm lneqZero n = ltToLneq sZero (sSucc n) $ cmpZero n lneqSucc n = ltToLneq n (sSucc n) $ ltSucc n succLneqSucc n m = start (n %:< m) === (sSucc n %:<= m) `because` lneqSuccLeq n m === (sSucc (sSucc n) %:<= sSucc m) `because` leqSucc' (sSucc n) m === (sSucc n %:< sSucc m) `because` sym (lneqSuccLeq (sSucc n) (sSucc m)) lneqRightPredSucc n m nLNEQm = ltRightPredSucc n m $ lneqToLT n m nLNEQm lneqSuccStepL n m snLNEQm = coerce (sym $ lneqSuccLeq n m) $ leqSuccStepL (sSucc n) m $ coerce (lneqSuccLeq (sSucc n) m) snLNEQm lneqSuccStepR n m nLNEQm = coerce (sym $ lneqSuccLeq n (sSucc m)) $ leqSuccStepR (sSucc n) m $ coerce (lneqSuccLeq n m) nLNEQm plusStrictMonotone n m l k nLNm lLNk = coerce (sym $ lneqSuccLeq (n %:+ l) (m %:+ k)) $ flip coerceLeqL (m %:+ k) (plusSuccL n l) $ plusMonotone (sSucc n) m l k (coerce (lneqSuccLeq n m) nLNm) (leqTrans l (sSucc l) k (leqSuccStepR l l (leqRefl l)) $ coerce (lneqSuccLeq l k) lLNk) maxZeroL n = leqToMax sZero n (leqZero n) maxZeroR n = geqToMax n sZero (leqZero n) minZeroL n = leqToMin sZero n (leqZero n) minZeroR n = geqToMin n sZero (leqZero n) minusSucc n m mLEQn = case leqWitness m n mLEQn of { DiffNat _ k -> start (sSucc n %:- m) =~= sSucc (m %:+ k) %:- m === (m %:+ sSucc k) %:- m `because` minusCongL (sym $ plusSuccR m k) m === (sSucc k %:+ m) %:- m `because` minusCongL (plusComm m (sSucc k)) m === sSucc k `because` plusMinus (sSucc k) m === sSucc (k %:+ m %:- m) `because` succCong (sym $ plusMinus k m) === sSucc (m %:+ k %:- m) `because` succCong (minusCongL (plusComm k m) m) =~= sSucc (n %:- m) } lneqZeroAbsurd n leq = succLeqZeroAbsurd n (coerce (lneqSuccLeq n sZero) leq) 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 }
- Data.Type.Natural.Class.Order: sFlipOrdering :: forall (t_azZ5 :: Ordering). Sing t_azZ5 -> Sing (Apply FlipOrderingSym0 t_azZ5 :: Ordering)
+ Data.Type.Natural.Class.Order: sFlipOrdering :: forall (t_azZ6 :: Ordering). Sing t_azZ6 -> Sing (Apply FlipOrderingSym0 t_azZ6 :: Ordering)
Files
- Data/Type/Natural.hs +20/−35
- Data/Type/Natural/Builtin.hs +16/−18
- Data/Type/Natural/Class/Order.hs +3/−5
- Data/Type/Ordinal.hs +12/−14
- type-natural.cabal +2/−2
Data/Type/Natural.hs view
@@ -151,9 +151,7 @@ reflToSEqual :: SNat n -> SNat m -> n :~: m -> IsTrue (n :== m) reflToSEqual SZ _ Refl = Witness-reflToSEqual (SS n) (SS m) Refl =- case reflToSEqual n m Refl of- Witness -> Witness+reflToSEqual (SS n) (SS m) Refl = reflToSEqual n m Refl reflToSEqual (SS _) SZ refl = case refl of {} sequalToRefl :: SNat n -> SNat m -> IsTrue (n :== m) -> n :~: m@@ -170,35 +168,27 @@ sequalSym SZ SZ = Refl sequalSym SZ (SS _) = Refl sequalSym (SS _) SZ = Refl-sequalSym (SS n) (SS m) =- case sequalSym n m of- Refl -> Refl+sequalSym (SS n) (SS m) = sequalSym n m sleqFlip :: SNat n -> SNat m -> (n :~: m -> Void) -> (m :<= n) :~: Not (n :<= m) sleqFlip SZ SZ neq = absurd $ neq Refl sleqFlip SZ (SS _) _ = Refl sleqFlip (SS _) SZ _ = Refl-sleqFlip (SS n) (SS m) neq =- case sleqFlip n m (neq . succCong) of- Refl -> Refl+sleqFlip (SS n) (SS m) neq = sleqFlip n m (neq . succCong) sLeqReflexive :: SNat n -> SNat m -> IsTrue (n :== m) -> IsTrue (n :<= m) sLeqReflexive SZ _ Witness = Witness-sLeqReflexive (SS n) (SS m) Witness =- case sLeqReflexive n m Witness of- Witness -> Witness+sLeqReflexive (SS n) (SS m) Witness = sLeqReflexive n m Witness sLeqReflexive (SS _) SZ witness = case witness of {} nonSLeqToLT :: (n :<= m) ~ 'False => SNat n -> SNat m -> Compare m n :~: 'LT-nonSLeqToLT n m =- case sequalSym n m of- Refl -> - case m %:== n of- STrue -> case sLeqReflexive n m Witness of {}- SFalse ->- case m %:<= n of- STrue -> Refl- SFalse -> case sleqFlip n m $ snequalToNoRefl n m Witness of {}+nonSLeqToLT n m = withRefl (sequalSym n m) $+ case m %:== n of+ STrue -> case sLeqReflexive n m Witness of {}+ SFalse ->+ case m %:<= n of+ STrue -> Refl+ SFalse -> case sleqFlip n m $ snequalToNoRefl n m Witness of {} instance PeanoOrder Nat where {-# SPECIALISE instance PeanoOrder Nat #-}@@ -229,20 +219,15 @@ flipCompare n m = case n %:== m of- STrue -> case sequalSym n m of- Refl -> Refl- SFalse ->- case sequalSym n m of- Refl -> - case n %:<= m of- STrue ->- case sleqFlip n m (snequalToNoRefl n m Witness) of- Refl -> case m %:<= n of- SFalse -> Refl- SFalse ->- case sleqFlip n m (snequalToNoRefl n m Witness) of- Refl -> case m %:<= n of- STrue -> Refl+ STrue -> withRefl (sequalSym n m) Refl+ SFalse -> withRefl (sequalSym n m) $+ case n %:<= m of+ STrue -> withRefl (sleqFlip n m (snequalToNoRefl n m Witness)) $+ case m %:<= n of+ SFalse -> Refl+ SFalse -> withRefl (sleqFlip n m (snequalToNoRefl n m Witness)) $+ case m %:<= n of+ STrue -> Refl minLeqL SZ SZ = Witness minLeqL SZ (SS _) = Witness
Data/Type/Natural/Builtin.hs view
@@ -46,10 +46,10 @@ import Data.Void (Void) import GHC.TypeLits (type (+), type (<=), type (<=?)) import qualified GHC.TypeLits as TL-import Proof.Equational (coerce)+import Proof.Equational (coerce, withRefl) import Proof.Equational (start, sym, (===), (=~=)) import Proof.Equational (because)-import Proof.Propositional (Empty (..), IsTrue (..))+import Proof.Propositional (Empty (..), IsTrue (..), withWitness) import Unsafe.Coerce (unsafeCoerce) -- | Type synonym for @'PN.Nat'@ to avoid confusion with built-in @'TL.Nat'@.@@ -66,7 +66,7 @@ viewNat :: Sing (n :: TL.Nat) -> ZeroOrSucc n viewNat n = case n %~ (sing :: Sing 0) of- Proved Refl -> IsZero+ Proved _ -> IsZero Disproved _ -> IsSucc (sPred n) sFromPeano :: Sing n -> Sing (FromPeano n)@@ -88,7 +88,7 @@ sToPeano :: Sing n -> Sing (ToPeano n) sToPeano sn = case sn %~ (sing :: Sing 0) of- Proved Refl -> SZ+ Proved eq -> withRefl eq SZ Disproved _pf -> coerce (sym (toPeanoSuccCong (sPred sn))) (SS (sToPeano (sPred sn))) -- litSuccInjective :: forall (n :: TL.Nat) (m :: TL.Nat).@@ -258,9 +258,9 @@ => Sing n -> Sing m -> ((ToPeano n) :<= (ToPeano m)) :~: 'True toPeanoMonotone sn sm = case sn %~ (sing :: Sing 0) of- Proved Refl -> Refl+ Proved eql -> withRefl eql Refl Disproved nPos -> case sm %~ (sing :: Sing 0) of- Proved Refl -> absurd $ nPos $ natLeqZero sn+ Proved _ -> absurd $ nPos $ natLeqZero sn Disproved mPos -> let pn = sPred sn pm = sPred sm@@ -367,25 +367,25 @@ leqToMax _ _ Witness = Refl geqToMax n m mLEQn = case leqToCmp m n mLEQn of- Left Refl -> Refl+ Left eql -> withRefl eql Refl Right mLTn -> maxCompareFlip n m mLTn geqToMin n m mLEQn = case leqToCmp m n mLEQn of- Left Refl -> Refl+ Left eql -> withRefl eql Refl Right mLTn -> minCompareFlip n m mLTn lneqReversed n m =- case flipCompare n m of- Refl -> case sCompare n m of+ withRefl (flipCompare n m) $+ case sCompare n m of SEQ -> Refl SLT -> Refl SGT -> Refl leqReversed n m =- case flipCompare n m of- Refl -> case sCompare n m of+ withRefl (flipCompare n m) $+ case sCompare n m of SEQ -> Refl SLT -> Refl SGT -> Refl@@ -397,12 +397,10 @@ =~= SFalse === (sSucc n %:<= n) `because` sym (succLeqAbsurd' n) === (sSucc n %:<= m) `because` sLeqCongR (sSucc n) (eqToRefl n m Refl)- SLT ->- case ltToSuccLeq n m Refl of- Witness ->- start (n %:< m)- =~= STrue- =~= (sSucc n %:<= m)+ SLT -> withWitness (ltToSuccLeq n m Refl) $+ start (n %:< m)+ =~= STrue+ =~= (sSucc n %:<= m) SGT -> case sSucc n %:<= m of SFalse -> Refl
Data/Type/Natural/Class/Order.hs view
@@ -249,7 +249,7 @@ -> Compare a b :~: 'LT leqToLT n m snLEQm = case leqToCmp (sSucc n) m snLEQm of- Left Refl ->+ Left eql -> withRefl eql $ start (sCompare n m) =~= sCompare n (sSucc n) === SLT `because` ltSucc n@@ -264,7 +264,7 @@ leqSucc :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> IsTrue (Succ n :<= Succ m) leqSucc n m nLEQm = case leqToCmp n m nLEQm of- Left Refl -> leqRefl (sSucc n)+ Left eql -> withRefl eql $ leqRefl (sSucc n) Right nLTm -> ltToLeq (sSucc n) (sSucc m) $ sym (cmpSucc n m) `trans` nLTm fromLeqView :: LeqView (n :: nat) m -> IsTrue (n :<= m)@@ -470,9 +470,7 @@ leqSucc' :: Sing (n :: nat) -> Sing m -> (n :<= m) :~: (Succ n :<= Succ m) leqSucc' n m = case n %:<= m of- STrue ->- case leqSucc n m Witness of- Witness -> Refl+ STrue -> withWitness (leqSucc n m Witness) Refl SFalse -> case sSucc n %:<= sSucc m of SFalse -> Refl
Data/Type/Ordinal.hs view
@@ -53,8 +53,8 @@ fromOLt :: forall nat n m. (PeanoOrder nat, (Succ n :< Succ m) ~ 'True, SingI m) => Sing (n :: nat) -> Ordinal m fromOLt n =- case coerce (sym $ succLneqSucc n (sing :: Sing m)) Witness of- Witness -> OLt n+ withRefl (sym $ succLneqSucc n (sing :: Sing m)) $+ OLt n -- | Pattern synonym representing the 0-th ordinal. pattern OZ :: forall nat (n :: nat). IsPeano nat@@ -135,32 +135,31 @@ enumOrdinal :: (PeanoOrder nat, SingI n) => Sing (n :: nat) -> [Ordinal n] enumOrdinal (Succ n) = withSingI n $- case lneqZero n of- Witness ->+ withWitness (lneqZero n) $ OLt sZero : map succOrd (enumOrdinal n) enumOrdinal _ = [] succOrd :: forall (n :: nat). (PeanoOrder nat, SingI n) => Ordinal n -> Ordinal (Succ n) succOrd (OLt n) =- case succLneqSucc n (sing :: Sing n) of- Refl -> OLt (sSucc n)+ withRefl (succLneqSucc n (sing :: Sing n)) $+ OLt (sSucc n) {-# INLINE succOrd #-} instance SingI n => Bounded (Ordinal ('PN.S n)) where minBound = OLt PN.SZ maxBound =- case leqRefl (sing :: Sing n) of- Witness -> sNatToOrd (sing :: Sing n)+ withWitness (leqRefl (sing :: Sing n)) $+ sNatToOrd (sing :: Sing n) instance (SingI m, SingI n, n ~ (m + 1)) => Bounded (Ordinal n) where minBound =- case lneqZero (sing :: Sing m) of- Witness -> OLt (sing :: Sing 0)+ withWitness (lneqZero (sing :: Sing m)) $+ OLt (sing :: Sing 0) {-# INLINE minBound #-} maxBound =- case lneqSucc (sing :: Sing m) of- Witness -> sNatToOrd (sing :: Sing m)+ withWitness (lneqSucc (sing :: Sing m)) $+ sNatToOrd (sing :: Sing m) {-# INLINE maxBound #-} @@ -232,8 +231,7 @@ => Ordinal n -> Ordinal m -> Ordinal (n :+ m) OLt k @+ OLt l = let (n, m) = (n :: Sing n, m :: Sing m)- in case plusStrictMonotone k n l m Witness Witness of- Witness -> OLt $ k %:+ l+ in withWitness (plusStrictMonotone k n l m Witness Witness) $ OLt $ k %:+ l -- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value. --
type-natural.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: type-natural-version: 0.6.1.0+version: 0.6.1.1 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.1 && < 1+ , equational-reasoning >= 0.4.1.1 && < 1 , monomorphic >= 0.0.3 , template-haskell >= 2.8 && < 3 , constraints >= 0.3 && < 0.9