@@ -2,8 +2,85 @@ module Data.Fin.Extra
22
33import Data.Fin
44
5+%access public export
6+%default total
7+
8+
59||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.
6−public export
710elemSmallerThanBound : (n : Fin m) -> LT (finToNat n) m
811elemSmallerThanBound FZ = LTESucc LTEZero
912elemSmallerThanBound (FS x) = LTESucc (elemSmallerThanBound x)
13+
14+||| Proof that application of finToNat the last element of Fin **S n** gives **n**.
15+finToNatLastIsBound : finToNat (Fin.last {n}) = n
16+finToNatLastIsBound {n=Z} = Refl
17+finToNatLastIsBound {n=S k} = rewrite finToNatLastIsBound {n=k} in Refl
18+
19+||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.
20+finToNatWeakenNeutral : {n : Fin m} -> finToNat (weaken n) = finToNat n
21+finToNatWeakenNeutral {n=FZ} = Refl
22+finToNatWeakenNeutral {m=S (S _)} {n=FS _} = cong finToNatWeakenNeutral
23+
24+||| Proof that it's possible to strengthen a weakened element of Fin **m**.
25+strengthenWeakenNeutral : (n : Fin m) -> strengthen (weaken n) = Right n
26+strengthenWeakenNeutral {m=S _} FZ = Refl
27+strengthenWeakenNeutral {m=S (S _)} (FS k) = rewrite strengthenWeakenNeutral k in Refl
28+
29+||| Proof that it's not possible to strengthen the last element of Fin **n**.
30+strengthenLastIsLeft : strengthen (Fin.last {n}) = Left (Fin.last {n})
31+strengthenLastIsLeft {n=Z} = Refl
32+strengthenLastIsLeft {n=S k} = rewrite strengthenLastIsLeft {n=k} in Refl
33+
34+||| Enumerate elements of Fin **n** backwards.
35+invFin : Fin n -> Fin n
36+invFin FZ = last
37+invFin {n=S (S _)} (FS k) = weaken (invFin k)
38+
39+||| Proof that an inverse of a weakened element of Fin **n** is a successive of an inverse of an original element.
40+invWeakenIsSucc : (m : Fin n) -> invFin (weaken m) = FS (invFin m)
41+invWeakenIsSucc FZ = Refl
42+invWeakenIsSucc {n=S (S _)} (FS k) = rewrite invWeakenIsSucc k in Refl
43+
44+||| Proof that double inversion of Fin **n** gives the original.
45+doubleInvFinSame : (m : Fin n) -> invFin (invFin m) = m
46+doubleInvFinSame {n=S Z} FZ = Refl
47+doubleInvFinSame {n=S (S k)} FZ = rewrite doubleInvFinSame {n=S k} FZ in Refl
48+doubleInvFinSame {n=S (S _)} (FS x) = trans (invWeakenIsSucc $ invFin x) (cong $ doubleInvFinSame x)
49+
50+||| Proof that an inverse of the last element of Fin (S **n**) in FZ.
51+invLastIsFZ : invFin (Fin.last {n}) = FZ
52+invLastIsFZ {n=Z} = Refl
53+invLastIsFZ {n=S k} = rewrite invLastIsFZ {n=k} in Refl
54+
55+||| Proof that it's possible to strengthen an inverse of a succesive element of Fin **n**.
56+strengthenNotLastIsRight : (m : Fin (S n)) -> strengthen (invFin (FS m)) = Right (invFin m)
57+strengthenNotLastIsRight m = strengthenWeakenNeutral (invFin m)
58+
59+||| Either tightens the bound on a Fin or proves that it's the last.
60+strengthen' : (m : Fin (S n)) -> Either (m = Fin.last) (m' : Fin n ** finToNat m = finToNat m')
61+strengthen' {n = Z} FZ = Left Refl
62+strengthen' {n = S k} FZ = Right (FZ ** Refl)
63+strengthen' {n = S k} (FS m) with (strengthen' m)
64+ | Left eq = Left $ cong eq
65+ | Right (m' ** eq) = Right (FS m' ** cong eq)
66+
67+||| A view of Nat as a quotient of some number and a finite remainder.
68+data FractionView : (n : Nat) -> (d : Nat) -> Type where
69+ Fraction : (n : Nat) -> (d : Nat) -> {auto ok: GT d Z} ->
70+ (q : Nat) -> (r : Fin d) ->
71+ q * d + finToNat r = n -> FractionView n d
72+
73+||| Converts Nat to the fractional view with a non-zero divisor.
74+divMod : (n, d : Nat) -> {auto ok: GT d Z} -> FractionView n d
75+divMod Z (S d) = Fraction Z (S d) Z FZ Refl
76+divMod (S n) (S d) with (divMod n (S d))
77+ | (Fraction n (S d) q r eq) with (strengthen' r)
78+ | Left eq' = Fraction (S n) (S d) (S q) FZ $
79+ rewrite sym eq in
80+ rewrite trans (cong {f=finToNat} eq') finToNatLastIsBound in
81+ cong $ trans
82+ (plusZeroRightNeutral (d + q * S d))
83+ (plusCommutative d (q * S d))
84+ | Right (r' ** eq') = Fraction (S n) (S d) q (FS r') $
85+ rewrite sym $ plusSuccRightSucc (q * S d) (finToNat r') in
86+ cong $ trans (sym $ cong {f=plus (q * S d)} eq') eq