Arithmetic.Lte

Special Inequalities

zero :: 0 <= a

Zero is less-than-or-equal-to any number.

reflexive :: a <= a

Any number is less-than-or-equal-to itself.

Substitution

substituteL :: (b :=: c) -> (b <= a) -> c <= a

Replace the left-hand side of a strict inequality with an equal number.

substituteR :: (b :=: c) -> (a <= b) -> a <= c

Replace the right-hand side of a strict inequality with an equal number.

Increment

incrementL :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a <= b) -> (c + a) <= (c + b)

Add a constant to the left-hand side of both sides of the inequality.

incrementR :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a <= b) -> (a + c) <= (b + c)

Add a constant to the right-hand side of both sides of the inequality.

Decrement

decrementL :: forall (c :: Nat) (a :: Nat) (b :: Nat). ((c + a) <= (c + b)) -> a <= b

Subtract a constant from the left-hand side of both sides of the inequality. This is the opposite of incrementL.

decrementR :: forall (c :: Nat) (a :: Nat) (b :: Nat). ((a + c) <= (b + c)) -> a <= b

Subtract a constant from the right-hand side of both sides of the inequality. This is the opposite of incrementR.

Weaken

weakenL :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a <= b) -> a <= (c + b)

Add a constant to the left-hand side of the right-hand side of the inequality.

weakenR :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a <= b) -> a <= (b + c)

Add a constant to the right-hand side of the right-hand side of the inequality.

Composition

transitive :: (a <= b) -> (b <= c) -> a <= c

Compose two inequalities using transitivity.

plus :: (a <= b) -> (c <= d) -> (a + c) <= (b + d)

Add two inequalities.

Convert Strict Inequality

fromStrict :: (a < b) -> a <= b

Weaken a strict inequality to a non-strict inequality.

Integration with GHC solver

constant :: forall a b. IsLte (CmpNat a b) ~ True => a <= b

Use GHC's built-in type-level arithmetic to prove that one number is less-than-or-equal-to another. The type-checker only reduces CmpNat if both arguments are constants.