From fec727c164f9f3967eb543406d082f89fe61c052 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Fri, 25 Nov 2022 15:31:29 +0000 Subject: Prove index property of shuffle. --- src/Soat/Data/Sublist.idr | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Soat/Data/Sublist.idr b/src/Soat/Data/Sublist.idr index 98e3c14..ec73723 100644 --- a/src/Soat/Data/Sublist.idr +++ b/src/Soat/Data/Sublist.idr @@ -68,3 +68,9 @@ public export shuffle : is `Sublist` js -> x ^ js -> x ^ is shuffle [] xs = [] shuffle (mem :: mems) xs = index xs mem :: shuffle mems xs + +public export +indexShuffle : (f : is `Sublist` js) -> {0 xs : x ^ js} -> (elem : Elem i is) + -> index (shuffle f xs) elem = index xs (curry f elem) +indexShuffle (mem :: mems) Here = Refl +indexShuffle (mem :: mems) (There elem) = indexShuffle mems elem -- cgit v1.2.3