Simplify Nat proofs

These changes are strictly nonfunctional.

libs/base/Data/Nat.idr

@@ -1,5 +1,7 @@
 module Data.Nat
 
+%default total
+
 export
 Uninhabited (Z = S n) where
   uninhabited Refl impossible
@@ -157,14 +159,12 @@ maximum (S n) (S m) = S (maximum n m)
 -- Proofs on S
 
 export
-eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->
-         S left = S right
-eqSucc left _ Refl = Refl
+eqSucc : (left, right : Nat) -> left = right -> S left = S right
+eqSucc _ _ Refl = Refl
 
 export
-succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->
-                left = right
-succInjective left _ Refl = Refl
+succInjective : (left, right : Nat) -> S left = S right -> left = right
+succInjective _ _ Refl = Refl
 
 export
 SIsNotZ : (S x = Z) -> Void
@@ -219,7 +219,7 @@ Integral Nat where
   div = divNat
   mod = modNat
 
-export
+export partial
 gcd : (a: Nat) -> (b: Nat) -> {auto ok: NotBothZero a b} -> Nat
 gcd a Z     = a
 gcd Z b     = b
@@ -250,89 +250,80 @@ cmp (S x) (S y) with (cmp x y)
   cmp (S x) (S x)           | CmpEQ   = CmpEQ
   cmp (S (y + (S k))) (S y) | CmpGT k = CmpGT k
 
--- Proofs on
+-- Proofs on +
 
 export
 plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
-plusZeroLeftNeutral right = Refl
+plusZeroLeftNeutral _ = Refl
 
 export
 plusZeroRightNeutral : (left : Nat) -> left + 0 = left
 plusZeroRightNeutral Z     = Refl
-plusZeroRightNeutral (S n) =
-  let inductiveHypothesis = plusZeroRightNeutral n in
-    rewrite inductiveHypothesis in Refl
+plusZeroRightNeutral (S n) = rewrite plusZeroRightNeutral n in Refl
 
 export
-plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
-  S (left + right) = left + (S right)
-plusSuccRightSucc Z right        = Refl
-plusSuccRightSucc (S left) right =
-  let inductiveHypothesis = plusSuccRightSucc left right in
-    rewrite inductiveHypothesis in Refl
+plusSuccRightSucc : (left, right : Nat) -> S (left + right) = left + (S right)
+plusSuccRightSucc Z _ = Refl
+plusSuccRightSucc (S left) right = rewrite plusSuccRightSucc left right in Refl
 
 export
-plusCommutative : (left : Nat) -> (right : Nat) ->
-  left + right = right + left
-plusCommutative Z        right = rewrite plusZeroRightNeutral right in Refl
+plusCommutative : (left, right : Nat) -> left + right = right + left
+plusCommutative Z right = rewrite plusZeroRightNeutral right in Refl
 plusCommutative (S left) right =
-  let inductiveHypothesis = plusCommutative left right in
-    rewrite inductiveHypothesis in
-      rewrite plusSuccRightSucc right left in Refl
+  rewrite plusCommutative left right in
+    rewrite plusSuccRightSucc right left in
+      Refl
 
 export
-plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
+plusAssociative : (left, centre, right : Nat) ->
   left + (centre + right) = (left + centre) + right
-plusAssociative Z        centre right = Refl
+plusAssociative Z _ _ = Refl
 plusAssociative (S left) centre right =
-  let inductiveHypothesis = plusAssociative left centre right in
-    rewrite inductiveHypothesis in Refl
+    rewrite plusAssociative left centre right in Refl
 
 export
-plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
-  (p : left = right) -> left + c = right + c
-plusConstantRight left _ c Refl = Refl
+plusConstantRight : (left, right, c : Nat) -> left = right ->
+  left + c = right + c
+plusConstantRight _ _ _ Refl = Refl
 
 export
-plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->
-  (p : left = right) -> c + left = c + right
-plusConstantLeft left _ c Refl = Refl
+plusConstantLeft : (left, right, c : Nat) -> left = right ->
+  c + left = c + right
+plusConstantLeft _ _ _ Refl = Refl
 
 export
 plusOneSucc : (right : Nat) -> 1 + right = S right
-plusOneSucc n = Refl
+plusOneSucc _ = Refl
 
 export
-plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
-  (p : left + right = left + right') -> right = right'
-plusLeftCancel Z        right right' p = p
+plusLeftCancel : (left, right, right' : Nat) ->
+  left + right = left + right' -> right = right'
+plusLeftCancel Z _ _ p = p
 plusLeftCancel (S left) right right' p =
-  let inductiveHypothesis = plusLeftCancel left right right' in
-    inductiveHypothesis (succInjective _ _ p)
+    plusLeftCancel left right right' (succInjective _ _ p)
 
 export
-plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
-  (p : left + right = left' + right) -> left = left'
-plusRightCancel left left' Z         p = rewrite sym (plusZeroRightNeutral left) in
-                                         rewrite sym (plusZeroRightNeutral left') in
-                                                 p
-plusRightCancel left left' (S right) p =
-  plusRightCancel left left' right
-    (succInjective _ _ (rewrite plusSuccRightSucc left right in
-                        rewrite plusSuccRightSucc left' right in p))
+plusRightCancel : (left, left', right : Nat) ->
+  left + right = left' + right -> left = left'
+plusRightCancel left left' right p =
+  plusLeftCancel right left left' $
+    rewrite plusCommutative right left in
+      rewrite plusCommutative right left' in
+        p
 
 export
-plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
-  (p : left + right = left) -> right = Z
-plusLeftLeftRightZero Z        right p = p
-plusLeftLeftRightZero (S left) right p =
-  plusLeftLeftRightZero left right (succInjective _ _ p)
+plusLeftLeftRightZero : (left, right : Nat) ->
+  left + right = left -> right = Z
+plusLeftLeftRightZero left right p =
+  plusLeftCancel left right Z $
+    rewrite plusZeroRightNeutral left in
+      p
 
 -- Proofs on *
 
 export
 multZeroLeftZero : (right : Nat) -> Z * right = Z
-multZeroLeftZero right = Refl
+multZeroLeftZero _ = Refl
 
 export
 multZeroRightZero : (left : Nat) -> left * Z = Z
@@ -340,97 +331,80 @@ multZeroRightZero Z        = Refl
 multZeroRightZero (S left) = multZeroRightZero left
 
 export
-multRightSuccPlus : (left : Nat) -> (right : Nat) ->
+multRightSuccPlus : (left, right : Nat) ->
   left * (S right) = left + (left * right)
-multRightSuccPlus Z        right = Refl
+multRightSuccPlus Z _ = Refl
 multRightSuccPlus (S left) right =
-  let inductiveHypothesis = multRightSuccPlus left right in
-    rewrite inductiveHypothesis in
-    rewrite plusAssociative left right (left * right) in
-    rewrite plusAssociative right left (left * right) in
-    rewrite plusCommutative right left in
-            Refl
+  rewrite multRightSuccPlus left right in
+  rewrite plusAssociative left right (left * right) in
+  rewrite plusAssociative right left (left * right) in
+  rewrite plusCommutative right left in
+          Refl
 
 export
-multLeftSuccPlus : (left : Nat) -> (right : Nat) ->
+multLeftSuccPlus : (left, right : Nat) ->
   (S left) * right = right + (left * right)
-multLeftSuccPlus left right = Refl
+multLeftSuccPlus _ _ = Refl
 
 export
-multCommutative : (left : Nat) -> (right : Nat) ->
-  left * right = right * left
-multCommutative Z right        = rewrite multZeroRightZero right in Refl
+multCommutative : (left, right : Nat) -> left * right = right * left
+multCommutative Z right = rewrite multZeroRightZero right in Refl
 multCommutative (S left) right =
-  let inductiveHypothesis = multCommutative left right in
-      rewrite inductiveHypothesis in
-      rewrite multRightSuccPlus right left in
-              Refl
+  rewrite multCommutative left right in
+  rewrite multRightSuccPlus right left in
+          Refl
 
 export
-multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
-  left * (centre + right) = (left * centre) + (left * right)
-multDistributesOverPlusRight Z        centre right = Refl
-multDistributesOverPlusRight (S left) centre right =
-  let inductiveHypothesis = multDistributesOverPlusRight left centre right in
-    rewrite inductiveHypothesis in
-    rewrite plusAssociative (centre + (left * centre)) right (left * right) in
-    rewrite sym (plusAssociative centre (left * centre) right) in
-    rewrite plusCommutative (left * centre) right in
-    rewrite plusAssociative centre right (left * centre) in
-    rewrite plusAssociative (centre + right) (left * centre) (left * right) in
-            Refl
-
-export
-multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
+multDistributesOverPlusLeft : (left, centre, right : Nat) ->
   (left + centre) * right = (left * right) + (centre * right)
-multDistributesOverPlusLeft Z        centre right = Refl
-multDistributesOverPlusLeft (S left) centre right =
-  let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
-    rewrite inductiveHypothesis in
-    rewrite plusAssociative right (left * right) (centre * right) in
-            Refl
+multDistributesOverPlusLeft Z _ _ = Refl
+multDistributesOverPlusLeft (S k) centre right =
+  rewrite multDistributesOverPlusLeft k centre right in
+    rewrite plusAssociative right (k * right) (centre * right) in
+      Refl
 
 export
-multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
+multDistributesOverPlusRight : (left, centre, right : Nat) ->
+  left * (centre + right) = (left * centre) + (left * right)
+multDistributesOverPlusRight left centre right =
+  rewrite multCommutative left (centre + right) in
+    rewrite multCommutative left centre in
+      rewrite multCommutative left right in
+  multDistributesOverPlusLeft centre right left
+
+export
+multAssociative : (left, centre, right : Nat) ->
   left * (centre * right) = (left * centre) * right
-multAssociative Z        centre right = Refl
+multAssociative Z _ _ = Refl
 multAssociative (S left) centre right =
-  let inductiveHypothesis = multAssociative left centre right in
-    rewrite inductiveHypothesis in
-    rewrite multDistributesOverPlusLeft centre (left * centre) right in
-            Refl
+  rewrite multAssociative left centre right in
+    rewrite multDistributesOverPlusLeft centre (mult left centre) right in
+      Refl
 
 export
 multOneLeftNeutral : (right : Nat) -> 1 * right = right
-multOneLeftNeutral Z         = Refl
-multOneLeftNeutral (S right) =
-  let inductiveHypothesis = multOneLeftNeutral right in
-    rewrite inductiveHypothesis in
-            Refl
+multOneLeftNeutral right = plusZeroRightNeutral right
 
 export
 multOneRightNeutral : (left : Nat) -> left * 1 = left
-multOneRightNeutral Z        = Refl
-multOneRightNeutral (S left) =
-  let inductiveHypothesis = multOneRightNeutral left in
-    rewrite inductiveHypothesis in
-            Refl
+multOneRightNeutral left = rewrite multCommutative left 1 in multOneLeftNeutral left
 
 
--- Proofs on -
+-- Proofs on minus
 
 export
-minusSuccSucc : (left : Nat) -> (right : Nat) -> minus (S left) (S right) = minus left right
-minusSuccSucc left right = Refl
+minusSuccSucc : (left, right : Nat) ->
+  minus (S left) (S right) = minus left right
+minusSuccSucc _ _ = Refl
 
 export
 minusZeroLeft : (right : Nat) -> minus 0 right = Z
-minusZeroLeft right = Refl
+minusZeroLeft - = Refl
 
 export
 minusZeroRight : (left : Nat) -> minus left 0 = left
-minusZeroRight Z        = Refl
-minusZeroRight (S left) = Refl
+minusZeroRight Z     = Refl
+minusZeroRight (S _) = Refl
 
 export
 minusZeroN : (n : Nat) -> Z = minus n n
@@ -445,53 +419,47 @@ minusOneSuccN (S n) = minusOneSuccN n
 export
 minusSuccOne : (n : Nat) -> minus (S n) 1 = n
 minusSuccOne Z     = Refl
-minusSuccOne (S n) = Refl
+minusSuccOne (S _) = Refl
 
 export
-minusPlusZero : (n : Nat) -> (m : Nat) -> minus n (n + m) = Z
-minusPlusZero Z     m = Refl
+minusPlusZero : (n, m : Nat) -> minus n (n + m) = Z
+minusPlusZero Z     _ = Refl
 minusPlusZero (S n) m = minusPlusZero n m
 
 export
-minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
+minusMinusMinusPlus : (left, centre, right : Nat) ->
   minus (minus left centre) right = minus left (centre + right)
-minusMinusMinusPlus Z        Z          right = Refl
-minusMinusMinusPlus (S left) Z          right = Refl
-minusMinusMinusPlus Z        (S centre) right = Refl
+minusMinusMinusPlus Z Z _ = Refl
+minusMinusMinusPlus (S _) Z _ = Refl
+minusMinusMinusPlus Z (S _) _ = Refl
 minusMinusMinusPlus (S left) (S centre) right =
-  let inductiveHypothesis = minusMinusMinusPlus left centre right in
-      rewrite inductiveHypothesis in
-              Refl
+  rewrite minusMinusMinusPlus left centre right in Refl
 
 export
-plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
+plusMinusLeftCancel : (left, right : Nat) -> (right' : Nat) ->
   minus (left + right) (left + right') = minus right right'
-plusMinusLeftCancel Z right right'        = Refl
+plusMinusLeftCancel Z _ _ = Refl
 plusMinusLeftCancel (S left) right right' =
-  let inductiveHypothesis = plusMinusLeftCancel left right right' in
-      rewrite inductiveHypothesis in
-              Refl
+  rewrite plusMinusLeftCancel left right right' in Refl
 
 export
-multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
-                               (minus left centre) * right = minus (left * right) (centre * right)
-multDistributesOverMinusLeft Z        Z          right = Refl
-multDistributesOverMinusLeft (S left) Z          right =
-  rewrite (minusZeroRight (plus right (mult left right))) in Refl
-multDistributesOverMinusLeft Z        (S centre) right = Refl
+multDistributesOverMinusLeft : (left, centre, right : Nat) ->
+  (minus left centre) * right = minus (left * right) (centre * right)
+multDistributesOverMinusLeft Z Z _ = Refl
+multDistributesOverMinusLeft (S left) Z right =
+  rewrite minusZeroRight (right + (left * right)) in Refl
+multDistributesOverMinusLeft Z (S _) _ = Refl
 multDistributesOverMinusLeft (S left) (S centre) right =
-  let inductiveHypothesis = multDistributesOverMinusLeft left centre right in
-      rewrite inductiveHypothesis in
-      rewrite plusMinusLeftCancel right (mult left right) (mult centre right) in
-              Refl
-
-export
-multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
-                                left * (minus centre right) = minus (left * centre) (left * right)
-multDistributesOverMinusRight left centre right =
-  rewrite multCommutative left (minus centre right) in
-  rewrite multDistributesOverMinusLeft centre right left in
-  rewrite multCommutative centre left in
-  rewrite multCommutative right left in
+  rewrite multDistributesOverMinusLeft left centre right in
+  rewrite plusMinusLeftCancel right (left * right) (centre * right) in
           Refl
 
+export
+multDistributesOverMinusRight : (left, centre, right : Nat) ->
+  left * (minus centre right) = minus (left * centre) (left * right)
+multDistributesOverMinusRight left centre right =
+    rewrite multCommutative left (minus centre right) in
+    rewrite multDistributesOverMinusLeft centre right left in
+    rewrite multCommutative centre left in
+    rewrite multCommutative right left in
+            Refl