idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-17 16:21:46 +03:00
Code Issues Projects Releases Wiki Activity
1d96dd2bd7
Idris2/libs/contrib/Data/Nat/Division.idr
Stefan Hoeck fb08004041
removed trailing whitespace (#955)
2021-01-21 11:33:03 +00:00

383 lines
17 KiB
Idris
Raw Blame History

||| Division theorem for (type-level) natural number division
module Data.Nat.Division
import Syntax.WithProof
import Syntax.PreorderReasoning
import Syntax.PreorderReasoning.Generic
import Data.Nat
import Data.Nat.Equational
import Data.Nat.Order
import Data.Nat.Order.Strict
import Data.Nat.Order.Properties
import Decidable.Order
import Decidable.Order.Strict
import Data.Nat.Properties
%default total
-- Division theorem --------------------
-- This is disgusting, but will do for now
||| Show that, if we have enough fuel, we have enough fuel for the
||| recursive call in `div'` and `mod'`.
fuelLemma : (numer, predDenom, fuel : Nat)
-> (enough : numer `LTE` (S fuel))
-> (recurse : Data.Nat.lte numer predDenom = False)
-> (numer `minus` (S predDenom)) `LTE` fuel
fuelLemma numer predDenom fuel enough recurse =
let denom : Nat
denom = S predDenom
numer' : Nat
numer' = numer `minus` denom
-- a bunch of inequational reasoning to show we have enough fuel
-- on the recursive call
denom_lte_numer : denom `LTE` numer
denom_lte_numer = Properties.notlteIsLT numer predDenom recurse
numer'_lt_numer : numer' `LT` numer
numer'_lt_numer = (minusPosLT denom numer
(LTESucc LTEZero)
denom_lte_numer)
succenough : S numer' `LTE` S fuel
succenough = transitive (S numer') numer (S fuel)
numer'_lt_numer
enough
in fromLteSucc succenough
-- equivalence between the duplicate definitions in Data.Nar ---
-- Internally, we use the two component definitions of divmod'
div'' : (fuel, numer, denom : Nat) -> Nat
div'' fuel numer denom = fst (divmod' fuel numer denom)
mod'' : (fuel, numer, denom : Nat) -> Nat
mod'' fuel numer denom = snd (divmod' fuel numer denom)
divmod'_eq_div'_mod' : (fuel, numer, denom : Nat)
-> (divmod' fuel numer denom) = (div' fuel numer denom, mod' fuel numer denom)
divmod'_eq_div'_mod' 0 numer denom = Refl
divmod'_eq_div'_mod' (S fuel) numer denom with (Data.Nat.lte numer denom)
divmod'_eq_div'_mod' (S fuel) numer denom | True = Refl
divmod'_eq_div'_mod' (S fuel) numer denom | False =
rewrite divmod'_eq_div'_mod' fuel (numer `minus` (S denom)) denom in
Refl
div''_eq_div' : (fuel, numer, denom : Nat)
-> div'' fuel numer denom = div' fuel numer denom
div''_eq_div' fuel numer denom = cong fst $
divmod'_eq_div'_mod' fuel numer denom
mod''_eq_mod' : (fuel, numer, denom : Nat)
-> mod'' fuel numer denom = mod' fuel numer denom
mod''_eq_mod' fuel numer denom = cong snd $
divmod'_eq_div'_mod' fuel numer denom
export
divmodNatNZeqDivMod : (numer, denom : Nat) -> (prf1, prf2, prf3 : Not (denom = 0))
-> (divmodNatNZ numer denom prf1) = (divNatNZ numer denom prf2, modNatNZ numer denom prf3)
divmodNatNZeqDivMod numer 0 prf1 prf2 prf3 = void $ prf1 Refl
divmodNatNZeqDivMod numer (S denom) prf1 prf2 prf3 = divmod'_eq_div'_mod' numer numer denom
export
fstDivmodNatNZeqDiv : (numer, denom : Nat) -> (prf1, prf2 : Not (denom = 0))
-> (fst $ divmodNatNZ numer denom prf1) = divNatNZ numer denom prf2
fstDivmodNatNZeqDiv numer denom prf1 prf2 =
rewrite divmodNatNZeqDivMod numer denom prf1 prf2 prf2 in
Refl
export
sndDivmodNatNZeqMod : (numer, denom : Nat) -> (prf1, prf2 : Not (denom = 0))
-> (snd $ divmodNatNZ numer denom prf1) = modNatNZ numer denom prf2
sndDivmodNatNZeqMod numer denom prf1 prf2 =
rewrite divmodNatNZeqDivMod numer denom prf1 prf2 prf2 in
Refl
-----------------------------------------------------------------------------
bound_mod'' : (fuel, numer, predDenom : Nat) -> (numer `LTE` fuel)
-> (mod'' fuel numer predDenom) `LTE` predDenom
bound_mod'' 0 0 predDenom LTEZero = LTEZero
bound_mod'' (S fuel) numer predDenom enough = case @@(Data.Nat.lte numer predDenom) of
(True ** numer_lte_predn) => rewrite numer_lte_predn in
Properties.lteIsLTE _ _ numer_lte_predn
(False ** numer_gte_n ) => rewrite numer_gte_n in
bound_mod'' fuel (numer `minus` (S predDenom)) predDenom
(fuelLemma numer predDenom fuel enough numer_gte_n)
export
boundModNatNZ : (numer, denom : Nat) -> (denom_nz : Not (denom = 0))
-> (modNatNZ numer denom denom_nz) `LT` denom
boundModNatNZ numer 0 denom_nz = void $ denom_nz Refl
boundModNatNZ numer (S predDenom) denom_nz = LTESucc $
rewrite sym $ mod''_eq_mod' numer numer predDenom in
bound_mod'' numer numer predDenom (reflexive numer)
divisionTheorem' : (numer, predDenom : Nat)
-> (fuel : Nat) -> (enough : numer `LTE` fuel)
-> numer = (mod'' fuel numer predDenom) + (div'' fuel numer predDenom) * (S predDenom)
divisionTheorem' 0 predDenom 0 LTEZero = Refl
divisionTheorem' numer predDenom (S fuel) enough with (@@(Data.Nat.lte numer predDenom))
divisionTheorem' numer predDenom (S fuel) enough | (True ** prf)
= rewrite prf in
rewrite plusZeroRightNeutral numer in Refl
divisionTheorem' numer predDenom (S fuel) enough | (False ** prf)
= rewrite prf in
let denom : Nat
denom = S predDenom
numer' : Nat
numer' = numer `minus` denom
denom_lte_numer : denom `LTE` numer
denom_lte_numer = Properties.notlteIsLT numer predDenom prf
enough' : numer' `LTE` fuel
enough' = fuelLemma numer predDenom fuel enough prf
inductionHypothesis : (numer'
= (mod'' fuel numer' predDenom) + (div'' fuel numer' predDenom) * denom)
inductionHypothesis = divisionTheorem' numer' predDenom fuel enough'
in sym $ Calc $
|~ (mod'' fuel numer' predDenom) + (denom + (div'' fuel numer' predDenom) * denom)
~~ (mod'' fuel numer' predDenom) + ((div'' fuel numer' predDenom) * denom + denom)
...(cong ((mod'' fuel numer' predDenom) +) $ plusCommutative
denom
((div'' fuel numer' predDenom) * denom))
~~((mod'' fuel numer' predDenom) + (div'' fuel numer' predDenom) * denom) + denom
...(plusAssociative
(mod'' fuel numer' predDenom)
((div'' fuel numer' predDenom) * denom)
denom)
~~ numer' + denom ...(cong (+ denom) $ sym inductionHypothesis)
~~ numer ...(plusMinusLte denom numer denom_lte_numer)
export
DivisionTheoremDivMod : (numer, denom : Nat) -> (prf : Not (denom = Z))
-> numer = snd ( divmodNatNZ numer denom prf)
+ (fst $ divmodNatNZ numer denom prf)*denom
DivisionTheoremDivMod numer 0 prf = void (prf Refl)
DivisionTheoremDivMod numer (S predDenom) prf
= divisionTheorem' numer predDenom numer (reflexive numer)
export
DivisionTheorem : (numer, denom : Nat) -> (prf1, prf2 : Not (denom = Z))
-> numer = (modNatNZ numer denom prf1) + (divNatNZ numer denom prf2)*denom
DivisionTheorem numer denom prf1 prf2
= rewrite sym $ fstDivmodNatNZeqDiv numer denom prf1 prf2 in
rewrite sym $ sndDivmodNatNZeqMod numer denom prf1 prf1 in
DivisionTheoremDivMod numer denom prf1
divmodZeroZero : (denom, fuel : Nat)
-> divmod' fuel 0 denom = (0,0)
divmodZeroZero denom 0 = Refl
divmodZeroZero denom (S fuel) = Refl
modZeroZero : (denom, fuel : Nat)
-> mod'' fuel 0 denom = 0
modZeroZero denom fuel = rewrite divmodZeroZero denom fuel in Refl
divZeroZero : (denom, fuel : Nat)
-> div'' fuel 0 denom = 0
divZeroZero denom fuel = rewrite divmodZeroZero denom fuel in Refl
divmodFuelLemma : (numer, denom, fuel1, fuel2 : Nat)
-> (enough1 : fuel1 `GTE` numer)
-> (enough2 : fuel2 `GTE` numer)
-> divmod' fuel1 numer denom = divmod' fuel2 numer denom
divmodFuelLemma 0 denom 0 fuel2 LTEZero enough2 = rewrite divmodZeroZero denom fuel2 in
Refl
divmodFuelLemma 0 denom (S fuel1) 0 enough1 LTEZero = Refl
divmodFuelLemma numer denom (S fuel1) (S fuel2) enough1 enough2 with (@@(Data.Nat.lte numer denom))
divmodFuelLemma numer denom (S fuel1) (S fuel2) enough1 enough2 | (True ** prf) =
rewrite prf in Refl
divmodFuelLemma numer denom (S fuel1) (S fuel2) enough1 enough2 | (False ** prf) =
rewrite prf in
rewrite divmodFuelLemma (numer `minus` (S denom)) denom fuel1 fuel2
(fuelLemma numer denom fuel1 enough1 prf)
(fuelLemma numer denom fuel2 enough2 prf) in
Refl
multiplicationLemma : (q, predn, r : Nat) -> q * (S predn) + r `LTE` 0 -> (q = 0, r = 0)
multiplicationLemma q predn r bound =
let r_eq_z : (r = 0)
r_eq_z = zeroPlusRightZero (q * (S predn)) r (sym $ lteZeroIsZero bound)
qn_eq_z : (q * (S predn) = 0)
qn_eq_z = zeroPlusLeftZero (q * (S predn)) r (sym $ lteZeroIsZero bound)
q_eq_z : q = 0
q_eq_z = case zeroMultEitherZero q (S predn) qn_eq_z of
Left q_eq_0 => q_eq_0
Right spred_eq_z impossible
in (q_eq_z, r_eq_z)
multiplesModuloZero : (fuel, predn, k : Nat)
-> (enough : fuel `GTE` k * (S predn) )
-> mod' fuel (k * (S predn)) predn = 0
multiplesModuloZero 0 predn k enough =
let (k_eq_z, _) = multiplicationLemma k predn 0
rewrite plusZeroRightNeutral (k * (S predn)) in
enough
in rewrite k_eq_z in
Refl
multiplesModuloZero (S fuel) predn 0 enough = Refl
multiplesModuloZero (S fuel) predn (S k) enough =
let n : Nat
n = S predn
n_lte_skn : n `LTE` (1 + k)*n
n_lte_skn = CalcWith {leq = LTE} $
|~ n
~~ n + 0 ...(sym $ plusZeroRightNeutral n)
~~ (1 + 0)*n ...(Refl)
<~ (1 + k)*n ...(multLteMonotoneLeft (1+0) (1+k) n $
plusLteMonotoneLeft 1 0 k LTEZero)
in case @@(Data.Nat.lte ((1 + k)*n) predn) of
(True ** skn_lte_predn) => absurd $ irreflexive {spo = Data.Nat.LT} predn
$ CalcWith {leq = LTE} $
|~ 1 + predn
~~ n ...(Refl)
~~ n + 0 ...(sym $ plusZeroRightNeutral n)
~~ (1 + 0)*n ...(Refl)
<~ (1 + k)*n ...(multLteMonotoneLeft (1+0) (1+k) n $
LTESucc LTEZero)
<~ predn ...(Properties.lteIsLTE _ _ skn_lte_predn)
(False ** prf) =>
rewrite prf in
let skn_minus_n_eq_kn : ((1 + k)*n `minus` n = k*n)
skn_minus_n_eq_kn = Calc $
|~ ((1+k)*n `minus` n)
~~ ((1+k)*n `minus` (n + 0)) ...(cong ((1+k)*n `minus`) $ sym $ plusZeroRightNeutral n)
~~ (n + k*n `minus` (n + 0)) ...(Refl)
~~ (k*n `minus` 0) ...(plusMinusLeftCancel n (k*n) 0)
~~ k*n ...(minusZeroRight (k*n))
in rewrite skn_minus_n_eq_kn in
multiplesModuloZero fuel predn k $
(rewrite sym $ skn_minus_n_eq_kn in
fuelLemma ((1 + k)*n) predn fuel enough prf)
-- We also want to show uniqueness of this decomposition
-- This is, of course, quite horrible, but I want this theorem in the stdlib
addMultipleMod': (fuel1, fuel2, predn, a, b : Nat) -> (enough1 : fuel1 `GTE` b * (S predn) + a)
-> (enough2 : fuel2 `GTE` a)
-> mod'' fuel1 (b * (S predn) + a) predn = mod'' fuel2 a predn
addMultipleMod' 0 fuel2 predn a b enough1 enough2
= let (b_eq_z, a_eq_z) = multiplicationLemma b predn a enough1
in rewrite a_eq_z in
rewrite b_eq_z in
rewrite modZeroZero predn fuel2 in
Refl
addMultipleMod' fuel1@(S _) fuel2 predn a 0 enough1 enough2 =
rewrite divmodFuelLemma a predn fuel1 fuel2 enough1 enough2 in
Refl
addMultipleMod' (S fuel1) fuel2 predn a (S k) enough1 enough2 =
let n : Nat
n = S predn
lhsarg_geq_predn : ((1 + k)*n + a) `GT` predn
lhsarg_geq_predn = CalcWith {leq = LTE} $
|~ n
~~ (1+0)*n ...(sym $ plusZeroRightNeutral n)
<~ (1+k)*n ...(multLteMonotoneLeft 1 (1+k) n $
LTESucc LTEZero)
<~ (1+k)*n + a ...(lteAddRight $ (1+k)*n)
prf1 : lte ((1 + k)*n + a) predn = False
prf1 = GTIsnotlte ((1 + k)*n + a) predn lhsarg_geq_predn
argsimplify : (((1 + k) *n + a ) `minus` n = k*n + a)
argsimplify = Calc $
|~ (((1+k)*n + a) `minus` n)
~~ (((n + k*n) + a) `minus` n) ...(Refl)
~~ ((n + (k*n + a)) `minus` (n + 0)) ...(cong2 minus
(sym $ plusAssociative n (k*n) a)
(sym $ plusZeroRightNeutral n))
~~ ((k*n + a) `minus` 0) ...(plusMinusLeftCancel n (k*n + a) 0)
~~ k*n + a ...(minusZeroRight (k*n + a))
in rewrite prf1 in
rewrite argsimplify in
addMultipleMod' fuel1 fuel2 predn a k
(rewrite sym argsimplify in
fuelLemma ((1+k)*n + a) predn fuel1 enough1 prf1)
enough2
addMultipleMod : (a, b, n : Nat) -> (n_neq_z1, n_neq_z2 : Not (n = 0))
-> snd (divmodNatNZ (a*n + b) n n_neq_z1) = snd (divmodNatNZ b n n_neq_z2)
addMultipleMod a b 0 n_neq_z1 n_neq_z2 = void (n_neq_z1 Refl)
addMultipleMod a b n@(S predn) n_neq_z1 n_neq_z2 =
addMultipleMod' (a*n + b) b predn b a (reflexive {po = LTE} _) (reflexive {po = LTE} _)
modBelowDenom : (r, n : Nat) -> (n_neq_z : Not (n = 0))
-> (r `LT` n)
-> snd (divmodNatNZ r n n_neq_z) = r
modBelowDenom 0 (S predn) n_neq_0 (LTESucc r_lte_predn) = Refl
modBelowDenom r@(S _) (S predn) n_neq_0 (LTESucc r_lte_predn) =
rewrite LteIslte r predn r_lte_predn in
Refl
modInjective : (r1, r2, n : Nat) -> (n_neq_z1, n_neq_z2 : Not (n = 0))
-> (r1 `LT` n)
-> (r2 `LT` n)
-> snd (divmodNatNZ r1 n n_neq_z1) = snd (divmodNatNZ r2 n n_neq_z2)
-> r1 = r2
modInjective r1 r2 n n_neq_z1 n_neq_z2 r1_lt_n r2_lt_n ri_mod_eq = Calc $
|~ r1
~~ snd (divmodNatNZ r1 n n_neq_z1) ...(sym $ modBelowDenom r1 n n_neq_z1 r1_lt_n)
~~ snd (divmodNatNZ r2 n n_neq_z2) ...(ri_mod_eq)
~~ r2 ...( modBelowDenom r2 n n_neq_z2 r2_lt_n)
step1 : (numer : Nat) -> (denom : Nat) -> (denom_nz : Not (denom = 0))
-> (q, r : Nat) -> (r `LT` denom) -> (numer = q * denom + r)
-> snd (divmodNatNZ numer denom denom_nz) = r
step1 x n n_nz q r r_lt_n x_eq_qnpr = Calc $
|~ snd(divmodNatNZ x n n_nz)
~~ snd(divmodNatNZ (q*n + r) n n_nz) ...(cong (\u => snd $ divmodNatNZ u n n_nz) $ x_eq_qnpr)
~~ snd(divmodNatNZ r n n_nz) ...(addMultipleMod q r n n_nz n_nz)
~~ r ...(modBelowDenom r n n_nz r_lt_n)
step2 : (numer : Nat) -> (denom : Nat) -> (denom_nz : Not (denom = 0))
-> (q, r : Nat) -> (r `LT` denom) -> (numer = q * denom + r)
-> fst (divmodNatNZ numer denom denom_nz) = q
step2 x n n_nz q r r_lt_n x_eq_qnr =
let mod_eq_r : (snd (divmodNatNZ x n n_nz) = r)
mod_eq_r = step1 x n n_nz q r r_lt_n x_eq_qnr
two_decompositions : (fst $ divmodNatNZ x n n_nz) * n + r = q * n + r
two_decompositions = Calc $
|~ (fst $ divmodNatNZ x n n_nz) * n + r
~~ (fst $ divmodNatNZ x n n_nz) * n + (snd $ divmodNatNZ x n n_nz)
...(cong (\ u =>
(fst $ divmodNatNZ x n n_nz)* n + u)
$ sym mod_eq_r)
~~ snd(divmodNatNZ x n n_nz) + fst (divmodNatNZ x n n_nz) * n
...(plusCommutative _ _)
~~ x ...(sym $ DivisionTheoremDivMod x n n_nz)
~~ q*n + r ...(x_eq_qnr)
in multRightCancel (fst $ divmodNatNZ x n n_nz) q n n_nz
$ plusRightCancel ((fst $ divmodNatNZ x n n_nz)* n) (q*n) r
$ two_decompositions
export
DivisionTheoremUniquenessDivMod : (numer : Nat) -> (denom : Nat) -> (denom_nz : Not (denom = 0))
-> (q, r : Nat) -> (r `LT` denom) -> (numer = q * denom + r)
-> divmodNatNZ numer denom denom_nz = (q, r)
DivisionTheoremUniquenessDivMod numer denom denom_nz q r x prf =
rewrite sym $ step1 numer denom denom_nz q r x prf in
rewrite sym $ step2 numer denom denom_nz q r x prf in
pair_eta _ -- Should idris be able to see this automatically? Maybe only with homogeneous equality?
where
-- Should this go elsewhere?
||| extensionality law for simple pairs
pair_eta : (x : (a,b)) -> x = (fst x, snd x)
pair_eta (x,y) = Refl
export
DivisionTheoremUniqueness : (numer : Nat) -> (denom : Nat) -> (denom_nz : Not (denom = 0))
-> (q, r : Nat) -> (r `LT` denom) -> (numer = q * denom + r)
-> (divNatNZ numer denom denom_nz = q, modNatNZ numer denom denom_nz = r)
DivisionTheoremUniqueness numer denom denom_nz q r x prf =
rewrite sym $ fstDivmodNatNZeqDiv numer denom denom_nz denom_nz in
rewrite sym $ sndDivmodNatNZeqMod numer denom denom_nz denom_nz in
rewrite DivisionTheoremUniquenessDivMod numer denom denom_nz q r x prf in
(Refl, Refl)
Reference in New Issue View Git Blame Copy Permalink