4 | import Data.List.Elem
5 | import Data.List.Elem.Extra
6 | import public Data.List.Equalities
8 | import TyRE.Extra.Pred
13 | extractBasedOnFst : (xs: List (a, b)) -> (xInXs: x `Elem` map Builtin.fst xs) -> b
14 | extractBasedOnFst [] xInXs = absurd xInXs
15 | extractBasedOnFst (x :: xs) Here = snd x
16 | extractBasedOnFst (x' :: xs) (There pos) = extractBasedOnFst xs pos
19 | extractBasedOnFstSpec : (xs : List a)
20 | -> (f : a -> (b, c)) -> (x : b)
21 | -> (xInXs : x `Elem` map Builtin.fst (map f xs))
22 | -> (e : a ** extractBasedOnFst (map f xs) xInXs = Builtin.snd (f e))
23 | extractBasedOnFstSpec [] _ _ Here impossible
24 | extractBasedOnFstSpec [] _ _ (There y) impossible
25 | extractBasedOnFstSpec (y :: xs) f (fst (f y)) Here = (
y ** Refl)
26 | extractBasedOnFstSpec (y :: xs) f x (There pos) = extractBasedOnFstSpec xs f x pos
29 | extractBasedOnFstAppLor : (xs : List (a, b))
30 | -> (ys : List (a, b))
32 | -> (xInApp : x `Elem` map Builtin.fst (xs ++ ys))
33 | -> Either (xInXs : x `Elem` map Builtin.fst xs
34 | ** extractBasedOnFst (xs ++ ys) xInApp = extractBasedOnFst xs xInXs)
35 | (xInYs : x `Elem` map Builtin.fst ys
36 | ** extractBasedOnFst (xs ++ ys) xInApp = extractBasedOnFst ys xInYs)
37 | extractBasedOnFstAppLor [] ys x xInApp = Right (
xInApp ** Refl)
38 | extractBasedOnFstAppLor ((x, r) :: xs) ys x Here = Left (
Here ** Refl)
39 | extractBasedOnFstAppLor ((x', r') :: xs) ys x (There pos) =
40 | case (extractBasedOnFstAppLor xs ys x pos) of
41 | Right (
xInXs ** extractEq)
=> Right (
xInXs ** extractEq)
42 | Left (
xInYs ** extractEq)
=> Left (
There xInYs ** extractEq)
46 | replicate : Nat -> (elem : a) -> SnocList a
47 | replicate 0 elem = [<]
48 | replicate (S k) elem = (replicate k elem) :< elem
51 | replicateForSucc : (k : Nat) -> (elem : a)
52 | -> ([< elem] ++ replicate k elem = replicate (S k) elem)
53 | replicateForSucc 0 elem = Refl
54 | replicateForSucc (S k) elem = cong (:< elem) (replicateForSucc k elem)
57 | bindSpec : (f : a -> List b) -> (p : Pred b) -> (q : Pred a) ->
58 | (spec : (x : a) -> (y: b ** (y `Elem` f x, p y)) -> q x) ->
60 | (prf : (y: b ** (y `Elem` (cs >>= f), p y))) ->
61 | (x : a ** (x `Elem` cs, q x,(y: b ** (y `Elem` (f x), p y))))
63 | bindSpec f p q spec [] prf = absurd $
fst $
snd prf
64 | bindSpec f p q spec (x :: xs) (
y ** (isElemF, satP))
=
65 | let hereOrThere = elemAppLorR (f x) (xs >>= f) (replace {p=(y `Elem`)} (bindConcatPrf _ _ _) isElemF)
66 | in case hereOrThere of
67 | (Left prf1) => (
x ** (Here, spec x (
y ** (prf1, satP))
, (
y ** (prf1, satP))
))
69 | let (
x ** (isElem, satQ, yInf))
= bindSpec f p q spec xs (
y ** (prf1, satP))
70 | in (
x ** (There isElem, satQ, yInf))
73 | mapSpec : (f : (a, b) -> c) -> (q : Pred (a,b)) -> (p : Pred c) -> (xs: List (a,b))
74 | -> ((x1 : a) -> (x2 : b) -> p(f(x1, x2)) -> q (x1, x2)) -> (y: c)
75 | -> (y `Elem` map f xs, p y)
76 | -> (x1: a ** (x2:b ** (prf: x1 `Elem` map Builtin.fst xs ** (extractBasedOnFst xs prf = x2, f(x1, x2) = y, q (x1, x2)))))
78 | mapSpec f q p [] spec y (isElem, satP) = absurd isElem
79 | mapSpec f q p ((x1,x2) :: xs) spec y (pos, satP) =
81 | Here => (
x1 ** (
x2 ** (
Here ** (Refl, Refl, spec x1 x2 satP))))
83 | let (
x1' ** (
x2' ** (
pos' ** (ex', eq', satQ'))))
=
84 | mapSpec f q p xs spec y (pos, satP)
85 | in (
x1' ** (
x2' ** (
There pos' ** (ex', eq', satQ'))))
88 | biMapOnFst : (xs : List (a, c)) -> (f : a -> b) -> (g : c -> d) -> (map Builtin.fst (map (bimap f g) xs) = map f (map Builtin.fst xs))
89 | biMapOnFst [] f g = Refl
90 | biMapOnFst ((fst, snd) :: xs) f g = cong (f fst ::) (biMapOnFst xs f g)
93 | elemMapRev : (xs : List a) -> (f : a -> b) -> {0 e : b} -> (e `Elem` map f xs) -> (e' : a ** (e' `Elem` xs, f e' = e))
94 | elemMapRev [] _ Here impossible
95 | elemMapRev [] _ (There pos) impossible
96 | elemMapRev (x :: xs) f Here = (
x ** (Here, Refl))
97 | elemMapRev (x :: xs) f (There pos) =
98 | let (
e' ** (pos', eq))
= elemMapRev xs f pos
99 | in (
e' ** (There pos', eq))
102 | eqForJust : (Just x = Just y) -> (x = y)
103 | eqForJust Refl = Refl