From 6df261f1c09a4f4df9030375c6874f5c4c8e8f83 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Fri, 25 Nov 2022 15:25:52 +0000 Subject: Prove properties about map. --- src/Soat/Data/Product.idr | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'src/Soat') diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr index f92c23c..c4a2acc 100644 --- a/src/Soat/Data/Product.idr +++ b/src/Soat/Data/Product.idr @@ -2,6 +2,7 @@ module Soat.Data.Product import Control.Relation import Data.List.Elem +import Soat.Relation %default total @@ -66,6 +67,23 @@ map : (f : (i : a) -> x i -> y i) -> {is : List a} -> x ^ is -> y ^ is map f [] = [] map f (x :: xs) = f _ x :: map f xs +public export +indexMap : {0 f : IFunc x y} -> (xs : x ^ is) -> (elem : Elem i is) + -> index (map f xs) elem = f i (index xs elem) +indexMap (x :: xs) Here = Refl +indexMap (x :: xs) (There elem) = indexMap xs elem + +public export +mapId : (xs : x ^ is) -> map (\_ => Basics.id) xs = xs +mapId [] = Refl +mapId (x :: xs) = cong ((::) x) $ mapId xs + +public export +mapComp : {0 f : IFunc y z} -> {0 g : IFunc x y} -> (xs : x ^ is) + -> map (\i => f i . g i) xs = map f (map g xs) +mapComp [] = Refl +mapComp (x :: xs) = cong ((::) (f _ (g _ x))) $ mapComp xs + public export (++) : x ^ is -> x ^ js -> x ^ (is ++ js) (++) [] ys = ys -- cgit v1.2.3