mirror of
https://github.com/idris-lang/Idris2.git
synced 2025-01-08 00:40:10 +03:00
31ffb4e5c7
Turns out that `Smaller` and `LT` won't unify because 1. the instance Sized Nat is not publicly exported 2. Smaller, and LT are stuck until fully applied The given changes make that go away.
52 lines
1.5 KiB
Idris
52 lines
1.5 KiB
Idris
||| Implementation of ordering relations for `Nat`ural numbers
|
|
module Data.Nat.Order
|
|
|
|
import Control.Relation
|
|
import Data.Nat
|
|
import Data.Fun
|
|
import Data.Rel
|
|
import Decidable.Decidable
|
|
import Decidable.Equality
|
|
|
|
%default total
|
|
|
|
public export
|
|
zeroNeverGreater : Not (LTE (S n) Z)
|
|
zeroNeverGreater LTEZero impossible
|
|
zeroNeverGreater (LTESucc _) impossible
|
|
|
|
public export
|
|
zeroAlwaysSmaller : {n : Nat} -> LTE Z n
|
|
zeroAlwaysSmaller = LTEZero
|
|
|
|
public export
|
|
ltesuccinjective : {0 n, m : Nat} -> Not (LTE n m) -> Not (LTE (S n) (S m))
|
|
ltesuccinjective disprf (LTESucc nLTEm) = void (disprf nLTEm)
|
|
ltesuccinjective disprf LTEZero impossible
|
|
|
|
public export
|
|
decideLTE : (n : Nat) -> (m : Nat) -> Dec (LTE n m)
|
|
decideLTE Z y = Yes LTEZero
|
|
decideLTE (S x) Z = No zeroNeverGreater
|
|
decideLTE (S x) (S y) with (decEq (S x) (S y))
|
|
decideLTE (S x) (S y) | Yes eq = rewrite eq in Yes (reflexive {rel = LTE})
|
|
decideLTE (S x) (S y) | No _ with (decideLTE x y)
|
|
decideLTE (S x) (S y) | No _ | Yes nLTEm = Yes (LTESucc nLTEm)
|
|
decideLTE (S x) (S y) | No _ | No nGTm = No (ltesuccinjective nGTm)
|
|
|
|
public export
|
|
Decidable 2 [Nat,Nat] LTE where
|
|
decide = decideLTE
|
|
|
|
public export
|
|
Decidable 2 [Nat,Nat] LT where
|
|
decide m = decideLTE (S m)
|
|
|
|
public export
|
|
lte : (m : Nat) -> (n : Nat) -> Dec (LTE m n)
|
|
lte m n = decide {ts = [Nat,Nat]} {p = LTE} m n
|
|
|
|
public export
|
|
shift : (m : Nat) -> (n : Nat) -> LTE m n -> LTE (S m) (S n)
|
|
shift m n mLTEn = LTESucc mLTEn
|