@@ -150,9 +150,9 @@ maximum left right =
150150--------------------------------------------------------------------------------
151151
152152-- Succ
153−succMonotonic : (left : Nat) -> (right : Nat) -> (p : left = right) ->
153+eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->
154154 S left = S right
155−succMonotonic left right refl = refl
155+eqSucc left right refl = refl
156156
157157succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->
158158 left = right
@@ -189,13 +189,13 @@ plusAssociative (S left) centre right =
189189 let inductiveHypothesis = plusAssociative left centre right in
190190 ?plusAssociativeStepCase
191191
192−plusMonotonicRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
192+plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
193193 (p : left = right) -> left + c = right + c
194−plusMonotonicRight left right c refl = refl
194+plusConstantRight left right c refl = refl
195195
196−plusMonotonicLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->
196+plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->
197197 (p : left = right) -> c + left = c + right
198−plusMonotonicLeft left right c refl = refl
198+plusConstantLeft left right c refl = refl
199199
200200plusOneSucc : (right : Nat) -> 1 + right = S right
201201plusOneSucc n = refl
@@ -302,6 +302,14 @@ minusOneSuccN : (n : Nat) -> S O = (S n) - n
302302minusOneSuccN O = refl
303303minusOneSuccN (S n) = minusOneSuccN n
304304
305+minusSuccOne : (n : Nat) -> S n - 1 = n
306+minusSuccOne O = refl
307+minusSuccOne (S n) = refl
308+
309+minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = O
310+minusPlusZero O m = refl
311+minusPlusZero (S n) m = minusPlusZero n m
312+
305313minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
306314 left - centre - right = left - (centre + right)
307315minusMinusMinusPlus O O right = refl
@@ -311,6 +319,28 @@ minusMinusMinusPlus (S left) (S centre) right =
311319 let inductiveHypothesis = minusMinusMinusPlus left centre right in
312320 ?minusMinusMinusPlusStepCase
313321
322+plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
323+ (left + right) - (left + right') = right - right'
324+plusMinusLeftCancel O right right' = refl
325+plusMinusLeftCancel (S left) right right' =
326+ let inductiveHypothesis = plusMinusLeftCancel left right right' in
327+ ?plusMinusLeftCancelStepCase
328+
329+multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
330+ (left - centre) * right = (left * right) - (centre * right)
331+multDistributesOverMinusLeft O O right = refl
332+multDistributesOverMinusLeft (S left) O right =
333+ ?multDistributesOverMinusLeftBaseCase
334+multDistributesOverMinusLeft O (S centre) right = refl
335+multDistributesOverMinusLeft (S left) (S centre) right =
336+ let inductiveHypothesis = multDistributesOverMinusLeft left centre right in
337+ ?multDistributesOverMinusLeftStepCase
338+
339+multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
340+ left * (centre - right) = (left * centre) - (left * right)
341+multDistributesOverMinusRight left centre right =
342+ ?multDistributesOverMinusRightBody
343+
314344-- Power
315345powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =
316346 base * (power base exp)
@@ -365,6 +395,94 @@ minusSuccPred (S left) (S right) =
365395 let inductiveHypothesis = minusSuccPred left right in
366396 ?minusSuccPredStepCase'
367397
398+-- boolElim
399+boolElimSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) ->
400+ S (boolElim cond t f) = boolElim cond (S t) (S f)
401+boolElimSuccSucc True t f = refl
402+boolElimSuccSucc False t f = refl
403+
404+boolElimPlusPlusLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->
405+ left + (boolElim cond t f) = boolElim cond (left + t) (left + f)
406+boolElimPlusPlusLeft True left t f = refl
407+boolElimPlusPlusLeft False left t f = refl
408+
409+boolElimPlusPlusRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->
410+ (boolElim cond t f) + right = boolElim cond (t + right) (f + right)
411+boolElimPlusPlusRight True right t f = refl
412+boolElimPlusPlusRight False right t f = refl
413+
414+boolElimMultMultLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->
415+ left * (boolElim cond t f) = boolElim cond (left * t) (left * f)
416+boolElimMultMultLeft True left t f = refl
417+boolElimMultMultLeft False left t f = refl
418+
419+boolElimMultMultRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->
420+ (boolElim cond t f) * right = boolElim cond (t * right) (f * right)
421+boolElimMultMultRight True right t f = refl
422+boolElimMultMultRight False right t f = refl
423+
424+-- Orders
425+lteNTrue : (n : Nat) -> lte n n = True
426+lteNTrue O = refl
427+lteNTrue (S n) = lteNTrue n
428+
429+lteSuccZeroFalse : (n : Nat) -> lte (S n) O = False
430+lteSuccZeroFalse O = refl
431+lteSuccZeroFalse (S n) = refl
432+
433+-- Minimum and maximum
434+minimumZeroZeroRight : (right : Nat) -> minimum 0 right = O
435+minimumZeroZeroRight O = refl
436+minimumZeroZeroRight (S right) = minimumZeroZeroRight right
437+
438+minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = O
439+minimumZeroZeroLeft O = refl
440+minimumZeroZeroLeft (S left) = refl
441+
442+minimumSuccSucc : (left : Nat) -> (right : Nat) ->
443+ minimum (S left) (S right) = S (minimum left right)
444+minimumSuccSucc O O = refl
445+minimumSuccSucc (S left) O = refl
446+minimumSuccSucc O (S right) = refl
447+minimumSuccSucc (S left) (S right) =
448+ let inductiveHypothesis = minimumSuccSucc left right in
449+ ?minimumSuccSuccStepCase
450+
451+minimumCommutative : (left : Nat) -> (right : Nat) ->
452+ minimum left right = minimum right left
453+minimumCommutative O O = refl
454+minimumCommutative O (S right) = refl
455+minimumCommutative (S left) O = refl
456+minimumCommutative (S left) (S right) =
457+ let inductiveHypothesis = minimumCommutative left right in
458+ ?minimumCommutativeStepCase
459+
460+maximumZeroNRight : (right : Nat) -> maximum O right = right
461+maximumZeroNRight O = refl
462+maximumZeroNRight (S right) = refl
463+
464+maximumZeroNLeft : (left : Nat) -> maximum left O = left
465+maximumZeroNLeft O = refl
466+maximumZeroNLeft (S left) = refl
467+
468+maximumSuccSucc : (left : Nat) -> (right : Nat) ->
469+ S (maximum left right) = maximum (S left) (S right)
470+maximumSuccSucc O O = refl
471+maximumSuccSucc (S left) O = refl
472+maximumSuccSucc O (S right) = refl
473+maximumSuccSucc (S left) (S right) =
474+ let inductiveHypothesis = maximumSuccSucc left right in
475+ ?maximumSuccSuccStepCase
476+
477+maximumCommutative : (left : Nat) -> (right : Nat) ->
478+ maximum left right = maximum right left
479+maximumCommutative O O = refl
480+maximumCommutative (S left) O = refl
481+maximumCommutative O (S right) = refl
482+maximumCommutative (S left) (S right) =
483+ let inductiveHypothesis = maximumCommutative left right in
484+ ?maximumCommutativeStepCase
485+
368486--------------------------------------------------------------------------------
369487-- Proofs
370488--------------------------------------------------------------------------------
@@ -525,6 +643,61 @@ plusZeroRightNeutralStepCase = proof {
525643 trivial;
526644}
527645
646+maximumCommutativeStepCase = proof {
647+ intros;
648+ rewrite (boolElimSuccSucc (lte left right) right left);
649+ rewrite (boolElimSuccSucc (lte right left) left right);
650+ rewrite inductiveHypothesis;
651+ trivial;
652+}
653+
654+maximumSuccSuccStepCase = proof {
655+ intros;
656+ rewrite sym (boolElimSuccSucc (lte left right) (S right) (S left));
657+ trivial;
658+}
659+
660+minimumCommutativeStepCase = proof {
661+ intros;
662+ rewrite (boolElimSuccSucc (lte left right) left right);
663+ rewrite (boolElimSuccSucc (lte right left) right left);
664+ rewrite inductiveHypothesis;
665+ trivial;
666+}
667+
668+minimumSuccSuccStepCase = proof {
669+ intros;
670+ rewrite (boolElimSuccSucc (lte left right) (S left) (S right));
671+ trivial;
672+}
673+
674+multDistributesOverMinusRightBody = proof {
675+ intros;
676+ rewrite sym (multCommutative left (minus centre right));
677+ rewrite sym (multDistributesOverMinusLeft centre right left);
678+ rewrite sym (multCommutative centre left);
679+ rewrite sym (multCommutative right left);
680+ trivial;
681+}
682+
683+multDistributesOverMinusLeftStepCase = proof {
684+ intros;
685+ rewrite sym (plusMinusLeftCancel right (mult left right) (mult centre right));
686+ trivial;
687+}
688+
689+multDistributesOverMinusLeftBaseCase = proof {
690+ intros;
691+ rewrite (minusZeroRight (plus right (mult left right)));
692+ trivial;
693+}
694+
695+plusMinusLeftCancelStepCase = proof {
696+ intros;
697+ rewrite inductiveHypothesis;
698+ trivial;
699+}
700+
528701minusMinusMinusPlusStepCase = proof {
529702 intros;
530703 rewrite inductiveHypothesis;