Skip to content

Commit ddda0d5

Browse files
buzdenbuzden
committed
Both fin "split" functions got their inverse "index" functons.
1 parent 84cb75e commit ddda0d5

File tree

1 file changed

+66
-38
lines changed

1 file changed

+66
-38
lines changed

‎libs/contrib/Data/Fin/Extra.idr

Lines changed: 66 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@ module Data.Fin.Extra
33
import Data.Fin
44
import Data.Nat
55

6+
import Syntax.WithProof
7+
68
%default total
79

810
-------------------------------
@@ -107,6 +109,13 @@ weakenNZero_preserves {a=S i} (FS x) = rewrite weakenNZero_preserves x in
107109
rewrite plusZeroRightNeutral i in
108110
Refl
109111

112+
export
113+
shift_FS_linear : (a : Nat) -> {0 b : Nat} -> (0 x : Fin b) -> shift a (FS x) = rewrite sym $ plusSuccRightSucc a b in FS (shift a x)
114+
shift_FS_linear Z x = Refl
115+
shift_FS_linear (S k) x = rewrite shift_FS_linear k x in
116+
rewrite plusSuccRightSucc k b in
117+
Refl
118+
110119
-----------------------------------
111120
--- Division-related properties ---
112121
-----------------------------------
@@ -246,49 +255,68 @@ plusAssociative (FS x) centre right {a=S i} = rewrite plusAssociative x centre r
246255
--- Splitting operations and their properties ---
247256
-------------------------------------------------
248257

249-
export
250-
splitSumFin : {a : Nat} -> Fin (a + b) -> Either (Fin a) (Fin b)
251-
splitSumFin {a=Z} x = Right x
252-
splitSumFin {a=S k} FZ = Left FZ
253-
splitSumFin {a=S k} (FS x) = mapFst FS $ splitSumFin x
258+
public export
259+
indexSum : {a : Nat} -> Either (Fin a) (Fin b) -> Fin (a + b)
260+
indexSum $ Left l = weakenN b l
261+
indexSum $ Right r = shift a r
254262

255-
export
256-
splitProdFin : {a, b : Nat} -> Fin (a * b) -> (Fin a, Fin b)
257-
splitProdFin {a=S _} x = case splitSumFin x of
263+
public export
264+
splitSum : {a : Nat} -> Fin (a + b) -> Either (Fin a) (Fin b)
265+
splitSum {a=Z} x = Right x
266+
splitSum {a=S k} FZ = Left FZ
267+
splitSum {a=S k} (FS x) = mapFst FS $ splitSum x
268+
269+
public export
270+
indexProd : {b : Nat} -> Fin a -> Fin b -> Fin (a * b)
271+
indexProd FZ = weakenN $ mult (pred a) b
272+
indexProd (FS x) = shift b . indexProd x
273+
274+
public export
275+
splitProd : {a, b : Nat} -> Fin (a * b) -> (Fin a, Fin b)
276+
splitProd {a=S _} x = case splitSum x of
258277
Left y => (FZ, y)
259-
Right y => mapFst FS $ splitProdFin y
278+
Right y => mapFst FS $ splitProd y
260279

261280
--- Properties ---
262281

282+
splitSum_of_weakenN : (l : Fin a) -> Left l = splitSum {b} (weakenN b l)
283+
splitSum_of_weakenN FZ = Refl
284+
splitSum_of_weakenN (FS x) = cong (mapFst FS) $ splitSum_of_weakenN {b} x
285+
286+
splitSum_of_shift : {a : Nat} -> (r : Fin b) -> Right r = splitSum {a} (shift a r)
287+
splitSum_of_shift {a=Z} r = Refl
288+
splitSum_of_shift {a=S k} r = cong (mapFst FS) $ splitSum_of_shift {a=k} r
289+
290+
export
291+
split_of_index_sum_inverse : {a : Nat} -> (e : Either (Fin a) (Fin b)) -> e = splitSum (indexSum e)
292+
split_of_index_sum_inverse (Left l) = splitSum_of_weakenN l
293+
split_of_index_sum_inverse (Right r) = splitSum_of_shift r
294+
295+
export
296+
index_of_split_sum_inverse : {a, b : Nat} -> (f : Fin (a + b)) -> f = indexSum (splitSum {a} {b} f)
297+
index_of_split_sum_inverse {a=Z} f = Refl
298+
index_of_split_sum_inverse {a=S k} FZ = Refl
299+
index_of_split_sum_inverse {a=S k} (FS x) with (index_of_split_sum_inverse {a=k} {b} x)
300+
index_of_split_sum_inverse {a=S _} (FS x) | sub with (splitSum x)
301+
index_of_split_sum_inverse {a=S _} (FS _) | sub | Left _ = rewrite sub in Refl
302+
index_of_split_sum_inverse {a=S _} (FS _) | sub | Right _ = rewrite sub in Refl
303+
263304
export
264-
splitSumFin_correctness : {a, b : Nat} -> (x : Fin $ a + b) ->
265-
case splitSumFin {a} {b} x of
266-
Left l => x = weakenN b l
267-
Right r => x = shift a r
268-
splitSumFin_correctness {a=Z} x = Refl
269-
splitSumFin_correctness {a=S k} FZ = Refl
270-
splitSumFin_correctness {a=S k} (FS x) with (splitSumFin_correctness x)
271-
splitSumFin_correctness {a=S k} (FS x) | subcorr with (splitSumFin x)
272-
splitSumFin_correctness {a=S k} (FS x) | subcorr | Left y = rewrite subcorr in Refl
273-
splitSumFin_correctness {a=S k} (FS x) | subcorr | Right y = rewrite subcorr in Refl
305+
split_of_index_prod_inverse : {a : Nat} -> (x : Fin a) -> (y : Fin b) -> (x, y) = splitProd (indexProd x y)
306+
split_of_index_prod_inverse {a=S k} FZ y = rewrite sym $ splitSum_of_weakenN {b=mult k b} y in Refl
307+
split_of_index_prod_inverse {a=S k} (FS x) y = rewrite sym $ splitSum_of_shift {a=b} $ indexProd x y in
308+
cong (mapFst FS) $ split_of_index_prod_inverse x y
274309

275310
export
276-
splitProdFin_correctness : {a, b : Nat} -> (x : Fin $ S a * S b) ->
277-
let (o, i) = splitProdFin {a=S a} {b=S b} x in
278-
x = i + o * last {n=S b}
279-
splitProdFin_correctness x with (splitSumFin_correctness {a=S b} x)
280-
splitProdFin_correctness x | sumcorr with (splitSumFin {a=S b} x)
281-
splitProdFin_correctness x | sumcorr | Left y = rewrite sumcorr in weakenNAsPlusFZ {a=mult a (S b)} y
282-
splitProdFin_correctness x | sumcorr | Right y with (a)
283-
splitProdFin_correctness x | sumcorr | Right y | S i with (splitProdFin_correctness y)
284-
splitProdFin_correctness x | sumcorr | Right y | S i | subcorr with (splitProdFin {a=S i} {b=S b} y)
285-
splitProdFin_correctness x | sumcorr | Right y | S i | subcorr | (oo, ii) =
286-
rewrite sumcorr in
287-
rewrite subcorr in
288-
rewrite sym $ plusSuccRightSucc ii $ last {n=b} + (oo * FS (last {n=b})) in
289-
rewrite shiftAsPlus {b} $ ii + (oo * FS (last {n=b})) in
290-
rewrite plusAssociative (last {n=b}) ii $ (oo * FS (last {n=b})) in
291-
rewrite plusCommutative (last {n=b}) ii in
292-
rewrite plusAssociative ii (last {n=b}) $ (oo * FS (last {n=b})) in
293-
rewrite plusSuccRightSucc b $ b + i * S b in
294-
Refl
311+
index_of_split_prod_inverse : {a, b : Nat} -> (f : Fin (a * b)) -> f = uncurry (indexProd {a} {b}) (splitProd {a} {b} f)
312+
index_of_split_prod_inverse {a=S k} f with (@@ splitSum f)
313+
index_of_split_prod_inverse f | (Left l ** prf) = rewrite prf in
314+
rewrite sym $ cong indexSum prf in
315+
index_of_split_sum_inverse f
316+
index_of_split_prod_inverse f | (Right r ** prf) = rewrite prf in
317+
rewrite index_of_split_sum_inverse {a=b} {b=mult k b} f in
318+
rewrite cong indexSum prf in
319+
rewrite indexProd_of_mapFst_FS {a=k} {b} $ splitProd r in
320+
cong (shift b) $ index_of_split_prod_inverse r where
321+
indexProd_of_mapFst_FS : {b : Nat} -> (x : (Fin a, Fin b)) -> uncurry (indexProd {b}) (mapFst FS x) = shift b (uncurry (indexProd {b}) x)
322+
indexProd_of_mapFst_FS (x, y) = Refl

0 commit comments

Comments
 (0)