Safe Haskell	None
Language	Haskell2010

Data.Type.Nat.LE

Contents

Relation
Decidability
Lemmas

Description

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.

Synopsis

class LE n m where
- leProof :: LEProof n m
data LEProof n m where
- LEZero :: LEProof ' Z m
- LESucc :: LEProof n m -> LEProof (' S n) (' S m)
withLEProof :: LEProof n m -> ( LE n m => r) -> r
decideLE :: forall n m. ( SNatI n, SNatI m) => Dec ( LEProof n m)
leZero :: LEProof ' Z n
leSucc :: LEProof n m -> LEProof (' S n) (' S m)
leRefl :: forall n. SNatI n => LEProof n n
leStep :: LEProof n m -> LEProof n (' S m)
leAsym :: LEProof n m -> LEProof m n -> n :~: m
leTrans :: LEProof n m -> LEProof m p -> LEProof n p
leSwap :: forall n m. ( SNatI n, SNatI m) => Neg ( LEProof n m) -> LEProof (' S m) n
leSwap' :: LEProof n m -> LEProof (' S m) n -> void
leStepL :: LEProof (' S n) m -> LEProof n m
lePred :: LEProof (' S n) (' S m) -> LEProof n m
proofZeroLEZero :: LEProof n ' Z -> n :~: ' Z

Relation

class LE n m where Source #

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

Methods

leProof :: LEProof n m Source #

Instances

Instances details

LE ' Z m Source #
Instance details Defined in Data.Type.Nat.LE Methods leProof :: LEProof ' Z m Source #
(m ~ ' S m', LE n m') => LE (' S n) m Source #
Instance details Defined in Data.Type.Nat.LE Methods leProof :: LEProof (' S n) m Source #

data LEProof n m where Source #

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

Constructors

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

Instances

Instances details

Eq ( LEProof n m) Source #	`LEProof` values are unique (not `Boring` though!).
Instance details Defined in Data.Type.Nat.LE Methods (==) :: LEProof n m -> LEProof n m -> Bool Source # (/=) :: LEProof n m -> LEProof n m -> Bool Source #
Ord ( LEProof n m) Source #
Instance details Defined in Data.Type.Nat.LE Methods compare :: LEProof n m -> LEProof n m -> Ordering Source # (<) :: LEProof n m -> LEProof n m -> Bool Source # (<=) :: LEProof n m -> LEProof n m -> Bool Source # (>) :: LEProof n m -> LEProof n m -> Bool Source # (>=) :: LEProof n m -> LEProof n m -> Bool Source # max :: LEProof n m -> LEProof n m -> LEProof n m Source # min :: LEProof n m -> LEProof n m -> LEProof n m Source #
Show ( LEProof n m) Source #
Instance details Defined in Data.Type.Nat.LE Methods showsPrec :: Int -> LEProof n m -> ShowS Source # show :: LEProof n m -> String Source # showList :: [ LEProof n m] -> ShowS Source #
( SNatI n, SNatI m) => Decidable ( LEProof n m) Source #
Instance details Defined in Data.Type.Nat.LE Methods decide :: Dec ( LEProof n m) Source #

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

Constructor LE dictionary from LEProof .

Decidability

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

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

Lemmas

Constructor like

leZero :: LEProof ' Z n Source #

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

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

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

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

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

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

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

Partial order

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

\(\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 Source #

\(\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 Source #

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

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

\(\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 Source #

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

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

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

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

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