From 4292d735eb86ba65f4a38df117f56c586e555fcd Mon Sep 17 00:00:00 2001 From: Nick Drozd Date: Fri, 5 Jun 2020 17:47:59 -0500 Subject: [PATCH 1/3] Simplify Nat proofs These changes are strictly nonfunctional. --- libs/base/Data/Nat.idr | 262 ++++++++++++++++++----------------------- 1 file changed, 115 insertions(+), 147 deletions(-) diff --git a/libs/base/Data/Nat.idr b/libs/base/Data/Nat.idr index a602d222f4..72d2be8a13 100644 --- a/libs/base/Data/Nat.idr +++ b/libs/base/Data/Nat.idr @@ -1,5 +1,7 @@ module Data.Nat +%default total + export Uninhabited (Z = S n) where uninhabited Refl impossible @@ -157,14 +159,12 @@ maximum (S n) (S m) = S (maximum n m) -- Proofs on S export -eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) -> - S left = S right -eqSucc left _ Refl = Refl +eqSucc : (left, right : Nat) -> left = right -> S left = S right +eqSucc _ _ Refl = Refl export -succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) -> - left = right -succInjective left _ Refl = Refl +succInjective : (left, right : Nat) -> S left = S right -> left = right +succInjective _ _ Refl = Refl export SIsNotZ : (S x = Z) -> Void @@ -219,7 +219,7 @@ Integral Nat where div = divNat mod = modNat -export +export partial gcd : (a: Nat) -> (b: Nat) -> {auto ok: NotBothZero a b} -> Nat gcd a Z = a gcd Z b = b @@ -250,89 +250,80 @@ cmp (S x) (S y) with (cmp x y) cmp (S x) (S x) | CmpEQ = CmpEQ cmp (S (y + (S k))) (S y) | CmpGT k = CmpGT k --- Proofs on +-- Proofs on + export plusZeroLeftNeutral : (right : Nat) -> 0 + right = right -plusZeroLeftNeutral right = Refl +plusZeroLeftNeutral _ = Refl export plusZeroRightNeutral : (left : Nat) -> left + 0 = left plusZeroRightNeutral Z = Refl -plusZeroRightNeutral (S n) = - let inductiveHypothesis = plusZeroRightNeutral n in - rewrite inductiveHypothesis in Refl +plusZeroRightNeutral (S n) = rewrite plusZeroRightNeutral n in Refl export -plusSuccRightSucc : (left : Nat) -> (right : Nat) -> - S (left + right) = left + (S right) -plusSuccRightSucc Z right = Refl -plusSuccRightSucc (S left) right = - let inductiveHypothesis = plusSuccRightSucc left right in - rewrite inductiveHypothesis in Refl +plusSuccRightSucc : (left, right : Nat) -> S (left + right) = left + (S right) +plusSuccRightSucc Z _ = Refl +plusSuccRightSucc (S left) right = rewrite plusSuccRightSucc left right in Refl export -plusCommutative : (left : Nat) -> (right : Nat) -> - left + right = right + left -plusCommutative Z right = rewrite plusZeroRightNeutral right in Refl +plusCommutative : (left, right : Nat) -> left + right = right + left +plusCommutative Z right = rewrite plusZeroRightNeutral right in Refl plusCommutative (S left) right = - let inductiveHypothesis = plusCommutative left right in - rewrite inductiveHypothesis in - rewrite plusSuccRightSucc right left in Refl + rewrite plusCommutative left right in + rewrite plusSuccRightSucc right left in + Refl export -plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) -> +plusAssociative : (left, centre, right : Nat) -> left + (centre + right) = (left + centre) + right -plusAssociative Z centre right = Refl +plusAssociative Z _ _ = Refl plusAssociative (S left) centre right = - let inductiveHypothesis = plusAssociative left centre right in - rewrite inductiveHypothesis in Refl + rewrite plusAssociative left centre right in Refl export -plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) -> - (p : left = right) -> left + c = right + c -plusConstantRight left _ c Refl = Refl +plusConstantRight : (left, right, c : Nat) -> left = right -> + left + c = right + c +plusConstantRight _ _ _ Refl = Refl export -plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) -> - (p : left = right) -> c + left = c + right -plusConstantLeft left _ c Refl = Refl +plusConstantLeft : (left, right, c : Nat) -> left = right -> + c + left = c + right +plusConstantLeft _ _ _ Refl = Refl export plusOneSucc : (right : Nat) -> 1 + right = S right -plusOneSucc n = Refl +plusOneSucc _ = Refl export -plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) -> - (p : left + right = left + right') -> right = right' -plusLeftCancel Z right right' p = p +plusLeftCancel : (left, right, right' : Nat) -> + left + right = left + right' -> right = right' +plusLeftCancel Z _ _ p = p plusLeftCancel (S left) right right' p = - let inductiveHypothesis = plusLeftCancel left right right' in - inductiveHypothesis (succInjective _ _ p) + plusLeftCancel left right right' (succInjective _ _ p) export -plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) -> - (p : left + right = left' + right) -> left = left' -plusRightCancel left left' Z p = rewrite sym (plusZeroRightNeutral left) in - rewrite sym (plusZeroRightNeutral left') in - p -plusRightCancel left left' (S right) p = - plusRightCancel left left' right - (succInjective _ _ (rewrite plusSuccRightSucc left right in - rewrite plusSuccRightSucc left' right in p)) +plusRightCancel : (left, left', right : Nat) -> + left + right = left' + right -> left = left' +plusRightCancel left left' right p = + plusLeftCancel right left left' $ + rewrite plusCommutative right left in + rewrite plusCommutative right left' in + p export -plusLeftLeftRightZero : (left : Nat) -> (right : Nat) -> - (p : left + right = left) -> right = Z -plusLeftLeftRightZero Z right p = p -plusLeftLeftRightZero (S left) right p = - plusLeftLeftRightZero left right (succInjective _ _ p) +plusLeftLeftRightZero : (left, right : Nat) -> + left + right = left -> right = Z +plusLeftLeftRightZero left right p = + plusLeftCancel left right Z $ + rewrite plusZeroRightNeutral left in + p -- Proofs on * export multZeroLeftZero : (right : Nat) -> Z * right = Z -multZeroLeftZero right = Refl +multZeroLeftZero _ = Refl export multZeroRightZero : (left : Nat) -> left * Z = Z @@ -340,97 +331,80 @@ multZeroRightZero Z = Refl multZeroRightZero (S left) = multZeroRightZero left export -multRightSuccPlus : (left : Nat) -> (right : Nat) -> +multRightSuccPlus : (left, right : Nat) -> left * (S right) = left + (left * right) -multRightSuccPlus Z right = Refl +multRightSuccPlus Z _ = Refl multRightSuccPlus (S left) right = - let inductiveHypothesis = multRightSuccPlus left right in - rewrite inductiveHypothesis in - rewrite plusAssociative left right (left * right) in - rewrite plusAssociative right left (left * right) in - rewrite plusCommutative right left in - Refl + rewrite multRightSuccPlus left right in + rewrite plusAssociative left right (left * right) in + rewrite plusAssociative right left (left * right) in + rewrite plusCommutative right left in + Refl export -multLeftSuccPlus : (left : Nat) -> (right : Nat) -> +multLeftSuccPlus : (left, right : Nat) -> (S left) * right = right + (left * right) -multLeftSuccPlus left right = Refl +multLeftSuccPlus _ _ = Refl export -multCommutative : (left : Nat) -> (right : Nat) -> - left * right = right * left -multCommutative Z right = rewrite multZeroRightZero right in Refl +multCommutative : (left, right : Nat) -> left * right = right * left +multCommutative Z right = rewrite multZeroRightZero right in Refl multCommutative (S left) right = - let inductiveHypothesis = multCommutative left right in - rewrite inductiveHypothesis in - rewrite multRightSuccPlus right left in - Refl + rewrite multCommutative left right in + rewrite multRightSuccPlus right left in + Refl export -multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) -> - left * (centre + right) = (left * centre) + (left * right) -multDistributesOverPlusRight Z centre right = Refl -multDistributesOverPlusRight (S left) centre right = - let inductiveHypothesis = multDistributesOverPlusRight left centre right in - rewrite inductiveHypothesis in - rewrite plusAssociative (centre + (left * centre)) right (left * right) in - rewrite sym (plusAssociative centre (left * centre) right) in - rewrite plusCommutative (left * centre) right in - rewrite plusAssociative centre right (left * centre) in - rewrite plusAssociative (centre + right) (left * centre) (left * right) in - Refl +multDistributesOverPlusLeft : (left, centre, right : Nat) -> + (left + centre) * right = (left * right) + (centre * right) +multDistributesOverPlusLeft Z _ _ = Refl +multDistributesOverPlusLeft (S k) centre right = + rewrite multDistributesOverPlusLeft k centre right in + rewrite plusAssociative right (k * right) (centre * right) in + Refl export -multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) -> - (left + centre) * right = (left * right) + (centre * right) -multDistributesOverPlusLeft Z centre right = Refl -multDistributesOverPlusLeft (S left) centre right = - let inductiveHypothesis = multDistributesOverPlusLeft left centre right in - rewrite inductiveHypothesis in - rewrite plusAssociative right (left * right) (centre * right) in - Refl +multDistributesOverPlusRight : (left, centre, right : Nat) -> + left * (centre + right) = (left * centre) + (left * right) +multDistributesOverPlusRight left centre right = + rewrite multCommutative left (centre + right) in + rewrite multCommutative left centre in + rewrite multCommutative left right in + multDistributesOverPlusLeft centre right left export -multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) -> +multAssociative : (left, centre, right : Nat) -> left * (centre * right) = (left * centre) * right -multAssociative Z centre right = Refl +multAssociative Z _ _ = Refl multAssociative (S left) centre right = - let inductiveHypothesis = multAssociative left centre right in - rewrite inductiveHypothesis in - rewrite multDistributesOverPlusLeft centre (left * centre) right in - Refl + rewrite multAssociative left centre right in + rewrite multDistributesOverPlusLeft centre (mult left centre) right in + Refl export multOneLeftNeutral : (right : Nat) -> 1 * right = right -multOneLeftNeutral Z = Refl -multOneLeftNeutral (S right) = - let inductiveHypothesis = multOneLeftNeutral right in - rewrite inductiveHypothesis in - Refl +multOneLeftNeutral right = plusZeroRightNeutral right export multOneRightNeutral : (left : Nat) -> left * 1 = left -multOneRightNeutral Z = Refl -multOneRightNeutral (S left) = - let inductiveHypothesis = multOneRightNeutral left in - rewrite inductiveHypothesis in - Refl +multOneRightNeutral left = rewrite multCommutative left 1 in multOneLeftNeutral left --- Proofs on - +-- Proofs on minus export -minusSuccSucc : (left : Nat) -> (right : Nat) -> minus (S left) (S right) = minus left right -minusSuccSucc left right = Refl +minusSuccSucc : (left, right : Nat) -> + minus (S left) (S right) = minus left right +minusSuccSucc _ _ = Refl export minusZeroLeft : (right : Nat) -> minus 0 right = Z -minusZeroLeft right = Refl +minusZeroLeft - = Refl export minusZeroRight : (left : Nat) -> minus left 0 = left -minusZeroRight Z = Refl -minusZeroRight (S left) = Refl +minusZeroRight Z = Refl +minusZeroRight (S _) = Refl export minusZeroN : (n : Nat) -> Z = minus n n @@ -445,53 +419,47 @@ minusOneSuccN (S n) = minusOneSuccN n export minusSuccOne : (n : Nat) -> minus (S n) 1 = n minusSuccOne Z = Refl -minusSuccOne (S n) = Refl +minusSuccOne (S _) = Refl export -minusPlusZero : (n : Nat) -> (m : Nat) -> minus n (n + m) = Z -minusPlusZero Z m = Refl +minusPlusZero : (n, m : Nat) -> minus n (n + m) = Z +minusPlusZero Z _ = Refl minusPlusZero (S n) m = minusPlusZero n m export -minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) -> +minusMinusMinusPlus : (left, centre, right : Nat) -> minus (minus left centre) right = minus left (centre + right) -minusMinusMinusPlus Z Z right = Refl -minusMinusMinusPlus (S left) Z right = Refl -minusMinusMinusPlus Z (S centre) right = Refl +minusMinusMinusPlus Z Z _ = Refl +minusMinusMinusPlus (S _) Z _ = Refl +minusMinusMinusPlus Z (S _) _ = Refl minusMinusMinusPlus (S left) (S centre) right = - let inductiveHypothesis = minusMinusMinusPlus left centre right in - rewrite inductiveHypothesis in - Refl + rewrite minusMinusMinusPlus left centre right in Refl export -plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) -> +plusMinusLeftCancel : (left, right : Nat) -> (right' : Nat) -> minus (left + right) (left + right') = minus right right' -plusMinusLeftCancel Z right right' = Refl +plusMinusLeftCancel Z _ _ = Refl plusMinusLeftCancel (S left) right right' = - let inductiveHypothesis = plusMinusLeftCancel left right right' in - rewrite inductiveHypothesis in - Refl + rewrite plusMinusLeftCancel left right right' in Refl export -multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) -> - (minus left centre) * right = minus (left * right) (centre * right) -multDistributesOverMinusLeft Z Z right = Refl -multDistributesOverMinusLeft (S left) Z right = - rewrite (minusZeroRight (plus right (mult left right))) in Refl -multDistributesOverMinusLeft Z (S centre) right = Refl +multDistributesOverMinusLeft : (left, centre, right : Nat) -> + (minus left centre) * right = minus (left * right) (centre * right) +multDistributesOverMinusLeft Z Z _ = Refl +multDistributesOverMinusLeft (S left) Z right = + rewrite minusZeroRight (right + (left * right)) in Refl +multDistributesOverMinusLeft Z (S _) _ = Refl multDistributesOverMinusLeft (S left) (S centre) right = - let inductiveHypothesis = multDistributesOverMinusLeft left centre right in - rewrite inductiveHypothesis in - rewrite plusMinusLeftCancel right (mult left right) (mult centre right) in - Refl + rewrite multDistributesOverMinusLeft left centre right in + rewrite plusMinusLeftCancel right (left * right) (centre * right) in + Refl export -multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) -> - left * (minus centre right) = minus (left * centre) (left * right) +multDistributesOverMinusRight : (left, centre, right : Nat) -> + left * (minus centre right) = minus (left * centre) (left * right) multDistributesOverMinusRight left centre right = - rewrite multCommutative left (minus centre right) in - rewrite multDistributesOverMinusLeft centre right left in - rewrite multCommutative centre left in - rewrite multCommutative right left in - Refl - + rewrite multCommutative left (minus centre right) in + rewrite multDistributesOverMinusLeft centre right left in + rewrite multCommutative centre left in + rewrite multCommutative right left in + Refl From 5665cfab21a456ae51047109ecdd9a7f168391b3 Mon Sep 17 00:00:00 2001 From: Nick Drozd Date: Fri, 5 Jun 2020 17:55:16 -0500 Subject: [PATCH 2/3] Copy over more Nat proofs --- libs/base/Data/Nat.idr | 95 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 94 insertions(+), 1 deletion(-) diff --git a/libs/base/Data/Nat.idr b/libs/base/Data/Nat.idr index 72d2be8a13..a8854de6a9 100644 --- a/libs/base/Data/Nat.idr +++ b/libs/base/Data/Nat.idr @@ -399,7 +399,7 @@ minusSuccSucc _ _ = Refl export minusZeroLeft : (right : Nat) -> minus 0 right = Z -minusZeroLeft - = Refl +minusZeroLeft _ = Refl export minusZeroRight : (left : Nat) -> minus left 0 = left @@ -463,3 +463,96 @@ multDistributesOverMinusRight left centre right = rewrite multCommutative centre left in rewrite multCommutative right left in Refl + +-- power proofs + +multPowerPowerPlus : (base, exp, exp' : Nat) -> + power base (exp + exp') = (power base exp) * (power base exp') +-- multPowerPowerPlus base Z exp' = +-- rewrite sym $ plusZeroRightNeutral (power base exp') in Refl +-- multPowerPowerPlus base (S exp) exp' = +-- rewrite multPowerPowerPlus base exp exp' in +-- rewrite sym $ multAssociative base (power base exp) (power base exp') in +-- Refl + +powerOneNeutral : (base : Nat) -> power base 1 = base +powerOneNeutral base = rewrite multCommutative base 1 in multOneLeftNeutral base + +powerOneSuccOne : (exp : Nat) -> power 1 exp = 1 +powerOneSuccOne Z = Refl +powerOneSuccOne (S exp) = rewrite powerOneSuccOne exp in Refl + +powerPowerMultPower : (base, exp, exp' : Nat) -> + power (power base exp) exp' = power base (exp * exp') +powerPowerMultPower _ exp Z = rewrite multZeroRightZero exp in Refl +powerPowerMultPower base exp (S exp') = + rewrite powerPowerMultPower base exp exp' in + rewrite multRightSuccPlus exp exp' in + rewrite sym $ multPowerPowerPlus base exp (exp * exp') in + Refl + +-- minimum / maximum proofs + +maximumAssociative : (l, c, r : Nat) -> + maximum l (maximum c r) = maximum (maximum l c) r +maximumAssociative Z _ _ = Refl +maximumAssociative (S _) Z _ = Refl +maximumAssociative (S _) (S _) Z = Refl +maximumAssociative (S k) (S j) (S i) = rewrite maximumAssociative k j i in Refl + +maximumCommutative : (l, r : Nat) -> maximum l r = maximum r l +maximumCommutative Z Z = Refl +maximumCommutative Z (S _) = Refl +maximumCommutative (S _) Z = Refl +maximumCommutative (S k) (S j) = rewrite maximumCommutative k j in Refl + +maximumIdempotent : (n : Nat) -> maximum n n = n +-- maximumIdempotent Z = Refl +-- maximumIdempotent (S k) = cong $ maximumIdempotent k + +minimumAssociative : (l, c, r : Nat) -> + minimum l (minimum c r) = minimum (minimum l c) r +minimumAssociative Z _ _ = Refl +minimumAssociative (S _) Z _ = Refl +minimumAssociative (S _) (S _) Z = Refl +minimumAssociative (S k) (S j) (S i) = rewrite minimumAssociative k j i in Refl + +minimumCommutative : (l, r : Nat) -> minimum l r = minimum r l +minimumCommutative Z Z = Refl +minimumCommutative Z (S _) = Refl +minimumCommutative (S _) Z = Refl +minimumCommutative (S k) (S j) = rewrite minimumCommutative k j in Refl + +minimumIdempotent : (n : Nat) -> minimum n n = n +-- minimumIdempotent Z = Refl +-- minimumIdempotent (S k) = cong (minimumIdempotent k) + +minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z +minimumZeroZeroLeft left = rewrite minimumCommutative left 0 in Refl + +minimumSuccSucc : (left, right : Nat) -> + minimum (S left) (S right) = S (minimum left right) +minimumSuccSucc _ _ = Refl + +maximumZeroNLeft : (left : Nat) -> maximum left Z = left +maximumZeroNLeft left = rewrite maximumCommutative left Z in Refl + +maximumSuccSucc : (left, right : Nat) -> + S (maximum left right) = maximum (S left) (S right) +maximumSuccSucc _ _ = Refl + +sucMaxL : (l : Nat) -> maximum (S l) l = (S l) +-- sucMaxL Z = Refl +-- sucMaxL (S l) = cong $ sucMaxL l + +sucMaxR : (l : Nat) -> maximum l (S l) = (S l) +-- sucMaxR Z = Refl +-- sucMaxR (S l) = cong $ sucMaxR l + +sucMinL : (l : Nat) -> minimum (S l) l = l +-- sucMinL Z = Refl +-- sucMinL (S l) = cong $ sucMinL l + +sucMinR : (l : Nat) -> minimum l (S l) = l +-- sucMinR Z = Refl +-- sucMinR (S l) = cong $ sucMinR l From 85c1e625876d4f3a2ae09159b889f0d07e6b0ee9 Mon Sep 17 00:00:00 2001 From: Nick Drozd Date: Sun, 7 Jun 2020 14:17:17 -0500 Subject: [PATCH 3/3] Update test --- tests/idris2/reflection003/expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/idris2/reflection003/expected b/tests/idris2/reflection003/expected index 583a49727e..19cf150ea4 100644 --- a/tests/idris2/reflection003/expected +++ b/tests/idris2/reflection003/expected @@ -12,4 +12,4 @@ Error during reflection: Still not trying refprims.idr:43:10--45:1:While processing right hand side of dummy3 at refprims.idr:43:1--45:1: Error during reflection: Undefined name refprims.idr:46:10--48:1:While processing right hand side of dummy4 at refprims.idr:46:1--48:1: -Error during reflection: failed after generating Main.{plus:5841} +Error during reflection: failed after generating Main.{plus:6081}