Simplify Decidable.Order

This commit makes strictly nonfunctional / style changes to the Order
module, like:

  - using `%default total` instead of explicitly marking every
    function as total;

  - grouping arguments of the same type, as in `(a, b, c : t)`;

  - underscoring unused arguments;

  - cutting the useless `implementation` keyword; and

  - proving interface constraints directly in implementation blocks.

All of these changes make the code a little nicer to look at.

Author: nickdrozd

libs/contrib/Decidable/Order.idr

@@ -7,33 +7,27 @@ import Data.Fun
 import Data.Rel
 
 %access public export
-
---------------------------------------------------------------------------------
--- Utility Lemmas
---------------------------------------------------------------------------------
+%default total
 
 --------------------------------------------------------------------------------
 -- Preorders, Posets, total Orders, Equivalencies, Congruencies
 --------------------------------------------------------------------------------
 
 interface Preorder t (po : t -> t -> Type) where
-  total transitive : (a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c
-  total reflexive : (a : t) -> po a a
+  transitive : (a, b, c : t) -> po a b -> po b c -> po a c
+  reflexive : (a : t) -> po a a
 
 interface (Preorder t po) => Poset t (po : t -> t -> Type) where
-  total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b
+  antisymmetric : (a, b : t) -> po a b -> po b a -> a = b
 
 interface (Poset t to) => Ordered t (to : t -> t -> Type) where
-  total order : (a : t) -> (b : t) -> Either (to a b) (to b a)
+  order : (a, b : t) -> Either (to a b) (to b a)
 
 interface (Preorder t eq) => Equivalence t (eq : t -> t -> Type) where
-  total symmetric : (a : t) -> (b : t) -> eq a b -> eq b a
+  symmetric : (a, b : t) -> eq a b -> eq b a
 
 interface (Equivalence t eq) => Congruence t (f : t -> t) (eq : t -> t -> Type) where
-  total congruent : (a : t) -> 
-                    (b : t) -> 
-                    eq a b -> 
-                    eq (f a) (f b)
+  congruent : (a, b : t) -> eq a b -> eq (f a) (f b)
 
 minimum : (Ordered t to) => t -> t -> t
 minimum {to} x y with (order {to} x y)
@@ -49,79 +43,62 @@ maximum {to} x y with (order {to} x y)
 -- Syntactic equivalence (=)
 --------------------------------------------------------------------------------
 
-implementation Preorder t ((=) {A = t} {B = t}) where
-  transitive a b c = trans {a = a} {b = b} {c = c}
-  reflexive a = Refl
+Preorder t (=) where
+  transitive _ _ _ = trans
+  reflexive _ = Refl
 
-implementation Equivalence t ((=) {A = t} {B = t}) where
-  symmetric a b prf = sym prf
+Equivalence t (=) where
+  symmetric _ _ = sym
 
-implementation Congruence t f ((=) {A = t} {B = t}) where
-  congruent a b = cong {a = a} {b = b} {f = f}
+Congruence t f (=) where
+  congruent _ _ = cong
 
 --------------------------------------------------------------------------------
 -- Natural numbers
 --------------------------------------------------------------------------------
 
-total LTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->
-                           LTE m n -> LTE n o ->
-                           LTE m o
-LTEIsTransitive Z n o                 LTEZero                  nlteo   = LTEZero
-LTEIsTransitive (S m) (S n) (S o) (LTESucc mlten)    (LTESucc nlteo)   = LTESucc (LTEIsTransitive m n o mlten nlteo)
-
-total LTEIsReflexive : (n : Nat) -> LTE n n
-LTEIsReflexive Z      = LTEZero
-LTEIsReflexive (S n)  = LTESucc (LTEIsReflexive n)
-
-implementation Preorder Nat LTE where
-  transitive = LTEIsTransitive
-  reflexive  = LTEIsReflexive
-
-total LTEIsAntisymmetric : (m : Nat) -> (n : Nat) ->
-                              LTE m n -> LTE n m -> m = n
-LTEIsAntisymmetric Z Z         LTEZero LTEZero = Refl
-LTEIsAntisymmetric (S n) (S m) (LTESucc mLTEn) (LTESucc nLTEm) with (LTEIsAntisymmetric n m mLTEn nLTEm)
-   LTEIsAntisymmetric (S n) (S n) (LTESucc mLTEn) (LTESucc nLTEm)    | Refl = Refl           
-
-
-implementation Poset Nat LTE where
-  antisymmetric = LTEIsAntisymmetric
-
-total zeroNeverGreater : {n : Nat} -> LTE (S n) Z -> Void
-zeroNeverGreater {n} LTEZero     impossible
-zeroNeverGreater {n} (LTESucc _) impossible
-
-total zeroAlwaysSmaller : {n : Nat} -> LTE Z n
-zeroAlwaysSmaller = LTEZero
-
-total ltesuccinjective : {n : Nat} -> {m : Nat} -> (LTE n m -> Void) -> LTE (S n) (S m) -> Void
-ltesuccinjective {n} {m} disprf (LTESucc nLTEm) = void (disprf nLTEm)
-ltesuccinjective {n} {m} disprf LTEZero         impossible
-
-
-total decideLTE : (n : Nat) -> (m : Nat) -> Dec (LTE n m)
-decideLTE    Z      y  = Yes LTEZero
-decideLTE (S x)     Z  = No  zeroNeverGreater
+Preorder Nat LTE where
+  transitive Z _ _ _ _ = LTEZero
+  transitive (S m) (S n) (S o) (LTESucc mlten) (LTESucc nlteo) =
+    LTESucc (transitive m n o mlten nlteo)
+
+  reflexive Z      = LTEZero
+  reflexive (S n)  = LTESucc (reflexive n)
+
+Poset Nat LTE where
+  antisymmetric Z Z LTEZero LTEZero = Refl
+  antisymmetric (S n) (S m) (LTESucc mLTEn) (LTESucc nLTEm)
+                with (antisymmetric n m mLTEn nLTEm)
+    antisymmetric _ _ _ _ | Refl = Refl
+
+decideLTE : (n, m : Nat) -> Dec (LTE n m)
+decideLTE    Z      _  = Yes LTEZero
+decideLTE (S _)     Z  = No  zeroNeverGreater where
+  zeroNeverGreater : LTE (S _) Z -> Void
+  zeroNeverGreater LTEZero     impossible
+  zeroNeverGreater (LTESucc _) impossible
 decideLTE (S x)   (S y) with (decEq (S x) (S y))
   | Yes eq      = rewrite eq in Yes (reflexive (S y))
   | No _ with (decideLTE x y)
     | Yes nLTEm = Yes (LTESucc nLTEm)
     | No  nGTm  = No (ltesuccinjective nGTm)
+    where
+      ltesuccinjective : (LTE n m -> Void) -> LTE (S n) (S m) -> Void
+      ltesuccinjective disprf (LTESucc nLTEm) = void (disprf nLTEm)
+      ltesuccinjective _ LTEZero impossible
 
-implementation Decidable [Nat,Nat] LTE where
+Decidable [Nat, Nat] LTE where
   decide = decideLTE
 
-total
-lte : (m : Nat) -> (n : Nat) -> Dec (LTE m n)
-lte m n = decide {ts = [Nat,Nat]} {p = LTE} m n
-
-total
-shift : (m : Nat) -> (n : Nat) -> LTE m n -> LTE (S m) (S n)
-shift m n mLTEn = LTESucc mLTEn
-      
-implementation Ordered Nat LTE where
-  order Z      n = Left LTEZero
-  order m      Z = Right LTEZero
+lte : (m, n : Nat) -> Dec (LTE m n)
+lte m n = decide {ts = [Nat, Nat]} {p = LTE} m n
+
+shift : (m, n : Nat) -> LTE m n -> LTE (S m) (S n)
+shift _ _ mLTEn = LTESucc mLTEn
+
+Ordered Nat LTE where
+  order Z      _ = Left LTEZero
+  order _      Z = Right LTEZero
   order (S k) (S j) with (order {to=LTE} k j)
     order (S k) (S j) | Left  prf = Left  (shift k j prf)
     order (S k) (S j) | Right prf = Right (shift j k prf)
@@ -132,25 +109,24 @@ implementation Ordered Nat LTE where
 
 using (k : Nat)
   data FinLTE : Fin k -> Fin k -> Type where
-    FromNatPrf : {m : Fin k} -> {n : Fin k} -> LTE (finToNat m) (finToNat n) -> FinLTE m n
+    FromNatPrf : LTE (finToNat m) (finToNat n) -> FinLTE m n
 
-  implementation Preorder (Fin k) FinLTE where
-    transitive m n o (FromNatPrf p1) (FromNatPrf p2) = 
-      FromNatPrf (LTEIsTransitive (finToNat m) (finToNat n) (finToNat o) p1 p2)
-    reflexive n = FromNatPrf (LTEIsReflexive (finToNat n))
+  Preorder (Fin k) FinLTE where
+    transitive m n o (FromNatPrf p1) (FromNatPrf p2) =
+      FromNatPrf (transitive (finToNat m) (finToNat n) (finToNat o) p1 p2)
+    reflexive n = FromNatPrf (reflexive (finToNat n))
 
-  implementation Poset (Fin k) FinLTE where
+  Poset (Fin k) FinLTE where
     antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) =
-      finToNatInjective m n (LTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)
-  
-  implementation Decidable [Fin k, Fin k] FinLTE where
+      finToNatInjective m n (antisymmetric (finToNat m) (finToNat n) p1 p2)
+
+  Decidable [Fin k, Fin k] FinLTE where
     decide m n with (decideLTE (finToNat m) (finToNat n))
       | Yes prf    = Yes (FromNatPrf prf)
-      | No  disprf = No (\ (FromNatPrf prf) => disprf prf)
+      | No  disprf = No (\(FromNatPrf prf) => disprf prf)
 
-  implementation Ordered (Fin k) FinLTE where
+  Ordered (Fin k) FinLTE where
     order m n =
-      either (Left . FromNatPrf) 
+      either (Left . FromNatPrf)
              (Right . FromNatPrf)
              (order (finToNat m) (finToNat n))
-