Data.Type.Nat.LE

Less-than-or-equal relation for (unary) natural numbers Nat.

There are at least three ways to encode this relation.

• \(zero : 0 \le m\) and \(succ : n \le m \to 1 + n \le 1 + m\) (this module),
• \(refl : n \le n \) and \(step : n \le m \to n \le 1 + m\) (Data.Type.Nat.LE.ReflStep),
• \(ex : \exists p. n + p \equiv m \) (tricky in Haskell).

Depending on a situation, usage ergonomics are different.

Relation

class LE n m where

Total order of Nat, less-than-or-Equal-to, \( \le \).

Methods

leProof :: LEProof n m

Instances

LE 'Z m

Defined in Data.Type.Nat.LE

Methods

leProof :: LEProof 'Z m

(m ~ 'S m', LE n m') => LE ('S n) m

Defined in Data.Type.Nat.LE

Methods

leProof :: LEProof ('S n) m

data LEProof n m where

An evidence of \(n \le m\). zero+succ definition.

Constructors

LEZero :: LEProof 'Z m

LESucc :: LEProof n m -> LEProof ('S n) ('S m)

Instances

Eq (LEProof n m)

LEProof values are unique (not Boring though!).

Defined in Data.Type.Nat.LE

Methods

(==) :: LEProof n m -> LEProof n m -> Bool

(/=) :: LEProof n m -> LEProof n m -> Bool

Ord (LEProof n m)

Defined in Data.Type.Nat.LE

Methods

compare :: LEProof n m -> LEProof n m -> Ordering

(<) :: LEProof n m -> LEProof n m -> Bool

(<=) :: LEProof n m -> LEProof n m -> Bool

(>) :: LEProof n m -> LEProof n m -> Bool

(>=) :: LEProof n m -> LEProof n m -> Bool

max :: LEProof n m -> LEProof n m -> LEProof n m

min :: LEProof n m -> LEProof n m -> LEProof n m

Show (LEProof n m)

Defined in Data.Type.Nat.LE

Methods

showsPrec :: Int -> LEProof n m -> ShowS

show :: LEProof n m -> String

showList :: [LEProof n m] -> ShowS

(SNatI n, SNatI m) => Decidable (LEProof n m)

Defined in Data.Type.Nat.LE

Methods

decide :: Dec (LEProof n m)

withLEProof :: LEProof n m -> (LE n m => r) -> r

Constructor LE dictionary from LEProof.

Decidability

decideLE :: forall n m. (SNatI n, SNatI m) => Dec (LEProof n m)

Find the LEProof n m, i.e. compare numbers.

Lemmas

Constructor like

leZero :: LEProof 'Z n

\(\forall n : \mathbb{N}, 0 \le n \)

leSucc :: LEProof n m -> LEProof ('S n) ('S m)

\(\forall n\, m : \mathbb{N}, n \le m \to 1 + n \le 1 + m \)

leRefl :: forall n. SNatI n => LEProof n n

\(\forall n : \mathbb{N}, n \le n \)

leStep :: LEProof n m -> LEProof n ('S m)

\(\forall n\, m : \mathbb{N}, n \le m \to n \le 1 + m \)

Partial order

leAsym :: LEProof n m -> LEProof m n -> n :~: m

\(\forall n\, m : \mathbb{N}, n \le m \to m \le n \to n \equiv m \)

leTrans :: LEProof n m -> LEProof m p -> LEProof n p

\(\forall n\, m\, p : \mathbb{N}, n \le m \to m \le p \to n \le p \)

Total order

leSwap :: forall n m. (SNatI n, SNatI m) => Neg (LEProof n m) -> LEProof ('S m) n

\(\forall n\, m : \mathbb{N}, \neg (n \le m) \to 1 + m \le n \)

leSwap' :: LEProof n m -> LEProof ('S m) n -> void

\(\forall n\, m : \mathbb{N}, n \le m \to \neg (1 + m \le n) \)

>>> leProof :: LEProof Nat2 Nat3
LESucc (LESucc LEZero)

>>> leSwap (leSwap' (leProof :: LEProof Nat2 Nat3))
LESucc (LESucc (LESucc LEZero))

>>> lePred (leSwap (leSwap' (leProof :: LEProof Nat2 Nat3)))
LESucc (LESucc LEZero)

More

leStepL :: LEProof ('S n) m -> LEProof n m

\(\forall n\, m : \mathbb{N}, 1 + n \le m \to n \le m \)

lePred :: LEProof ('S n) ('S m) -> LEProof n m

\(\forall n\, m : \mathbb{N}, 1 + n \le 1 + m \to n \le m \)

proofZeroLEZero :: LEProof n 'Z -> n :~: 'Z

\(\forall n\ : \mathbb{N}, n \le 0 \to n \equiv 0 \)