[ new ] Data.OpenUnion (#1050)

libs/contrib/Control/Validation.idr

@@ -11,7 +11,6 @@ module Control.Validation
 -- failing early with a nice error message if it isn't.
 
 import Control.Monad.Identity
-import Control.Monad.Syntax
 import Control.Monad.Error.Either
 import Data.Nat
 import Data.Strings

libs/contrib/Data/List/AtIndex.idr

@@ -0,0 +1,109 @@
+module Data.List.AtIndex
+
+import Data.DPair
+import Data.List.HasLength
+import Data.Nat
+import Decidable.Equality
+
+%default total
+
+||| @AtIndex witnesses the fact that a natural number encodes a membership proof.
+||| It is meant to be used as a runtime-irrelevant gadget to guarantee that the
+||| natural number is indeed a valid index.
+public export
+data AtIndex : a -> List a -> Nat -> Type where
+  Z : AtIndex a (a :: as) Z
+  S : AtIndex a as n -> AtIndex a (b :: as) (S n)
+
+||| Inversion principle for Z constructor
+export
+inverseZ : AtIndex x (y :: xs) Z -> x === y
+inverseZ Z = Refl
+
+||| inversion principle for S constructor
+export
+inverseS : AtIndex x (y :: xs) (S n) -> AtIndex x xs n
+inverseS (S p) = p
+
+||| An empty list cannot possibly have members
+export
+Uninhabited (AtIndex a [] n) where
+  uninhabited Z impossible
+  uninhabited (S _) impossible
+
+||| For a given list and a given index, there is only one possible value
+||| stored at that index in that list
+export
+atIndexUnique : AtIndex a as n -> AtIndex b as n -> a === b
+atIndexUnique Z Z = Refl
+atIndexUnique (S p) (S q) = atIndexUnique p q
+
+||| Provided that equality is decidable, we can look for the first occurence
+||| of a value inside of a list
+public export
+find : DecEq a => (x : a) -> (xs : List a) -> Dec (Subset Nat (AtIndex x xs))
+find x [] = No (\ p => void (absurd (snd p)))
+find x (y :: xs) with (decEq x y)
+  find x (x :: xs) | Yes Refl = Yes (Element Z Z)
+  find x (y :: xs) | No neqxy = case find x xs of
+      Yes (Element n prf) => Yes (Element (S n) (S prf))
+      No notInxs => No \case
+        (Element Z p) => void (neqxy (inverseZ p))
+        (Element (S n) prf) => absurd (notInxs (Element n (inverseS prf)))
+
+||| If the equality is not decidable, we may instead rely on interface resolution
+public export
+interface FindElement (0 t : a) (0 ts : List a) where
+  findElement : Subset Nat (AtIndex t ts)
+
+FindElement t (t :: ts) where
+  findElement = Element 0 Z
+
+FindElement t ts => FindElement t (u :: ts) where
+  findElement = let (Element n prf) = findElement in
+                Element (S n) (S prf)
+
+||| Given an index, we can decide whether there is a value corresponding to it
+public export
+lookup : (n : Nat) -> (xs : List a) -> Dec (Subset a (\ x => AtIndex x xs n))
+lookup n [] = No (\ p => void (absurd (snd p)))
+lookup Z (x :: xs) = Yes (Element x Z)
+lookup (S n) (x :: xs) = case lookup n xs of
+  Yes (Element x p) => Yes (Element x (S p))
+  No notInxs => No (\ (Element x p) => void (notInxs (Element x (inverseS p))))
+
+||| An AtIndex proof implies that n is less than the length of the list indexed into
+public export
+inRange : (n : Nat) -> (xs : List a) -> (0 _ : AtIndex x xs n) -> LTE n (length xs)
+inRange n [] p = void (absurd p)
+inRange Z (x :: xs) p = LTEZero
+inRange (S n) (x :: xs) p = LTESucc (inRange n xs (inverseS p))
+
+|||
+export
+weakenR : AtIndex x xs n -> AtIndex x (xs ++ ys) n
+weakenR Z = Z
+weakenR (S p) = S (weakenR p)
+
+export
+weakenL : (p : Subset Nat (HasLength ws)) -> AtIndex x xs n -> AtIndex x (ws ++ xs) (fst p + n)
+weakenL m p = case view m of
+  Z     => p
+  (S m) => S (weakenL m p)
+
+export
+strengthenL : (p : Subset Nat (HasLength xs)) ->
+              lt n (fst p) === True ->
+              AtIndex x (xs ++ ys) n -> AtIndex x xs n
+strengthenL m lt idx = case view m of
+  S m => case idx of
+    Z => Z
+    S idx => S (strengthenL m lt idx)
+
+export
+strengthenR : (p : Subset Nat (HasLength ws)) ->
+              lte (fst p) n === True ->
+              AtIndex x (ws ++ xs) n -> AtIndex x xs (minus n (fst p))
+strengthenR m lt idx = case view m of
+  Z => rewrite minusZeroRight n in idx
+  S m => case idx of S idx => strengthenR m lt idx

libs/contrib/Data/List/HasLength.idr

@@ -0,0 +1,138 @@
+||| This module implements a relation between a natural number and a list.
+||| The relation witnesses the fact the number is the length of the list.
+|||
+||| It is meant to be used in a runtime-irrelevant fashion in computations
+||| manipulating data indexed over lists where the computation actually only
+||| depends on the length of said lists.
+|||
+||| Instead of writing:
+||| ```
+||| f0 : (xs : List a) -> P xs
+||| ```
+|||
+||| We would write either of:
+||| ```
+||| f1 : (n : Nat) -> (0 _ : HasLength xs n) -> P xs
+||| f2 : (n : Subset n (HasLength xs)) -> P xs
+||| ```
+|||
+||| See `sucR` for an example where the update to the runtime-relevant Nat is O(1)
+||| but the udpate to the list (were we to keep it around) an O(n) traversal.
+
+module Data.List.HasLength
+
+import Data.DPair
+import Data.List
+
+%default total
+
+------------------------------------------------------------------------
+-- Type
+
+||| Ensure that the list's length is the provided natural number
+public export
+data HasLength : List a -> Nat -> Type where
+  Z : HasLength [] Z
+  S : HasLength xs n -> HasLength (x :: xs) (S n)
+
+------------------------------------------------------------------------
+-- Properties
+
+||| The length is unique
+export
+hasLengthUnique : HasLength xs m -> HasLength xs n -> m === n
+hasLengthUnique Z Z = Refl
+hasLengthUnique (S p) (S q) = cong S (hasLengthUnique p q)
+
+||| This specification corresponds to the length function
+export
+hasLength : (xs : List a) -> HasLength xs (length xs)
+hasLength [] = Z
+hasLength (_ :: xs) = S (hasLength xs)
+
+export
+map : (f : a -> b) -> HasLength xs n -> HasLength (map f xs) n
+map f Z = Z
+map f (S n) = S (map f n)
+
+||| @sucR demonstrates that snoc only increases the lenght by one
+||| So performing this operation while carrying the list around would cost O(n)
+||| but relying on n together with an erased HasLength proof instead is O(1)
+export
+sucR : HasLength xs n -> HasLength (snoc xs x) (S n)
+sucR Z = S Z
+sucR (S n) = S (sucR n)
+
+------------------------------------------------------------------------
+-- Views
+
+namespace SubsetView
+
+  ||| We provide this view as a convenient way to perform nested pattern-matching
+  ||| on values of type `Subset Nat (HasLength xs)`. Functions using this view will
+  ||| be seen as terminating as long as the index list `xs` is left untouched.
+  ||| See e.g. listTerminating below for such a function.
+  public export
+  data View : (xs : List a) -> Subset Nat (HasLength xs) -> Type where
+    Z : View [] (Element Z Z)
+    S : (p : Subset Nat (HasLength xs)) -> View (x :: xs) (Element (S (fst p)) (S (snd p)))
+
+  ||| This auxiliary function gets around the limitation of the check ensuring that
+  ||| we do not match on runtime-irrelevant data to produce runtime-relevant data.
+  viewZ : (0 p : HasLength xs Z) -> View xs (Element Z p)
+  viewZ Z = Z
+
+  ||| This auxiliary function gets around the limitation of the check ensuring that
+  ||| we do not match on runtime-irrelevant data to produce runtime-relevant data.
+  viewS : (n : Nat) -> (0 p : HasLength xs (S n)) -> View xs (Element (S n) p)
+  viewS n (S p) = S (Element n p)
+
+  ||| Proof that the view covers all possible cases.
+  export
+  view : (p : Subset Nat (HasLength xs)) -> View xs p
+  view (Element Z p) = viewZ p
+  view (Element (S n) p) = viewS n p
+
+namespace CurriedView
+
+  ||| We provide this view as a convenient way to perform nested pattern-matching
+  ||| on pairs of values of type `n : Nat` and `HasLength xs n`. If transformations
+  ||| to the list between recursive calls (e.g. mapping over the list) that prevent
+  ||| it from being a valid termination metric, it is best to take the Nat argument
+  ||| separately from the HasLength proof and the Subset view is not as useful anymore.
+  ||| See e.g. natTerminating below for (a contrived example of) such a function.
+  public export
+  data View : (xs : List a) -> (n : Nat) -> HasLength xs n -> Type where
+    Z : View [] Z Z
+    S : (n : Nat) -> (0 p : HasLength xs n) -> View (x :: xs) (S n) (S p)
+
+  ||| Proof that the view covers all possible cases.
+  export
+  view : (n : Nat) -> (0 p : HasLength xs n) -> View xs n p
+  view Z Z = Z
+  view (S n) (S p) = S n p
+
+------------------------------------------------------------------------
+-- Examples
+
+-- /!\ Do NOT re-export these examples
+
+listTerminating : (p : Subset Nat (HasLength xs)) -> HasLength (xs ++ [x]) (S (fst p))
+listTerminating p = case view p of
+  Z => S Z
+  S p => S (listTerminating p)
+
+data P : List Nat -> Type where
+  PNil : P []
+  PCon : P (map id xs) -> P (x :: xs)
+
+covering
+notListTerminating : (p : Subset Nat (HasLength xs)) -> P xs
+notListTerminating p = case view p of
+  Z => PNil
+  S p => PCon (notListTerminating {xs = map id (tail xs)} (record { snd $= map id } p))
+
+natTerminating : (n : Nat) -> (0 p : HasLength xs n) -> P xs
+natTerminating n p = case view n p of
+  Z => PNil
+  S n p => PCon (natTerminating n (map id p))

libs/contrib/Data/Nat/Order/Properties.idr

@@ -25,18 +25,31 @@ lteReflection 0 b = RTrue LTEZero
 lteReflection (S k) 0 = RFalse \sk_lte_z => absurd sk_lte_z
 lteReflection (S a) (S b) = LTESuccInjectiveMonotone a b (lteReflection a b)
 
+export
+ltReflection : (a, b : Nat) -> Reflects (a `LT` b) (a `lt` b)
+ltReflection a = lteReflection (S a)
+
 -- For example:
 export
 lteIsLTE : (a, b : Nat) -> a `lte` b = True -> a `LTE` b
 lteIsLTE  a b prf = invert (replace {p = Reflects (a `LTE` b)} prf (lteReflection a b))
 
+export
+notlteIsNotLTE : (a, b : Nat) -> a `lte` b = False -> Not (a `LTE` b)
+notlteIsNotLTE a b prf = invert (replace {p = Reflects (a `LTE` b)} prf (lteReflection a b))
+
+
 export
 notlteIsLT : (a, b : Nat) -> a `lte` b = False -> b `LT` a
 notlteIsLT a b prf = notLTImpliesGTE
                        \prf' =>
                          (invert $ replace {p = Reflects (S a `LTE` S b)} prf
                                  $ lteReflection (S a) (S b)) prf'
 
+export
+notltIsGTE : (a, b : Nat) -> (a `lt` b) === False -> a `GTE` b
+notltIsGTE a b p = notLTImpliesGTE (notlteIsNotLTE (S a) b p)
+
 
 -- The converse to lteIsLTE:
 export