Modulefin-0.3.2Haskell2010

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.

1 type
1 class
13 values

Packagefin-0.3.2
Exports15
LanguageHaskell2010
LicenceBSD-3-Clause
SourceLE.hs

Relation

3 declarations

classclass LE (n :: Nat) (m :: Nat) where

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

Methods

leProof :: LEProof n m

Instances2LE

LE 'Z mDefined in fin-0.3.2 · Data.Type.Nat.LE
(m ~ 'S m', LE n m') => LE ('S n) mDefined in fin-0.3.2 · Data.Type.Nat.LE

datadata LEProof (n :: Nat) (m :: Nat) where

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

Constructors

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

Instances6Eq, Ord, Show, Absurd, Boring, Decidable

Eq (LEProof n m)Defined in fin-0.3.2 · Data.Type.Nat.LE
LEProof values are unique (not Boring though!).
Ord (LEProof n m)Defined in fin-0.3.2 · Data.Type.Nat.LE
Show (LEProof n m)Defined in fin-0.3.2 · Data.Type.Nat.LE
(LE m n, n' ~ 'S n) => Absurd (LEProof n' m)Defined in fin-0.3.2 · Data.Type.Nat.LE
LE n m => Boring (LEProof n m)Defined in fin-0.3.2 · Data.Type.Nat.LE
(SNatI n, SNatI m) => Decidable (LEProof n m)Defined in fin-0.3.2 · Data.Type.Nat.LE

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

Constructor LE dictionary from LEProof.

Decidability

1 declaration

valuedecideLE :: (SNatI n, SNatI m) => Dec (LEProof n m)

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

Lemmas

0 declarations

Constructor like

valueleZero :: LEProof 'Z n

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

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

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

valueleRefl :: SNatI n => LEProof n n

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

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

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

Partial order

valueleAsym :: LEProof n m -> LEProof m n -> n :~: m

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

valueleTrans :: 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

valueleSwap :: (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

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

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

Example1 expression

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

Example1 expression

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

Example1 expression

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

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

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

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

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

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

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

Relation

Methods

Constructors

Decidability

Lemmas

Constructor like

Partial order

Total order

More