Add some helpers for transforming equations and inequalities on Nat.

libs/contrib/Data/Nat/Equational.idr

@@ -0,0 +1,70 @@
+module Data.Nat.Equational
+
+import Data.Nat
+
+%default total
+
+
+||| Subtract a number from both sides of an equation.
+||| Due to partial nature of subtraction in natural numbers, an equation of
+||| special form is required in order for subtraction to be total.
+export
+subtractEqLeft : (a : Nat) -> {b, c : Nat} -> a + b = a + c -> b = c
+subtractEqLeft 0 prf = prf
+subtractEqLeft (S k) prf = subtractEqLeft k $ succInjective (k + b) (k + c) prf
+
+||| Subtract a number from both sides of an equation.
+||| Due to partial nature of subtraction in natural numbers, an equation of
+||| special form is required in order for subtraction to be total.
+export
+subtractEqRight : {a, b : Nat} -> (c : Nat) -> a + c = b + c -> a = b
+subtractEqRight c prf =
+    subtractEqLeft c $
+    rewrite plusCommutative c a in
+    rewrite plusCommutative c b in
+    prf
+
+||| Add a number to both sides of an inequality
+export
+plusLteLeft : (a : Nat) -> {b, c : Nat} -> LTE b c -> LTE (a + b) (a + c)
+plusLteLeft 0 bLTEc = bLTEc
+plusLteLeft (S k) bLTEc = LTESucc $ plusLteLeft k bLTEc
+
+||| Add a number to both sides of an inequality
+export
+plusLteRight : {a, b : Nat} -> (c : Nat) -> LTE a b -> LTE (a + c) (b + c)
+plusLteRight c aLTEb =
+    rewrite plusCommutative a c in
+    rewrite plusCommutative b c in
+    plusLteLeft c aLTEb
+
+||| Subtract a number from both sides of an inequality.
+||| Due to partial nature of subtraction, we require an inequality of special form.
+export
+subtractLteLeft : (a : Nat) -> {b, c : Nat} -> LTE (a + b) (a + c) -> LTE b c
+subtractLteLeft 0 abLTEac = abLTEac
+subtractLteLeft (S k) abLTEac = subtractLteLeft k $ fromLteSucc abLTEac
+
+||| Subtract a number from both sides of an inequality.
+||| Due to partial nature of subtraction, we require an inequality of special form.
+export
+subtractLteRight : {a, b : Nat} -> (c : Nat) -> LTE (a + c) (b + c) -> LTE a b
+subtractLteRight c acLTEbc =
+    subtractLteLeft c $
+    rewrite plusCommutative c a in
+    rewrite plusCommutative c b in
+    acLTEbc
+
+||| If one of the factors of a product is greater than 0, then the other factor
+||| is less than or equal to the product..
+export
+rightFactorLteProduct : (a, b : Nat) -> LTE b (S a * b)
+rightFactorLteProduct a b = lteAddRight b
+
+||| If one of the factors of a product is greater than 0, then the other factor
+||| is less than or equal to the product..
+export
+leftFactorLteProduct : (a, b : Nat) -> LTE a (a * S b)
+leftFactorLteProduct a b =
+    rewrite multRightSuccPlus a b in
+    lteAddRight a