@@ -95,6 +95,43 @@ data SubList : List a -> List a -> Type where
95 SubNil : SubList [] xs
95 SubNil : SubList [] xs
96 InList : SubElem x ys -> SubList xs ys -> SubList (x :: xs) ys
96 InList : SubElem x ys -> SubList xs ys -> SubList (x :: xs) ys
98+-- Some useful hints for proof construction in polymorphic programs
101+dropFirst : SubList xs ys -> SubList xs (x :: ys)
102+dropFirst SubNil = SubNil
103+dropFirst (InList el sub) = InList (S el) (dropFirst sub)
107+subListId : (xs : List a) -> SubList xs xs
108+subListId [] = SubNil
109+subListId (x :: xs) = InList Z (dropFirst (subListId xs))
112+inSuffix : SubElem x ys -> SubList xs ys -> SubElem x (zs ++ ys)
113+inSuffix {zs = []} el sub = el
114+inSuffix {zs = (x :: xs)} el sub = S (inSuffix el sub)
118+dropPrefix : SubList xs ys -> SubList xs (zs ++ ys)
119+dropPrefix SubNil = SubNil
120+dropPrefix (InList el sub) = InList (inSuffix el sub) (dropPrefix sub)
123+inPrefix : SubElem x ys -> SubList xs ys -> SubElem x (ys ++ zs)
124+inPrefix {zs = []} {ys} el sub
125+ = rewrite appendNilRightNeutral ys in el
126+inPrefix {zs = (x :: xs)} Z sub = Z
127+inPrefix {zs = (x :: xs)} (S y) sub = S (inPrefix y SubNil)
131+dropSuffix : SubList xs ys -> SubList xs (ys ++ zs)
132+dropSuffix SubNil = SubNil
133+dropSuffix (InList el sub) = InList (inPrefix el sub) (dropSuffix sub)
98namespace Env
135namespace Env
99 public export
136 public export
100 data Env : (m : Type -> Type) -> List EFFECT -> Type where
137 data Env : (m : Type -> Type) -> List EFFECT -> Type where