diff options
Diffstat (limited to 'src/Inky/Context.idr')
| -rw-r--r-- | src/Inky/Context.idr | 646 |
1 files changed, 0 insertions, 646 deletions
diff --git a/src/Inky/Context.idr b/src/Inky/Context.idr deleted file mode 100644 index 586aae2..0000000 --- a/src/Inky/Context.idr +++ /dev/null @@ -1,646 +0,0 @@ -module Inky.Context - -import public Data.Singleton -import public Data.So - -import Data.Bool.Decidable -import Data.Maybe.Decidable -import Data.DPair -import Data.Nat -import Decidable.Equality - --- Contexts -------------------------------------------------------------------- - -export -infix 2 :- - -public export -record Assoc (a : Type) where - constructor (:-) - name : String - value : a - -public export -Functor Assoc where - map f x = x.name :- f x.value - -namespace Irrelevant - public export - record Assoc0 (a : Type) where - constructor (:-) - 0 name : String - value : a - - public export - Functor Assoc0 where - map f x = x.name :- f x.value - -public export -data Context : Type -> Type where - Lin : Context a - (:<) : Context a -> Assoc a -> Context a - -public export -Functor Context where - map f [<] = [<] - map f (ctx :< x) = map f ctx :< map f x - -public export -Foldable Context where - foldr f x [<] = x - foldr f x (ctx :< (_ :- y)) = foldr f (f y x) ctx - - foldl f x [<] = x - foldl f x (ctx :< (_ :- y)) = f (foldl f x ctx) y - - null [<] = True - null (ctx :< x) = False - -%name Context ctx - -public export -data Length : Context a -> Type where - Z : Length [<] - S : Length ctx -> Length (ctx :< x) - -%name Length len - -public export -(++) : Context a -> Context a -> Context a -ctx ++ [<] = ctx -ctx ++ ctx' :< x = (ctx ++ ctx') :< x - -export -appendLinLeftNeutral : (ctx : Context a) -> [<] ++ ctx = ctx -appendLinLeftNeutral [<] = Refl -appendLinLeftNeutral (ctx :< x) = cong (:< x) $ appendLinLeftNeutral ctx - -public export -lengthAppend : Length ctx1 -> Length ctx2 -> Length (ctx1 ++ ctx2) -lengthAppend len1 Z = len1 -lengthAppend len1 (S len2) = S (lengthAppend len1 len2) - -length : Context a -> Nat -length [<] = 0 -length (ctx :< x) = S (length ctx) - --- Variables ------------------------------------------------------------------- - -export prefix 2 %% - -public export -data VarPos : (ctx : Context a) -> (0 x : String) -> a -> Type where - [search ctx] - Here : VarPos (ctx :< (x :- v)) x v - There : VarPos ctx x v -> VarPos (ctx :< y) x v - -public export -record Var (ctx : Context a) (v : a) where - constructor (%%) - 0 name : String - {auto pos : VarPos ctx name v} - -%name VarPos pos -%name Var i, j, k - -public export -toVar : VarPos ctx x v -> Var ctx v -toVar pos = (%%) x {pos} - -public export -toNat : VarPos ctx x v -> Nat -toNat Here = 0 -toNat (There pos) = S (toNat pos) - -public export -ThereVar : Var ctx v -> Var (ctx :< x) v -ThereVar i = toVar (There i.pos) - -export -Show (VarPos ctx x v) where - show i = show (toNat i) - -export -Show (Var ctx v) where - show i = show i.pos - --- Basic Properties - -export -thereCong : - {0 i : VarPos ctx x v} -> {0 j : VarPos ctx y v} -> i = j -> - There {y = z} i = There {y = z} j -thereCong Refl = Refl - -export -toVarCong : {0 i : VarPos ctx x v} -> {0 j : VarPos ctx y w} -> i = j -> toVar i = toVar j -toVarCong Refl = Refl - -export -toNatCong : {0 i : VarPos ctx x v} -> {0 j : VarPos ctx y w} -> i = j -> toNat i = toNat j -toNatCong Refl = Refl - -export -toNatCong' : {0 i, j : Var ctx v} -> i = j -> toNat i.pos = toNat j.pos -toNatCong' Refl = Refl - -export -toNatInjective : {i : VarPos ctx x v} -> {j : VarPos ctx y w} -> (0 _ : toNat i = toNat j) -> i = j -toNatInjective {i = Here} {j = Here} prf = Refl -toNatInjective {i = There i} {j = There j} prf with (toNatInjective {i} {j} $ injective prf) - toNatInjective {i = There i} {j = There .(i)} prf | Refl = Refl - -export -toVarInjective : {i : VarPos ctx x v} -> {j : VarPos ctx y v} -> (0 _ : toVar i = toVar j) -> i = j -toVarInjective prf = toNatInjective $ toNatCong' prf - --- Decidable Equality - -export -eq : Var ctx v -> Var ctx w -> Bool -eq i j = toNat i.pos == toNat j.pos - -public export -Eq (Var {a} ctx v) where - (==) = eq - -reflectPosEq : - (i : VarPos ctx x v) -> - (j : VarPos ctx y w) -> - (i = j) `Reflects` (toNat i == toNat j) -reflectPosEq Here Here = RTrue Refl -reflectPosEq Here (There j) = RFalse (\case Refl impossible) -reflectPosEq (There i) Here = RFalse (\case Refl impossible) -reflectPosEq (There i) (There j) with (reflectPosEq i j) | (toNat i == toNat j) - reflectPosEq (There i) (There .(i)) | RTrue Refl | _ = RTrue Refl - _ | RFalse neq | _ = RFalse (\case Refl => neq Refl) - -export -reflectEq : (i : Var {a} ctx v) -> (j : Var ctx w) -> (i = j) `Reflects` (i `eq` j) -reflectEq ((%%) x {pos = pos1}) ((%%) y {pos = pos2}) - with (reflectPosEq pos1 pos2) | (toNat pos1 == toNat pos2) - _ | RTrue eq | _ = RTrue (toVarCong eq) - _ | RFalse neq | _ = RFalse (\case Refl => neq Refl) - --- Weakening - -public export -wknLPos : VarPos ctx1 x v -> Length ctx2 -> VarPos (ctx1 ++ ctx2) x v -wknLPos pos Z = pos -wknLPos pos (S len) = There (wknLPos pos len) - -public export -wknRPos : VarPos ctx2 x v -> VarPos (ctx1 ++ ctx2) x v -wknRPos Here = Here -wknRPos (There pos) = There (wknRPos pos) - -public export -splitPos : Length ctx2 -> VarPos (ctx1 ++ ctx2) x v -> Either (VarPos ctx1 x v) (VarPos ctx2 x v) -splitPos Z pos = Left pos -splitPos (S len) Here = Right Here -splitPos (S len) (There pos) = mapSnd There $ splitPos len pos - -public export -wknL : {auto len : Length ctx2} -> Var ctx1 v -> Var (ctx1 ++ ctx2) v -wknL i = toVar $ wknLPos i.pos len - -public export -wknR : Var ctx2 v -> Var (ctx1 ++ ctx2) v -wknR i = toVar $ wknRPos i.pos - -public export -split : {auto len : Length ctx2} -> Var (ctx1 ++ ctx2) x -> Either (Var ctx1 x) (Var ctx2 x) -split i = bimap toVar toVar $ splitPos len i.pos - -export -lift : - {auto len : Length ctx} -> - (forall x. Var ctx1 x -> Var ctx2 x) -> - Var (ctx1 ++ ctx) x -> Var (ctx2 ++ ctx) x -lift f = either (wknL {len} . f) wknR . split {len} - --- Names - -nameOfPos : {ctx : Context a} -> VarPos ctx x v -> Singleton x -nameOfPos Here = Val x -nameOfPos (There pos) = nameOfPos pos - -export -nameOf : {ctx : Context a} -> (i : Var ctx v) -> Singleton i.name -nameOf i = nameOfPos i.pos - --- Search - -lookupPos : (x : String) -> (ctx : Context a) -> Maybe (v ** VarPos ctx x v) -lookupPos x [<] = Nothing -lookupPos x (ctx :< (y :- v)) = - case decEq x y of - Yes Refl => Just (v ** Here) - No neq => bimap id There <$> lookupPos x ctx - -export -lookup : (x : String) -> (ctx : Context a) -> Maybe (v ** Var ctx v) -lookup x ctx = bimap id toVar <$> lookupPos x ctx - --- Environments ---------------------------------------------------------------- - -namespace Quantifier - public export - data All : (0 p : a -> Type) -> Context a -> Type where - Lin : All p [<] - (:<) : - All p ctx -> (px : Assoc0 (p x.value)) -> - {auto 0 prf : px.name = x.name} -> - All p (ctx :< x) - - %name Quantifier.All env - - public export - indexAllPos : VarPos ctx x v -> All p ctx -> p v - indexAllPos Here (env :< px) = px.value - indexAllPos (There pos) (env :< px) = indexAllPos pos env - - public export - indexAll : Var ctx v -> All p ctx -> p v - indexAll i env = indexAllPos i.pos env - - export - mapProperty : ({0 x : a} -> p x -> q x) -> All p ctx -> All q ctx - mapProperty f [<] = [<] - mapProperty f (env :< (x :- px)) = mapProperty f env :< (x :- f px) - - public export - (++) : All p ctx1 -> All p ctx2 -> All p (ctx1 ++ ctx2) - env1 ++ [<] = env1 - env1 ++ env2 :< px = (env1 ++ env2) :< px - - public export - split : Length ctx2 -> All p (ctx1 ++ ctx2) -> (All p ctx1, All p ctx2) - split Z env = (env, [<]) - split (S len) (env :< px) = mapSnd (:< px) $ split len env - --- Rows ------------------------------------------------------------------------ - -namespace Row - ||| Contexts where names are unique. - public export - data Row : Type -> Type - - public export - freshIn : String -> Row a -> Bool - - data Row where - Lin : Row a - (:<) : (row : Row a) -> (x : Assoc a) -> {auto 0 fresh : So (x.name `freshIn` row)} -> Row a - - x `freshIn` [<] = True - x `freshIn` (row :< y) = x /= y.name && (x `freshIn` row) - - %name Row row - - public export - map : (a -> b) -> Row a -> Row b - export - 0 mapFresh : (f : a -> b) -> (row : Row a) -> So (x `freshIn` row) -> So (x `freshIn` map f row) - - map f [<] = [<] - map f ((:<) row x {fresh}) = (:<) (map f row) (map f x) {fresh = mapFresh f row fresh} - - mapFresh f [<] = id - mapFresh f (row :< (y :- _)) = andSo . mapSnd (mapFresh f row) . soAnd - - Functor Row where - map = Row.map - - public export - Foldable Row where - foldr f x [<] = x - foldr f x (row :< (_ :- y)) = foldr f (f y x) row - - foldl f x [<] = x - foldl f x (row :< (_ :- y)) = f (foldl f x row) y - - null [<] = True - null (row :< x) = False - - ||| Forget the freshness of names. - public export - forget : Row a -> Context a - forget [<] = [<] - forget (row :< x) = forget row :< x - - export - extend : Row a -> Assoc a -> Maybe (Row a) - extend row (x :- v) = - case choose (x `freshIn` row) of - Left fresh => Just (row :< (x :- v)) - Right _ => Nothing - - -- Equality -- - - soUnique : (x, y : So b) -> x = y - soUnique Oh Oh = Refl - - export - snocCong2 : - {0 row1, row2 : Row a} -> row1 = row2 -> - {0 x, y : Assoc a} -> x = y -> - {0 fresh1 : So (x.name `freshIn` row1)} -> - {0 fresh2 : So (y.name `freshIn` row2)} -> - row1 :< x = row2 :< y - snocCong2 Refl Refl = rewrite soUnique fresh1 fresh2 in Refl - - -- Variables aren't fresh -- - - -- NOTE: cannot implement - 0 strEqReflect : (x, y : String) -> (x = y) `Reflects` (x == y) - strEqReflect x y = believe_me () - - 0 strEqRefl : (x : String) -> Not (So (x /= x)) - strEqRefl x prf with (strEqReflect x x) | (x == x) - _ | RTrue _ | _ = absurd prf - _ | RFalse neq | _ = neq Refl - - export - 0 varPosNotFresh : VarPos (forget row) x v -> Not (So (x `freshIn` row)) - varPosNotFresh {row = row :< (x :- v)} Here fresh = strEqRefl x (fst $ soAnd fresh) - varPosNotFresh {row = row :< y} (There pos) fresh = varPosNotFresh pos (snd $ soAnd fresh) - - export - varUniqueIndex : (row : Row a) -> VarPos (forget row) x v -> VarPos (forget row) x w -> v = w - varUniqueIndex (row :< (x :- _)) Here Here = Refl - varUniqueIndex ((:<) row (x :- _) {fresh}) Here (There pos2) = void $ varPosNotFresh pos2 fresh - varUniqueIndex ((:<) row (x :- _) {fresh}) (There pos1) Here = void $ varPosNotFresh pos1 fresh - varUniqueIndex (row :< (y :- _)) (There pos1) (There pos2) = varUniqueIndex row pos1 pos2 - - -- Equivalence -- - - export infix 6 <~> - - public export - data Step : Row a -> Row a -> Type where - Cong : - Step row1 row2 -> (0 x : Assoc a) -> - {0 fresh1 : So (x.name `freshIn` row1)} -> - {0 fresh2 : So (x.name `freshIn` row2)} -> - Step (row1 :< x) (row2 :< x) - Swap : - (0 x : Assoc a) -> (0 y : Assoc a) -> - {0 fresh1 : So (x.name `freshIn` row)} -> - {0 fresh2 : So (y.name `freshIn` row :< x)} -> - {0 fresh3 : So (y.name `freshIn` row)} -> - {0 fresh4 : So (x.name `freshIn` row :< y)} -> - Step (row :< x :< y) (row :< y :< x) - - public export - data (<~>) : Row a -> Row a -> Type where - Nil : row <~> row - (::) : Step row1 row2 -> row2 <~> row3 -> row1 <~> row3 - - %name Step step - %name (<~>) prf - - export - trans : row1 <~> row2 -> row2 <~> row3 -> row1 <~> row3 - trans [] prf = prf - trans (step :: prf1) prf2 = step :: trans prf1 prf2 - - symStep : Step row1 row2 -> Step row2 row1 - symStep (Cong step x) = Cong (symStep step) x - symStep (Swap x y) = Swap y x - - export - sym : row1 <~> row2 -> row2 <~> row1 - sym [] = [] - sym (step :: prf) = trans (sym prf) [symStep step] - - equivLengthStep : Step row1 row2 -> length (forget row1) = length (forget row2) - equivLengthStep (Cong step x) = cong S (equivLengthStep step) - equivLengthStep (Swap x y) = Refl - - equivLength : row1 <~> row2 -> length (forget row1) = length (forget row2) - equivLength [] = Refl - equivLength (step :: prf) = trans (equivLengthStep step) (equivLength prf) - - export - Uninhabited ((:<) row x {fresh} <~> [<]) where - uninhabited prf = absurd (equivLength prf) - - export - Uninhabited ([<] <~> (:<) row x {fresh}) where - uninhabited prf = absurd (equivLength prf) - - 0 equivFreshInStep : Step row1 row2 -> So (x `freshIn` row1) -> So (x `freshIn` row2) - equivFreshInStep (Cong step y) = andSo . mapSnd (equivFreshInStep step) . soAnd - equivFreshInStep (Swap {row} (y :- v) (z :- w)) = - andSo . mapSnd andSo . - (\(prf1, prf2, prf3) => (prf2, prf1, prf3)) . - mapSnd (soAnd {a = x /= y, b = freshIn x row}) . soAnd - - 0 equivFreshIn : row1 <~> row2 -> So (x `freshIn` row1) -> So (x `freshIn` row2) - equivFreshIn [] = id - equivFreshIn (step :: prf) = equivFreshIn prf . equivFreshInStep step - - cong : - row1 <~> row2 -> (0 x : Assoc a) -> - {0 fresh1 : So (x.name `freshIn` row1)} -> - {0 fresh2 : So (x.name `freshIn` row2)} -> - row1 :< x <~> row2 :< x - cong [] x = rewrite soUnique fresh1 fresh2 in [] - cong (step :: prf) x = - let 0 fresh' = equivFreshInStep step fresh1 in - Cong step x {fresh2 = fresh'} :: cong prf x - - -- Removal -- - - public export - removePos : (row : Row a) -> VarPos (forget row) x v -> (Singleton v, Row a) - export - 0 removePosFresh : - (row : Row a) -> (pos : VarPos (forget row) x v) -> - So (y `freshIn` row) -> So (y `freshIn` snd (removePos row pos)) - - removePos (row :< (_ :- v)) Here = (Val v, row) - removePos ((:<) row x {fresh}) (There pos) = - ( fst (removePos row pos) - , (:<) (snd $ removePos row pos) x {fresh = removePosFresh row pos fresh} - ) - - removePosFresh (row :< _) Here = snd . soAnd - removePosFresh ((:<) row (z :- v) {fresh}) (There pos) = - andSo . mapSnd (removePosFresh row pos) . soAnd - - public export - remove : (row : Row a) -> Var (forget row) v -> (Singleton v, Row a) - remove row i = removePos row i.pos - - -- Reflection - - -- NOTE: cannot implement - 0 soNotSym : {x, y : String} -> So (x /= y) -> So (y /= x) - soNotSym = believe_me - - 0 freshNotPos : (row : Row a) -> VarPos (forget row) x v -> So (y `freshIn` row) -> So (y /= x) - freshNotPos (row :< _) Here = fst . soAnd - freshNotPos (row :< x) (There pos) = freshNotPos row pos . snd . soAnd - - export - 0 removedIsFresh : - (row : Row a) -> (pos : VarPos (forget row) x v) -> - So (x `freshIn` snd (removePos row pos)) - removedIsFresh ((:<) row _ {fresh}) Here = fresh - removedIsFresh ((:<) row (y :- v) {fresh}) (There pos) = - andSo (soNotSym (freshNotPos row pos fresh), removedIsFresh row pos) - - export - reflectRemovePos : - (row : Row a) -> (pos : VarPos (forget row) x v) -> - (:<) (snd $ removePos row pos) (x :- v) {fresh = removedIsFresh row pos} <~> row - reflectRemovePos ((:<) row _ {fresh}) Here = [] - reflectRemovePos ((:<) row (y :- w) {fresh}) (There pos) = - ( Swap (y :- w) (x :- v) - {fresh4 = andSo (freshNotPos row pos fresh, removePosFresh row pos fresh)} - :: cong (reflectRemovePos row pos) (y :- w)) - - -- Tracing Variables -- - - equivVarPosStep : Step row1 row2 -> VarPos (forget row1) x v -> VarPos (forget row2) x v - equivVarPosStep (Cong step _) Here = Here - equivVarPosStep (Cong step y) (There pos) = There (equivVarPosStep step pos) - equivVarPosStep (Swap y _) Here = There Here - equivVarPosStep (Swap _ z) (There Here) = Here - equivVarPosStep (Swap y z) (There (There pos)) = There (There pos) - - export - equivVarPos : row1 <~> row2 -> VarPos (forget row1) x v -> VarPos (forget row2) x v - equivVarPos [] = id - equivVarPos (step :: prf) = equivVarPos prf . equivVarPosStep step - - removePosInjectiveStep : - (prf : Step row1 row2) -> (pos : VarPos (forget row1) x v) -> - snd (removePos row1 pos) <~> snd (removePos row2 (equivVarPosStep prf pos)) - removePosInjectiveStep (Cong step _) Here = [step] - removePosInjectiveStep (Cong step (y :- v)) (There pos) = - cong (removePosInjectiveStep step pos) (y :- v) - removePosInjectiveStep (Swap (y :- v) _) Here = cong [] (y :- v) - removePosInjectiveStep (Swap _ (z :- v)) (There Here) = cong [] (z :- v) - removePosInjectiveStep (Swap (y :- v) (z :- w)) (There (There pos)) = [Swap (y :- v) (z :- w)] - - export - removePosInjective : - (prf : row1 <~> row2) -> (pos : VarPos (forget row1) x v) -> - snd (removePos row1 pos) <~> snd (removePos row2 (equivVarPos prf pos)) - removePosInjective [] pos = [] - removePosInjective (step :: prf) pos = - trans (removePosInjectiveStep step pos) (removePosInjective prf $ equivVarPosStep step pos) - - export - equivVarUnique : - {0 fresh1 : So (x `freshIn` row1)} -> - {0 fresh2 : So (x `freshIn` row2)} -> - (prf : row1 :< (x :- v) <~> row2 :< (x :- v)) -> - equivVarPos prf Here = Here - equivVarUnique prf with (equivVarPos prf Here) - _ | Here = Refl - _ | There pos = void $ varPosNotFresh pos fresh2 - - -- Partial Removal -- - - FreshOrNothing : String -> Maybe (a, Row a) -> Type - FreshOrNothing x Nothing = () - FreshOrNothing x (Just (a, row)) = So (x `freshIn` row) - - removeHelper : - (m : Maybe (a, Row a)) -> (x : Assoc a) -> - (0 fresh : FreshOrNothing x.name m) -> - Maybe (a, Row a) - removeHelper Nothing x fresh = Nothing - removeHelper (Just (v, row)) x fresh = Just (v, row :< x) - - ||| Attempt to remove the value at name `x` from the row. - export - remove' : String -> Row a -> Maybe (a, Row a) - removeFresh : - (x : String) -> (row : Row a) -> - {y : String} -> So (y `freshIn` row) -> FreshOrNothing y (remove' x row) - - remove' x [<] = Nothing - remove' x ((:<) row (y :- v) {fresh}) = - if y == x - then Just (v, row) - else removeHelper (remove' x row) (y :- v) (removeFresh x row fresh) - - removeFresh x [<] prf = () - removeFresh x (row :< (y :- v)) {y = z} prf with (y == x) - _ | True = snd (soAnd prf) - _ | False with (removeFresh x row $ snd $ soAnd prf) | (remove' x row) - _ | _ | Nothing = () - _ | prf' | Just (v', row') = andSo (fst (soAnd prf), prf') - - -- Reflection - - notSoToSoNot : {b : Bool} -> Not (So b) -> So (not b) - notSoToSoNot {b = False} nprf = Oh - notSoToSoNot {b = True} nprf = absurd (nprf Oh) - - 0 reflectRemoveHelper : {x, y : String} -> Not (x = y) -> Not (So (x == y)) - reflectRemoveHelper neq eq with (strEqReflect x y) | (x == y) - reflectRemoveHelper neq Oh | RTrue eq | _ = neq eq - - reflectRemoveHelper' : - {0 fresh1 : So (y `freshIn` row1)} -> - (x : String) -> Not (y = x) -> - (0 fresh2 : So (x `freshIn` row2)) -> (prf : row1 :< (y :- v) <~> row2 :< (x :- v')) -> - ( pos : VarPos (forget row2) y v - ** snd (removePos (row2 :< (x :- v')) (equivVarPos prf Here)) <~> - (:<) (snd (removePos row2 pos)) (x :- v') - {fresh = removePosFresh row2 pos {y = x} fresh2}) - reflectRemoveHelper' x neq fresh2 prf with (equivVarPos prf Here) - reflectRemoveHelper' x neq fresh2 prf | Here = absurd (neq Refl) - reflectRemoveHelper' x neq fresh2 prf | There pos = - (pos ** []) - - public export - Remove : String -> Row a -> a -> Row a -> Type - Remove x row v row' = - Exists {type = So (x `freshIn` row')} (\fresh => row <~> row' :< (x :- v)) - - export - removeUnique : - (x : String) -> (row1 : Row a) -> - Remove x row1 v row2 -> Remove x row1 w row3 -> (v = w, row2 <~> row3) - removeUnique x row1 (Evidence fresh1 prf1) (Evidence fresh2 prf2) = - let eq = varUniqueIndex row1 (equivVarPos (sym prf1) Here) (equivVarPos (sym prf2) Here) in - let - prf : row2 :< (x :- v) <~> row3 :< (x :- v) - prf = trans (sym prf1) (rewrite eq in prf2) - in - ( eq - , replace - {p = \pos => row2 <~> snd (removePos (row3 :< (x :- v)) pos)} - (equivVarUnique prf) - (removePosInjective prf Here)) - - export - 0 reflectRemove : - (x : String) -> (row : Row a) -> - uncurry (Remove x row) `OnlyWhen` remove' x row - reflectRemove x [<] = RNothing (\(v, row), (Evidence _ prf) => absurd prf) - reflectRemove x ((:<) row (y :- v) {fresh}) with (strEqReflect y x) | (y == x) - _ | RTrue eq | _ = rewrite sym eq in RJust (Evidence fresh []) - _ | RFalse neq | _ with (reflectRemove x row, removeFresh x row {y}) | (remove' x row) - _ | (RJust (Evidence fresh' prf), mkFresh) | Just (v', row') = - RJust (Evidence - (andSo (notSoToSoNot (reflectRemoveHelper (\eq => neq $ sym eq)), fresh')) - (trans - (cong prf (y :- v) - {fresh2 = andSo (notSoToSoNot (reflectRemoveHelper neq), mkFresh fresh)}) - [Swap (x :- v') (y :- v)])) - _ | (RNothing nprf, mkFresh) | _ = - RNothing (\(v', row'), (Evidence fresh' prf) => - let (pos ** prf') = reflectRemoveHelper' x neq fresh' prf in - void $ - nprf (v', snd (remove row' ((%%) y {pos}))) $ - Evidence - (removePosFresh row' pos fresh') - (trans (removePosInjective prf Here) prf')) |