mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-17 16:21:46 +03:00
0c1a124704
Division Theorem. For every natural number `x` and positive natural
number `n`, there is a unique decomposition:
`x = q*n + r`
with `q`,`r` natural and `r` < `n`.
`q` is the quotient when dividing `x` by `n`
`r` is the remainder when dividing `x` by `n`.
This commit adds a proof for this fact, in case
we want to reason about modular arithmetic (for example, when dealing
with binary representations). A future, more systematic, development could
perhaps follow: @clayrat 's (idris1) port of Coq's binary arithmetics:
https://github.com/sbp/idris-bi/blob/master/src/Data/Bin/DivMod.idr
https://github.com/sbp/idris-bi/blob/master/src/Data/Biz/DivMod.idr
https://github.com/sbp/idris-bi/blob/master/src/Data/BizMod2/DivMod.idr
In the process, it bulks up the stdlib with:
+ a generic PreorderReasoning module for arbitrary preorders,
analogous for the equational reasoning module
+ some missing facts about Nat operations.
+ Refactor some Nat order properties using a 'reflect' function
Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
37 lines
1.1 KiB
Idris
37 lines
1.1 KiB
Idris
||| Implementing `Decidable.Order.Strict` for `Data.Nat.LT`
|
|
module Data.Nat.Order.Strict
|
|
|
|
import Decidable.Order
|
|
import Decidable.Order.Strict
|
|
import Decidable.Equality
|
|
import Data.Nat
|
|
import Data.Nat.Order
|
|
|
|
export
|
|
irreflexiveLTE : (a : Nat) -> Not (a `LT` a)
|
|
irreflexiveLTE 0 z_lt_z impossible
|
|
irreflexiveLTE (S a) (LTESucc a_lt_a) = irreflexiveLTE a a_lt_a
|
|
|
|
export
|
|
StrictPreorder Nat LT where
|
|
irreflexive = irreflexiveLTE
|
|
transitive a b c a_lt_b b_lt_c = transitive {po = LTE} (S a) b c
|
|
a_lt_b
|
|
(transitive {po = LTE} b (S b) c
|
|
(lteSuccRight (reflexive b))
|
|
b_lt_c)
|
|
|
|
public export
|
|
decLT : (a, b : Nat) -> DecOrdering {lt = LT} a b
|
|
decLT 0 0 = DecEQ Refl
|
|
decLT 0 (S b) = DecLT (LTESucc LTEZero)
|
|
decLT (S a) 0 = DecGT (LTESucc LTEZero)
|
|
decLT (S a) (S b) = case decLT a b of
|
|
DecLT a_lt_b => DecLT (LTESucc a_lt_b)
|
|
DecEQ Refl => DecEQ Refl
|
|
DecGT b_lt_a => DecGT (LTESucc b_lt_a)
|
|
|
|
public export
|
|
StrictOrdered Nat LT where
|
|
order = decLT
|