Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[ libs ] Add public export modifiers to arithmetic inequality proofs #3377

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

[ libs ] Add public export modifiers to arithmetic inequality proofs #3377

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions CHANGELOG_NEXT.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -217,6 +217,17 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO

* Added implementations of `Foldable` and `Traversable` for `Control.Monad.Identity`

* Multiple functions in `Data.Nat` and `Data.Nat.Order.Properties` (mostly inequality proofs) are now `public export`:
- `fromLteSucc`
- `lteSuccLeft`, `lteSuccRight`
- `lteAddRight`
- `divCeilNZ` (it is `total` now as well)
- `plusLteMonotoneLeft`, `plusLteMonotoneRight`, `plusLteMonotone`
- `minusPos`, `minusLteMonotone`, `minusLtMonotone`
- `minusLTE`, `minusPosLT`
- `multLteMonotoneLeft`, `multLteMonotoneRight`
- `decomposeLte`

#### Contrib

* `Data.List.Lazy` was moved from `contrib` to `base`.
Expand Down
25 changes: 12 additions & 13 deletions libs/base/Data/Nat.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -174,7 +174,7 @@ export
succNotLTEzero : Not (LTE (S m) Z)
succNotLTEzero LTEZero impossible

export
public export
fromLteSucc : LTE (S m) (S n) -> LTE m n
fromLteSucc (LTESucc x) = x

Expand Down Expand Up @@ -220,16 +220,16 @@ ltRecall : LT m n -> {p : Nat -> Nat} -> (0 prf : LT (p m) q) -> LT (p m) q
ltRecall {m} x prf with (lteRecallLeft x)
ltRecall {m = m} x prf | (S m ** Refl) = irrelevantLte prf

export
public export
lteSuccRight : LTE n m -> LTE n (S m)
lteSuccRight LTEZero = LTEZero
lteSuccRight (LTESucc x) = LTESucc (lteSuccRight x)

export
public export
lteSuccLeft : LTE (S n) m -> LTE n m
lteSuccLeft (LTESucc x) = lteSuccRight x

export
public export
lteAddRight : (n : Nat) -> LTE n (n + m)
lteAddRight Z = LTEZero
lteAddRight (S k) {m} = LTESucc (lteAddRight {m} k)
Expand Down Expand Up @@ -374,8 +374,7 @@ export partial
divNat : Nat -> Nat -> Nat
divNat left (S right) = divNatNZ left (S right) SIsNonZero

export
covering
public export
divCeilNZ : Nat -> (y: Nat) -> (0 _ : NonZero y) -> Nat
divCeilNZ x y p = case (modNatNZ x y p) of
Z => divNatNZ x y p
Expand Down Expand Up @@ -516,8 +515,8 @@ plusLeftLeftRightZero left right p =
~~ left ...(p)
~~ left + 0 ..<(plusZeroRightNeutral left)

export
plusLteMonotoneRight : (p, q, r : Nat) -> q `LTE` r -> (q+p) `LTE` (r+p)
public export
plusLteMonotoneRight : (p, q, r : Nat) -> q `LTE` r -> (q + p) `LTE` (r + p)
plusLteMonotoneRight p Z r LTEZero = CalcSmart {leq = LTE} $
|~ 0 + p
<~ p + r ...(lteAddRight p)
Expand All @@ -527,7 +526,7 @@ plusLteMonotoneRight p (S q) (S r) (LTESucc q_lte_r) =
|~ q + p
<~ r + p ...(plusLteMonotoneRight p q r q_lte_r)

export
public export
plusLteMonotoneLeft : (p, q, r : Nat) -> q `LTE` r -> (p + q) `LTE` (p + r)
plusLteMonotoneLeft p q r q_lt_r = CalcSmart {leq = LTE} $
|~ p + q
Expand All @@ -536,7 +535,7 @@ plusLteMonotoneLeft p q r q_lt_r = CalcSmart {leq = LTE} $
<~ p + r .=.(plusCommutative r p)


export
public export
plusLteMonotone : {m, n, p, q : Nat} -> m `LTE` n -> p `LTE` q ->
(m + p) `LTE` (n + q)
plusLteMonotone left right = CalcSmart {leq = LTE} $
Expand Down Expand Up @@ -679,19 +678,19 @@ minusPlusZero : (n, m : Nat) -> minus n (n + m) = Z
minusPlusZero Z _ = Refl
minusPlusZero (S n) m = minusPlusZero n m

export
public export
minusPos : m `LT` n -> Z `LT` minus n m
minusPos lt = case view lt of
LTZero => ltZero
LTSucc lt => minusPos lt

export
public export
minusLteMonotone : {p : Nat} -> m `LTE` n -> minus m p `LTE` minus n p
minusLteMonotone LTEZero = LTEZero
minusLteMonotone {p = Z} prf@(LTESucc _) = prf
minusLteMonotone {p = S p} (LTESucc lte) = minusLteMonotone lte

export
public export
minusLtMonotone : m `LT` n -> p `LT` n -> minus m p `LT` minus n p
minusLtMonotone {m} {p} mltn pltn = case view pltn of
LTZero => ltRecall {p = (`minus` 0)} mltn $ CalcSmart {leq = LT} $
Expand Down
14 changes: 7 additions & 7 deletions libs/base/Data/Nat/Order/Properties.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ GTIsnotlte a b prf =
succNotLTEpred $ transitive prf contra

||| Subtracting a number gives a smaller number
export
public export
minusLTE : (a,b : Nat) -> (b `minus` a) `LTE` b
minusLTE a 0 = LTEZero
minusLTE 0 (S _) = reflexive
Expand All @@ -81,15 +81,15 @@ minusLTE (S a) (S b) =
(lteSuccRight reflexive)

||| Subtracting a positive number gives a strictly smaller number
export
public export
minusPosLT : (a,b : Nat) -> 0 `LT` a -> a `LTE` b -> (b `minus` a) `LT` b
minusPosLT 0 b z_lt_z a_lte_b impossible
minusPosLT (S a) 0 z_lt_sa a_lte_b impossible
minusPosLT (S a) (S b) z_lt_sa a_lte_b = LTESucc (minusLTE a b)

-- This is the opposite of the convention in `Data.Nat`, but 'monotone on the left' means the below
export
multLteMonotoneRight : (l, a, b : Nat) -> a `LTE` b -> l*a `LTE` l*b
public export
multLteMonotoneRight : (l, a, b : Nat) -> a `LTE` b -> (l * a) `LTE` (l * b)
multLteMonotoneRight 0 a b _ = LTEZero
multLteMonotoneRight (S k) a b a_lte_b = CalcWith {leq = LTE} $
|~ (1 + k) * a
Expand All @@ -99,8 +99,8 @@ multLteMonotoneRight (S k) a b a_lte_b = CalcWith {leq = LTE} $
multLteMonotoneRight k a b a_lte_b)
~~ (1 + k) * b ...(Refl)

export
multLteMonotoneLeft : (a, b, r : Nat) -> a `LTE` b -> a*r `LTE` b*r
public export
multLteMonotoneLeft : (a, b, r : Nat) -> a `LTE` b -> (a * r) `LTE` (b * r)
multLteMonotoneLeft a b r a_lt_b =
rewrite multCommutative a r in
rewrite multCommutative b r in
Expand All @@ -113,7 +113,7 @@ lteNotLtEq a b a_lte_b not_n_lte_n =
in antisymmetric a_lte_b b_lte_a

-- Try succ left element LTE. Returns LT if successful, otherwise proof of equality a and b
export
public export
decomposeLte : (a, b : Nat) -> LTE a b -> Either (LT a b) (a = b)
decomposeLte a b a_lte_b with (isLT a b)
decomposeLte a b a_lte_b | Yes a_lt_b = Left a_lt_b
Expand Down