From ab36ad71cff4cf77fa1e565308abb9e7713cba41 Mon Sep 17 00:00:00 2001 From: Nick Drozd Date: Sun, 18 Jul 2021 14:49:46 -0500 Subject: [PATCH] Simplify a few Factor proofs A few proofs have been rewritten, a few unnecessary cases cut, and lots of unnecessary "explicit implicits" have been cut. Probably these implicits were required when the code was initially written, and inference has improved since then. --- libs/contrib/Data/Nat/Factor.idr | 167 +++++++++++++++---------------- 1 file changed, 80 insertions(+), 87 deletions(-) diff --git a/libs/contrib/Data/Nat/Factor.idr b/libs/contrib/Data/Nat/Factor.idr index b0b3e27e7..df74bfc42 100644 --- a/libs/contrib/Data/Nat/Factor.idr +++ b/libs/contrib/Data/Nat/Factor.idr @@ -62,7 +62,7 @@ Uninhabited (Factor Z (S n)) where ||| Given a statement that p is factor of n, return its cofactor. export cofactor : Factor p n -> (q : Nat ** Factor q n) -cofactor (CofactorExists {n} {p} q prf) = +cofactor (CofactorExists q prf) = (q ** CofactorExists p $ rewrite multCommutative q p in prf) ||| 1 is a factor of any natural number. @@ -74,24 +74,26 @@ oneIsFactor (S k) = CofactorExists (S k) (rewrite plusZeroRightNeutral k in Refl ||| 1 is the only factor of itself export oneSoleFactorOfOne : (a : Nat) -> Factor a 1 -> a = 1 -oneSoleFactorOfOne Z (CofactorExists q prf) = absurd $ uninhabited prf -oneSoleFactorOfOne (S Z) (CofactorExists _ _) = Refl +oneSoleFactorOfOne 0 (CofactorExists _ prf) = sym prf +oneSoleFactorOfOne 1 _ = Refl oneSoleFactorOfOne (S (S k)) (CofactorExists Z prf) = - absurd . uninhabited $ replace {p = \x => 1 = x} (multZeroRightZero k) prf + absurd . uninhabited $ trans prf $ multCommutative k 0 oneSoleFactorOfOne (S (S k)) (CofactorExists (S j) prf) = - absurd . uninhabited . succInjective 0 (S j + (j + (k * S j))) $ - replace {p = \x => 1 = S x} (sym $ plusSuccRightSucc j (j + (k * S j))) prf + absurd . uninhabited $ + trans + (succInjective 0 (j + S (j + (k * S j))) prf) + (plusCommutative j (S (j + (k * S j)))) ||| Every natural number is factor of itself. export Reflexive Nat Factor where - reflexive {x} = CofactorExists 1 $ rewrite multOneRightNeutral x in Refl + reflexive = CofactorExists 1 $ rewrite multOneRightNeutral x in Refl ||| Factor relation is transitive. If b is factor of a and c is b factor of c ||| is also a factor of a. export Transitive Nat Factor where - transitive {x} (CofactorExists qb prfAB) (CofactorExists qc prfBC) = + transitive (CofactorExists qb prfAB) (CofactorExists qc prfBC) = CofactorExists (qb * qc) $ rewrite prfBC in rewrite prfAB in @@ -106,12 +108,11 @@ multOneSoleNeutral Z b prf = rewrite sym $ plusZeroRightNeutral b in sym prf multOneSoleNeutral (S k) Z prf = - absurd . uninhabited $ - replace {p = \x => S (S k) = x} (multZeroRightZero k) prf + absurd . uninhabited $ trans prf $ multCommutative k 0 multOneSoleNeutral (S k) (S Z) prf = Refl multOneSoleNeutral (S k) (S (S j)) prf = absurd . uninhabited . - subtractEqLeft k {b = 0} {c = S j + S (j + (k * S j))} $ + subtractEqLeft k {c = S j + S (j + (k * S j))} $ rewrite plusSuccRightSucc j (S (j + (k * S j))) in rewrite plusZeroRightNeutral k in rewrite plusAssociative k j (S (S (j + (k * S j)))) in @@ -129,8 +130,8 @@ multOneSoleNeutral (S k) (S (S j)) prf = ||| If a is a factor of b and b is a factor of a, then a = b. public export Antisymmetric Nat Factor where - antisymmetric {x = Z} (CofactorExists qa prfAB) (CofactorExists qb prfBA) = sym prfAB - antisymmetric {x = S _} {y = Z} (CofactorExists qa prfAB) (CofactorExists qb prfBA) = prfBA + antisymmetric {x = Z} (CofactorExists _ prfAB) _ = sym prfAB + antisymmetric {y = Z} _ (CofactorExists _ prfBA) = prfBA antisymmetric {x = S a} {y = S _} (CofactorExists qa prfAB) (CofactorExists qb prfBA) = let qIs1 = multOneSoleNeutral a (qa * qb) $ rewrite multAssociative (S a) qa qb in @@ -146,13 +147,13 @@ PartialOrder Nat Factor where ||| No number can simultaneously be and not be a factor of another number. export -factorNotFactorAbsurd : {n, p : Nat} -> Factor p n -> Not (NotFactor p n) -factorNotFactorAbsurd {n = S k} {p = Z} (CofactorExists q prf) (ZeroNotFactorS k) = +factorNotFactorAbsurd : Factor p n -> Not (NotFactor p n) +factorNotFactorAbsurd (CofactorExists _ prf) (ZeroNotFactorS _) = uninhabited prf -factorNotFactorAbsurd {n} {p} (CofactorExists q prf) (ProperRemExists q' r contra) with (cmp q q') - factorNotFactorAbsurd {n} {p} (CofactorExists q prf) (ProperRemExists (q + S d) r contra) | CmpLT d = +factorNotFactorAbsurd (CofactorExists q prf) (ProperRemExists q' r contra) with (cmp q q') + factorNotFactorAbsurd (CofactorExists q prf) (ProperRemExists (q + S d) r contra) | CmpLT d = SIsNotZ . - subtractEqLeft (p * q) {b = S ((p * S d) + finToNat r)} {c = 0} $ + subtractEqLeft (p * q) {b = S ((p * S d) + finToNat r)} $ rewrite plusZeroRightNeutral (p * q) in rewrite plusSuccRightSucc (p * S d) (finToNat r) in rewrite plusAssociative (p * q) (p * S d) (S (finToNat r)) in @@ -160,16 +161,15 @@ factorNotFactorAbsurd {n} {p} (CofactorExists q prf) (ProperRemExists q' r contr rewrite sym contra in rewrite sym prf in Refl - factorNotFactorAbsurd {n} {p} (CofactorExists q prf) (ProperRemExists q r contra) | CmpEQ = - uninhabited . - subtractEqLeft (p * q) {b = (S (finToNat r))} {c = 0} $ - rewrite plusZeroRightNeutral (p * q) in - rewrite sym contra in - prf - factorNotFactorAbsurd {n} {p} (CofactorExists (q + S d) prf) (ProperRemExists q r contra) | CmpGT d = - let srEQpPlusPD = the (plus p (mult p d) = S (finToNat r)) $ + factorNotFactorAbsurd (CofactorExists q prf) (ProperRemExists q r contra) | CmpEQ = + SIsNotZ $ sym $ + plusLeftCancel (p * q) 0 (S (finToNat r)) $ + trans (plusZeroRightNeutral (p * q)) $ + trans (sym prf) contra + factorNotFactorAbsurd (CofactorExists (q + S d) prf) (ProperRemExists q r contra) | CmpGT d = + let srEQpPlusPD = the (p + (p * d) = S (finToNat r)) $ rewrite sym $ multRightSuccPlus p d in - subtractEqLeft (p * q) {b = p * (S d)} {c = S (finToNat r)} $ + subtractEqLeft (p * q) $ rewrite sym $ multDistributesOverPlusRight p q (S d) in rewrite sym contra in sym prf @@ -178,13 +178,12 @@ factorNotFactorAbsurd {n} {p} (CofactorExists q prf) (ProperRemExists q' r contr Z => uninhabited srEQpPlusPD (S k) => succNotLTEzero . - subtractLteLeft k {b = S (d + (k * d))} {c = 0} $ + subtractLteLeft k {b = S (d + (k * d))} $ rewrite sym $ plusSuccRightSucc k (d + (k * d)) in rewrite plusZeroRightNeutral k in rewrite srEQpPlusPD in elemSmallerThanBound r - ||| Anything is a factor of 0. export anythingFactorZero : (a : Nat) -> Factor a 0 @@ -199,7 +198,7 @@ multFactor p q = CofactorExists q Refl export factorLteNumber : Factor p n -> {auto positN : LTE 1 n} -> LTE p n factorLteNumber (CofactorExists Z prf) = - let nIsZero = replace {p = \x => n = x} (multZeroRightZero p) prf + let nIsZero = trans prf $ multCommutative p 0 oneLteZero = replace {p = LTE 1} nIsZero positN in absurd $ succNotLTEzero oneLteZero @@ -253,7 +252,7 @@ plusFactor (CofactorExists qn prfN) (CofactorExists qm prfM) = ||| it would be more difficult to prove, since minus lacks certain properties ||| that one would expect from decent subtraction. export -minusFactor : {a, b, p : Nat} -> Factor p (a + b) -> Factor p a -> Factor p b +minusFactor : {b : Nat} -> Factor p (a + b) -> Factor p a -> Factor p b minusFactor (CofactorExists qab prfAB) (CofactorExists qa prfA) = CofactorExists (minus qab qa) ( rewrite multDistributesOverMinusRight p qab qa in @@ -274,11 +273,10 @@ decFactor n (S d) = let Fraction n (S d) q r prf = Data.Fin.Extra.divMod n (S d) in case r of FZ => - let prf = - replace {p = \x => x = n} (plusZeroRightNeutral (q + (d * q))) $ - replace {p = \x => x + 0 = n} (multCommutative q (S d)) prf - in - ItIsFactor $ CofactorExists q (sym prf) + ItIsFactor $ CofactorExists q $ + rewrite sym prf in + rewrite plusCommutative (q * (S d)) 0 in + multCommutative q (S d) (FS pr) => ItIsNotFactor $ ProperRemExists q pr ( @@ -290,7 +288,7 @@ decFactor n (S d) = ||| For all p greater than 1, if p is a factor of n, then it is NOT a factor ||| of (n + 1). export -factNotSuccFact : {n, p : Nat} -> GT p 1 -> Factor p n -> NotFactor p (S n) +factNotSuccFact : {p : Nat} -> GT p 1 -> Factor p n -> NotFactor p (S n) factNotSuccFact {p = Z} pGt1 (CofactorExists q prf) = absurd $ succNotLTEzero pGt1 factNotSuccFact {p = S Z} pGt1 (CofactorExists q prf) = @@ -313,12 +311,12 @@ using (p : Nat) ||| The relation of greatest common divisor is symmetric. public export Symmetric Nat (GCD p) where - symmetric {x = Z} {y = Z} (MkGCD {notBothZero} _ _) impossible - symmetric {x = S a} {y} (MkGCD {notBothZero = LeftIsNotZero} cf greatest) = - MkGCD {notBothZero = RightIsNotZero} (symmetric {ty = Nat} cf) $ + symmetric {x = Z} {y = Z} (MkGCD _ _) impossible + symmetric {x = S _} (MkGCD cf greatest) = + MkGCD (symmetric {ty = Nat} cf) $ \q, cf => greatest q (symmetric {ty = Nat} cf) - symmetric {x} {y = S b} (MkGCD {notBothZero = RightIsNotZero} cf greatest) = - MkGCD {notBothZero = LeftIsNotZero} (symmetric {ty = Nat} cf) $ + symmetric {y = S _} (MkGCD cf greatest) = + MkGCD (symmetric {ty = Nat} cf) $ \q, cf => greatest q (symmetric {ty = Nat} cf) ||| If p is a common factor of a and b, then it is also a factor of their GCD. @@ -328,7 +326,6 @@ commonFactorAlsoFactorOfGCD : {p : Nat} -> Factor p a -> Factor p b -> GCD q a b commonFactorAlsoFactorOfGCD pfa pfb (MkGCD _ greatest) = greatest p (CommonFactorExists p pfa pfb) - ||| 1 is a common factor of any pair of natural numbers. export oneCommonFactor : (a, b : Nat) -> CommonFactor 1 a b @@ -339,10 +336,9 @@ oneCommonFactor a b = CommonFactorExists 1 ||| Any natural number is a common factor of itself and itself. export selfIsCommonFactor : (a : Nat) -> {auto ok : LTE 1 a} -> CommonFactor a a a -selfIsCommonFactor Z = absurd $ succNotLTEzero ok -selfIsCommonFactor (S k) = - let prf = reflexive {x = S k} in - CommonFactorExists (S k) prf prf +selfIsCommonFactor a = + let prf = reflexive {x = a} in + CommonFactorExists a prf prf -- Some helpers for the gcd function. data Search : Type where @@ -358,41 +354,42 @@ Sized Search where size (SearchArgs a b _) = a + b notLteAndGt : (a, b : Nat) -> LTE a b -> Not (GT a b) -notLteAndGt Z b aLteB aGtB = succNotLTEzero aGtB -notLteAndGt (S k) Z aLteB aGtB = succNotLTEzero aLteB +notLteAndGt Z _ _ aGtB = succNotLTEzero aGtB +notLteAndGt (S _) Z aLteB _ = succNotLTEzero aLteB notLteAndGt (S k) (S j) aLteB aGtB = notLteAndGt k j (fromLteSucc aLteB) (fromLteSucc aGtB) gcd_step : (x : Search) -> - (rec : (y : Search) -> Smaller y x -> (f : Nat ** GCD f (left y) (right y))) -> - (f : Nat ** GCD f (left x) (right x)) + (rec : (y : Search) -> Smaller y x -> + (f : Nat ** GCD f (left y) (right y))) -> + (f : Nat ** GCD f (left x) (right x)) gcd_step (SearchArgs Z _ bLteA {bNonZero}) _ = absurd . succNotLTEzero $ transitive {ty = Nat} bNonZero bLteA gcd_step (SearchArgs _ Z _ {bNonZero}) _ = absurd $ succNotLTEzero bNonZero -gcd_step (SearchArgs (S a) (S b) bLteA {bNonZero}) rec = case divMod (S a) (S b) of +gcd_step (SearchArgs (S a) (S b) bLteA) rec = + case divMod (S a) (S b) of Fraction (S a) (S b) q FZ prf => - let sbIsFactor = the (S a = plus q (mult b q)) + let sbIsFactor = rewrite multCommutative b q in rewrite sym $ multRightSuccPlus q b in replace {p = \x => S a = x} (plusZeroRightNeutral (q * S b)) $ sym prf skDividesA = CofactorExists q sbIsFactor skDividesB = reflexive {x = S b} - greatest = the - ((q' : Nat) -> CommonFactor q' (S a) (S b) -> Factor q' (S b)) - (\q', (CommonFactorExists q' _ qfb) => qfb) in - (S b ** MkGCD (CommonFactorExists (S b) skDividesA skDividesB) greatest) + (S b ** MkGCD (CommonFactorExists (S b) skDividesA skDividesB) + (\q', (CommonFactorExists q' _ qfb) => qfb)) Fraction (S a) (S b) q (FS r) prf => let rLtSb = lteSuccRight $ elemSmallerThanBound r - qGt1 = the (LTE 1 q) $ case q of + _ = the (LTE 1 q) $ case q of Z => absurd . notLteAndGt (S $ finToNat r) b (elemSmallerThanBound r) $ replace {p = LTE (S b)} (sym prf) bLteA (S k) => LTESucc LTEZero - smaller = the (LTE (S (S (plus b (S (finToNat r))))) (S (plus a (S b)))) $ - rewrite plusCommutative a (S b) in - LTESucc . LTESucc . plusLteLeft b . fromLteSucc $ transitive {ty = Nat} (elemSmallerThanBound $ FS r) bLteA (f ** MkGCD (CommonFactorExists f prfSb prfRem) greatestSbSr) = - rec (SearchArgs (S b) (S $ finToNat r) rLtSb) smaller - prfSa = the (Factor f (S a)) $ + rec (SearchArgs (S b) (S $ finToNat r) rLtSb) $ + rewrite plusCommutative a (S b) in + LTESucc . LTESucc . plusLteLeft b . fromLteSucc $ + transitive {rel = LTE} (elemSmallerThanBound $ FS r) bLteA + + prfSa = rewrite sym prf in rewrite multCommutative q (S b) in plusFactor (multNAlsoFactor prfSb q) prfRem @@ -400,10 +397,9 @@ gcd_step (SearchArgs (S a) (S b) bLteA {bNonZero}) rec = case divMod (S a) (S b) ((q' : Nat) -> CommonFactor q' (S a) (S b) -> Factor q' f) (\q', (CommonFactorExists q' qfa qfb) => let sbfqSb = - the (Factor (S b) (q * S b)) $ rewrite multCommutative q (S b) in multFactor (S b) q - rightPrf = minusFactor {a = q * S b} {b = S (finToNat r)} + rightPrf = minusFactor {a = q * S b} (rewrite prf in qfa) (transitive {ty = Nat} qfb sbfqSb) in @@ -429,42 +425,41 @@ gcd a Z = ) gcd (S a) (S b) with (cmp (S a) (S b)) gcd (S (b + S d)) (S b) | CmpGT d = - let aGtB = the (LTE (S b) (S (b + S d))) $ - rewrite sym $ plusSuccRightSucc b d in - LTESucc . lteSuccRight $ lteAddRight b - in - sizeInd gcd_step $ SearchArgs (S (b + S d)) (S b) aGtB + sizeInd gcd_step $ + SearchArgs (S (b + S d)) (S b) $ + rewrite sym $ plusSuccRightSucc b d in + LTESucc . lteSuccRight $ lteAddRight b + gcd (S a) (S a) | CmpEQ = - let greatest = the - ((q : Nat) -> CommonFactor q (S a) (S a) -> Factor q (S a)) - (\q, (CommonFactorExists q qfa _) => qfa) - in - (S a ** MkGCD (selfIsCommonFactor (S a)) greatest) + (S a ** MkGCD (selfIsCommonFactor (S a)) + (\q, (CommonFactorExists q qfa _) => qfa)) + gcd (S a) (S (a + S d)) | CmpLT d = - let aGtB = the (LTE (S a) (S (plus a (S d)))) $ - rewrite sym $ plusSuccRightSucc a d in - LTESucc . lteSuccRight $ lteAddRight a - (f ** MkGCD prf greatest) = sizeInd gcd_step $ SearchArgs (S (a + S d)) (S a) aGtB + let (f ** MkGCD prf greatest) = + sizeInd gcd_step $ + SearchArgs (S (a + S d)) (S a) $ + rewrite sym $ plusSuccRightSucc a d in + LTESucc . lteSuccRight $ lteAddRight a in - (f ** MkGCD (symmetric {ty = Nat} prf) (\q, cf => greatest q $ symmetric {ty = Nat} cf)) + (f ** MkGCD (symmetric {ty = Nat} prf) + (\q, cf => greatest q $ symmetric {ty = Nat} cf)) ||| For every two natural numbers there is a unique greatest common divisor. export -gcdUnique : {a, b, p, q : Nat} -> GCD p a b -> GCD q a b -> p = q +gcdUnique : GCD p a b -> GCD q a b -> p = q gcdUnique (MkGCD pCFab greatestP) (MkGCD qCFab greatestQ) = antisymmetric (greatestQ p pCFab) (greatestP q qCFab) - divByGcdHelper : (a, b, c : Nat) -> GCD (S a) (S a * S b) (S a * c) -> GCD 1 (S b) c divByGcdHelper a b c (MkGCD _ greatest) = MkGCD (CommonFactorExists 1 (oneIsFactor (S b)) (oneIsFactor c)) $ \q, (CommonFactorExists q (CofactorExists qb prfQB) (CofactorExists qc prfQC)) => - let qFab = CofactorExists {n = S a * S b} {p = q * S a} qb + let qFab = CofactorExists qb rewrite multCommutative q (S a) in rewrite sym $ multAssociative (S a) q qb in rewrite sym $ prfQB in Refl - qFac = CofactorExists {n = S a * c} {p = q * S a} qc + qFac = CofactorExists qc rewrite multCommutative q (S a) in rewrite sym $ multAssociative (S a) q qc in rewrite sym $ prfQC in @@ -481,13 +476,11 @@ divByGcdHelper a b c (MkGCD _ greatest) = rewrite multCommutative q f in sym qf1 - ||| For every two natural numbers, if we divide both of them by their GCD, ||| the GCD of resulting numbers will always be 1. export divByGcdGcdOne : {a, b, c : Nat} -> GCD a (a * b) (a * c) -> GCD 1 b c -divByGcdGcdOne {a = Z} (MkGCD {notBothZero = LeftIsNotZero} _ _) impossible -divByGcdGcdOne {a = Z} (MkGCD {notBothZero = RightIsNotZero} _ _) impossible +divByGcdGcdOne {a = Z} (MkGCD _ _) impossible divByGcdGcdOne {a = S a} {b = Z} {c = Z} (MkGCD {notBothZero} _ _) = case replace {p = \x => NotBothZero x x} (multZeroRightZero (S a)) notBothZero of LeftIsNotZero impossible