fin-0.1: Nat and Fin: peano naturals and finite numbers

Data.Type.Nat.LE

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

# Relation

class LE n m where Source #

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

Methods

Instances
 LE Z m Source # Instance detailsDefined in Data.Type.Nat.LE Methods (m ~ S m', LE n m') => LE (S n) m Source # Instance detailsDefined in Data.Type.Nat.LE MethodsleProof :: 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
 Eq (LEProof n m) Source # LEProof values are unique (not Boring though!). Instance detailsDefined in Data.Type.Nat.LE Methods(==) :: LEProof n m -> LEProof n m -> Bool #(/=) :: LEProof n m -> LEProof n m -> Bool # Ord (LEProof n m) Source # Instance detailsDefined in Data.Type.Nat.LE Methodscompare :: 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) Source # Instance detailsDefined in Data.Type.Nat.LE MethodsshowsPrec :: Int -> LEProof n m -> ShowS #show :: LEProof n m -> String #showList :: [LEProof n m] -> ShowS # (SNatI n, SNatI m) => Decidable (LEProof n m) Source # Instance detailsDefined in Data.Type.Nat.LE Methodsdecide :: Dec (LEProof n m) #

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

$$\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$$

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