From 8a01c4644124a2ecaed2d58ff48bc41b02c84faf Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Thu, 16 Jan 2025 15:49:13 -0500
Subject: [PATCH] Add subset proofs to util

---
 src/Util/Eff.md | 64 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)

diff --git a/src/Util/Eff.md b/src/Util/Eff.md
index 40517ea..1b51cba 100644
--- a/src/Util/Eff.md
+++ b/src/Util/Eff.md
@@ -6,6 +6,7 @@ Contains utility functions extending the functionality of the `eff` package.
 module Util.Eff
 
 import Control.Eff
+import Data.Subset
 import Text.ANSI
 
 import System
@@ -180,3 +181,66 @@ oneOfM : Has (Choose) fs => Foldable f =>
     f (Eff fs a) -> Eff fs a
 oneOfM x = foldl alt empty x
 ```
+
+## Subset
+
+Reorder the first two elements of the first argument of a subset
+
+```idris
+public export
+subsetReorderLeft : Subset (x :: g :: xs) ys -> Subset (g :: x :: xs) ys
+subsetReorderLeft (e :: (e' :: subset)) = e' :: e :: subset
+```
+
+Add the same element to both arguments of a subset
+
+```idris
+public export
+subsetConsBoth : {0 xs, ys : List a} -> {0 g : a} -> Subset xs ys 
+  -> Subset (g :: xs) (g :: ys)
+subsetConsBoth {xs = []} {ys = ys} [] = [Z]
+subsetConsBoth {xs = (x :: xs)} {ys} (e :: subset) = 
+  let rest = S e :: subsetConsBoth subset {g}
+  in subsetReorderLeft rest
+```
+
+A list is always a subset of itself
+
+```idris
+public export
+subsetReflexive : {xs : List a} -> Subset xs xs
+subsetReflexive {xs = []} = []
+subsetReflexive {xs = (x :: xs)} = 
+  let rest = subsetReflexive {xs} 
+  in subsetConsBoth rest
+```
+
+If `xs` is a subset of `ys`, then it is also a subset of `ys + g`
+
+```idris
+public export
+subsetConsRight : {0 g: _} -> {0 xs, ys: _} -> Subset xs ys -> Subset xs (g :: ys)
+subsetConsRight {xs = []} {ys = ys} [] = []
+subsetConsRight {xs = (x :: xs)} {ys} (e :: subset) = 
+  S e :: subsetConsRight subset {g}
+```
+
+`xs` is always a subset of `xs + g`
+
+```idris
+public export
+trivialSubset : {0 g : a} -> {xs : List a} -> Subset xs (g :: xs)
+trivialSubset = subsetConsRight subsetReflexive
+```
+
+`fs - f` is always a subset of `f`
+
+```idris
+public export
+minusLemma : {fs : List a} -> {0 x : a} -> {auto prf : Has x fs} 
+  -> Subset (fs - x) fs
+minusLemma {fs = (_ :: vs)} {prf = Z} = trivialSubset
+minusLemma {fs = (w :: vs)} {prf = (S y)} = 
+  let rest = minusLemma {fs = vs} {prf = y}
+  in subsetConsBoth rest
+```