git.iko.soy/Idris-dev
on master help sign in
Merge pull request #7 from dpmulligan/master
86c2beeEdwin Brady
lib/prelude/nat.idr+294−40
compare with master
unifiedsplit
@@ -91,9 +91,9 @@ pred (S n) = n
91--------------------------------------------------------------------------------
91--------------------------------------------------------------------------------
92
92
93fib : Nat -> Nat
93fib : Nat -> Nat
94−fib O = O
94+fib O = 0
95−fib (S O) = S O
95+fib (S O) = 1
96−fib (S (S n)) = plus (fib (S n)) (fib n)
96+fib (S (S n)) = fib (S n) + fib n
97
97
98--------------------------------------------------------------------------------
98--------------------------------------------------------------------------------
99-- GCD and LCM
99-- GCD and LCM
@@ -149,112 +149,133 @@ maximum left right =
149--------------------------------------------------------------------------------
149--------------------------------------------------------------------------------
150
150
151-- Succ
151-- Succ
152−succMonotonic : (left : Nat) -> (right : Nat) -> (p : left = right) ->
152+eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->
153 S left = S right
153 S left = S right
154−succMonotonic left right refl = refl
154+eqSucc left right refl = refl
155
155
156succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->
156succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->
157 left = right
157 left = right
158succInjective left right refl = refl
158succInjective left right refl = refl
159
159
160-- Plus
160-- Plus
161−plusZeroLeftNeutral : (right : Nat) -> plus O right = right
161+plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
162plusZeroLeftNeutral right = refl
162plusZeroLeftNeutral right = refl
163
163
164−plusZeroRightNeutral : (left : Nat) -> plus left O = left
164+plusZeroRightNeutral : (left : Nat) -> left + 0 = left
165plusZeroRightNeutral O = refl
165plusZeroRightNeutral O = refl
166plusZeroRightNeutral (S n) =
166plusZeroRightNeutral (S n) =
167 let inductiveHypothesis = plusZeroRightNeutral n in
167 let inductiveHypothesis = plusZeroRightNeutral n in
168 ?plusZeroRightNeutralStepCase
168 ?plusZeroRightNeutralStepCase
169
169
170plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
170plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
171− S (plus left right) = plus left (S right)
171+ S (left + right) = left + (S right)
172plusSuccRightSucc O right = refl
172plusSuccRightSucc O right = refl
173plusSuccRightSucc (S left) right =
173plusSuccRightSucc (S left) right =
174 let inductiveHypothesis = plusSuccRightSucc left right in
174 let inductiveHypothesis = plusSuccRightSucc left right in
175 ?plusSuccRightSuccStepCase
175 ?plusSuccRightSuccStepCase
176
176
177plusCommutative : (left : Nat) -> (right : Nat) ->
177plusCommutative : (left : Nat) -> (right : Nat) ->
178− plus left right = plus right left
178+ left + right = right + left
179plusCommutative O right = ?plusCommutativeBaseCase
179plusCommutative O right = ?plusCommutativeBaseCase
180plusCommutative (S left) right =
180plusCommutative (S left) right =
181 let inductiveHypothesis = plusCommutative left right in
181 let inductiveHypothesis = plusCommutative left right in
182 ?plusCommutativeStepCase
182 ?plusCommutativeStepCase
183
183
184plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
184plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
185− plus left (plus centre right) = plus (plus left centre) right
185+ left + (centre + right) = (left + centre) + right
186plusAssociative O centre right = refl
186plusAssociative O centre right = refl
187plusAssociative (S left) centre right =
187plusAssociative (S left) centre right =
188 let inductiveHypothesis = plusAssociative left centre right in
188 let inductiveHypothesis = plusAssociative left centre right in
189 ?plusAssociativeStepCase
189 ?plusAssociativeStepCase
190
190
191−plusMonotonicRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
191+plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
192− (p : left = right) -> plus left c = plus right c
192+ (p : left = right) -> left + c = right + c
193−plusMonotonicRight left right c refl = refl
193+plusConstantRight left right c refl = refl
194
194
195−plusMonotonicLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->
195+plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->
196− (p : left = right) -> plus c left = plus c right
196+ (p : left = right) -> c + left = c + right
197−plusMonotonicLeft left right c refl = refl
197+plusConstantLeft left right c refl = refl
198
198
199−plusOneSucc : (right : Nat) -> plus (S O) right = S right
199+plusOneSucc : (right : Nat) -> 1 + right = S right
200plusOneSucc n = refl
200plusOneSucc n = refl
201
201
202+plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
203+ (p : left + right = left + right') -> right = right'
204+plusLeftCancel O right right' p = ?plusLeftCancelBaseCase
205+plusLeftCancel (S left) right right' p =
206+ let inductiveHypothesis = plusLeftCancel left right right' in
207+ ?plusLeftCancelStepCase
208+
209+plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
210+ (p : left + right = left' + right) -> left = left'
211+plusRightCancel left left' O p = ?plusRightCancelBaseCase
212+plusRightCancel left left' (S right) p =
213+ let inductiveHypothesis = plusRightCancel left left' right in
214+ ?plusRightCancelStepCase
215+
216+plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
217+ (p : left + right = left) -> right = O
218+plusLeftLeftRightZero O right p = ?plusLeftLeftRightZeroBaseCase
219+plusLeftLeftRightZero (S left) right p =
220+ let inductiveHypothesis = plusLeftLeftRightZero left right in
221+ ?plusLeftLeftRightZeroStepCase
222+
202-- Mult
223-- Mult
203−multZeroLeftZero : (right : Nat) -> mult O right = O
224+multZeroLeftZero : (right : Nat) -> O * right = O
204multZeroLeftZero right = refl
225multZeroLeftZero right = refl
205
226
206−multZeroRightZero : (left : Nat) -> mult left O = O
227+multZeroRightZero : (left : Nat) -> left * O = O
207multZeroRightZero O = refl
228multZeroRightZero O = refl
208multZeroRightZero (S left) =
229multZeroRightZero (S left) =
209 let inductiveHypothesis = multZeroRightZero left in
230 let inductiveHypothesis = multZeroRightZero left in
210 ?multZeroRightZeroStepCase
231 ?multZeroRightZeroStepCase
211
232
212multRightSuccPlus : (left : Nat) -> (right : Nat) ->
233multRightSuccPlus : (left : Nat) -> (right : Nat) ->
213− mult left (S right) = plus left (mult left right)
234+ left * (S right) = left + (left * right)
214multRightSuccPlus O right = refl
235multRightSuccPlus O right = refl
215multRightSuccPlus (S left) right =
236multRightSuccPlus (S left) right =
216 let inductiveHypothesis = multRightSuccPlus left right in
237 let inductiveHypothesis = multRightSuccPlus left right in
217 ?multRightSuccPlusStepCase
238 ?multRightSuccPlusStepCase
218
239
219multLeftSuccPlus : (left : Nat) -> (right : Nat) ->
240multLeftSuccPlus : (left : Nat) -> (right : Nat) ->
220− mult (S left) right = plus right (mult left right)
241+ (S left) * right = right + (left * right)
221multLeftSuccPlus left right = refl
242multLeftSuccPlus left right = refl
222
243
223multCommutative : (left : Nat) -> (right : Nat) ->
244multCommutative : (left : Nat) -> (right : Nat) ->
224− mult left right = mult right left
245+ left * right = right * left
225multCommutative O right = ?multCommutativeBaseCase
246multCommutative O right = ?multCommutativeBaseCase
226multCommutative (S left) right =
247multCommutative (S left) right =
227 let inductiveHypothesis = multCommutative left right in
248 let inductiveHypothesis = multCommutative left right in
228 ?multCommutativeStepCase
249 ?multCommutativeStepCase
229
250
230multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
251multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
231− mult left (plus centre right) = plus (mult left centre) (mult left right)
252+ left * (centre + right) = (left * centre) + (left * right)
232multDistributesOverPlusRight O centre right = refl
253multDistributesOverPlusRight O centre right = refl
233multDistributesOverPlusRight (S left) centre right =
254multDistributesOverPlusRight (S left) centre right =
234 let inductiveHypothesis = multDistributesOverPlusRight left centre right in
255 let inductiveHypothesis = multDistributesOverPlusRight left centre right in
235 ?multDistributesOverPlusRightStepCase
256 ?multDistributesOverPlusRightStepCase
236
257
237multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
258multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
238− mult (plus left centre) right = plus (mult left right) (mult centre right)
259+ (left + centre) * right = (left * right) + (centre * right)
239multDistributesOverPlusLeft O centre right = refl
260multDistributesOverPlusLeft O centre right = refl
240multDistributesOverPlusLeft (S left) centre right =
261multDistributesOverPlusLeft (S left) centre right =
241 let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
262 let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
242 ?multDistributesOverPlusLeftStepCase
263 ?multDistributesOverPlusLeftStepCase
243
264
244multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
265multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
245− mult left (mult centre right) = mult (mult left centre) right
266+ left * (centre * right) = (left * centre) * right
246multAssociative O centre right = refl
267multAssociative O centre right = refl
247multAssociative (S left) centre right =
268multAssociative (S left) centre right =
248 let inductiveHypothesis = multAssociative left centre right in
269 let inductiveHypothesis = multAssociative left centre right in
249 ?multAssociativeStepCase
270 ?multAssociativeStepCase
250
271
251−multOneLeftNeutral : (right : Nat) -> mult (S O) right = right
272+multOneLeftNeutral : (right : Nat) -> 1 * right = right
252multOneLeftNeutral O = refl
273multOneLeftNeutral O = refl
253multOneLeftNeutral (S right) =
274multOneLeftNeutral (S right) =
254 let inductiveHypothesis = multOneLeftNeutral right in
275 let inductiveHypothesis = multOneLeftNeutral right in
255 ?multOneLeftNeutralStepCase
276 ?multOneLeftNeutralStepCase
256
277
257−multOneRightNeutral : (left : Nat) -> mult left (S O) = left
278+multOneRightNeutral : (left : Nat) -> left * 1 = left
258multOneRightNeutral O = refl
279multOneRightNeutral O = refl
259multOneRightNeutral (S left) =
280multOneRightNeutral (S left) =
260 let inductiveHypothesis = multOneRightNeutral left in
281 let inductiveHypothesis = multOneRightNeutral left in
@@ -262,59 +283,98 @@ multOneRightNeutral (S left) =
262
283
263-- Minus
284-- Minus
264minusSuccSucc : (left : Nat) -> (right : Nat) ->
285minusSuccSucc : (left : Nat) -> (right : Nat) ->
265− minus (S left) (S right) = minus left right
286+ (S left) - (S right) = left - right
266minusSuccSucc left right = refl
287minusSuccSucc left right = refl
267
288
268−minusZeroLeft : (right : Nat) -> minus O right = O
289+minusZeroLeft : (right : Nat) -> 0 - right = O
269minusZeroLeft right = refl
290minusZeroLeft right = refl
270
291
271−minusZeroRight : (left : Nat) -> minus left O = left
292+minusZeroRight : (left : Nat) -> left - 0 = left
272minusZeroRight O = refl
293minusZeroRight O = refl
273minusZeroRight (S left) = refl
294minusZeroRight (S left) = refl
274
295
275−minusZeroN : (n : Nat) -> O = minus n n
296+minusZeroN : (n : Nat) -> O = n - n
276minusZeroN O = refl
297minusZeroN O = refl
277minusZeroN (S n) = minusZeroN n
298minusZeroN (S n) = minusZeroN n
278
299
279−minusOneSuccN : (n : Nat) -> S O = minus (S n) n
300+minusOneSuccN : (n : Nat) -> S O = (S n) - n
280minusOneSuccN O = refl
301minusOneSuccN O = refl
281minusOneSuccN (S n) = minusOneSuccN n
302minusOneSuccN (S n) = minusOneSuccN n
282
303
304+minusSuccOne : (n : Nat) -> S n - 1 = n
305+minusSuccOne O = refl
306+minusSuccOne (S n) = refl
307+
308+minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = O
309+minusPlusZero O m = refl
310+minusPlusZero (S n) m = minusPlusZero n m
311+
312+minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
313+ left - centre - right = left - (centre + right)
314+minusMinusMinusPlus O O right = refl
315+minusMinusMinusPlus (S left) O right = refl
316+minusMinusMinusPlus O (S centre) right = refl
317+minusMinusMinusPlus (S left) (S centre) right =
318+ let inductiveHypothesis = minusMinusMinusPlus left centre right in
319+ ?minusMinusMinusPlusStepCase
320+
321+plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
322+ (left + right) - (left + right') = right - right'
323+plusMinusLeftCancel O right right' = refl
324+plusMinusLeftCancel (S left) right right' =
325+ let inductiveHypothesis = plusMinusLeftCancel left right right' in
326+ ?plusMinusLeftCancelStepCase
327+
328+multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
329+ (left - centre) * right = (left * right) - (centre * right)
330+multDistributesOverMinusLeft O O right = refl
331+multDistributesOverMinusLeft (S left) O right =
332+ ?multDistributesOverMinusLeftBaseCase
333+multDistributesOverMinusLeft O (S centre) right = refl
334+multDistributesOverMinusLeft (S left) (S centre) right =
335+ let inductiveHypothesis = multDistributesOverMinusLeft left centre right in
336+ ?multDistributesOverMinusLeftStepCase
337+
338+multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
339+ left * (centre - right) = (left * centre) - (left * right)
340+multDistributesOverMinusRight left centre right =
341+ ?multDistributesOverMinusRightBody
342+
283-- Power
343-- Power
284powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =
344powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =
285− mult base (power base exp)
345+ base * (power base exp)
286powerSuccPowerLeft base exp = refl
346powerSuccPowerLeft base exp = refl
287
347
288multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
348multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
289− mult (power base exp) (power base exp') = power base (plus exp exp')
349+ (power base exp) * (power base exp') = power base (exp + exp')
290multPowerPowerPlus base O exp' = ?multPowerPowerPlusBaseCase
350multPowerPowerPlus base O exp' = ?multPowerPowerPlusBaseCase
291multPowerPowerPlus base (S exp) exp' =
351multPowerPowerPlus base (S exp) exp' =
292 let inductiveHypothesis = multPowerPowerPlus base exp exp' in
352 let inductiveHypothesis = multPowerPowerPlus base exp exp' in
293 ?multPowerPowerPlusStepCase
353 ?multPowerPowerPlusStepCase
294
354
295−powerZeroOne : (base : Nat) -> power base O = S O
355+powerZeroOne : (base : Nat) -> power base 0 = S O
296powerZeroOne base = refl
356powerZeroOne base = refl
297
357
298−powerOneNeutral : (base : Nat) -> power base (S O) = base
358+powerOneNeutral : (base : Nat) -> power base 1 = base
299powerOneNeutral O = refl
359powerOneNeutral O = refl
300powerOneNeutral (S base) =
360powerOneNeutral (S base) =
301 let inductiveHypothesis = powerOneNeutral base in
361 let inductiveHypothesis = powerOneNeutral base in
302 ?powerOneNeutralStepCase
362 ?powerOneNeutralStepCase
303
363
304−powerOneSuccOne : (exp : Nat) -> power (S O) exp = S O
364+powerOneSuccOne : (exp : Nat) -> power 1 exp = S O
305powerOneSuccOne O = refl
365powerOneSuccOne O = refl
306powerOneSuccOne (S exp) =
366powerOneSuccOne (S exp) =
307 let inductiveHypothesis = powerOneSuccOne exp in
367 let inductiveHypothesis = powerOneSuccOne exp in
308 ?powerOneSuccOneStepCase
368 ?powerOneSuccOneStepCase
309
369
310−powerSuccSuccMult : (base : Nat) -> power base (S (S O)) = mult base base
370+powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
311powerSuccSuccMult O = refl
371powerSuccSuccMult O = refl
312powerSuccSuccMult (S base) =
372powerSuccSuccMult (S base) =
313 let inductiveHypothesis = powerSuccSuccMult base in
373 let inductiveHypothesis = powerSuccSuccMult base in
314 ?powerSuccSuccMultStepCase
374 ?powerSuccSuccMultStepCase
315
375
316powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
376powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
317− power (power base exp) exp' = power base (mult exp exp')
377+ power (power base exp) exp' = power base (exp * exp')
318powerPowerMultPower base exp O = ?powerPowerMultPowerBaseCase
378powerPowerMultPower base exp O = ?powerPowerMultPowerBaseCase
319powerPowerMultPower base exp (S exp') =
379powerPowerMultPower base exp (S exp') =
320 let inductiveHypothesis = powerPowerMultPower base exp exp' in
380 let inductiveHypothesis = powerPowerMultPower base exp exp' in
@@ -325,7 +385,7 @@ predSucc : (n : Nat) -> pred (S n) = n
325predSucc n = refl
385predSucc n = refl
326
386
327minusSuccPred : (left : Nat) -> (right : Nat) ->
387minusSuccPred : (left : Nat) -> (right : Nat) ->
328− minus left (S right) = pred (minus left right)
388+ left - (S right) = pred (left - right)
329minusSuccPred O right = refl
389minusSuccPred O right = refl
330minusSuccPred (S left) O =
390minusSuccPred (S left) O =
331 let inductiveHypothesis = minusSuccPred left O in
391 let inductiveHypothesis = minusSuccPred left O in
@@ -334,6 +394,94 @@ minusSuccPred (S left) (S right) =
334 let inductiveHypothesis = minusSuccPred left right in
394 let inductiveHypothesis = minusSuccPred left right in
335 ?minusSuccPredStepCase'
395 ?minusSuccPredStepCase'
336
396
397+-- boolElim
398+boolElimSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) ->
399+ S (boolElim cond t f) = boolElim cond (S t) (S f)
400+boolElimSuccSucc True t f = refl
401+boolElimSuccSucc False t f = refl
402+
403+boolElimPlusPlusLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->
404+ left + (boolElim cond t f) = boolElim cond (left + t) (left + f)
405+boolElimPlusPlusLeft True left t f = refl
406+boolElimPlusPlusLeft False left t f = refl
407+
408+boolElimPlusPlusRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->
409+ (boolElim cond t f) + right = boolElim cond (t + right) (f + right)
410+boolElimPlusPlusRight True right t f = refl
411+boolElimPlusPlusRight False right t f = refl
412+
413+boolElimMultMultLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->
414+ left * (boolElim cond t f) = boolElim cond (left * t) (left * f)
415+boolElimMultMultLeft True left t f = refl
416+boolElimMultMultLeft False left t f = refl
417+
418+boolElimMultMultRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->
419+ (boolElim cond t f) * right = boolElim cond (t * right) (f * right)
420+boolElimMultMultRight True right t f = refl
421+boolElimMultMultRight False right t f = refl
422+
423+-- Orders
424+lteNTrue : (n : Nat) -> lte n n = True
425+lteNTrue O = refl
426+lteNTrue (S n) = lteNTrue n
427+
428+lteSuccZeroFalse : (n : Nat) -> lte (S n) O = False
429+lteSuccZeroFalse O = refl
430+lteSuccZeroFalse (S n) = refl
431+
432+-- Minimum and maximum
433+minimumZeroZeroRight : (right : Nat) -> minimum 0 right = O
434+minimumZeroZeroRight O = refl
435+minimumZeroZeroRight (S right) = minimumZeroZeroRight right
436+
437+minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = O
438+minimumZeroZeroLeft O = refl
439+minimumZeroZeroLeft (S left) = refl
440+
441+minimumSuccSucc : (left : Nat) -> (right : Nat) ->
442+ minimum (S left) (S right) = S (minimum left right)
443+minimumSuccSucc O O = refl
444+minimumSuccSucc (S left) O = refl
445+minimumSuccSucc O (S right) = refl
446+minimumSuccSucc (S left) (S right) =
447+ let inductiveHypothesis = minimumSuccSucc left right in
448+ ?minimumSuccSuccStepCase
449+
450+minimumCommutative : (left : Nat) -> (right : Nat) ->
451+ minimum left right = minimum right left
452+minimumCommutative O O = refl
453+minimumCommutative O (S right) = refl
454+minimumCommutative (S left) O = refl
455+minimumCommutative (S left) (S right) =
456+ let inductiveHypothesis = minimumCommutative left right in
457+ ?minimumCommutativeStepCase
458+
459+maximumZeroNRight : (right : Nat) -> maximum O right = right
460+maximumZeroNRight O = refl
461+maximumZeroNRight (S right) = refl
462+
463+maximumZeroNLeft : (left : Nat) -> maximum left O = left
464+maximumZeroNLeft O = refl
465+maximumZeroNLeft (S left) = refl
466+
467+maximumSuccSucc : (left : Nat) -> (right : Nat) ->
468+ S (maximum left right) = maximum (S left) (S right)
469+maximumSuccSucc O O = refl
470+maximumSuccSucc (S left) O = refl
471+maximumSuccSucc O (S right) = refl
472+maximumSuccSucc (S left) (S right) =
473+ let inductiveHypothesis = maximumSuccSucc left right in
474+ ?maximumSuccSuccStepCase
475+
476+maximumCommutative : (left : Nat) -> (right : Nat) ->
477+ maximum left right = maximum right left
478+maximumCommutative O O = refl
479+maximumCommutative (S left) O = refl
480+maximumCommutative O (S right) = refl
481+maximumCommutative (S left) (S right) =
482+ let inductiveHypothesis = maximumCommutative left right in
483+ ?maximumCommutativeStepCase
484+
337--------------------------------------------------------------------------------
485--------------------------------------------------------------------------------
338-- Proofs
486-- Proofs
339--------------------------------------------------------------------------------
487--------------------------------------------------------------------------------
@@ -494,3 +642,109 @@ plusZeroRightNeutralStepCase = proof {
494 trivial;
642 trivial;
495}
643}
496
644
645+maximumCommutativeStepCase = proof {
646+ intros;
647+ rewrite (boolElimSuccSucc (lte left right) right left);
648+ rewrite (boolElimSuccSucc (lte right left) left right);
649+ rewrite inductiveHypothesis;
650+ trivial;
651+}
652+
653+maximumSuccSuccStepCase = proof {
654+ intros;
655+ rewrite sym (boolElimSuccSucc (lte left right) (S right) (S left));
656+ trivial;
657+}
658+
659+minimumCommutativeStepCase = proof {
660+ intros;
661+ rewrite (boolElimSuccSucc (lte left right) left right);
662+ rewrite (boolElimSuccSucc (lte right left) right left);
663+ rewrite inductiveHypothesis;
664+ trivial;
665+}
666+
667+minimumSuccSuccStepCase = proof {
668+ intros;
669+ rewrite (boolElimSuccSucc (lte left right) (S left) (S right));
670+ trivial;
671+}
672+
673+multDistributesOverMinusRightBody = proof {
674+ intros;
675+ rewrite sym (multCommutative left (minus centre right));
676+ rewrite sym (multDistributesOverMinusLeft centre right left);
677+ rewrite sym (multCommutative centre left);
678+ rewrite sym (multCommutative right left);
679+ trivial;
680+}
681+
682+multDistributesOverMinusLeftStepCase = proof {
683+ intros;
684+ rewrite sym (plusMinusLeftCancel right (mult left right) (mult centre right));
685+ trivial;
686+}
687+
688+multDistributesOverMinusLeftBaseCase = proof {
689+ intros;
690+ rewrite (minusZeroRight (plus right (mult left right)));
691+ trivial;
692+}
693+
694+plusMinusLeftCancelStepCase = proof {
695+ intros;
696+ rewrite inductiveHypothesis;
697+ trivial;
698+}
699+
700+minusMinusMinusPlusStepCase = proof {
701+ intros;
702+ rewrite inductiveHypothesis;
703+ trivial;
704+}
705+
706+plusLeftLeftRightZeroBaseCase = proof {
707+ intros;
708+ rewrite p;
709+ trivial;
710+}
711+
712+plusLeftLeftRightZeroStepCase = proof {
713+ intros;
714+ refine inductiveHypothesis;
715+ let p' = succInjective (plus left right) left p;
716+ rewrite p';
717+ trivial;
718+}
719+
720+plusRightCancelStepCase = proof {
721+ intros;
722+ refine inductiveHypothesis;
723+ refine succInjective;
724+ rewrite sym (plusSuccRightSucc left right);
725+ rewrite sym (plusSuccRightSucc left' right);
726+ rewrite p;
727+ trivial;
728+}
729+
730+plusRightCancelBaseCase = proof {
731+ intros;
732+ rewrite (plusZeroRightNeutral left);
733+ rewrite (plusZeroRightNeutral left');
734+ rewrite p;
735+ trivial;
736+}
737+
738+plusLeftCancelStepCase = proof {
739+ intros;
740+ let injectiveProof = succInjective (plus left right) (plus left right') p;
741+ rewrite (inductiveHypothesis injectiveProof);
742+ trivial;
743+}
744+
745+plusLeftCancelBaseCase = proof {
746+ intros;
747+ rewrite p;
748+ trivial;
749+}
750+