add min/max functions and theorems

src/Data/Nat.hs

@@ -19,7 +19,7 @@ import Data.Bool
 import Data.Integer              (Integer)
 import Data.Function             (id, const, (∘))
 import Data.TypeClass            (Eq, Show, Num, Enum, Bounded)
-import Data.Singletons.TH hiding ((:<), (:>), (%:<), Refl)
+import Data.Singletons.TH hiding ((:<), (:>), (%:<), Refl, Min, sMin, Max, sMax)
 
 import qualified Data.TypeClass as T
 
@@ -66,6 +66,15 @@ singletons [d|
   (>) ∷ ℕ → ℕ → 𝔹
   n > m = (¬) (n < m)
 
+  min ∷ ℕ → ℕ → ℕ
+  min Z    _ = Z
+  min _    Z = Z
+  min (S n) (S m) = S (min n m)
+
+  max ∷ ℕ → ℕ → ℕ
+  max Z        n  = n
+  max n        Z  = n
+  max (S n) (S m) = S (max n m)
   |]
 
 
@@ -157,6 +166,17 @@ plus_assoc (SS a) b c = cong SS (plus_assoc a b c)
 
 -- | Commutative property of addition
 plus_commut ∷ Sℕ n → Sℕ m → (n :+ m) :≡ (m :+ n)
-plus_commut n   SZ    = plus_right_id n
+plus_commut n  SZ    = plus_right_id n
 plus_commut n  (SS m) =
   sym (succ_right n m) ∾ cong SS (plus_commut n m) ∾ succ_left m n
+
+-- | Minimum of itself
+min_self ∷ Sℕ n → Min n n :≡ n
+min_self SZ     = Refl
+min_self (SS n) = cong SS (min_self n)
+
+-- | Maximum of itself
+max_self ∷ Sℕ n → Max n n :≡ n
+max_self SZ     = Refl
+max_self (SS n) = cong SS (max_self n)
+