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 mandsucc : n \le m \to 1 + n \le 1 + m(this module),refl : n \le nandstep : 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.
- Packagefin-0.3.2
- Exports15
- LanguageHaskell2010
- LicenceBSD-3-Clause
- SourceLE.hs
Relation
An evidence of n \le m. zero+succ definition.
Instances6Eq, Ord, Show, Absurd, Boring, Decidable
Eq (LEProof n m)Defined in fin-0.3.2 · Data.Type.Nat.LEOrd (LEProof n m)Defined in fin-0.3.2 · Data.Type.Nat.LEShow (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.LELE 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
Decidability
Find the LEProof n m, i.e. compare numbers.
Lemmas
Constructor like
\forall n : \mathbb{N}, 0 \le n
\forall n\, m : \mathbb{N}, n \le m \to 1 + n \le 1 + m
\forall n : \mathbb{N}, n \le n
\forall n\, m : \mathbb{N}, n \le m \to n \le 1 + m
Partial order
\forall n\, m : \mathbb{N}, n \le m \to m \le n \to n \equiv m
\forall n\, m\, p : \mathbb{N}, n \le m \to m \le p \to n \le p
Total order
\forall n\, m : \mathbb{N}, \neg (n \le m) \to 1 + m \le n
\forall n\, m : \mathbb{N}, n \le m \to \neg (1 + m \le n)
leProof :: LEProof Nat2 Nat3LESucc (LESucc LEZero)
leSwap (leSwap' (leProof :: LEProof Nat2 Nat3))LESucc (LESucc (LESucc LEZero))
lePred (leSwap (leSwap' (leProof :: LEProof Nat2 Nat3)))LESucc (LESucc LEZero)
More
\forall n\, m : \mathbb{N}, 1 + n \le m \to n \le m
\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