git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4818 from nickdrozd/proofs
3d83aa0Niklas Larsson
libs/contrib/Data/Nat/Parity.idr+123−69
compare with master
unifiedsplit
@@ -2,18 +2,9 @@ module Data.Nat.Parity
2
2
3%access public export
3%access public export
4
4
5−--------------------------------------------------------------------------------
5+----------------------------------------
6−-- Parity
7−--------------------------------------------------------------------------------
8
6
9−mutual
7+-- Type-level, constructive definitions of parity.
10− even : Nat -> Bool
11− even Z = True
12− even (S k) = odd k
13−
14− odd : Nat -> Bool
15− odd Z = False
16− odd (S k) = even k
17
8
18||| A nat is Even when it is twice some other nat.
9||| A nat is Even when it is twice some other nat.
19Even : Nat -> Type
10Even : Nat -> Type
@@ -23,6 +14,8 @@ Even n = (half : Nat ** n = half * 2)
23Odd : Nat -> Type
14Odd : Nat -> Type
24Odd n = (haf : Nat ** n = S $ haf * 2)
15Odd n = (haf : Nat ** n = S $ haf * 2)
25
16
17+----------------------------------------
18+
26||| Two more than an Even is Even.
19||| Two more than an Even is Even.
27add2Even : Even n -> Even (2 + n)
20add2Even : Even n -> Even (2 + n)
28add2Even (half ** pf) = (S half ** cong {f = (+) 2} pf)
21add2Even (half ** pf) = (S half ** cong {f = (+) 2} pf)
@@ -52,20 +45,73 @@ succDoublePredPred {k = S _} prf = cong {f = Nat.pred} prf
52predEvenOdd : Even (S n) -> Odd n
45predEvenOdd : Even (S n) -> Odd n
53predEvenOdd (half ** pf) = (pred half ** succDoublePredPred pf)
46predEvenOdd (half ** pf) = (pred half ** succDoublePredPred pf)
54
47
48+----------------------------------------
49+
50+-- Boolean definitions of parity.
51+
52+mutual
53+ even : Nat -> Bool
54+ even Z = True
55+ even (S k) = odd k
56+
57+ odd : Nat -> Bool
58+ odd Z = False
59+ odd (S k) = even k
60+
61+----------------------------------------
62+
63+-- The boolean and type-level definitions are equivalent in the sense
64+-- that a proof of one can be gotten from a proof of the other.
65+
66+mutual
67+ ||| Evens are even.
68+ evenEven : Even n -> even n = True
69+ evenEven {n = Z} _ = Refl
70+ evenEven {n = S _} pf = oddOdd $ predEvenOdd pf
71+
72+ ||| Odds are odd.
73+ oddOdd : Odd n -> odd n = True
74+ oddOdd {n = Z} (_ ** pf) = absurd pf
75+ oddOdd {n = S _} pf = evenEven $ predOddEven pf
76+
77+mutual
78+ ||| If it's even, it's Even.
79+ evenEvenConverse : even n = True -> Even n
80+ evenEvenConverse {n = Z} prf = (0 ** Refl)
81+ evenEvenConverse {n = S k} prf =
82+ let (haf ** pf) = oddOddConverse prf in
83+ (S haf ** cong pf)
84+
85+ ||| If it's odd, it's Odd
86+ oddOddConverse : odd n = True -> Odd n
87+ oddOddConverse {n = Z} prf = absurd prf
88+ oddOddConverse {n = S k} prf =
89+ let (half ** pf) = evenEvenConverse prf in
90+ (half ** cong pf)
91+
92+----------------------------------------
93+
94+||| Every nat is either even or odd.
95+evenorodd : (n : Nat) -> Either (even n = True) (odd n = True)
96+evenorodd Z = Left Refl
97+evenorodd (S k) = case evenorodd k of
98+ Left l => Right l
99+ Right r => Left r
100+
55||| Every nat is either Even or Odd.
101||| Every nat is either Even or Odd.
56evenOrOdd : (n : Nat) -> Either (Even n) (Odd n)
102evenOrOdd : (n : Nat) -> Either (Even n) (Odd n)
57−evenOrOdd Z = Left (0 ** Refl)
103+evenOrOdd n = case evenorodd n of
58−evenOrOdd (S k) = case evenOrOdd k of
104+ Left e => Left $ evenEvenConverse e
59− Left (half ** pf) => Right (half ** cong {f = S} pf)
105+ Right o => Right $ oddOddConverse o
60− Right (haf ** pf) => Left (S haf ** cong {f = S} pf)
106+
107+||| No nat is both even and odd.
108+notevenandodd : even n = True -> odd n = True -> Void
109+notevenandodd {n = Z} en on = absurd on
110+notevenandodd {n = S _} en on = notevenandodd on en
61
111
62||| No nat is both Even and Odd.
112||| No nat is both Even and Odd.
63notEvenAndOdd : Even n -> Odd n -> Void
113notEvenAndOdd : Even n -> Odd n -> Void
64−notEvenAndOdd {n = Z} _ (_ ** odd) = absurd odd
114+notEvenAndOdd en on = notevenandodd (evenEven en) (oddOdd on)
65−notEvenAndOdd {n = (S k)} (half ** even) (haf ** odd) =
66− notEvenAndOdd {n = k}
67− (haf ** cong {f = Nat.pred} odd)
68− (pred half ** succDoublePredPred even)
69
115
70||| Evenness is decidable.
116||| Evenness is decidable.
71evenDec : (n : Nat) -> Dec $ Even n
117evenDec : (n : Nat) -> Dec $ Even n
@@ -79,42 +125,46 @@ oddDec n = case evenOrOdd n of
79 Left even => No $ notEvenAndOdd even
125 Left even => No $ notEvenAndOdd even
80 Right odd => Yes odd
126 Right odd => Yes odd
81
127
82−mutual
128+----------------------------------------
83− ||| Evens are even.
84− evenEven : Even n -> even n = True
85− evenEven {n = Z} _ = Refl
86− evenEven {n = S _} pf = oddOdd $ predEvenOdd pf
87
129
88− ||| Odds are odd.
130+||| An Odd is the successor of an Even.
89− oddOdd : Odd n -> odd n = True
131+oddSuccEven : Odd n -> (m : Nat ** (n = S m, Even m))
90− oddOdd {n = Z} (_ ** pf) = absurd pf
132+oddSuccEven (haf ** pf) = (haf * 2 ** (pf, (haf ** Refl)))
91− oddOdd {n = S _} pf = evenEven $ predOddEven pf
92
133
93||| Even plus Even is Even.
134||| Even plus Even is Even.
94evenPlusEven : Even j -> Even k -> Even (j + k)
135evenPlusEven : Even j -> Even k -> Even (j + k)
95evenPlusEven (half_j ** pf_j) (half_k ** pf_k) =
136evenPlusEven (half_j ** pf_j) (half_k ** pf_k) =
96− rewrite pf_j in
97− rewrite pf_k in
98− (half_j + half_k **
137+ (half_j + half_k **
138+ rewrite pf_j in
139+ rewrite pf_k in
99 sym $ multDistributesOverPlusLeft half_j half_k 2)
140 sym $ multDistributesOverPlusLeft half_j half_k 2)
100
141
101−||| Odd plus Odd is Even.
142+||| Odd plus Even is Odd.
102−oddPlusOdd : Odd j -> Odd k -> Even (j + k)
143+oddPlusEven : Odd j -> Even k -> Odd (j + k)
103−oddPlusOdd (haf_j ** pf_j) (haf_k ** pf_k) =
144+oddPlusEven oj ek =
104− rewrite pf_j in
145+ let
105− rewrite pf_k in
146+ (i ** (ipj, ei)) = oddSuccEven oj
106− rewrite sym $ plusSuccRightSucc (haf_j * 2) (haf_k * 2) in
147+ (half_ik ** eik) = evenPlusEven ei ek
107− rewrite sym $ multDistributesOverPlusLeft haf_j haf_k 2 in
148+ in
108− (S (haf_j + haf_k) ** Refl)
149+ (half_ik **
150+ rewrite ipj in
151+ cong {f = S} eik)
109
152
110||| Even plus Odd is Odd.
153||| Even plus Odd is Odd.
111evenPlusOdd : Even j -> Odd k -> Odd (j + k)
154evenPlusOdd : Even j -> Odd k -> Odd (j + k)
112−evenPlusOdd (half_j ** pf_j) (haf_k ** pf_k) =
155+evenPlusOdd {j} {k} ej ok = rewrite plusCommutative j k in oddPlusEven ok ej
113− rewrite pf_j in
156+
114− rewrite pf_k in
157+||| Odd plus Odd is Even.
115− rewrite sym $ plusSuccRightSucc (half_j * 2) (haf_k * 2) in
158+oddPlusOdd : Odd j -> Odd k -> Even (j + k)
116− rewrite sym $ multDistributesOverPlusLeft half_j haf_k 2 in
159+oddPlusOdd oj ok =
160+ let
161+ (i ** (ipj, ei)) = oddSuccEven oj
162+ (haf_ik ** oik) = evenPlusOdd ei ok
163+ in
164+ (S haf_ik **
165+ rewrite ipj in
166+ rewrite oik in
117− (half_j + haf_k ** Refl)
167+ Refl)
118
168
119||| A helper fact.
169||| A helper fact.
120multShuffle : (a, b, c : Nat) ->
170multShuffle : (a, b, c : Nat) ->
@@ -129,35 +179,39 @@ multShuffle a b c =
129||| Even times Even is Even.
179||| Even times Even is Even.
130evenMultEven : Even j -> Even k -> Even (j * k)
180evenMultEven : Even j -> Even k -> Even (j * k)
131evenMultEven (half_j ** pf_j) (half_k ** pf_k) =
181evenMultEven (half_j ** pf_j) (half_k ** pf_k) =
132− rewrite pf_j in
133− rewrite pf_k in
134− (half_j * half_k * 2 **
182+ (half_j * half_k * 2 **
183+ rewrite pf_j in
184+ rewrite pf_k in
135 multShuffle half_j half_k 2)
185 multShuffle half_j half_k 2)
136
186
187+||| Odd times Even is Even.
188+oddMultEven : Odd j -> Even k -> Even (j * k)
189+oddMultEven oj (half_k ** pf_k) =
190+ let
191+ (i ** (ipj, ei)) = oddSuccEven oj
192+ (half_ik ** oik) = evenMultEven ei (half_k ** pf_k)
193+ in
194+ (half_k + half_ik **
195+ rewrite multDistributesOverPlusLeft half_k half_ik 2 in
196+ rewrite ipj in
197+ rewrite oik in
198+ rewrite pf_k in
199+ Refl)
200+
137||| Even times Odd is Even.
201||| Even times Odd is Even.
138evenMultOdd : Even j -> Odd k -> Even (j * k)
202evenMultOdd : Even j -> Odd k -> Even (j * k)
139−evenMultOdd (half_j ** pf_j) (haf_k ** pf_k) =
203+evenMultOdd {j} {k} ej ok = rewrite multCommutative j k in oddMultEven ok ej
140− let half = half_j * haf_k * 2 in
141− rewrite pf_j in
142− rewrite pf_k in
143− rewrite multRightSuccPlus (half_j * 2) (haf_k * 2) in
144− rewrite multShuffle half_j haf_k 2 in
145− (half_j + half **
146− sym $ multDistributesOverPlusLeft half_j half 2)
147
204
148||| Odd times Odd is Odd.
205||| Odd times Odd is Odd.
149oddMultOdd : Odd j -> Odd k -> Odd (j * k)
206oddMultOdd : Odd j -> Odd k -> Odd (j * k)
150−oddMultOdd (haf_j ** pf_j) (haf_k ** pf_k) =
207+oddMultOdd oj (haf_k ** pf_k) =
151 let
208 let
152− haf = haf_j * haf_k * 2
209+ (i ** (ipj, ei)) = oddSuccEven oj
153− rem = haf_j + haf_k
210+ (half_ik ** eik) = evenMultOdd ei (haf_k ** pf_k)
154 in
211 in
155− rewrite pf_j in
212+ (haf_k + half_ik **
156− rewrite pf_k in
213+ rewrite multDistributesOverPlusLeft haf_k half_ik 2 in
157− rewrite multRightSuccPlus (haf_j * 2) (haf_k * 2) in
214+ rewrite ipj in
158− rewrite multShuffle haf_j haf_k 2 in
215+ rewrite eik in
159− rewrite plusAssociative (haf_k * 2) (haf_j * 2) (haf * 2) in
216+ rewrite pf_k in
160− rewrite sym $ multDistributesOverPlusLeft haf_k haf_j 2 in
161− rewrite plusCommutative haf_k haf_j in
162− rewrite sym $ multDistributesOverPlusLeft rem haf 2 in
163− (rem + haf ** Refl)
217+ Refl)
libs/prelude/Prelude/Nat.idr+23−43
@@ -512,19 +512,18 @@ plusLeftCancel (S left) right right' p =
512
512
513total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
513total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
514 (p : left + right = left' + right) -> left = left'
514 (p : left + right = left' + right) -> left = left'
515−plusRightCancel left left' Z p = rewrite sym (plusZeroRightNeutral left) in
515+plusRightCancel left left' right p =
516− rewrite sym (plusZeroRightNeutral left') in
516+ plusLeftCancel right left left' $
517− p
517+ rewrite plusCommutative right left in
518−plusRightCancel left left' (S right) p =
518+ rewrite plusCommutative right left' in
519− plusRightCancel left left' right
519+ p
520− (succInjective _ _ (rewrite plusSuccRightSucc left right in
521− rewrite plusSuccRightSucc left' right in p))
522
520
523total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
521total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
524 (p : left + right = left) -> right = Z
522 (p : left + right = left) -> right = Z
525−plusLeftLeftRightZero Z right p = p
523+plusLeftLeftRightZero left right p =
526−plusLeftLeftRightZero (S left) right p =
524+ plusLeftCancel left right Z $
527− plusLeftLeftRightZero left right (succInjective _ _ p)
525+ rewrite plusZeroRightNeutral left in
526+ p
528
527
529-- Mult
528-- Mult
530total multZeroLeftZero : (right : Nat) -> Z * right = Z
529total multZeroLeftZero : (right : Nat) -> Z * right = Z
@@ -573,12 +572,11 @@ multDistributesOverPlusRight (S left) centre right =
573
572
574total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
573total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
575 (left + centre) * right = (left * right) + (centre * right)
574 (left + centre) * right = (left * right) + (centre * right)
576−multDistributesOverPlusLeft Z centre right = Refl
575+multDistributesOverPlusLeft left centre right =
577−multDistributesOverPlusLeft (S left) centre right =
576+ rewrite multCommutative (left + centre) right in
578− let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
577+ rewrite multCommutative left right in
579− rewrite inductiveHypothesis in
578+ rewrite multCommutative centre right in
580− rewrite plusAssociative right (mult left right) (mult centre right) in
579+ multDistributesOverPlusRight right left centre
581− Refl
582
580
583total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
581total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
584 left * (centre * right) = (left * centre) * right
582 left * (centre * right) = (left * centre) * right
@@ -597,11 +595,7 @@ multOneLeftNeutral (S right) =
597 Refl
595 Refl
598
596
599total multOneRightNeutral : (left : Nat) -> left * 1 = left
597total multOneRightNeutral : (left : Nat) -> left * 1 = left
600−multOneRightNeutral Z = Refl
598+multOneRightNeutral left = rewrite multCommutative left 1 in multOneLeftNeutral left
601−multOneRightNeutral (S left) =
602− let inductiveHypothesis = multOneRightNeutral left in
603− rewrite inductiveHypothesis in
604− Refl
605
599
606-- Minus
600-- Minus
607total minusSuccSucc : (left : Nat) -> (right : Nat) ->
601total minusSuccSucc : (left : Nat) -> (right : Nat) ->
@@ -689,10 +683,7 @@ total powerZeroOne : (base : Nat) -> power base 0 = S Z
689powerZeroOne base = Refl
683powerZeroOne base = Refl
690
684
691total powerOneNeutral : (base : Nat) -> power base 1 = base
685total powerOneNeutral : (base : Nat) -> power base 1 = base
692−powerOneNeutral Z = Refl
686+powerOneNeutral base = rewrite multCommutative base 1 in multOneLeftNeutral base
693−powerOneNeutral (S base) =
694− let inductiveHypothesis = powerOneNeutral base in
695− rewrite inductiveHypothesis in Refl
696
687
697total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z
688total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z
698powerOneSuccOne Z = Refl
689powerOneSuccOne Z = Refl
@@ -701,8 +692,7 @@ powerOneSuccOne (S exp) =
701 rewrite inductiveHypothesis in Refl
692 rewrite inductiveHypothesis in Refl
702
693
703total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
694total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
704−powerSuccSuccMult Z = Refl
705−powerSuccSuccMult (S base) = rewrite multOneRightNeutral base in Refl
695+powerSuccSuccMult base = rewrite multOneRightNeutral base in Refl
706
696
707total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
697total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
708 power (power base exp) exp' = power base (exp * exp')
698 power (power base exp) exp' = power base (exp * exp')
@@ -796,34 +786,24 @@ minimumIdempotent Z = Refl
796minimumIdempotent (S k) = cong (minimumIdempotent k)
786minimumIdempotent (S k) = cong (minimumIdempotent k)
797
787
798total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z
788total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z
799−minimumZeroZeroRight Z = Refl
789+minimumZeroZeroRight right = Refl
800−minimumZeroZeroRight (S right) = minimumZeroZeroRight right
801
790
802total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
791total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
803−minimumZeroZeroLeft Z = Refl
792+minimumZeroZeroLeft left = rewrite minimumCommutative left 0 in Refl
804−minimumZeroZeroLeft (S left) = Refl
805
793
806total minimumSuccSucc : (left : Nat) -> (right : Nat) ->
794total minimumSuccSucc : (left : Nat) -> (right : Nat) ->
807 minimum (S left) (S right) = S (minimum left right)
795 minimum (S left) (S right) = S (minimum left right)
808−minimumSuccSucc Z Z = Refl
796+minimumSuccSucc left right = Refl
809−minimumSuccSucc (S left) Z = Refl
810−minimumSuccSucc Z (S right) = Refl
811−minimumSuccSucc (S left) (S right) = Refl
812
797
813total maximumZeroNRight : (right : Nat) -> maximum Z right = right
798total maximumZeroNRight : (right : Nat) -> maximum Z right = right
814−maximumZeroNRight Z = Refl
799+maximumZeroNRight right = Refl
815−maximumZeroNRight (S right) = Refl
816
800
817total maximumZeroNLeft : (left : Nat) -> maximum left Z = left
801total maximumZeroNLeft : (left : Nat) -> maximum left Z = left
818−maximumZeroNLeft Z = Refl
802+maximumZeroNLeft left = rewrite maximumCommutative left Z in Refl
819−maximumZeroNLeft (S left) = Refl
820
803
821total maximumSuccSucc : (left : Nat) -> (right : Nat) ->
804total maximumSuccSucc : (left : Nat) -> (right : Nat) ->
822 S (maximum left right) = maximum (S left) (S right)
805 S (maximum left right) = maximum (S left) (S right)
823−maximumSuccSucc Z Z = Refl
806+maximumSuccSucc left right = Refl
824−maximumSuccSucc (S left) Z = Refl
825−maximumSuccSucc Z (S right) = Refl
826−maximumSuccSucc (S left) (S right) = Refl
827
807
828total sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
808total sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
829sucMaxL Z = Refl
809sucMaxL Z = Refl