git.iko.soy/Idris-dev
on master help sign in
Merge pull request #8 from dpmulligan/master
9f842bdEdwin Brady
contribs/gtksourceview-2.0-language-spec/idris.lang+2
compare with master
unifiedsplit
@@ -200,6 +200,8 @@
200 <keyword>tactics</keyword>
200 <keyword>tactics</keyword>
201 <keyword>static</keyword>
201 <keyword>static</keyword>
202 <keyword>impossible</keyword>
202 <keyword>impossible</keyword>
203+ <keyword>total</keyword>
204+ <keyword>assert_total</keyword>
203 </context>
205 </context>
204
206
205 <context id="tactic" style-ref="tactic">
207 <context id="tactic" style-ref="tactic">
lib/prelude/nat.idr+160−85
@@ -15,11 +15,11 @@ data Nat
15-- Syntactic tests
15-- Syntactic tests
16--------------------------------------------------------------------------------
16--------------------------------------------------------------------------------
17
17
18−isZero : Nat -> Bool
18+total isZero : Nat -> Bool
19isZero O = True
19isZero O = True
20isZero (S n) = False
20isZero (S n) = False
21
21
22−isSucc : Nat -> Bool
22+total isSucc : Nat -> Bool
23isSucc O = False
23isSucc O = False
24isSucc (S n) = True
24isSucc (S n) = True
25
25
@@ -27,20 +27,20 @@ isSucc (S n) = True
27-- Basic arithmetic functions
27-- Basic arithmetic functions
28--------------------------------------------------------------------------------
28--------------------------------------------------------------------------------
29
29
30−plus : Nat -> Nat -> Nat
30+total plus : Nat -> Nat -> Nat
31plus O right = right
31plus O right = right
32plus (S left) right = S (plus left right)
32plus (S left) right = S (plus left right)
33
33
34−mult : Nat -> Nat -> Nat
34+total mult : Nat -> Nat -> Nat
35mult O right = O
35mult O right = O
36mult (S left) right = plus right $ mult left right
36mult (S left) right = plus right $ mult left right
37
37
38−minus : Nat -> Nat -> Nat
38+total minus : Nat -> Nat -> Nat
39minus O right = O
39minus O right = O
40minus left O = left
40minus left O = left
41minus (S left) (S right) = minus left right
41minus (S left) (S right) = minus left right
42
42
43−power : Nat -> Nat -> Nat
43+total power : Nat -> Nat -> Nat
44power base O = S O
44power base O = S O
45power base (S exp) = mult base $ power base exp
45power base (S exp) = mult base $ power base exp
46
46
@@ -68,21 +68,60 @@ instance Num Nat where
68 (-) = minus
68 (-) = minus
69 (*) = mult
69 (*) = mult
70
70
71− fromInteger = intToNat where
71+ fromInteger = fromInteger'
72+ where
72 %assert_total
73 %assert_total
73− intToNat : Int -> Nat
74+ fromInteger' : Int -> Nat
74− intToNat 0 = O
75+ fromInteger' 0 = O
76+ fromInteger' n =
77+ if (n > 0) then
75− intToNat n = if (n > 0) then S (fromInteger (n-1)) else O
78+ S (fromInteger' (n - 1))
76−
79+ else
77−--------------------------------------------------------------------------------
80+ O
78−-- Division and modulus
81+
79−--------------------------------------------------------------------------------
82+record Multiplicative : Set where
83+ getMultiplicative : Nat -> Multiplicative
84+
85+record Additive : Set where
86+ getAdditive : Nat -> Additive
87+
88+instance Semigroup Multiplicative where
89+ left <.> right = getMultiplicative $ left' * right'
90+ where
91+ left' : Nat
92+ left' =
93+ case left of
94+ getMultiplicative m => m
95+
96+ right' : Nat
97+ right' =
98+ case right of
99+ getMultiplicative m => m
100+
101+instance Semigroup Additive where
102+ left <.> right = getAdditive $ left' + right'
103+ where
104+ left' : Nat
105+ left' =
106+ case left of
107+ getAdditive m => m
108+
109+ right' : Nat
110+ right' =
111+ case right of
112+ getAdditive m => m
113+
114+instance Monoid Multiplicative where
115+ neutral = getMultiplicative $ S O
116+
117+instance Monoid Additive where
118+ neutral = getAdditive $ O
80
119
81--------------------------------------------------------------------------------
120--------------------------------------------------------------------------------
82-- Auxilliary notions
121-- Auxilliary notions
83--------------------------------------------------------------------------------
122--------------------------------------------------------------------------------
84
123
85−pred : Nat -> Nat
124+total pred : Nat -> Nat
86pred O = O
125pred O = O
87pred (S n) = n
126pred (S n) = n
88
127
@@ -90,9 +129,9 @@ pred (S n) = n
90-- Fibonacci and factorial
129-- Fibonacci and factorial
91--------------------------------------------------------------------------------
130--------------------------------------------------------------------------------
92
131
93−fib : Nat -> Nat
132+total fib : Nat -> Nat
94−fib O = 0
133+fib O = O
95−fib (S O) = 1
134+fib (S O) = S O
96fib (S (S n)) = fib (S n) + fib n
135fib (S (S n)) = fib (S n) + fib n
97
136
98--------------------------------------------------------------------------------
137--------------------------------------------------------------------------------
@@ -107,113 +146,141 @@ data LTE : Nat -> Nat -> Set where
107 lteZero : LTE O right
146 lteZero : LTE O right
108 lteSucc : LTE left right -> LTE (S left) (S right)
147 lteSucc : LTE left right -> LTE (S left) (S right)
109
148
110−GTE : Nat -> Nat -> Set
149+total GTE : Nat -> Nat -> Set
111GTE left right = LTE right left
150GTE left right = LTE right left
112
151
113−LT : Nat -> Nat -> Set
152+total LT : Nat -> Nat -> Set
114LT left right = LTE (S left) right
153LT left right = LTE (S left) right
115
154
116−GT : Nat -> Nat -> Set
155+total GT : Nat -> Nat -> Set
117GT left right = LT right left
156GT left right = LT right left
118
157
119−lte : Nat -> Nat -> Bool
158+total lte : Nat -> Nat -> Bool
120lte O right = True
159lte O right = True
121lte left O = False
160lte left O = False
122lte (S left) (S right) = lte left right
161lte (S left) (S right) = lte left right
123
162
124−gte : Nat -> Nat -> Bool
163+total gte : Nat -> Nat -> Bool
125gte left right = lte right left
164gte left right = lte right left
126
165
127−lt : Nat -> Nat -> Bool
166+total lt : Nat -> Nat -> Bool
128lt left right = lte (S left) right
167lt left right = lte (S left) right
129
168
130−gt : Nat -> Nat -> Bool
169+total gt : Nat -> Nat -> Bool
131gt left right = lt right left
170gt left right = lt right left
132
171
133−minimum : Nat -> Nat -> Nat
172+total minimum : Nat -> Nat -> Nat
134minimum left right =
173minimum left right =
135 if lte left right then
174 if lte left right then
136 left
175 left
137 else
176 else
138 right
177 right
139
178
140−maximum : Nat -> Nat -> Nat
179+total maximum : Nat -> Nat -> Nat
141maximum left right =
180maximum left right =
142 if lte left right then
181 if lte left right then
143 right
182 right
144 else
183 else
145 left
184 left
146
185
186+--------------------------------------------------------------------------------
187+-- Division and modulus
188+--------------------------------------------------------------------------------
189+
190+total mod : Nat -> Nat -> Nat
191+mod left O = left
192+mod left (S right) = mod' left left right
193+ where
194+ total mod' : Nat -> Nat -> Nat -> Nat
195+ mod' O centre right = centre
196+ mod' (S left) centre right =
197+ if lte centre right then
198+ centre
199+ else
200+ mod' left (centre - (S right)) right
201+
202+total div : Nat -> Nat -> Nat
203+div left O = S left -- div by zero
204+div left (S right) = div' left left right
205+ where
206+ total div' : Nat -> Nat -> Nat -> Nat
207+ div' O centre right = O
208+ div' (S left) centre right =
209+ if lte centre right then
210+ O
211+ else
212+ S (div' left (centre - (S right)) right)
213+
147--------------------------------------------------------------------------------
214--------------------------------------------------------------------------------
148-- Properties
215-- Properties
149--------------------------------------------------------------------------------
216--------------------------------------------------------------------------------
150
217
151-- Succ
218-- Succ
152−eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->
219+total eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->
153 S left = S right
220 S left = S right
154eqSucc left right refl = refl
221eqSucc left right refl = refl
155
222
156−succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->
223+total succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->
157 left = right
224 left = right
158succInjective left right refl = refl
225succInjective left right refl = refl
159
226
160-- Plus
227-- Plus
161−plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
228+total plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
162plusZeroLeftNeutral right = refl
229plusZeroLeftNeutral right = refl
163
230
164−plusZeroRightNeutral : (left : Nat) -> left + 0 = left
231+total plusZeroRightNeutral : (left : Nat) -> left + 0 = left
165plusZeroRightNeutral O = refl
232plusZeroRightNeutral O = refl
166plusZeroRightNeutral (S n) =
233plusZeroRightNeutral (S n) =
167 let inductiveHypothesis = plusZeroRightNeutral n in
234 let inductiveHypothesis = plusZeroRightNeutral n in
168 ?plusZeroRightNeutralStepCase
235 ?plusZeroRightNeutralStepCase
169
236
170−plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
237+total plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
171 S (left + right) = left + (S right)
238 S (left + right) = left + (S right)
172plusSuccRightSucc O right = refl
239plusSuccRightSucc O right = refl
173plusSuccRightSucc (S left) right =
240plusSuccRightSucc (S left) right =
174 let inductiveHypothesis = plusSuccRightSucc left right in
241 let inductiveHypothesis = plusSuccRightSucc left right in
175 ?plusSuccRightSuccStepCase
242 ?plusSuccRightSuccStepCase
176
243
177−plusCommutative : (left : Nat) -> (right : Nat) ->
244+total plusCommutative : (left : Nat) -> (right : Nat) ->
178 left + right = right + left
245 left + right = right + left
179plusCommutative O right = ?plusCommutativeBaseCase
246plusCommutative O right = ?plusCommutativeBaseCase
180plusCommutative (S left) right =
247plusCommutative (S left) right =
181 let inductiveHypothesis = plusCommutative left right in
248 let inductiveHypothesis = plusCommutative left right in
182 ?plusCommutativeStepCase
249 ?plusCommutativeStepCase
183
250
184−plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
251+total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
185 left + (centre + right) = (left + centre) + right
252 left + (centre + right) = (left + centre) + right
186plusAssociative O centre right = refl
253plusAssociative O centre right = refl
187plusAssociative (S left) centre right =
254plusAssociative (S left) centre right =
188 let inductiveHypothesis = plusAssociative left centre right in
255 let inductiveHypothesis = plusAssociative left centre right in
189 ?plusAssociativeStepCase
256 ?plusAssociativeStepCase
190
257
191−plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
258+total plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
192 (p : left = right) -> left + c = right + c
259 (p : left = right) -> left + c = right + c
193plusConstantRight left right c refl = refl
260plusConstantRight left right c refl = refl
194
261
195−plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->
262+total plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->
196 (p : left = right) -> c + left = c + right
263 (p : left = right) -> c + left = c + right
197plusConstantLeft left right c refl = refl
264plusConstantLeft left right c refl = refl
198
265
199−plusOneSucc : (right : Nat) -> 1 + right = S right
266+total plusOneSucc : (right : Nat) -> 1 + right = S right
200plusOneSucc n = refl
267plusOneSucc n = refl
201
268
202−plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
269+total plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
203 (p : left + right = left + right') -> right = right'
270 (p : left + right = left + right') -> right = right'
204plusLeftCancel O right right' p = ?plusLeftCancelBaseCase
271plusLeftCancel O right right' p = ?plusLeftCancelBaseCase
205plusLeftCancel (S left) right right' p =
272plusLeftCancel (S left) right right' p =
206 let inductiveHypothesis = plusLeftCancel left right right' in
273 let inductiveHypothesis = plusLeftCancel left right right' in
207 ?plusLeftCancelStepCase
274 ?plusLeftCancelStepCase
208
275
209−plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
276+total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
210 (p : left + right = left' + right) -> left = left'
277 (p : left + right = left' + right) -> left = left'
211plusRightCancel left left' O p = ?plusRightCancelBaseCase
278plusRightCancel left left' O p = ?plusRightCancelBaseCase
212plusRightCancel left left' (S right) p =
279plusRightCancel left left' (S right) p =
213 let inductiveHypothesis = plusRightCancel left left' right in
280 let inductiveHypothesis = plusRightCancel left left' right in
214 ?plusRightCancelStepCase
281 ?plusRightCancelStepCase
215
282
216−plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
283+total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
217 (p : left + right = left) -> right = O
284 (p : left + right = left) -> right = O
218plusLeftLeftRightZero O right p = ?plusLeftLeftRightZeroBaseCase
285plusLeftLeftRightZero O right p = ?plusLeftLeftRightZeroBaseCase
219plusLeftLeftRightZero (S left) right p =
286plusLeftLeftRightZero (S left) right p =
@@ -221,95 +288,95 @@ plusLeftLeftRightZero (S left) right p =
221 ?plusLeftLeftRightZeroStepCase
288 ?plusLeftLeftRightZeroStepCase
222
289
223-- Mult
290-- Mult
224−multZeroLeftZero : (right : Nat) -> O * right = O
291+total multZeroLeftZero : (right : Nat) -> O * right = O
225multZeroLeftZero right = refl
292multZeroLeftZero right = refl
226
293
227−multZeroRightZero : (left : Nat) -> left * O = O
294+total multZeroRightZero : (left : Nat) -> left * O = O
228multZeroRightZero O = refl
295multZeroRightZero O = refl
229multZeroRightZero (S left) =
296multZeroRightZero (S left) =
230 let inductiveHypothesis = multZeroRightZero left in
297 let inductiveHypothesis = multZeroRightZero left in
231 ?multZeroRightZeroStepCase
298 ?multZeroRightZeroStepCase
232
299
233−multRightSuccPlus : (left : Nat) -> (right : Nat) ->
300+total multRightSuccPlus : (left : Nat) -> (right : Nat) ->
234 left * (S right) = left + (left * right)
301 left * (S right) = left + (left * right)
235multRightSuccPlus O right = refl
302multRightSuccPlus O right = refl
236multRightSuccPlus (S left) right =
303multRightSuccPlus (S left) right =
237 let inductiveHypothesis = multRightSuccPlus left right in
304 let inductiveHypothesis = multRightSuccPlus left right in
238 ?multRightSuccPlusStepCase
305 ?multRightSuccPlusStepCase
239
306
240−multLeftSuccPlus : (left : Nat) -> (right : Nat) ->
307+total multLeftSuccPlus : (left : Nat) -> (right : Nat) ->
241 (S left) * right = right + (left * right)
308 (S left) * right = right + (left * right)
242multLeftSuccPlus left right = refl
309multLeftSuccPlus left right = refl
243
310
244−multCommutative : (left : Nat) -> (right : Nat) ->
311+total multCommutative : (left : Nat) -> (right : Nat) ->
245 left * right = right * left
312 left * right = right * left
246multCommutative O right = ?multCommutativeBaseCase
313multCommutative O right = ?multCommutativeBaseCase
247multCommutative (S left) right =
314multCommutative (S left) right =
248 let inductiveHypothesis = multCommutative left right in
315 let inductiveHypothesis = multCommutative left right in
249 ?multCommutativeStepCase
316 ?multCommutativeStepCase
250
317
251−multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
318+total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
252 left * (centre + right) = (left * centre) + (left * right)
319 left * (centre + right) = (left * centre) + (left * right)
253multDistributesOverPlusRight O centre right = refl
320multDistributesOverPlusRight O centre right = refl
254multDistributesOverPlusRight (S left) centre right =
321multDistributesOverPlusRight (S left) centre right =
255 let inductiveHypothesis = multDistributesOverPlusRight left centre right in
322 let inductiveHypothesis = multDistributesOverPlusRight left centre right in
256 ?multDistributesOverPlusRightStepCase
323 ?multDistributesOverPlusRightStepCase
257
324
258−multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
325+total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
259 (left + centre) * right = (left * right) + (centre * right)
326 (left + centre) * right = (left * right) + (centre * right)
260multDistributesOverPlusLeft O centre right = refl
327multDistributesOverPlusLeft O centre right = refl
261multDistributesOverPlusLeft (S left) centre right =
328multDistributesOverPlusLeft (S left) centre right =
262 let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
329 let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
263 ?multDistributesOverPlusLeftStepCase
330 ?multDistributesOverPlusLeftStepCase
264
331
265−multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
332+total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
266 left * (centre * right) = (left * centre) * right
333 left * (centre * right) = (left * centre) * right
267multAssociative O centre right = refl
334multAssociative O centre right = refl
268multAssociative (S left) centre right =
335multAssociative (S left) centre right =
269 let inductiveHypothesis = multAssociative left centre right in
336 let inductiveHypothesis = multAssociative left centre right in
270 ?multAssociativeStepCase
337 ?multAssociativeStepCase
271
338
272−multOneLeftNeutral : (right : Nat) -> 1 * right = right
339+total multOneLeftNeutral : (right : Nat) -> 1 * right = right
273multOneLeftNeutral O = refl
340multOneLeftNeutral O = refl
274multOneLeftNeutral (S right) =
341multOneLeftNeutral (S right) =
275 let inductiveHypothesis = multOneLeftNeutral right in
342 let inductiveHypothesis = multOneLeftNeutral right in
276 ?multOneLeftNeutralStepCase
343 ?multOneLeftNeutralStepCase
277
344
278−multOneRightNeutral : (left : Nat) -> left * 1 = left
345+total multOneRightNeutral : (left : Nat) -> left * 1 = left
279multOneRightNeutral O = refl
346multOneRightNeutral O = refl
280multOneRightNeutral (S left) =
347multOneRightNeutral (S left) =
281 let inductiveHypothesis = multOneRightNeutral left in
348 let inductiveHypothesis = multOneRightNeutral left in
282 ?multOneRightNeutralStepCase
349 ?multOneRightNeutralStepCase
283
350
284-- Minus
351-- Minus
285−minusSuccSucc : (left : Nat) -> (right : Nat) ->
352+total minusSuccSucc : (left : Nat) -> (right : Nat) ->
286 (S left) - (S right) = left - right
353 (S left) - (S right) = left - right
287minusSuccSucc left right = refl
354minusSuccSucc left right = refl
288
355
289−minusZeroLeft : (right : Nat) -> 0 - right = O
356+total minusZeroLeft : (right : Nat) -> 0 - right = O
290minusZeroLeft right = refl
357minusZeroLeft right = refl
291
358
292−minusZeroRight : (left : Nat) -> left - 0 = left
359+total minusZeroRight : (left : Nat) -> left - 0 = left
293minusZeroRight O = refl
360minusZeroRight O = refl
294minusZeroRight (S left) = refl
361minusZeroRight (S left) = refl
295
362
296−minusZeroN : (n : Nat) -> O = n - n
363+total minusZeroN : (n : Nat) -> O = n - n
297minusZeroN O = refl
364minusZeroN O = refl
298minusZeroN (S n) = minusZeroN n
365minusZeroN (S n) = minusZeroN n
299
366
300−minusOneSuccN : (n : Nat) -> S O = (S n) - n
367+total minusOneSuccN : (n : Nat) -> S O = (S n) - n
301minusOneSuccN O = refl
368minusOneSuccN O = refl
302minusOneSuccN (S n) = minusOneSuccN n
369minusOneSuccN (S n) = minusOneSuccN n
303
370
304−minusSuccOne : (n : Nat) -> S n - 1 = n
371+total minusSuccOne : (n : Nat) -> S n - 1 = n
305minusSuccOne O = refl
372minusSuccOne O = refl
306minusSuccOne (S n) = refl
373minusSuccOne (S n) = refl
307
374
308−minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = O
375+total minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = O
309minusPlusZero O m = refl
376minusPlusZero O m = refl
310minusPlusZero (S n) m = minusPlusZero n m
377minusPlusZero (S n) m = minusPlusZero n m
311
378
312−minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
379+total minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
313 left - centre - right = left - (centre + right)
380 left - centre - right = left - (centre + right)
314minusMinusMinusPlus O O right = refl
381minusMinusMinusPlus O O right = refl
315minusMinusMinusPlus (S left) O right = refl
382minusMinusMinusPlus (S left) O right = refl
@@ -318,14 +385,14 @@ minusMinusMinusPlus (S left) (S centre) right =
318 let inductiveHypothesis = minusMinusMinusPlus left centre right in
385 let inductiveHypothesis = minusMinusMinusPlus left centre right in
319 ?minusMinusMinusPlusStepCase
386 ?minusMinusMinusPlusStepCase
320
387
321−plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
388+total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
322 (left + right) - (left + right') = right - right'
389 (left + right) - (left + right') = right - right'
323plusMinusLeftCancel O right right' = refl
390plusMinusLeftCancel O right right' = refl
324plusMinusLeftCancel (S left) right right' =
391plusMinusLeftCancel (S left) right right' =
325 let inductiveHypothesis = plusMinusLeftCancel left right right' in
392 let inductiveHypothesis = plusMinusLeftCancel left right right' in
326 ?plusMinusLeftCancelStepCase
393 ?plusMinusLeftCancelStepCase
327
394
328−multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
395+total multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
329 (left - centre) * right = (left * right) - (centre * right)
396 (left - centre) * right = (left * right) - (centre * right)
330multDistributesOverMinusLeft O O right = refl
397multDistributesOverMinusLeft O O right = refl
331multDistributesOverMinusLeft (S left) O right =
398multDistributesOverMinusLeft (S left) O right =
@@ -335,45 +402,45 @@ multDistributesOverMinusLeft (S left) (S centre) right =
335 let inductiveHypothesis = multDistributesOverMinusLeft left centre right in
402 let inductiveHypothesis = multDistributesOverMinusLeft left centre right in
336 ?multDistributesOverMinusLeftStepCase
403 ?multDistributesOverMinusLeftStepCase
337
404
338−multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
405+total multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
339 left * (centre - right) = (left * centre) - (left * right)
406 left * (centre - right) = (left * centre) - (left * right)
340multDistributesOverMinusRight left centre right =
407multDistributesOverMinusRight left centre right =
341 ?multDistributesOverMinusRightBody
408 ?multDistributesOverMinusRightBody
342
409
343-- Power
410-- Power
344−powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =
411+total powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =
345 base * (power base exp)
412 base * (power base exp)
346powerSuccPowerLeft base exp = refl
413powerSuccPowerLeft base exp = refl
347
414
348−multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
415+total multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
349 (power base exp) * (power base exp') = power base (exp + exp')
416 (power base exp) * (power base exp') = power base (exp + exp')
350multPowerPowerPlus base O exp' = ?multPowerPowerPlusBaseCase
417multPowerPowerPlus base O exp' = ?multPowerPowerPlusBaseCase
351multPowerPowerPlus base (S exp) exp' =
418multPowerPowerPlus base (S exp) exp' =
352 let inductiveHypothesis = multPowerPowerPlus base exp exp' in
419 let inductiveHypothesis = multPowerPowerPlus base exp exp' in
353 ?multPowerPowerPlusStepCase
420 ?multPowerPowerPlusStepCase
354
421
355−powerZeroOne : (base : Nat) -> power base 0 = S O
422+total powerZeroOne : (base : Nat) -> power base 0 = S O
356powerZeroOne base = refl
423powerZeroOne base = refl
357
424
358−powerOneNeutral : (base : Nat) -> power base 1 = base
425+total powerOneNeutral : (base : Nat) -> power base 1 = base
359powerOneNeutral O = refl
426powerOneNeutral O = refl
360powerOneNeutral (S base) =
427powerOneNeutral (S base) =
361 let inductiveHypothesis = powerOneNeutral base in
428 let inductiveHypothesis = powerOneNeutral base in
362 ?powerOneNeutralStepCase
429 ?powerOneNeutralStepCase
363
430
364−powerOneSuccOne : (exp : Nat) -> power 1 exp = S O
431+total powerOneSuccOne : (exp : Nat) -> power 1 exp = S O
365powerOneSuccOne O = refl
432powerOneSuccOne O = refl
366powerOneSuccOne (S exp) =
433powerOneSuccOne (S exp) =
367 let inductiveHypothesis = powerOneSuccOne exp in
434 let inductiveHypothesis = powerOneSuccOne exp in
368 ?powerOneSuccOneStepCase
435 ?powerOneSuccOneStepCase
369
436
370−powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
437+total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
371powerSuccSuccMult O = refl
438powerSuccSuccMult O = refl
372powerSuccSuccMult (S base) =
439powerSuccSuccMult (S base) =
373 let inductiveHypothesis = powerSuccSuccMult base in
440 let inductiveHypothesis = powerSuccSuccMult base in
374 ?powerSuccSuccMultStepCase
441 ?powerSuccSuccMultStepCase
375
442
376−powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
443+total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
377 power (power base exp) exp' = power base (exp * exp')
444 power (power base exp) exp' = power base (exp * exp')
378powerPowerMultPower base exp O = ?powerPowerMultPowerBaseCase
445powerPowerMultPower base exp O = ?powerPowerMultPowerBaseCase
379powerPowerMultPower base exp (S exp') =
446powerPowerMultPower base exp (S exp') =
@@ -381,10 +448,10 @@ powerPowerMultPower base exp (S exp') =
381 ?powerPowerMultPowerStepCase
448 ?powerPowerMultPowerStepCase
382
449
383-- Pred
450-- Pred
384−predSucc : (n : Nat) -> pred (S n) = n
451+total predSucc : (n : Nat) -> pred (S n) = n
385predSucc n = refl
452predSucc n = refl
386
453
387−minusSuccPred : (left : Nat) -> (right : Nat) ->
454+total minusSuccPred : (left : Nat) -> (right : Nat) ->
388 left - (S right) = pred (left - right)
455 left - (S right) = pred (left - right)
389minusSuccPred O right = refl
456minusSuccPred O right = refl
390minusSuccPred (S left) O =
457minusSuccPred (S left) O =
@@ -395,50 +462,50 @@ minusSuccPred (S left) (S right) =
395 ?minusSuccPredStepCase'
462 ?minusSuccPredStepCase'
396
463
397-- boolElim
464-- boolElim
398−boolElimSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) ->
465+total boolElimSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) ->
399 S (boolElim cond t f) = boolElim cond (S t) (S f)
466 S (boolElim cond t f) = boolElim cond (S t) (S f)
400boolElimSuccSucc True t f = refl
467boolElimSuccSucc True t f = refl
401boolElimSuccSucc False t f = refl
468boolElimSuccSucc False t f = refl
402
469
403−boolElimPlusPlusLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->
470+total boolElimPlusPlusLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->
404 left + (boolElim cond t f) = boolElim cond (left + t) (left + f)
471 left + (boolElim cond t f) = boolElim cond (left + t) (left + f)
405boolElimPlusPlusLeft True left t f = refl
472boolElimPlusPlusLeft True left t f = refl
406boolElimPlusPlusLeft False left t f = refl
473boolElimPlusPlusLeft False left t f = refl
407
474
408−boolElimPlusPlusRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->
475+total boolElimPlusPlusRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->
409 (boolElim cond t f) + right = boolElim cond (t + right) (f + right)
476 (boolElim cond t f) + right = boolElim cond (t + right) (f + right)
410boolElimPlusPlusRight True right t f = refl
477boolElimPlusPlusRight True right t f = refl
411boolElimPlusPlusRight False right t f = refl
478boolElimPlusPlusRight False right t f = refl
412
479
413−boolElimMultMultLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->
480+total boolElimMultMultLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->
414 left * (boolElim cond t f) = boolElim cond (left * t) (left * f)
481 left * (boolElim cond t f) = boolElim cond (left * t) (left * f)
415boolElimMultMultLeft True left t f = refl
482boolElimMultMultLeft True left t f = refl
416boolElimMultMultLeft False left t f = refl
483boolElimMultMultLeft False left t f = refl
417
484
418−boolElimMultMultRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->
485+total boolElimMultMultRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->
419 (boolElim cond t f) * right = boolElim cond (t * right) (f * right)
486 (boolElim cond t f) * right = boolElim cond (t * right) (f * right)
420boolElimMultMultRight True right t f = refl
487boolElimMultMultRight True right t f = refl
421boolElimMultMultRight False right t f = refl
488boolElimMultMultRight False right t f = refl
422
489
423-- Orders
490-- Orders
424−lteNTrue : (n : Nat) -> lte n n = True
491+total lteNTrue : (n : Nat) -> lte n n = True
425lteNTrue O = refl
492lteNTrue O = refl
426lteNTrue (S n) = lteNTrue n
493lteNTrue (S n) = lteNTrue n
427
494
428−lteSuccZeroFalse : (n : Nat) -> lte (S n) O = False
495+total lteSuccZeroFalse : (n : Nat) -> lte (S n) O = False
429lteSuccZeroFalse O = refl
496lteSuccZeroFalse O = refl
430lteSuccZeroFalse (S n) = refl
497lteSuccZeroFalse (S n) = refl
431
498
432-- Minimum and maximum
499-- Minimum and maximum
433−minimumZeroZeroRight : (right : Nat) -> minimum 0 right = O
500+total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = O
434minimumZeroZeroRight O = refl
501minimumZeroZeroRight O = refl
435minimumZeroZeroRight (S right) = minimumZeroZeroRight right
502minimumZeroZeroRight (S right) = minimumZeroZeroRight right
436
503
437−minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = O
504+total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = O
438minimumZeroZeroLeft O = refl
505minimumZeroZeroLeft O = refl
439minimumZeroZeroLeft (S left) = refl
506minimumZeroZeroLeft (S left) = refl
440
507
441−minimumSuccSucc : (left : Nat) -> (right : Nat) ->
508+total minimumSuccSucc : (left : Nat) -> (right : Nat) ->
442 minimum (S left) (S right) = S (minimum left right)
509 minimum (S left) (S right) = S (minimum left right)
443minimumSuccSucc O O = refl
510minimumSuccSucc O O = refl
444minimumSuccSucc (S left) O = refl
511minimumSuccSucc (S left) O = refl
@@ -447,7 +514,7 @@ minimumSuccSucc (S left) (S right) =
447 let inductiveHypothesis = minimumSuccSucc left right in
514 let inductiveHypothesis = minimumSuccSucc left right in
448 ?minimumSuccSuccStepCase
515 ?minimumSuccSuccStepCase
449
516
450−minimumCommutative : (left : Nat) -> (right : Nat) ->
517+total minimumCommutative : (left : Nat) -> (right : Nat) ->
451 minimum left right = minimum right left
518 minimum left right = minimum right left
452minimumCommutative O O = refl
519minimumCommutative O O = refl
453minimumCommutative O (S right) = refl
520minimumCommutative O (S right) = refl
@@ -456,15 +523,15 @@ minimumCommutative (S left) (S right) =
456 let inductiveHypothesis = minimumCommutative left right in
523 let inductiveHypothesis = minimumCommutative left right in
457 ?minimumCommutativeStepCase
524 ?minimumCommutativeStepCase
458
525
459−maximumZeroNRight : (right : Nat) -> maximum O right = right
526+total maximumZeroNRight : (right : Nat) -> maximum O right = right
460maximumZeroNRight O = refl
527maximumZeroNRight O = refl
461maximumZeroNRight (S right) = refl
528maximumZeroNRight (S right) = refl
462
529
463−maximumZeroNLeft : (left : Nat) -> maximum left O = left
530+total maximumZeroNLeft : (left : Nat) -> maximum left O = left
464maximumZeroNLeft O = refl
531maximumZeroNLeft O = refl
465maximumZeroNLeft (S left) = refl
532maximumZeroNLeft (S left) = refl
466
533
467−maximumSuccSucc : (left : Nat) -> (right : Nat) ->
534+total maximumSuccSucc : (left : Nat) -> (right : Nat) ->
468 S (maximum left right) = maximum (S left) (S right)
535 S (maximum left right) = maximum (S left) (S right)
469maximumSuccSucc O O = refl
536maximumSuccSucc O O = refl
470maximumSuccSucc (S left) O = refl
537maximumSuccSucc (S left) O = refl
@@ -473,7 +540,7 @@ maximumSuccSucc (S left) (S right) =
473 let inductiveHypothesis = maximumSuccSucc left right in
540 let inductiveHypothesis = maximumSuccSucc left right in
474 ?maximumSuccSuccStepCase
541 ?maximumSuccSuccStepCase
475
542
476−maximumCommutative : (left : Nat) -> (right : Nat) ->
543+total maximumCommutative : (left : Nat) -> (right : Nat) ->
477 maximum left right = maximum right left
544 maximum left right = maximum right left
478maximumCommutative O O = refl
545maximumCommutative O O = refl
479maximumCommutative (S left) O = refl
546maximumCommutative (S left) O = refl
@@ -482,6 +549,11 @@ maximumCommutative (S left) (S right) =
482 let inductiveHypothesis = maximumCommutative left right in
549 let inductiveHypothesis = maximumCommutative left right in
483 ?maximumCommutativeStepCase
550 ?maximumCommutativeStepCase
484
551
552+-- div and mod
553+total modZeroZero : (n : Nat) -> mod 0 n = O
554+modZeroZero O = refl
555+modZeroZero (S n) = refl
556+
485--------------------------------------------------------------------------------
557--------------------------------------------------------------------------------
486-- Proofs
558-- Proofs
487--------------------------------------------------------------------------------
559--------------------------------------------------------------------------------
@@ -642,6 +714,9 @@ plusZeroRightNeutralStepCase = proof {
642 trivial;
714 trivial;
643}
715}
644
716
717+
718+---------- Proofs ----------
719+
645maximumCommutativeStepCase = proof {
720maximumCommutativeStepCase = proof {
646 intros;
721 intros;
647 rewrite (boolElimSuccSucc (lte left right) right left);
722 rewrite (boolElimSuccSucc (lte left right) right left);