0 | module Data.Nat.Equational
 1 |
 2 | import Data.Nat
 3 |
 4 | %default total
 5 |
 6 |
 7 | ||| Subtract a number from both sides of an equation.
 8 | ||| Due to partial nature of subtraction in natural numbers, an equation of
 9 | ||| special form is required in order for subtraction to be total.
10 | export
11 | subtractEqLeft : (a : Nat) -> {b, c : Nat} -> a + b = a + c -> b = c
12 | subtractEqLeft 0 prf = prf
13 | subtractEqLeft (S k) prf = subtractEqLeft k $ injective prf
14 |
15 | ||| Subtract a number from both sides of an equation.
16 | ||| Due to partial nature of subtraction in natural numbers, an equation of
17 | ||| special form is required in order for subtraction to be total.
18 | export
19 | subtractEqRight : {a, b : Nat} -> (c : Nat) -> a + c = b + c -> a = b
20 | subtractEqRight c prf =
21 |     subtractEqLeft c $
22 |     rewrite plusCommutative c a in
23 |     rewrite plusCommutative c b in
24 |     prf
25 |
26 | ||| Add a number to both sides of an inequality
27 | export
28 | plusLteLeft : (a : Nat) -> {b, c : Nat} -> LTE b c -> LTE (a + b) (a + c)
29 | plusLteLeft 0 bLTEc = bLTEc
30 | plusLteLeft (S k) bLTEc = LTESucc $ plusLteLeft k bLTEc
31 |
32 | ||| Add a number to both sides of an inequality
33 | export
34 | plusLteRight : {a, b : Nat} -> (c : Nat) -> LTE a b -> LTE (a + c) (b + c)
35 | plusLteRight c aLTEb =
36 |     rewrite plusCommutative a c in
37 |     rewrite plusCommutative b c in
38 |     plusLteLeft c aLTEb
39 |
40 | ||| Only 0 is lte 0
41 | ||| Useful when the argument is an open term
42 | export
43 | lteZeroIsZero : a `LTE` 0 -> a = 0
44 | lteZeroIsZero LTEZero = Refl
45 |
46 | ||| Subtract a number from both sides of an inequality.
47 | ||| Due to partial nature of subtraction, we require an inequality of special form.
48 | export
49 | subtractLteLeft : (a : Nat) -> {b, c : Nat} -> LTE (a + b) (a + c) -> LTE b c
50 | subtractLteLeft 0 abLTEac = abLTEac
51 | subtractLteLeft (S k) abLTEac = subtractLteLeft k $ fromLteSucc abLTEac
52 |
53 | ||| Subtract a number from both sides of an inequality.
54 | ||| Due to partial nature of subtraction, we require an inequality of special form.
55 | export
56 | subtractLteRight : {a, b : Nat} -> (c : Nat) -> LTE (a + c) (b + c) -> LTE a b
57 | subtractLteRight c acLTEbc =
58 |     subtractLteLeft c $
59 |     rewrite plusCommutative c a in
60 |     rewrite plusCommutative c b in
61 |     acLTEbc
62 |
63 | ||| If one of the factors of a product is greater than 0, then the other factor
64 | ||| is less than or equal to the product..
65 | export
66 | rightFactorLteProduct : (a, b : Nat) -> LTE b (S a * b)
67 | rightFactorLteProduct a b = lteAddRight b
68 |
69 | ||| If one of the factors of a product is greater than 0, then the other factor
70 | ||| is less than or equal to the product..
71 | export
72 | leftFactorLteProduct : (a, b : Nat) -> LTE a (a * S b)
73 | leftFactorLteProduct a b =
74 |     rewrite multRightSuccPlus a b in
75 |     lteAddRight a
76 |