Arithmetic.Lt

Special Inequalities

zero :: 0 < 1

Zero is less than one.

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 strict 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 strict inequality.

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 strict 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 strict inequality.

Composition

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

Add a strict inequality to a nonstrict inequality.

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

Compose two strict inequalities using transitivity.

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

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

Compose a strict inequality (the first argument) with a nonstrict inequality (the second argument).

Convert to Inequality

toLteL :: (a < b) -> (1 + a) <= b

toLteR :: (a < b) -> (a + 1) <= b

Absurdities

absurd :: (n < 0) -> void

Nothing is less than zero.

Integration with GHC solver

constant :: forall a b. CmpNat a b ~ LT => a < b

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