mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-18 08:42:11 +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>
32 lines
921 B
Idris
32 lines
921 B
Idris
module Data.Bool.Decidable
|
|
|
|
import Decidable.Equality
|
|
import Data.Void
|
|
|
|
public export
|
|
data Reflects : Type -> Bool -> Type where
|
|
RTrue : p -> Reflects p True
|
|
RFalse : Not p -> Reflects p False
|
|
|
|
public export
|
|
recompute : Dec a -> (0 x : a) -> a
|
|
recompute (Yes x) _ = x
|
|
recompute (No contra) x = absurdity $ contra x
|
|
|
|
public export
|
|
invert : {0 b : Bool} -> {0 p : Type} -> Reflects p b -> if b then p else Not p
|
|
invert {b = True} (RTrue x ) = x
|
|
invert {b = False} (RFalse nx) = nx
|
|
|
|
public export
|
|
remember : {b : Bool} -> {0 p : Type} -> (if b then p else Not p) -> Reflects p b
|
|
remember {b = True } = RTrue
|
|
remember {b = False} = RFalse
|
|
|
|
public export
|
|
reflect : {c : Bool} -> Reflects p b -> (if c then p else Not p) -> b = c
|
|
reflect {c = True } (RTrue x) _ = Refl
|
|
reflect {c = True } (RFalse nx) x = absurd $ nx x
|
|
reflect {c = False} (RTrue x) nx = absurd $ nx x
|
|
reflect {c = False} (RFalse nx) _ = Refl
|