mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-21 10:41:59 +03:00
2ae330785b
* [contrib] Add misc libraries to contrib Expose some `private` function in libs/base that I needed, and seem like their visibility was forgotten I'd appreciate a code review, especially to tell me I'm re-implementing something that's already elsewhere in the library Mostly extending existing functionality: * `Data/Void.idr`: add some utility functions for manipulating absurdity. * `Decidable/Decidable/Extra.idr`: add support for double negation elimination in decidable relations * `Data/Fun/Extra.idr`: + add `application` (total and partil) for n-ary functions + add (slightly) dependent versions of these operations * `Decidable/Order/Strict.idr`: a strict preorder is what you get when you remove the diagonal from a pre-order. For example, `<` is the associated preorder for `<=` over `Nat`. Analogous to `Decidable.Order`. The proof search mechanism struggled a bit, so I had to hack it --- sorry. Eventually we should move `Data.Fun.Extra.Pointwise` to `Data.Vect.Quantifiers` in base but we don't have any interesting uses for it at the moment so it's not urgent. Co-authored by @gallais
43 lines
1.3 KiB
Idris
43 lines
1.3 KiB
Idris
module Data.Rel
|
|
|
|
import Data.Fun
|
|
|
|
||| Build an n-ary relation type from a Vect of Types
|
|
public export
|
|
Rel : Vect n Type -> Type
|
|
Rel ts = Fun ts Type
|
|
|
|
||| Universal quantification of a n-ary Relation over its
|
|
||| arguments to build a (function) type from a `Rel` type
|
|
|||
|
|
||| ```
|
|
||| λ> All [Nat,Nat] LTE
|
|
||| (x : Nat) -> (x : Nat) -> LTE x x
|
|
||| ```
|
|
public export
|
|
All : (ts : Vect n Type) -> (p : Rel ts) -> Type
|
|
All [] p = p
|
|
All (t :: ts) p = (x : t) -> All ts (p x)
|
|
|
|
||| Existential quantification of a n-ary relation over its
|
|
||| arguments to build a dependent pair (eg. Sigma type).
|
|
|||
|
|
||| Given a (type of) relation `p : [t_1, t_2 ... t_n] x r` where `t_i` and `r` are
|
|
||| types, `Ex` builds the type `Σ (x_1 : t_1). Σ (x_2 : t_2) ... . r`
|
|
||| For example:
|
|
||| ```
|
|
||| λ> Ex [Nat,Nat] LTE
|
|
||| (x : Nat ** (x : Nat ** LTE x x))
|
|
||| ```
|
|
||| Which is the type of a pair of natural numbers along with a proof that the first
|
|
||| is smaller or equal than the second.
|
|
public export
|
|
Ex : (ts : Vect n Type) -> (p : Rel ts) -> Type
|
|
Ex [] p = p
|
|
Ex (t :: ts) p = (x : t ** Ex ts (p x))
|
|
|
|
||| Map a type-level function over the co-domain of a n-ary Relation
|
|
public export
|
|
liftRel : (ts : Vect n Type) -> (p : Rel ts) -> (Type -> Type) -> Type
|
|
liftRel ts p f = All ts $ map @{Nary} f p
|