mirror of
https://github.com/idris-lang/Idris2.git
synced 2025-01-05 06:37:23 +03:00
74 lines
2.1 KiB
Idris
74 lines
2.1 KiB
Idris
||| Implementation of ordering relations for `Nat`ural numbers
|
|
module Data.Nat.Order
|
|
|
|
import Data.Nat
|
|
import Data.Fun
|
|
import Data.Rel
|
|
import Decidable.Decidable
|
|
|
|
%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
|
|
|
|
-- Remove any time after release of 0.6.0
|
|
||| Deprecated. Use `Nat.isLTE`.
|
|
public export
|
|
decideLTE : (n : Nat) -> (m : Nat) -> Dec (LTE n m)
|
|
decideLTE = isLTE
|
|
|
|
||| If a predicate is decidable then we can decide whether it holds on
|
|
||| a bounded domain.
|
|
public export
|
|
decideLTBounded :
|
|
{0 p : Nat -> Type} ->
|
|
((n : Nat) -> Dec (p n)) ->
|
|
(n : Nat) -> Dec ((k : Nat) -> k `LT` n -> p k)
|
|
decideLTBounded pdec 0 = Yes (\ k, bnd => absurd bnd)
|
|
decideLTBounded pdec (S n) with (pdec 0)
|
|
_ | No np0 = No (\ prf => np0 (prf 0 (LTESucc LTEZero)))
|
|
_ | Yes p0 with (decideLTBounded (\ n => pdec (S n)) n)
|
|
_ | No nprf = No (\ prf => nprf (\ k, bnd => prf (S k) (LTESucc bnd)))
|
|
_ | Yes prf = Yes $ \ k, bnd =>
|
|
case view bnd of
|
|
LTZero => p0
|
|
(LTSucc bnd) => prf _ bnd
|
|
|
|
||| If a predicate is decidable then we can decide whether it holds on
|
|
||| a bounded domain.
|
|
public export
|
|
decideLTEBounded :
|
|
{0 p : Nat -> Type} ->
|
|
((n : Nat) -> Dec (p n)) ->
|
|
(n : Nat) -> Dec ((k : Nat) -> k `LTE` n -> p k)
|
|
decideLTEBounded pdec n with (decideLTBounded pdec (S n))
|
|
_ | Yes prf = Yes (\ k, bnd => prf k (LTESucc bnd))
|
|
_ | No nprf = No (\ prf => nprf (\ k, bnd => prf k (fromLteSucc bnd)))
|
|
|
|
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
|