git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4820 from nickdrozd/reverse
93cfe98Niklas Larsson
docs/reference/misc.rst+5−5
compare with master
unifiedsplit
@@ -115,11 +115,11 @@ Here is an example:
115 import Syntax.PreorderReasoning
115 import Syntax.PreorderReasoning
116 multThree : (a, b, c : Nat) -> a * b * c = c * a * b
116 multThree : (a, b, c : Nat) -> a * b * c = c * a * b
117 multThree a b c =
117 multThree a b c =
118− (a * b * c) ={ sym (multAssociative a b c) }=
118+ (a * b * c) ={ sym (multAssociative a b c) }=
119− (a * (b * c)) ={ cong (multCommutative b c) }=
119+ (a * (b * c)) ={ cong (multCommutative b c) }=
120− (a * (c * b)) ={ multAssociative a c b }=
120+ (a * (c * b)) ={ multAssociative a c b }=
121− (a * c * b) ={ cong {f = (* b)} (multCommutative a c) }=
121+ (a * c * b) ={ cong {f = (* b)} (multCommutative a c) }=
122− (c * a * b) QED
122+ (c * a * b) QED
123
123
124Note that the parentheses are required -- only a simple expression can
124Note that the parentheses are required -- only a simple expression can
125be on the left of ``={ }=`` or ``QED``. Also, when using preorder
125be on the left of ``={ }=`` or ``QED``. Also, when using preorder
libs/base/Control/Isomorphism.idr+20−23
@@ -17,21 +17,22 @@ record Iso a b where
17
17
18-- Isomorphism properties
18-- Isomorphism properties
19
19
20−||| Isomorphism is Reflexive
20+||| Isomorphism is reflexive
21isoRefl : Iso a a
21isoRefl : Iso a a
22−isoRefl = MkIso id id (\x => Refl) (\x => Refl)
22+isoRefl = MkIso id id (\_ => Refl) (\_ => Refl)
23
23
24||| Isomorphism is transitive
24||| Isomorphism is transitive
25isoTrans : Iso a b -> Iso b c -> Iso a c
25isoTrans : Iso a b -> Iso b c -> Iso a c
26isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
26isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
27− MkIso (\x => to' (to x))
27+ MkIso xto xfrom xtoFrom xfromTo where
28− (\y => from (from' y))
28+ xto : a -> c
29− (\y => (to' (to (from (from' y)))) ={ cong (toFrom (from' y)) }=
29+ xto = to' . to
30+ xfrom : c -> a
31+ xfrom = from . from'
32+ xtoFrom : (z : c) -> xto (xfrom z) = z
30− (to' (from' y)) ={ toFrom' y }=
33+ xtoFrom z = rewrite toFrom $ from' z in toFrom' z
31− y QED)
34+ xfromTo : (x : a) -> xfrom (xto x) = x
32− (\x => (from (from' (to' (to x)))) ={ cong (fromTo' (to x)) }=
35+ xfromTo x = rewrite fromTo' (to x) in fromTo x
33− (from (to x)) ={ fromTo x }=
34− x QED)
35
36
36Category Iso where
37Category Iso where
37 id = isoRefl
38 id = isoRefl
@@ -99,8 +100,7 @@ eitherBotRight = isoTrans eitherComm eitherBotLeft
99
100
100||| Isomorphism is a congruence with regards to disjunction
101||| Isomorphism is a congruence with regards to disjunction
101eitherCong : Iso a a' -> Iso b b' -> Iso (Either a b) (Either a' b')
102eitherCong : Iso a a' -> Iso b b' -> Iso (Either a b) (Either a' b')
102−eitherCong {a = a} {a' = a'} {b = b} {b' = b'}
103− (MkIso to from toFrom fromTo)
103+eitherCong (MkIso to from toFrom fromTo)
104 (MkIso to' from' toFrom' fromTo') =
104 (MkIso to' from' toFrom' fromTo') =
105 MkIso (eitherMap to to') (eitherMap from from') ok1 ok2
105 MkIso (eitherMap to to') (eitherMap from from') ok1 ok2
106 where eitherMap : (c -> c') -> (d -> d') -> Either c d -> Either c' d'
106 where eitherMap : (c -> c') -> (d -> d') -> Either c d -> Either c' d'
@@ -143,9 +143,7 @@ pairAssoc = MkIso to from ok1 ok2
143
143
144||| Conjunction with truth is a no-op
144||| Conjunction with truth is a no-op
145pairUnitRight : Iso (a, ()) a
145pairUnitRight : Iso (a, ()) a
146−pairUnitRight = MkIso fst (\x => (x, ())) (\x => Refl) ok
146+pairUnitRight = MkIso fst (\x => (x, ())) (\_ => Refl) (\(_, ()) => Refl)
147− where ok : (x : (a, ())) -> (fst x, ()) = x
148− ok (x, ()) = Refl
149
147
150||| Conjunction with truth is a no-op
148||| Conjunction with truth is a no-op
151pairUnitLeft : Iso ((), a) a
149pairUnitLeft : Iso ((), a) a
@@ -161,8 +159,7 @@ pairBotRight = isoTrans pairComm pairBotLeft
161
159
162||| Isomorphism is a congruence with regards to conjunction
160||| Isomorphism is a congruence with regards to conjunction
163pairCong : Iso a a' -> Iso b b' -> Iso (a, b) (a', b')
161pairCong : Iso a a' -> Iso b b' -> Iso (a, b) (a', b')
164−pairCong {a = a} {a' = a'} {b = b} {b' = b'}
165− (MkIso to from toFrom fromTo)
162+pairCong (MkIso to from toFrom fromTo)
166 (MkIso to' from' toFrom' fromTo') =
163 (MkIso to' from' toFrom' fromTo') =
167 MkIso to'' from'' iso1 iso2
164 MkIso to'' from'' iso1 iso2
168 where to'' : (a, b) -> (a', b')
165 where to'' : (a, b) -> (a', b')
@@ -205,7 +202,7 @@ distribLeft = MkIso to from toFrom fromTo
205
202
206||| Products distribute over sums
203||| Products distribute over sums
207distribRight : Iso (a, Either b c) (Either (a, b) (a, c))
204distribRight : Iso (a, Either b c) (Either (a, b) (a, c))
208−distribRight {a} {b} {c} = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm
205+distribRight = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm
209
206
210
207
211-- Enable preorder reasoning syntax over isomorphisms
208-- Enable preorder reasoning syntax over isomorphisms
@@ -222,7 +219,7 @@ step a iso1 iso2 = isoTrans iso1 iso2
222-- Isomorphisms over Maybe
219-- Isomorphisms over Maybe
223||| Isomorphism is a congruence with respect to Maybe
220||| Isomorphism is a congruence with respect to Maybe
224maybeCong : Iso a b -> Iso (Maybe a) (Maybe b)
221maybeCong : Iso a b -> Iso (Maybe a) (Maybe b)
225−maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2
222+maybeCong (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2
226 where ok1 : (y : Maybe b) -> map to (map from y) = y
223 where ok1 : (y : Maybe b) -> map to (map from y) = y
227 ok1 Nothing = Refl
224 ok1 Nothing = Refl
228 ok1 (Just x) = (Just (to (from x))) ={ cong (toFrom x) }= (Just x) QED
225 ok1 (Just x) = (Just (to (from x))) ={ cong (toFrom x) }= (Just x) QED
@@ -253,7 +250,7 @@ maybeVoidUnit = (Maybe Void) ={ maybeEither }=
253 () QED
250 () QED
254
251
255eitherMaybeLeftMaybe : Iso (Either (Maybe a) b) (Maybe (Either a b))
252eitherMaybeLeftMaybe : Iso (Either (Maybe a) b) (Maybe (Either a b))
256−eitherMaybeLeftMaybe {a} {b} =
253+eitherMaybeLeftMaybe =
257 (Either (Maybe a) b) ={ eitherCongLeft maybeEither }=
254 (Either (Maybe a) b) ={ eitherCongLeft maybeEither }=
258 (Either (Either a ()) b) ={ eitherAssoc }=
255 (Either (Either a ()) b) ={ eitherAssoc }=
259 (Either a (Either () b)) ={ eitherCongRight eitherComm }=
256 (Either a (Either () b)) ={ eitherCongRight eitherComm }=
@@ -263,7 +260,7 @@ eitherMaybeLeftMaybe {a} {b} =
263
260
264
261
265eitherMaybeRightMaybe : Iso (Either a (Maybe b)) (Maybe (Either a b))
262eitherMaybeRightMaybe : Iso (Either a (Maybe b)) (Maybe (Either a b))
266−eitherMaybeRightMaybe {a} {b} =
263+eitherMaybeRightMaybe =
267 (Either a (Maybe b)) ={ eitherComm }=
264 (Either a (Maybe b)) ={ eitherComm }=
268 (Either (Maybe b) a) ={ eitherMaybeLeftMaybe }=
265 (Either (Maybe b) a) ={ eitherMaybeLeftMaybe }=
269 (Maybe (Either b a)) ={ maybeCong eitherComm }=
266 (Maybe (Either b a)) ={ maybeCong eitherComm }=
@@ -288,8 +285,8 @@ maybeIsoS = MkIso forth back fb bf
288 fb (FS x) = Refl
285 fb (FS x) = Refl
289
286
290finZeroBot : Iso (Fin 0) Void
287finZeroBot : Iso (Fin 0) Void
291−finZeroBot = MkIso (\x => void (uninhabited x))
288+finZeroBot = MkIso (void . uninhabited)
292− (\x => void x)
289+ void
293 (\x => void x)
290 (\x => void x)
294 (\x => void (uninhabited x))
291 (\x => void (uninhabited x))
295
292
libs/contrib/Control/Algebra/Laws.idr+128−80
@@ -6,98 +6,146 @@ import Interfaces.Verified
6
6
7%access export
7%access export
8
8
9+||| -(-x) = x in any verified group.
10+inverseSquaredIsIdentity : VerifiedGroup t => (x : t) ->
11+ inverse (inverse x) = x
12+inverseSquaredIsIdentity x =
13+ let
14+ ix = inverse x
15+ iix = inverse ix
16+ in
17+ rewrite sym $ monoidNeutralIsNeutralR iix in
18+ rewrite sym $ groupInverseIsInverseL x in
19+ rewrite sym $ semigroupOpIsAssociative x ix iix in
20+ rewrite groupInverseIsInverseL ix in
21+ monoidNeutralIsNeutralL x
22+
9−||| A prof that -0 = 0 in any verified group.
23+||| -0 = 0 in any verified group.
10−inverseNeutralIsNeutral : VerifiedGroup t => inverse (the t A.neutral) = A.neutral
24+inverseNeutralIsNeutral : VerifiedGroup t =>
25+ inverse (the t A.neutral) = A.neutral
11inverseNeutralIsNeutral {t} =
26inverseNeutralIsNeutral {t} =
12− let zero = the t neutral
27+ let e = the t neutral in
13− step1 = cong {f = (<+> inverse zero)} (the (zero = zero) Refl)
14− step2 = replace {P = \x => zero <+> inverse zero = x} (groupInverseIsInverseL zero) step1
28+ rewrite sym $ cong {f = inverse} (groupInverseIsInverseL e) in
15− in
16− replace {P = \x => x = neutral} (monoidNeutralIsNeutralR $ inverse zero) step2
29+ rewrite monoidNeutralIsNeutralR $ inverse e in
30+ inverseSquaredIsIdentity e
17
31
18−||| A proof that -(-x) = x in any verified group.
32+||| -(x + y) = -y + -x in any verified group.
19−inverseSquaredIsIdentity : VerifiedGroup t => (x : t) -> inverse (inverse x) = x
33+inverseOfSum : VerifiedGroup t => (l, r : t) ->
20−inverseSquaredIsIdentity {t} x =
34+ inverse (l <+> r) = inverse r <+> inverse l
35+inverseOfSum {t} l r =
36+ let
21− let zero = the t neutral
37+ e = the t neutral
22− step1 = cong {f = (x <+>)} (groupInverseIsInverseL (inverse x))
38+ il = inverse l
23− step2 = replace {P = \r => r = x <+> neutral} (semigroupOpIsAssociative x (inverse x) (inverse $ inverse x)) step1
39+ ir = inverse r
24− step3 = replace {P = \r => r <+> inverse (inverse x) = x <+> neutral} (groupInverseIsInverseL x) step2
40+ sum = l <+> r
41+ ilr = inverse sum
42+ iril = ir <+> il
43+ ile = il <+> e
44+ in
45+ -- expand
25− step4 = replace {P = \r => r = x <+> neutral} (monoidNeutralIsNeutralR (inverse $ inverse x)) step3
46+ rewrite sym $ monoidNeutralIsNeutralR ilr in
26− in
47+ rewrite sym $ groupInverseIsInverseR r in
48+ rewrite sym $ monoidNeutralIsNeutralL ir in
49+ rewrite sym $ groupInverseIsInverseR l in
50+ -- shuffle
51+ rewrite semigroupOpIsAssociative ir il l in
52+ rewrite sym $ semigroupOpIsAssociative iril l r in
53+ rewrite sym $ semigroupOpIsAssociative iril sum ilr in
54+ -- contract
55+ rewrite sym $ monoidNeutralIsNeutralL il in
56+ rewrite groupInverseIsInverseL sum in
57+ rewrite sym $ semigroupOpIsAssociative (ir <+> ile) l ile in
58+ rewrite semigroupOpIsAssociative l il e in
59+ rewrite groupInverseIsInverseL l in
27− replace {P = \r => inverse (inverse x) = r} (monoidNeutralIsNeutralL x) step4
60+ rewrite monoidNeutralIsNeutralL e in
61+ Refl
28
62
29−||| A proof that -(x + y) = -x - y in any verified abelian group.
63+||| -(x + y) = -x + -y in any verified abelian group.
30−inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) -> inverse (l <+> r) = inverse l <+> inverse r
64+inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) ->
65+ inverse (l <+> r) = inverse l <+> inverse r
31−inverseDistributesOverGroupOp {t} l r =
66+inverseDistributesOverGroupOp l r =
32− let step1 = replace {P = \x => x = neutral} (sym $ groupInverseIsInverseL (l <+> r)) $ the (the t neutral = neutral) Refl
33− step2 = cong {f = ((inverse r) <+>) . ((inverse l) <+>)} step1
34− step3 = replace {P = \x => inverse r <+> (inverse l <+> (l <+> r <+> inverse (l <+> r))) = inverse r <+> x} (monoidNeutralIsNeutralL (inverse l)) step2
35− step4 = replace {P = \x => x = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r) (inverse l) (l <+> r <+> inverse (l <+> r))) step3
36− step5 = replace {P = \x => x = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r <+> inverse l) (l <+> r) (inverse (l <+> r))) step4
37− step6 = replace {P = \x => x <+> inverse (l <+> r) = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r <+> inverse l) l r) step5
38− step7 = replace {P = \x => x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (sym $ semigroupOpIsAssociative (inverse r) (inverse l) l) step6
39− step8 = replace {P = \x => inverse r <+> x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (groupInverseIsInverseR l) step7
40− step9 = replace {P = \x => x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (monoidNeutralIsNeutralL (inverse r)) step8
41− step10 = replace {P = \x => x <+> inverse (l <+> r) = inverse r <+> inverse l} (groupInverseIsInverseR r) step9
42− step11 = replace {P = \x => x = inverse r <+> inverse l} (monoidNeutralIsNeutralR (inverse (l <+> r))) step10
43− in
44− replace {P = \x => inverse (l <+> r) = x} (abelianGroupOpIsCommutative (inverse r) (inverse l)) step11
67+ rewrite abelianGroupOpIsCommutative (inverse l) (inverse r) in
68+ inverseOfSum l r
45
69
46−||| A proof that anything multiplied by zero yields zero back.
70+||| Anything multiplied by zero yields zero back in a verified ring.
47−multNeutralAbsorbingL : VerifiedRingWithUnity t => (r : t) -> A.neutral <.> r = A.neutral
71+multNeutralAbsorbingL : VerifiedRing t => (r : t) ->
72+ A.neutral <.> r = A.neutral
48−multNeutralAbsorbingL r =
73+multNeutralAbsorbingL {t} r =
49− let step1 = the (unity <.> r = r) (ringWithUnityIsUnityR r)
74+ let
75+ e = the t neutral
76+ ir = inverse r
77+ exr = e <.> r
78+ iexr = inverse exr
79+ in
50− step2 = replace {P = \x => x <.> r = r} (sym $ monoidNeutralIsNeutralR unity) step1
80+ rewrite sym $ monoidNeutralIsNeutralR exr in
51− step3 = replace {P = \x => x = r} (ringOpIsDistributiveR neutral unity r) step2
81+ rewrite sym $ groupInverseIsInverseR exr in
52− step4 = replace {P = \x => neutral <.> r <+> x = r} (ringWithUnityIsUnityR r) step3
53− step5 = cong {f = \x => x <+> inverse r} step4
54− step6 = replace {P = \x => x = r <+> inverse r} (sym $ semigroupOpIsAssociative (neutral <.> r) r (inverse r)) step5
82+ rewrite sym $ semigroupOpIsAssociative iexr exr ((iexr <+> exr) <.> r) in
55− step7 = replace {P = \x => neutral <.> r <+> x = x} (groupInverseIsInverseL r) step6
83+ rewrite groupInverseIsInverseR exr in
56− in
84+ rewrite sym $ ringOpIsDistributiveR e e r in
57− replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (neutral <.> r)) step7
85+ rewrite monoidNeutralIsNeutralR e in
86+ groupInverseIsInverseR exr
58
87
59−||| A proof that anything multiplied by zero yields zero back.
88+||| Anything multiplied by zero yields zero back in a verified ring.
60−multNeutralAbsorbingR : VerifiedRingWithUnity t => (l : t) -> l <.> A.neutral = A.neutral
89+multNeutralAbsorbingR : VerifiedRing t => (l : t) ->
90+ l <.> A.neutral = A.neutral
61−multNeutralAbsorbingR l =
91+multNeutralAbsorbingR {t} l =
62− let step1 = the (l <.> unity = l) (ringWithUnityIsUnityL l)
92+ let
63− step2 = replace {P = \x => l <.> x = l} (sym $ monoidNeutralIsNeutralR unity) step1
93+ e = the t neutral
64− step3 = replace {P = \x => x = l} (ringOpIsDistributiveL l neutral unity) step2
94+ il = inverse l
65− step4 = replace {P = \x => l <.> neutral <+> x = l} (ringWithUnityIsUnityL l) step3
95+ lxe = l <.> e
66− step5 = cong {f = \x => x <+> inverse l} step4
96+ ilxe = inverse lxe
97+ in
98+ rewrite sym $ monoidNeutralIsNeutralL lxe in
99+ rewrite sym $ groupInverseIsInverseL lxe in
67− step6 = replace {P = \x => x = l <+> inverse l} (sym $ semigroupOpIsAssociative (l <.> neutral) l (inverse l)) step5
100+ rewrite semigroupOpIsAssociative (l <.> (lxe <+> ilxe)) lxe ilxe in
68− step7 = replace {P = \x => l <.> neutral <+> x = x} (groupInverseIsInverseL l) step6
101+ rewrite groupInverseIsInverseL lxe in
69− in
102+ rewrite sym $ ringOpIsDistributiveL l e e in
70− replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (l <.> neutral)) step7
103+ rewrite monoidNeutralIsNeutralL e in
104+ groupInverseIsInverseL lxe
71
105
72−||| A proof that inverse operator can be extracted before multiplication
106+||| Inverse operator can be extracted before multiplication.
73||| (-x)y = -(xy)
107||| (-x)y = -(xy)
74−multInverseInversesL : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> r = inverse (l <.> r)
108+multInverseInversesL : VerifiedRing t => (l, r : t) ->
109+ inverse l <.> r = inverse (l <.> r)
75multInverseInversesL l r =
110multInverseInversesL l r =
111+ let
112+ il = inverse l
113+ lxr = l <.> r
114+ ilxr = il <.> r
115+ i_lxr = inverse lxr
116+ in
117+ rewrite sym $ monoidNeutralIsNeutralR ilxr in
118+ rewrite sym $ groupInverseIsInverseR lxr in
119+ rewrite sym $ semigroupOpIsAssociative i_lxr lxr ilxr in
120+ rewrite sym $ ringOpIsDistributiveR l il r in
76− let step1 = replace {P = \x => x <.> r = neutral} (sym $ groupInverseIsInverseL l) (multNeutralAbsorbingL r)
121+ rewrite groupInverseIsInverseL l in
77− step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveR l (inverse l) r) step1
122+ rewrite multNeutralAbsorbingL r in
78− step3 = cong {f = ((inverse (l <.> r)) <+>)} step2
79− step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> inverse l <.> r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3
123+ monoidNeutralIsNeutralL i_lxr
80− step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (inverse l <.> r)) step4
81− step6 = replace {P = \x => x <+> inverse l <.> r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5
82− in
83− replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (inverse l <.> r)) step6
84
124
85−||| A proof that inverse operator can be extracted before multiplication
125+||| Inverse operator can be extracted before multiplication.
86||| x(-y) = -(xy)
126||| x(-y) = -(xy)
87−multInverseInversesR : VerifiedRingWithUnity t => (l, r : t) -> l <.> inverse r = inverse (l <.> r)
127+multInverseInversesR : VerifiedRing t => (l, r : t) ->
128+ l <.> inverse r = inverse (l <.> r)
88multInverseInversesR l r =
129multInverseInversesR l r =
89− let step1 = replace {P = \x => l <.> x = neutral} (sym $ groupInverseIsInverseL r) (multNeutralAbsorbingR l)
130+ let
90− step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveL l r (inverse r)) step1
131+ ir = inverse r
91− step3 = cong {f = ((inverse (l <.> r)) <+>)} step2
132+ lxr = l <.> r
133+ lxir = l <.> ir
134+ ilxr = inverse lxr
135+ in
92− step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> l <.> inverse r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3
136+ rewrite sym $ monoidNeutralIsNeutralL lxir in
137+ rewrite sym $ groupInverseIsInverseL lxr in
93− step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (l <.> inverse r)) step4
138+ rewrite semigroupOpIsAssociative lxir lxr ilxr in
139+ rewrite sym $ ringOpIsDistributiveL l ir r in
94− step6 = replace {P = \x => x <+> l <.> inverse r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5
140+ rewrite groupInverseIsInverseR r in
95− in
141+ rewrite multNeutralAbsorbingR l in
96− replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (l <.> inverse r)) step6
142+ monoidNeutralIsNeutralR ilxr
97
143
98−||| A proof that multiplication of inverses is the same as multiplication of original
144+||| Multiplication of inverses is the same as multiplication of
99−||| elements. (-x)(-y) = xy
145+||| original elements.
146+||| (-x)(-y) = xy
100−multNegativeByNegativeIsPositive : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> inverse r = l <.> r
147+multNegativeByNegativeIsPositive : VerifiedRing t => (l, r : t) ->
148+ inverse l <.> inverse r = l <.> r
101multNegativeByNegativeIsPositive l r =
149multNegativeByNegativeIsPositive l r =
102 rewrite multInverseInversesR (inverse l) r in
150 rewrite multInverseInversesR (inverse l) r in
103 rewrite sym $ multInverseInversesL (inverse l) r in
151 rewrite sym $ multInverseInversesL (inverse l) r in
libs/contrib/Data/List/Extra.idrdeleted−46
@@ -1,46 +0,0 @@
1−module Data.List.Extra
2−
3−%default total
4−%access export
5−
6−||| The final segment of the accumulator is the final segment of the result.
7−reverseOntoAcc : (xs, ys, zs : List a) ->
8− reverseOnto (ys ++ zs) xs = (reverseOnto ys xs) ++ zs
9−reverseOntoAcc [] _ _ = Refl
10−reverseOntoAcc (x :: xs) (ys) (zs) = reverseOntoAcc xs (x :: ys) zs
11−
12−||| Serves as a specification for reverseOnto.
13−reverseOntoSpec : (xs, ys : List a) -> reverseOnto xs ys = reverse ys ++ xs
14−reverseOntoSpec xs ys = reverseOntoAcc ys [] xs
15−
16−||| The reverse of an empty list is an empty list. Together with reverseCons,
17−||| serves as a specification for reverse.
18−reverseNil : reverse [] = []
19−reverseNil = Refl
20−
21−||| The reverse of a cons is the reverse of the tail followed by the head.
22−||| Together with reverseNil serves as a specification for reverse.
23−reverseCons : (x : a) -> (xs : List a) -> reverse (x::xs) = reverse xs ++ [x]
24−reverseCons x xs = reverseOntoSpec [x] xs
25−
26−||| Reversing an append is appending reversals backwards.
27−reverseAppend : (xs, ys : List a) ->
28− reverse (xs ++ ys) = reverse ys ++ reverse xs
29−reverseAppend [] ys = sym (appendNilRightNeutral (reverse ys))
30−reverseAppend (x :: xs) ys =
31− rewrite reverseCons x (xs ++ ys) in
32− rewrite reverseAppend xs ys in
33− rewrite reverseCons x xs in
34− sym $ appendAssociative (reverse ys) (reverse xs) [x]
35−
36−||| Reversing a singleton list is a no-op.
37−reverseSingletonId : (x : a) -> reverse [x] = [x]
38−reverseSingletonId _ = Refl
39−
40−||| Reversing a reverse gives the original.
41−reverseReverseId : (xs : List a) -> reverse (reverse xs) = xs
42−reverseReverseId [] = Refl
43−reverseReverseId (x :: xs) =
44− rewrite reverseCons x xs in
45− rewrite reverseAppend (reverse xs) [x] in
46− cong $ reverseReverseId xs
libs/contrib/Data/List/Reverse.idrnew file+99
@@ -0,0 +1,99 @@
1+||| Properties of the reverse function.
2+module Data.List.Reverse
3+
4+%default total
5+%access export
6+
7+||| The final segment of the accumulator is the final segment of the result.
8+reverseOntoAcc : (xs, ys, zs : List a) ->
9+ reverseOnto (ys ++ zs) xs = (reverseOnto ys xs) ++ zs
10+reverseOntoAcc [] _ _ = Refl
11+reverseOntoAcc (x :: xs) (ys) (zs) = reverseOntoAcc xs (x :: ys) zs
12+
13+||| Serves as a specification for reverseOnto.
14+reverseOntoSpec : (xs, ys : List a) -> reverseOnto xs ys = reverse ys ++ xs
15+reverseOntoSpec xs ys = reverseOntoAcc ys [] xs
16+
17+||| The reverse of an empty list is an empty list. Together with reverseCons,
18+||| serves as a specification for reverse.
19+reverseNil : reverse [] = []
20+reverseNil = Refl
21+
22+||| The reverse of a cons is the reverse of the tail followed by the head.
23+||| Together with reverseNil serves as a specification for reverse.
24+reverseCons : (x : a) -> (xs : List a) -> reverse (x::xs) = reverse xs ++ [x]
25+reverseCons x xs = reverseOntoSpec [x] xs
26+
27+||| Reversing an append is appending reversals backwards.
28+reverseAppend : (xs, ys : List a) ->
29+ reverse (xs ++ ys) = reverse ys ++ reverse xs
30+reverseAppend [] ys = sym (appendNilRightNeutral (reverse ys))
31+reverseAppend (x :: xs) ys =
32+ rewrite reverseCons x (xs ++ ys) in
33+ rewrite reverseAppend xs ys in
34+ rewrite reverseCons x xs in
35+ sym $ appendAssociative (reverse ys) (reverse xs) [x]
36+
37+||| A recursive definition of reverse.
38+reverseRec : List a -> List a
39+reverseRec [] = []
40+reverseRec (x :: xs) = reverseRec xs ++ [x]
41+
42+||| The iterative and recursive defintions of reverse are the same.
43+reverseEquiv : (xs : List a) -> reverseRec xs = reverse xs
44+reverseEquiv [] = Refl
45+reverseEquiv (x :: xs) =
46+ rewrite reverseEquiv xs in
47+ rewrite reverseAppend [x] xs in
48+ Refl
49+
50+||| Reversing a singleton list is a no-op.
51+reverseSingletonId : (x : a) -> reverse [x] = [x]
52+reverseSingletonId _ = Refl
53+
54+||| Reversing a reverse gives the original.
55+reverseReverseId : (xs : List a) -> reverse (reverse xs) = xs
56+reverseReverseId [] = Refl
57+reverseReverseId (x :: xs) =
58+ rewrite reverseCons x xs in
59+ rewrite reverseAppend (reverse xs) [x] in
60+ cong $ reverseReverseId xs
61+
62+||| Reversing onto preserves list length.
63+reverseOntoLength : (xs, acc : List a) ->
64+ length $ reverseOnto acc xs = length acc + length xs
65+reverseOntoLength [] acc = rewrite plusZeroRightNeutral (length acc) in Refl
66+reverseOntoLength (x :: xs) acc =
67+ rewrite reverseOntoLength xs (x :: acc) in
68+ plusSuccRightSucc (length acc) (length xs)
69+
70+||| Reversing preserves list length.
71+reverseLength : (xs : List a) -> length $ reverse xs = length xs
72+reverseLength xs = reverseOntoLength xs []
73+
74+||| Equal reversed lists are equal.
75+reverseEqual : (xs, ys : List a) -> reverse xs = reverse ys -> xs = ys
76+reverseEqual xs ys prf =
77+ rewrite sym $ reverseReverseId xs in
78+ rewrite prf in
79+ reverseReverseId ys
80+
81+||| Do geese see God?
82+data Palindrome : (xs : List a) -> Type where
83+ Empty : Palindrome []
84+ Single : Palindrome [_]
85+ Multi : Palindrome xs -> Palindrome $ [x] ++ xs ++ [x]
86+
87+||| A Palindrome reversed is itself.
88+palindromeReverse : (xs : List a) -> Palindrome xs -> reverse xs = xs
89+palindromeReverse [] Empty = Refl
90+palindromeReverse [_] Single = Refl
91+palindromeReverse ([x] ++ ys ++ [x]) (Multi pf) =
92+ rewrite reverseAppend ([x] ++ ys) [x] in
93+ rewrite reverseAppend [x] ys in
94+ rewrite palindromeReverse ys pf in
95+ Refl
96+
97+||| Only Palindromes are equal to their own reverse.
98+postulate -- This is a tough one. Any takers?
99+reversePalindrome : (xs : List a) -> reverse xs = xs -> Palindrome xs
libs/contrib/contrib.ipkg+1−1
@@ -43,7 +43,7 @@ modules = CFFI
43 , Data.Heap
43 , Data.Heap
44 , Data.IOArray
44 , Data.IOArray
45 , Data.List.Zipper
45 , Data.List.Zipper
46− , Data.List.Extra
46+ , Data.List.Reverse
47
47
48 , Data.Matrix
48 , Data.Matrix
49 , Data.Matrix.Algebraic
49 , Data.Matrix.Algebraic
libs/prelude/Prelude/Nat.idr+14−23
@@ -557,26 +557,21 @@ multCommutative (S left) right =
557 rewrite multRightSuccPlus right left in
557 rewrite multRightSuccPlus right left in
558 Refl
558 Refl
559
559
560−total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
561− left * (centre + right) = (left * centre) + (left * right)
562−multDistributesOverPlusRight Z centre right = Refl
563−multDistributesOverPlusRight (S left) centre right =
564− let inductiveHypothesis = multDistributesOverPlusRight left centre right in
565− rewrite inductiveHypothesis in
566− rewrite plusAssociative (plus centre (mult left centre)) right (mult left right) in
567− rewrite sym (plusAssociative centre (mult left centre) right) in
568− rewrite plusCommutative (mult left centre) right in
569− rewrite plusAssociative centre right (mult left centre) in
570− rewrite plusAssociative (plus centre right) (mult left centre) (mult left right) in
571− Refl
572−
573total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
560total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
574 (left + centre) * right = (left * right) + (centre * right)
561 (left + centre) * right = (left * right) + (centre * right)
575−multDistributesOverPlusLeft left centre right =
562+multDistributesOverPlusLeft Z centre right = Refl
576− rewrite multCommutative (left + centre) right in
563+multDistributesOverPlusLeft (S k) centre right =
564+ rewrite multDistributesOverPlusLeft k centre right in
565+ rewrite plusAssociative right (k * right) (centre * right) in
566+ Refl
567+
568+total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
569+ left * (centre + right) = (left * centre) + (left * right)
570+multDistributesOverPlusRight left centre right =
571+ rewrite multCommutative left (centre + right) in
577− rewrite multCommutative left right in
572+ rewrite multCommutative left centre in
578− rewrite multCommutative centre right in
573+ rewrite multCommutative left right in
579− multDistributesOverPlusRight right left centre
574+ multDistributesOverPlusLeft centre right left
580
575
581total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
576total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
582 left * (centre * right) = (left * centre) * right
577 left * (centre * right) = (left * centre) * right
@@ -588,11 +583,7 @@ multAssociative (S left) centre right =
588 Refl
583 Refl
589
584
590total multOneLeftNeutral : (right : Nat) -> 1 * right = right
585total multOneLeftNeutral : (right : Nat) -> 1 * right = right
591−multOneLeftNeutral Z = Refl
586+multOneLeftNeutral right = plusZeroRightNeutral right
592−multOneLeftNeutral (S right) =
593− let inductiveHypothesis = multOneLeftNeutral right in
594− rewrite inductiveHypothesis in
595− Refl
596
587
597total multOneRightNeutral : (left : Nat) -> left * 1 = left
588total multOneRightNeutral : (left : Nat) -> left * 1 = left
598multOneRightNeutral left = rewrite multCommutative left 1 in multOneLeftNeutral left
589multOneRightNeutral left = rewrite multCommutative left 1 in multOneLeftNeutral left