0 | ||| Result-type changing `Fin` arithmetics
  1 | module Data.Fin.Arith
  2 |
  3 | import public Data.Fin
  4 |
  5 | import Syntax.PreorderReasoning
  6 |
  7 | %default total
  8 |
  9 | ||| Addition of `Fin`s as bounded naturals.
 10 | ||| The resulting type has the smallest possible bound
 11 | ||| as illustrated by the relations with the `last` function.
 12 | public export
 13 | (+) : {m, n : Nat} -> Fin m -> Fin (S n) -> Fin (m + n)
 14 | (+) FZ y = coerce (cong S $ plusCommutative n (pred m)) (weakenN (pred m) y)
 15 | (+) (FS x) y = FS (x + y)
 16 |
 17 | ||| Multiplication of `Fin`s as bounded naturals.
 18 | ||| The resulting type has the smallest possible bound
 19 | ||| as illustated by the relations with the `last` function.
 20 | public export
 21 | (*) : {m, n : Nat} -> Fin (S m) -> Fin (S n) -> Fin (S (m * n))
 22 | (*) FZ _ = FZ
 23 | (*) {m = S _} (FS x) y = y + x * y
 24 |
 25 | --- Properties ---
 26 |
 27 | -- Relation between `+` and `*` and their counterparts on `Nat`
 28 |
 29 | export
 30 | finToNatPlusHomo : {m, n : Nat} -> (x : Fin m) -> (y : Fin (S n)) ->
 31 |                    finToNat (x + y) = finToNat x + finToNat y
 32 | finToNatPlusHomo FZ _
 33 |   = finToNatQuotient $ transitive
 34 |      (coerceEq _)
 35 |      (weakenNNeutral _ _)
 36 | finToNatPlusHomo (FS x) y = cong S (finToNatPlusHomo x y)
 37 |
 38 | export
 39 | finToNatMultHomo : {m, n : Nat} -> (x : Fin (S m)) -> (y : Fin (S n)) ->
 40 |                    finToNat (x * y) = finToNat x * finToNat y
 41 | finToNatMultHomo FZ _ = Refl
 42 | finToNatMultHomo {m = S _} (FS x) y = Calc $
 43 |   |~ finToNat (FS x * y)
 44 |   ~~ finToNat (y + x * y)                 ...( Refl )
 45 |   ~~ finToNat y + finToNat (x * y)        ...( finToNatPlusHomo y (x * y) )
 46 |   ~~ finToNat y + finToNat x * finToNat y ...( cong (finToNat y +) (finToNatMultHomo x y) )
 47 |   ~~ finToNat (FS x) * finToNat y         ...( Refl )
 48 |
 49 | -- Relations to `Fin`'s `last`
 50 |
 51 | export
 52 | plusPreservesLast : (m, n : Nat) -> Fin.last {n=m} + Fin.last {n} = Fin.last
 53 | plusPreservesLast Z     n
 54 |   = homoPointwiseIsEqual $ transitive
 55 |       (coerceEq _)
 56 |       (weakenNNeutral _ _)
 57 | plusPreservesLast (S m) n = cong FS (plusPreservesLast m n)
 58 |
 59 | export
 60 | multPreservesLast : (m, n : Nat) -> Fin.last {n=m} * Fin.last {n} = Fin.last
 61 | multPreservesLast Z n = Refl
 62 | multPreservesLast (S m) n = Calc $
 63 |   |~ last + (last * last)
 64 |   ~~ last + last          ...( cong (last +) (multPreservesLast m n) )
 65 |   ~~ last                 ...( plusPreservesLast n (m * n) )
 66 |
 67 | -- General addition properties
 68 |
 69 | export
 70 | plusSuccRightSucc : {m, n : Nat} -> (left : Fin m) -> (right : Fin (S n)) ->
 71 |                     FS (left + right) ~~~ left + FS right
 72 | plusSuccRightSucc FZ        right = FS $ congCoerce reflexive
 73 | plusSuccRightSucc (FS left) right = FS $ plusSuccRightSucc left right
 74 |
 75 | -- Relations to `Fin`-specific `shift` and `weaken`
 76 |
 77 | export
 78 | shiftAsPlus : {m, n : Nat} -> (k : Fin (S m)) ->
 79 |               shift n k ~~~ last {n} + k
 80 | shiftAsPlus {n=Z}   k =
 81 |   symmetric $ transitive (coerceEq _) (weakenNNeutral _ _)
 82 | shiftAsPlus {n=S n} k = FS (shiftAsPlus k)
 83 |
 84 | export
 85 | weakenNAsPlusFZ : {m, n : Nat} -> (k : Fin n) ->
 86 |                   weakenN m k = k + the (Fin (S m)) FZ
 87 | weakenNAsPlusFZ FZ = Refl
 88 | weakenNAsPlusFZ (FS k) = cong FS (weakenNAsPlusFZ k)
 89 |
 90 | export
 91 | weakenNPlusHomo : {0 m, n : Nat} -> (k : Fin p) ->
 92 |                   weakenN n (weakenN m k) ~~~ weakenN (m + n) k
 93 | weakenNPlusHomo FZ = FZ
 94 | weakenNPlusHomo (FS k) = FS (weakenNPlusHomo k)
 95 |
 96 | export
 97 | weakenNOfPlus :
 98 |   {m, n : Nat} -> (k : Fin m) -> (l : Fin (S n)) ->
 99 |   weakenN w (k + l) ~~~ weakenN w k + l
100 | weakenNOfPlus FZ l
101 |   = transitive (congWeakenN (coerceEq _))
102 |   $ transitive (weakenNPlusHomo l)
103 |   $ symmetric (coerceEq _)
104 | weakenNOfPlus (FS k) l = FS (weakenNOfPlus k l)
105 | -- General addition properties (continued)
106 |
107 | export
108 | plusZeroLeftNeutral : (k : Fin (S n)) -> FZ + k ~~~ k
109 | plusZeroLeftNeutral k = transitive (coerceEq _) (weakenNNeutral _ k)
110 |
111 | export
112 | congPlusLeft : {m, n, p : Nat} -> {k : Fin m} -> {l : Fin n} ->
113 |                (c : Fin (S p)) -> k ~~~ l -> k + c ~~~ l + c
114 | congPlusLeft c FZ
115 |   = transitive (plusZeroLeftNeutral c)
116 |                (symmetric $ plusZeroLeftNeutral c)
117 | congPlusLeft c (FS prf) = FS (congPlusLeft c prf)
118 |
119 | export
120 | plusZeroRightNeutral : (k : Fin m) -> k + FZ ~~~ k
121 | plusZeroRightNeutral FZ = FZ
122 | plusZeroRightNeutral (FS k) = FS (plusZeroRightNeutral k)
123 |
124 | export
125 | congPlusRight : {m, n, p : Nat} -> {k : Fin (S n)} -> {l : Fin (S p)} ->
126 |                 (c : Fin m) -> k ~~~ l -> c + k ~~~ c + l
127 | congPlusRight c FZ
128 |   = transitive (plusZeroRightNeutral c)
129 |                (symmetric $ plusZeroRightNeutral c)
130 | congPlusRight {n = S _} {p = S _} c (FS prf)
131 |   = transitive (symmetric $ plusSuccRightSucc c _)
132 |   $ transitive (FS $ congPlusRight c prf)
133 |                (plusSuccRightSucc c _)
134 | congPlusRight {p = Z} c (FS prf) impossible
135 |
136 | export
137 | plusCommutative : {m, n : Nat} -> (left : Fin (S m)) -> (right : Fin (S n)) ->
138 |                   left + right ~~~ right + left
139 | plusCommutative FZ        right
140 |   = transitive (plusZeroLeftNeutral right)
141 |                (symmetric $ plusZeroRightNeutral right)
142 | plusCommutative {m = S _} (FS left) right
143 |   = transitive (FS (plusCommutative left right))
144 |                (plusSuccRightSucc right left)
145 |
146 | export
147 | plusAssociative :
148 |   {m, n, p : Nat} ->
149 |   (left : Fin m) -> (centre : Fin (S n)) -> (right : Fin (S p)) ->
150 |   left + (centre + right) ~~~ (left + centre) + right
151 | plusAssociative FZ centre right
152 |   = transitive (plusZeroLeftNeutral (centre + right))
153 |                (congPlusLeft right (symmetric $ plusZeroLeftNeutral centre))
154 | plusAssociative (FS left) centre right = FS (plusAssociative left centre right)
155 |