0 | ||| Some properties of functions defined in `Data.Fin`
  1 | module Data.Fin.Properties
  2 |
  3 | import public Data.Fin
  4 |
  5 | import Syntax.PreorderReasoning
  6 |
  7 | %default total
  8 |
  9 | -------------------------------
 10 | --- `finToNat`'s properties ---
 11 | -------------------------------
 12 |
 13 | ||| A Fin's underlying natural number is smaller than the bound
 14 | export
 15 | elemSmallerThanBound : (n : Fin m) -> finToNat n `LT` m
 16 | elemSmallerThanBound FZ = LTESucc LTEZero
 17 | elemSmallerThanBound (FS x) = LTESucc (elemSmallerThanBound x)
 18 |
 19 | ||| Last's underlying natural number is the bound's predecessor
 20 | export
 21 | finToNatLastIsBound : {n : Nat} -> finToNat (Fin.last {n}) = n
 22 | finToNatLastIsBound {n=Z} = Refl
 23 | finToNatLastIsBound {n=S k} = cong S finToNatLastIsBound
 24 |
 25 | ||| Weaken does not modify the underlying natural number
 26 | export
 27 | finToNatWeakenNeutral : {n : Fin m} -> finToNat (weaken n) = finToNat n
 28 | finToNatWeakenNeutral = finToNatQuotient (weakenNeutral n)
 29 |
 30 | ||| WeakenN does not modify the underlying natural number
 31 | export
 32 | finToNatWeakenNNeutral : (0 m : Nat) -> (k : Fin n) ->
 33 |                          finToNat (weakenN m k) = finToNat k
 34 | finToNatWeakenNNeutral m k = finToNatQuotient (weakenNNeutral m k)
 35 |
 36 | ||| `Shift k` shifts the underlying natural number by `k`.
 37 | export
 38 | finToNatShift : (k : Nat) -> (a : Fin n) -> finToNat (shift k a) = k + finToNat a
 39 | finToNatShift Z     a = Refl
 40 | finToNatShift (S k) a = cong S (finToNatShift k a)
 41 |
 42 | ----------------------------------------------------
 43 | --- Complement (inversion) function's properties ---
 44 | ----------------------------------------------------
 45 |
 46 | export
 47 | complementSpec : {n : _} -> (i : Fin n) -> 1 + finToNat i + finToNat (complement i) = n
 48 | complementSpec {n = S k} FZ = cong S finToNatLastIsBound
 49 | complementSpec (FS k) = let H = complementSpec k in
 50 |   let h = finToNatWeakenNeutral {n = complement k} in
 51 |   cong S (rewrite h in H)
 52 |
 53 | ||| The inverse of a weakened element is the successor of its inverse
 54 | export
 55 | complementWeakenIsFS : {n : Nat} -> (m : Fin n) -> complement (weaken m) = FS (complement m)
 56 | complementWeakenIsFS FZ = Refl
 57 | complementWeakenIsFS (FS k) = cong weaken (complementWeakenIsFS k)
 58 |
 59 | export
 60 | complementLastIsFZ : {n : Nat} -> complement (last {n}) = FZ
 61 | complementLastIsFZ {n = Z} = Refl
 62 | complementLastIsFZ {n = S n} = cong weaken (complementLastIsFZ {n})
 63 |
 64 | ||| `complement` is involutive (i.e. applied twice it is the identity)
 65 | export
 66 | complementInvolutive : {n : Nat} -> (m : Fin n) -> complement (complement m) = m
 67 | complementInvolutive FZ = complementLastIsFZ
 68 | complementInvolutive (FS k) = Calc $
 69 |    |~ complement (complement (FS k))
 70 |    ~~ complement (weaken (complement k)) ...( Refl )
 71 |    ~~ FS (complement (complement k))     ...( complementWeakenIsFS (complement k) )
 72 |    ~~ FS k                       ...( cong FS (complementInvolutive k) )
 73 |
 74 | --------------------------------
 75 | --- Strengthening properties ---
 76 | --------------------------------
 77 |
 78 | ||| It's possible to strengthen a weakened element of Fin **m**.
 79 | export
 80 | strengthenWeakenIsRight : (n : Fin m) -> strengthen (weaken n) = Just n
 81 | strengthenWeakenIsRight FZ = Refl
 82 | strengthenWeakenIsRight (FS k) = rewrite strengthenWeakenIsRight k in Refl
 83 |
 84 | ||| It's not possible to strengthen the last element of Fin **n**.
 85 | export
 86 | strengthenLastIsLeft : {n : Nat} -> strengthen (Fin.last {n}) = Nothing
 87 | strengthenLastIsLeft {n=Z} = Refl
 88 | strengthenLastIsLeft {n=S k} = rewrite strengthenLastIsLeft {n=k} in Refl
 89 |
 90 | ||| It's possible to strengthen the inverse of a successor
 91 | export
 92 | strengthenNotLastIsRight : {n : Nat} -> (m : Fin n) -> strengthen (complement (FS m)) = Just (complement m)
 93 | strengthenNotLastIsRight m = strengthenWeakenIsRight (complement m)
 94 |
 95 | ||| Either tightens the bound on a Fin or proves that it's the last.
 96 | export
 97 | strengthen' : {n : Nat} -> (m : Fin (S n)) ->
 98 |               Either (m = Fin.last) (m' : Fin n ** finToNat m = finToNat m')
 99 | strengthen' {n = Z} FZ = Left Refl
100 | strengthen' {n = S k} FZ = Right (FZ ** Refl)
101 | strengthen' {n = S k} (FS m) = case strengthen' m of
102 |     Left eq => Left $ cong FS eq
103 |     Right (m' ** eq) => Right (FS m' ** cong S eq)
104 |
105 | ----------------------------
106 | --- Weakening properties ---
107 | ----------------------------
108 |
109 | export
110 | weakenNZeroIdentity : (k : Fin n) ->  weakenN 0 k ~~~ k
111 | weakenNZeroIdentity FZ = FZ
112 | weakenNZeroIdentity (FS k) = FS (weakenNZeroIdentity k)
113 |
114 | export
115 | shiftFSLinear : (m : Nat) -> (f : Fin n) -> shift m (FS f) ~~~ FS (shift m f)
116 | shiftFSLinear Z     f = reflexive
117 | shiftFSLinear (S m) f = FS (shiftFSLinear m f)
118 |
119 | export
120 | shiftLastIsLast : (m : Nat) -> {n : Nat} ->
121 |                   shift m (Fin.last {n}) ~~~ Fin.last {n=m+n}
122 | shiftLastIsLast Z = reflexive
123 | shiftLastIsLast (S m) = FS (shiftLastIsLast m)
124 |