Merge pull request #4818 from nickdrozd/proofs

Simplify some Nat proofs
2024-09-11 08:55:23 +03:00 · 2020-02-29 14:19:08 +01:00 · 2020-02-29 14:19:08 +01:00 · 3d83aa0345
commit 3d83aa0345
parent 10b7fe8bca 1653d3ead0
2 changed files with 146 additions and 112 deletions
--- a/libs/contrib/Data/Nat/Parity.idr
+++ b/libs/contrib/Data/Nat/Parity.idr
@ -2,18 +2,9 @@ module Data.Nat.Parity

 %access public export

--------------------------------------------------------------------------------
-- Parity
--------------------------------------------------------------------------------
+----------------------------------------

-mutual
-  even : Nat -> Bool
-  even Z = True
-  even (S k) = odd k
-
-  odd : Nat -> Bool
-  odd Z = False
-  odd (S k) = even k
+-- Type-level, constructive definitions of parity.

 ||| A nat is Even when it is twice some other nat.
 Even : Nat -> Type
@ -23,6 +14,8 @@ Even n = (half : Nat ** n = half * 2)
 Odd : Nat -> Type
 Odd n = (haf : Nat ** n = S $ haf * 2)

+----------------------------------------
+
 ||| Two more than an Even is Even.
 add2Even : Even n -> Even (2 + n)
 add2Even (half ** pf) = (S half ** cong {f = (+) 2} pf)
@ -52,20 +45,73 @@ succDoublePredPred {k = S _} prf = cong {f = Nat.pred} prf
 predEvenOdd : Even (S n) -> Odd n
 predEvenOdd (half ** pf) = (pred half ** succDoublePredPred pf)

+----------------------------------------
+
+-- Boolean definitions of parity.
+
+mutual
+  even : Nat -> Bool
+  even Z = True
+  even (S k) = odd k
+
+  odd : Nat -> Bool
+  odd Z = False
+  odd (S k) = even k
+
+----------------------------------------
+
+-- The boolean and type-level definitions are equivalent in the sense
+-- that a proof of one can be gotten from a proof of the other.
+
+mutual
+  ||| Evens are even.
+  evenEven : Even n -> even n = True
+  evenEven {n = Z} _ = Refl
+  evenEven {n = S _} pf = oddOdd $ predEvenOdd pf
+
+  ||| Odds are odd.
+  oddOdd : Odd n -> odd n = True
+  oddOdd {n = Z} (_ ** pf) = absurd pf
+  oddOdd {n = S _} pf = evenEven $ predOddEven pf
+
+mutual
+  ||| If it's even, it's Even.
+  evenEvenConverse : even n = True -> Even n
+  evenEvenConverse {n = Z} prf = (0 ** Refl)
+  evenEvenConverse {n = S k} prf =
+    let (haf ** pf) = oddOddConverse prf in
+      (S haf ** cong pf)
+
+  ||| If it's odd, it's Odd
+  oddOddConverse : odd n = True -> Odd n
+  oddOddConverse {n = Z} prf = absurd prf
+  oddOddConverse {n = S k} prf =
+    let (half ** pf) = evenEvenConverse prf in
+      (half ** cong pf)
+
+----------------------------------------
+
+||| Every nat is either even or odd.
+evenorodd : (n : Nat) -> Either (even n = True) (odd n = True)
+evenorodd Z = Left Refl
+evenorodd (S k) = case evenorodd k of
+  Left l => Right l
+  Right r => Left r
+
 ||| Every nat is either Even or Odd.
 evenOrOdd : (n : Nat) -> Either (Even n) (Odd n)
-evenOrOdd Z = Left (0 ** Refl)
-evenOrOdd (S k) = case evenOrOdd k of
-  Left (half ** pf) => Right (half ** cong {f = S} pf)
-  Right (haf ** pf) => Left (S haf ** cong {f = S} pf)
+evenOrOdd n = case evenorodd n of
+  Left e => Left $ evenEvenConverse e
+  Right o => Right $ oddOddConverse o
+
+||| No nat is both even and odd.
+notevenandodd : even n = True -> odd n = True -> Void
+notevenandodd {n = Z} en on = absurd on
+notevenandodd {n = S _} en on = notevenandodd on en

 ||| No nat is both Even and Odd.
 notEvenAndOdd : Even n -> Odd n -> Void
-notEvenAndOdd {n = Z} _ (_ ** odd) = absurd odd
-notEvenAndOdd {n = (S k)} (half ** even) (haf ** odd) =
-  notEvenAndOdd {n = k}
-   (haf ** cong {f = Nat.pred} odd)
-   (pred half ** succDoublePredPred even)
+notEvenAndOdd en on = notevenandodd (evenEven en) (oddOdd on)

 ||| Evenness is decidable.
 evenDec : (n : Nat) -> Dec $ Even n
@ -79,42 +125,46 @@ oddDec n = case evenOrOdd n of
  Left even => No $ notEvenAndOdd even
  Right odd => Yes odd

-mutual
-  ||| Evens are even.
-  evenEven : Even n -> even n = True
-  evenEven {n = Z} _ = Refl
-  evenEven {n = S _} pf = oddOdd $ predEvenOdd pf
+----------------------------------------

-  ||| Odds are odd.
-  oddOdd : Odd n -> odd n = True
-  oddOdd {n = Z} (_ ** pf) = absurd pf
-  oddOdd {n = S _} pf = evenEven $ predOddEven pf
+||| An Odd is the successor of an Even.
+oddSuccEven : Odd n -> (m : Nat ** (n = S m, Even m))
+oddSuccEven (haf ** pf) = (haf * 2 ** (pf, (haf ** Refl)))

 ||| Even plus Even is Even.
 evenPlusEven : Even j -> Even k -> Even (j + k)
 evenPlusEven (half_j ** pf_j) (half_k ** pf_k) =
-  rewrite pf_j in
-    rewrite pf_k in
-      (half_j + half_k **
+  (half_j + half_k **
+    rewrite pf_j in
+      rewrite pf_k in
        sym $ multDistributesOverPlusLeft half_j half_k 2)

-||| Odd plus Odd is Even.
-oddPlusOdd : Odd j -> Odd k -> Even (j + k)
-oddPlusOdd (haf_j ** pf_j) (haf_k ** pf_k) =
-  rewrite pf_j in
-    rewrite pf_k in
-      rewrite sym $ plusSuccRightSucc (haf_j * 2) (haf_k * 2) in
-        rewrite sym $ multDistributesOverPlusLeft haf_j haf_k 2 in
-          (S (haf_j + haf_k) ** Refl)
+||| Odd plus Even is Odd.
+oddPlusEven : Odd j -> Even k -> Odd (j + k)
+oddPlusEven oj ek =
+  let
+    (i ** (ipj, ei)) = oddSuccEven oj
+    (half_ik ** eik) = evenPlusEven ei ek
+      in
+  (half_ik **
+    rewrite ipj in
+      cong {f = S} eik)

 ||| Even plus Odd is Odd.
 evenPlusOdd : Even j -> Odd k -> Odd (j + k)
-evenPlusOdd (half_j ** pf_j) (haf_k ** pf_k) =
-  rewrite pf_j in
-    rewrite pf_k in
-      rewrite sym $ plusSuccRightSucc (half_j * 2) (haf_k * 2) in
-        rewrite sym $ multDistributesOverPlusLeft half_j haf_k 2 in
-          (half_j + haf_k ** Refl)
+evenPlusOdd {j} {k} ej ok = rewrite plusCommutative j k in oddPlusEven ok ej
+
+||| Odd plus Odd is Even.
+oddPlusOdd : Odd j -> Odd k -> Even (j + k)
+oddPlusOdd oj ok =
+  let
+    (i ** (ipj, ei)) = oddSuccEven oj
+    (haf_ik ** oik) = evenPlusOdd ei ok
+      in
+  (S haf_ik **
+    rewrite ipj in
+      rewrite oik in
+        Refl)

 ||| A helper fact.
 multShuffle : (a, b, c : Nat) ->
@ -129,35 +179,39 @@ multShuffle a b c =
 ||| Even times Even is Even.
 evenMultEven : Even j -> Even k -> Even (j * k)
 evenMultEven (half_j ** pf_j) (half_k ** pf_k) =
-  rewrite pf_j in
-    rewrite pf_k in
-      (half_j * half_k * 2 **
+  (half_j * half_k * 2 **
+    rewrite pf_j in
+      rewrite pf_k in
        multShuffle half_j half_k 2)

+||| Odd times Even is Even.
+oddMultEven : Odd j -> Even k -> Even (j * k)
+oddMultEven oj (half_k ** pf_k) =
+  let
+    (i ** (ipj, ei)) = oddSuccEven oj
+    (half_ik ** oik) = evenMultEven ei (half_k ** pf_k)
+      in
+  (half_k + half_ik **
+    rewrite multDistributesOverPlusLeft half_k half_ik 2 in
+      rewrite ipj in
+        rewrite oik in
+          rewrite pf_k in
+            Refl)
+
 ||| Even times Odd is Even.
 evenMultOdd : Even j -> Odd k -> Even (j * k)
-evenMultOdd (half_j ** pf_j) (haf_k ** pf_k) =
-  let half = half_j * haf_k * 2 in
-    rewrite pf_j in
-      rewrite pf_k in
-        rewrite multRightSuccPlus (half_j * 2) (haf_k * 2) in
-          rewrite multShuffle half_j haf_k 2 in
-            (half_j + half **
-              sym $ multDistributesOverPlusLeft half_j half 2)
+evenMultOdd {j} {k} ej ok = rewrite multCommutative j k in oddMultEven ok ej

 ||| Odd times Odd is Odd.
 oddMultOdd : Odd j -> Odd k -> Odd (j * k)
-oddMultOdd (haf_j ** pf_j) (haf_k ** pf_k) =
+oddMultOdd oj (haf_k ** pf_k) =
  let
-    haf = haf_j * haf_k * 2
-    rem = haf_j + haf_k
+    (i ** (ipj, ei)) = oddSuccEven oj
+    (half_ik ** eik) = evenMultOdd ei (haf_k ** pf_k)
      in
-  rewrite pf_j in
-    rewrite pf_k in
-      rewrite multRightSuccPlus (haf_j * 2) (haf_k * 2) in
-        rewrite multShuffle haf_j haf_k 2 in
-          rewrite plusAssociative (haf_k * 2) (haf_j * 2) (haf * 2) in
-            rewrite sym $ multDistributesOverPlusLeft haf_k haf_j 2 in
-              rewrite plusCommutative haf_k haf_j in
-                rewrite sym $ multDistributesOverPlusLeft rem haf 2 in
-                  (rem + haf ** Refl)
+  (haf_k + half_ik **
+    rewrite multDistributesOverPlusLeft haf_k half_ik 2 in
+      rewrite ipj in
+        rewrite eik in
+          rewrite pf_k in
+            Refl)
--- a/libs/prelude/Prelude/Nat.idr
+++ b/libs/prelude/Prelude/Nat.idr
@ -512,19 +512,18 @@ plusLeftCancel (S left) right right' p =

 total 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 p =
+  plusLeftCancel right left left' $
+    rewrite plusCommutative right left in
+      rewrite plusCommutative right left' in
+        p

 total 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 p =
+  plusLeftCancel left right Z $
+    rewrite plusZeroRightNeutral left in
+      p

 -- Mult
 total multZeroLeftZero : (right : Nat) -> Z * right = Z
@ -573,12 +572,11 @@ multDistributesOverPlusRight (S left) centre right =

 total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (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 (mult left right) (mult centre right) in
-            Refl
+multDistributesOverPlusLeft left centre right =
+  rewrite multCommutative (left + centre) right in
+    rewrite multCommutative left right in
+      rewrite multCommutative centre right in
+        multDistributesOverPlusRight right left centre

 total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
  left * (centre * right) = (left * centre) * right
@ -597,11 +595,7 @@ multOneLeftNeutral (S right) =
            Refl

 total 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

 -- Minus
 total minusSuccSucc : (left : Nat) -> (right : Nat) ->
@ -689,10 +683,7 @@ total powerZeroOne : (base : Nat) -> power base 0 = S Z
 powerZeroOne base = Refl

 total powerOneNeutral : (base : Nat) -> power base 1 = base
-powerOneNeutral Z        = Refl
-powerOneNeutral (S base) =
-  let inductiveHypothesis = powerOneNeutral base in
-    rewrite inductiveHypothesis in Refl
+powerOneNeutral base = rewrite multCommutative base 1 in multOneLeftNeutral base

 total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z
 powerOneSuccOne Z       = Refl
@ -701,8 +692,7 @@ powerOneSuccOne (S exp) =
    rewrite inductiveHypothesis in Refl

 total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
-powerSuccSuccMult Z        = Refl
-powerSuccSuccMult (S base) = rewrite multOneRightNeutral base in Refl
+powerSuccSuccMult base = rewrite multOneRightNeutral base in Refl

 total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
  power (power base exp) exp' = power base (exp * exp')
@ -796,34 +786,24 @@ minimumIdempotent Z = Refl
 minimumIdempotent (S k) = cong (minimumIdempotent k)

 total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z
-minimumZeroZeroRight Z = Refl
-minimumZeroZeroRight (S right) = minimumZeroZeroRight right
+minimumZeroZeroRight right = Refl

 total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
-minimumZeroZeroLeft Z        = Refl
-minimumZeroZeroLeft (S left) = Refl
+minimumZeroZeroLeft left = rewrite minimumCommutative left 0 in Refl

 total minimumSuccSucc : (left : Nat) -> (right : Nat) ->
  minimum (S left) (S right) = S (minimum left right)
-minimumSuccSucc Z        Z         = Refl
-minimumSuccSucc (S left) Z         = Refl
-minimumSuccSucc Z        (S right) = Refl
-minimumSuccSucc (S left) (S right) = Refl
+minimumSuccSucc left right = Refl

 total maximumZeroNRight : (right : Nat) -> maximum Z right = right
-maximumZeroNRight Z         = Refl
-maximumZeroNRight (S right) = Refl
+maximumZeroNRight right = Refl

 total maximumZeroNLeft : (left : Nat) -> maximum left Z = left
-maximumZeroNLeft Z        = Refl
-maximumZeroNLeft (S left) = Refl
+maximumZeroNLeft left = rewrite maximumCommutative left Z in Refl

 total maximumSuccSucc : (left : Nat) -> (right : Nat) ->
  S (maximum left right) = maximum (S left) (S right)
-maximumSuccSucc Z        Z         = Refl
-maximumSuccSucc (S left) Z         = Refl
-maximumSuccSucc Z        (S right) = Refl
-maximumSuccSucc (S left) (S right) = Refl
+maximumSuccSucc left right = Refl

 total sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
 sucMaxL Z = Refl