@@ -92,9 +92,9 @@ pred (S n) = n
9292--------------------------------------------------------------------------------
9393
9494fib : Nat -> Nat
95−fib O = O
96−fib (S O) = S O
97−fib (S (S n)) = plus (fib (S n)) (fib n)
95+fib O = 0
96+fib (S O) = 1
97+fib (S (S n)) = fib (S n) + fib n
9898
9999--------------------------------------------------------------------------------
100100-- GCD and LCM
@@ -159,103 +159,124 @@ succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->
159159succInjective left right refl = refl
160160
161161-- Plus
162−plusZeroLeftNeutral : (right : Nat) -> plus O right = right
162+plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
163163plusZeroLeftNeutral right = refl
164164
165−plusZeroRightNeutral : (left : Nat) -> plus left O = left
165+plusZeroRightNeutral : (left : Nat) -> left + 0 = left
166166plusZeroRightNeutral O = refl
167167plusZeroRightNeutral (S n) =
168168 let inductiveHypothesis = plusZeroRightNeutral n in
169169 ?plusZeroRightNeutralStepCase
170170
171171plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
172− S (plus left right) = plus left (S right)
172+ S (left + right) = left + (S right)
173173plusSuccRightSucc O right = refl
174174plusSuccRightSucc (S left) right =
175175 let inductiveHypothesis = plusSuccRightSucc left right in
176176 ?plusSuccRightSuccStepCase
177177
178178plusCommutative : (left : Nat) -> (right : Nat) ->
179− plus left right = plus right left
179+ left + right = right + left
180180plusCommutative O right = ?plusCommutativeBaseCase
181181plusCommutative (S left) right =
182182 let inductiveHypothesis = plusCommutative left right in
183183 ?plusCommutativeStepCase
184184
185185plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
186− plus left (plus centre right) = plus (plus left centre) right
186+ left + (centre + right) = (left + centre) + right
187187plusAssociative O centre right = refl
188188plusAssociative (S left) centre right =
189189 let inductiveHypothesis = plusAssociative left centre right in
190190 ?plusAssociativeStepCase
191191
192192plusMonotonicRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
193− (p : left = right) -> plus left c = plus right c
193+ (p : left = right) -> left + c = right + c
194194plusMonotonicRight left right c refl = refl
195195
196196plusMonotonicLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->
197− (p : left = right) -> plus c left = plus c right
197+ (p : left = right) -> c + left = c + right
198198plusMonotonicLeft left right c refl = refl
199199
200−plusOneSucc : (right : Nat) -> plus (S O) right = S right
200+plusOneSucc : (right : Nat) -> 1 + right = S right
201201plusOneSucc n = refl
202202
203+plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
204+ (p : left + right = left + right') -> right = right'
205+plusLeftCancel O right right' p = ?plusLeftCancelBaseCase
206+plusLeftCancel (S left) right right' p =
207+ let inductiveHypothesis = plusLeftCancel left right right' in
208+ ?plusLeftCancelStepCase
209+
210+plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
211+ (p : left + right = left' + right) -> left = left'
212+plusRightCancel left left' O p = ?plusRightCancelBaseCase
213+plusRightCancel left left' (S right) p =
214+ let inductiveHypothesis = plusRightCancel left left' right in
215+ ?plusRightCancelStepCase
216+
217+plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
218+ (p : left + right = left) -> right = O
219+plusLeftLeftRightZero O right p = ?plusLeftLeftRightZeroBaseCase
220+plusLeftLeftRightZero (S left) right p =
221+ let inductiveHypothesis = plusLeftLeftRightZero left right in
222+ ?plusLeftLeftRightZeroStepCase
223+
203224-- Mult
204−multZeroLeftZero : (right : Nat) -> mult O right = O
225+multZeroLeftZero : (right : Nat) -> O * right = O
205226multZeroLeftZero right = refl
206227
207−multZeroRightZero : (left : Nat) -> mult left O = O
228+multZeroRightZero : (left : Nat) -> left * O = O
208229multZeroRightZero O = refl
209230multZeroRightZero (S left) =
210231 let inductiveHypothesis = multZeroRightZero left in
211232 ?multZeroRightZeroStepCase
212233
213234multRightSuccPlus : (left : Nat) -> (right : Nat) ->
214− mult left (S right) = plus left (mult left right)
235+ left * (S right) = left + (left * right)
215236multRightSuccPlus O right = refl
216237multRightSuccPlus (S left) right =
217238 let inductiveHypothesis = multRightSuccPlus left right in
218239 ?multRightSuccPlusStepCase
219240
220241multLeftSuccPlus : (left : Nat) -> (right : Nat) ->
221− mult (S left) right = plus right (mult left right)
242+ (S left) * right = right + (left * right)
222243multLeftSuccPlus left right = refl
223244
224245multCommutative : (left : Nat) -> (right : Nat) ->
225− mult left right = mult right left
246+ left * right = right * left
226247multCommutative O right = ?multCommutativeBaseCase
227248multCommutative (S left) right =
228249 let inductiveHypothesis = multCommutative left right in
229250 ?multCommutativeStepCase
230251
231252multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
232− mult left (plus centre right) = plus (mult left centre) (mult left right)
253+ left * (centre + right) = (left * centre) + (left * right)
233254multDistributesOverPlusRight O centre right = refl
234255multDistributesOverPlusRight (S left) centre right =
235256 let inductiveHypothesis = multDistributesOverPlusRight left centre right in
236257 ?multDistributesOverPlusRightStepCase
237258
238259multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
239− mult (plus left centre) right = plus (mult left right) (mult centre right)
260+ (left + centre) * right = (left * right) + (centre * right)
240261multDistributesOverPlusLeft O centre right = refl
241262multDistributesOverPlusLeft (S left) centre right =
242263 let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
243264 ?multDistributesOverPlusLeftStepCase
244265
245266multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
246− mult left (mult centre right) = mult (mult left centre) right
267+ left * (centre * right) = (left * centre) * right
247268multAssociative O centre right = refl
248269multAssociative (S left) centre right =
249270 let inductiveHypothesis = multAssociative left centre right in
250271 ?multAssociativeStepCase
251272
252−multOneLeftNeutral : (right : Nat) -> mult (S O) right = right
273+multOneLeftNeutral : (right : Nat) -> 1 * right = right
253274multOneLeftNeutral O = refl
254275multOneLeftNeutral (S right) =
255276 let inductiveHypothesis = multOneLeftNeutral right in
256277 ?multOneLeftNeutralStepCase
257278
258−multOneRightNeutral : (left : Nat) -> mult left (S O) = left
279+multOneRightNeutral : (left : Nat) -> left * 1 = left
259280multOneRightNeutral O = refl
260281multOneRightNeutral (S left) =
261282 let inductiveHypothesis = multOneRightNeutral left in
@@ -263,59 +284,68 @@ multOneRightNeutral (S left) =
263284
264285-- Minus
265286minusSuccSucc : (left : Nat) -> (right : Nat) ->
266− minus (S left) (S right) = minus left right
287+ (S left) - (S right) = left - right
267288minusSuccSucc left right = refl
268289
269−minusZeroLeft : (right : Nat) -> minus O right = O
290+minusZeroLeft : (right : Nat) -> 0 - right = O
270291minusZeroLeft right = refl
271292
272−minusZeroRight : (left : Nat) -> minus left O = left
293+minusZeroRight : (left : Nat) -> left - 0 = left
273294minusZeroRight O = refl
274295minusZeroRight (S left) = refl
275296
276−minusZeroN : (n : Nat) -> O = minus n n
297+minusZeroN : (n : Nat) -> O = n - n
277298minusZeroN O = refl
278299minusZeroN (S n) = minusZeroN n
279300
280−minusOneSuccN : (n : Nat) -> S O = minus (S n) n
301+minusOneSuccN : (n : Nat) -> S O = (S n) - n
281302minusOneSuccN O = refl
282303minusOneSuccN (S n) = minusOneSuccN n
283304
305+minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
306+ left - centre - right = left - (centre + right)
307+minusMinusMinusPlus O O right = refl
308+minusMinusMinusPlus (S left) O right = refl
309+minusMinusMinusPlus O (S centre) right = refl
310+minusMinusMinusPlus (S left) (S centre) right =
311+ let inductiveHypothesis = minusMinusMinusPlus left centre right in
312+ ?minusMinusMinusPlusStepCase
313+
284314-- Power
285315powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =
286− mult base (power base exp)
316+ base * (power base exp)
287317powerSuccPowerLeft base exp = refl
288318
289319multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
290− mult (power base exp) (power base exp') = power base (plus exp exp')
320+ (power base exp) * (power base exp') = power base (exp + exp')
291321multPowerPowerPlus base O exp' = ?multPowerPowerPlusBaseCase
292322multPowerPowerPlus base (S exp) exp' =
293323 let inductiveHypothesis = multPowerPowerPlus base exp exp' in
294324 ?multPowerPowerPlusStepCase
295325
296−powerZeroOne : (base : Nat) -> power base O = S O
326+powerZeroOne : (base : Nat) -> power base 0 = S O
297327powerZeroOne base = refl
298328
299−powerOneNeutral : (base : Nat) -> power base (S O) = base
329+powerOneNeutral : (base : Nat) -> power base 1 = base
300330powerOneNeutral O = refl
301331powerOneNeutral (S base) =
302332 let inductiveHypothesis = powerOneNeutral base in
303333 ?powerOneNeutralStepCase
304334
305−powerOneSuccOne : (exp : Nat) -> power (S O) exp = S O
335+powerOneSuccOne : (exp : Nat) -> power 1 exp = S O
306336powerOneSuccOne O = refl
307337powerOneSuccOne (S exp) =
308338 let inductiveHypothesis = powerOneSuccOne exp in
309339 ?powerOneSuccOneStepCase
310340
311−powerSuccSuccMult : (base : Nat) -> power base (S (S O)) = mult base base
341+powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
312342powerSuccSuccMult O = refl
313343powerSuccSuccMult (S base) =
314344 let inductiveHypothesis = powerSuccSuccMult base in
315345 ?powerSuccSuccMultStepCase
316346
317347powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
318− power (power base exp) exp' = power base (mult exp exp')
348+ power (power base exp) exp' = power base (exp * exp')
319349powerPowerMultPower base exp O = ?powerPowerMultPowerBaseCase
320350powerPowerMultPower base exp (S exp') =
321351 let inductiveHypothesis = powerPowerMultPower base exp exp' in
@@ -326,7 +356,7 @@ predSucc : (n : Nat) -> pred (S n) = n
326356predSucc n = refl
327357
328358minusSuccPred : (left : Nat) -> (right : Nat) ->
329− minus left (S right) = pred (minus left right)
359+ left - (S right) = pred (left - right)
330360minusSuccPred O right = refl
331361minusSuccPred (S left) O =
332362 let inductiveHypothesis = minusSuccPred left O in
@@ -495,3 +525,54 @@ plusZeroRightNeutralStepCase = proof {
495525 trivial;
496526}
497527
528+minusMinusMinusPlusStepCase = proof {
529+ intros;
530+ rewrite inductiveHypothesis;
531+ trivial;
532+}
533+
534+plusLeftLeftRightZeroBaseCase = proof {
535+ intros;
536+ rewrite p;
537+ trivial;
538+}
539+
540+plusLeftLeftRightZeroStepCase = proof {
541+ intros;
542+ refine inductiveHypothesis;
543+ let p' = succInjective (plus left right) left p;
544+ rewrite p';
545+ trivial;
546+}
547+
548+plusRightCancelStepCase = proof {
549+ intros;
550+ refine inductiveHypothesis;
551+ refine succInjective;
552+ rewrite sym (plusSuccRightSucc left right);
553+ rewrite sym (plusSuccRightSucc left' right);
554+ rewrite p;
555+ trivial;
556+}
557+
558+plusRightCancelBaseCase = proof {
559+ intros;
560+ rewrite (plusZeroRightNeutral left);
561+ rewrite (plusZeroRightNeutral left');
562+ rewrite p;
563+ trivial;
564+}
565+
566+plusLeftCancelStepCase = proof {
567+ intros;
568+ let injectiveProof = succInjective (plus left right) (plus left right') p;
569+ rewrite (inductiveHypothesis injectiveProof);
570+ trivial;
571+}
572+
573+plusLeftCancelBaseCase = proof {
574+ intros;
575+ rewrite p;
576+ trivial;
577+}
578+