module Quox.NatExtra import public Data.Nat import public Data.Nat.Properties import public Data.Nat.Division import Data.DPair import Data.SnocList import Data.Vect %default total public export data LTE' : Nat -> Nat -> Type where LTERefl : LTE' n n LTESuccR : LTE' m n -> LTE' m (S n) %builtin Natural LTE' public export %hint lteZero' : {n : Nat} -> LTE' 0 n lteZero' {n = 0} = LTERefl lteZero' {n = S n} = LTESuccR lteZero' public export %hint lteSucc' : LTE' m n -> LTE' (S m) (S n) lteSucc' LTERefl = LTERefl lteSucc' (LTESuccR p) = LTESuccR $ lteSucc' p public export fromLte : {n : Nat} -> LTE m n -> LTE' m n fromLte LTEZero = lteZero' fromLte (LTESucc p) = lteSucc' $ fromLte p public export toLte : {n : Nat} -> m `LTE'` n -> m `LTE` n toLte LTERefl = reflexive toLte (LTESuccR p) = lteSuccRight (toLte p) private 0 baseNZ : n `GTE` 2 => NonZero n baseNZ @{LTESucc _} = SIsNonZero parameters {base : Nat} {auto 0 _ : base `GTE` 2} (chars : Vect base Char) private showAtBase' : List Char -> Nat -> List Char showAtBase' acc 0 = acc showAtBase' acc k = let dig = natToFinLT (modNatNZ k base baseNZ) @{boundModNatNZ {}} in showAtBase' (index dig chars :: acc) (assert_smaller k $ divNatNZ k base baseNZ) export showAtBase : Nat -> String showAtBase = pack . showAtBase' [] export showHex : Nat -> String showHex = showAtBase $ fromList $ unpack "0123456789ABCDEF" n2i = natToInteger i2n = fromInteger {ty = Nat} private partial %inline divNatViaInteger : (m, n : Nat) -> Nat divNatViaInteger m n = i2n $ n2i m `div` n2i n %transform "divNat" divNat = divNatViaInteger private %inline divNatViaIntegerNZ : (m, n : Nat) -> (0 _ : NonZero n) -> Nat divNatViaIntegerNZ m n _ = assert_total divNatViaInteger m n %transform "divNatNZ" divNatNZ = divNatViaIntegerNZ private partial %inline modNatViaInteger : (m, n : Nat) -> Nat modNatViaInteger m n = i2n $ n2i m `mod` n2i n %transform "modNat" modNat = modNatViaInteger private %inline modNatViaIntegerNZ : (m, n : Nat) -> (0 _ : NonZero n) -> Nat modNatViaIntegerNZ m n _ = assert_total modNatViaInteger m n %transform "modNatNZ" modNatNZ = modNatViaIntegerNZ public export data ViewLsb : Nat -> Type where Lsb0 : (n : Nat) -> (0 eq : n' = 2 * n) -> ViewLsb n' Lsb1 : (n : Nat) -> (0 eq : n' = S (2 * n)) -> ViewLsb n' %name ViewLsb p, q public export data IsLsb0 : ViewLsb n -> Type where ItIsLsb0 : IsLsb0 (Lsb0 n eq) public export data IsLsb1 : ViewLsb n -> Type where ItIsLsb1 : IsLsb1 (Lsb1 n eq) export 0 lsbMutex : n = (2 * a) -> n = S (2 * b) -> Void lsbMutex ev od {n = 0} impossible lsbMutex ev od {n = 1} {a = S a} {b = 0} = let ev = injective ev in let s = sym $ plusSuccRightSucc a (a + 0) in absurd $ trans ev s lsbMutex ev od {n = S (S n)} {a = S a} {b = S b} = let ev = injective $ trans (injective ev) (sym $ plusSuccRightSucc a (a + 0)) in let od = trans (injective $ injective od) (sym $ plusSuccRightSucc b (b + 0)) in lsbMutex ev od public export %hint doubleIsLsb0 : (p : ViewLsb (2 * n)) -> IsLsb0 p doubleIsLsb0 (Lsb0 k eq) = ItIsLsb0 doubleIsLsb0 (Lsb1 k eq) = void $ absurd $ lsbMutex Refl eq public export %hint sDoubleIsLsb1 : (p : ViewLsb (S (2 * n))) -> IsLsb1 p sDoubleIsLsb1 (Lsb1 k eq) = ItIsLsb1 sDoubleIsLsb1 (Lsb0 k eq) = void $ absurd $ lsbMutex Refl (sym eq) export fromLsb0 : (p : ViewLsb n) -> (0 _ : IsLsb0 p) => Subset Nat (\n' => n = 2 * n') fromLsb0 (Lsb0 n' eq) @{ItIsLsb0} = Element n' eq export fromLsb1 : (p : ViewLsb n) -> (0 _ : IsLsb1 p) => Subset Nat (\n' => n = S (2 * n')) fromLsb1 (Lsb1 n' eq) @{ItIsLsb1} = Element n' eq private viewLsb' : (m, d : Nat) -> (0 _ : m `LT` 2) -> ViewLsb (m + 2 * d) viewLsb' 0 d p = Lsb0 d Refl viewLsb' 1 d p = Lsb1 d Refl viewLsb' (S (S _)) _ (LTESucc p) = void $ absurd p export viewLsb : (n : Nat) -> ViewLsb n viewLsb n = let 0 nz : NonZero 2 = %search in rewrite DivisionTheorem n 2 nz nz in rewrite multCommutative (divNatNZ n 2 nz) 2 in viewLsb' (modNatNZ n 2 nz) (divNatNZ n 2 nz) (boundModNatNZ n 2 nz) export 0 doubleInj : {m, n : Nat} -> 2 * m = 2 * n -> m = n doubleInj eq = multRightCancel m n 2 %search $ trans (multCommutative m 2) $ trans eq (multCommutative 2 n) export 0 sDoubleInj : {m, n : Nat} -> S (2 * m) = S (2 * n) -> m = n sDoubleInj eq = doubleInj $ injective eq export 0 lsbOdd : (n : Nat) -> (eq ** viewLsb (S (2 * n)) = Lsb1 n eq) lsbOdd n with (viewLsb (S (2 * n))) _ | Lsb0 _ eq = void $ absurd $ lsbMutex Refl (sym eq) _ | Lsb1 n' eq with (sDoubleInj eq) lsbOdd n | (Lsb1 n eq) | Refl = (eq ** Refl) export 0 lsbEven : (n : Nat) -> (eq ** viewLsb (2 * n) = Lsb0 n eq) lsbEven n with (viewLsb (2 * n)) _ | Lsb1 _ eq = void $ absurd $ lsbMutex Refl eq _ | Lsb0 n' eq with (doubleInj eq) lsbEven n | Lsb0 n eq | Refl = (eq ** Refl)