[ contrib ] Arithmetic on Fin

[buzden]

There are three more or less separate changes (that correspond to separate commits):

• improvement in Data.Fin.Extra module's sectioning -- or else it becomes a mess;
• Data.Fin.Extra contains a function proving properties of relation between finToNat and weaken, I propose similar functions for finToNat regarding to weakenN and shift;
• addition of functions that realise somewhat a linearity property of Fin:
  • going from Fin of sum to (type) sum of Fins: Fin (a+b) -> Either (Fin a) (Fin b);
  • going from Fin of product to (type) product of Fins: Fin (a*b) -> (Fin a, Fin b).

[gallais]

Pretty sure these are the more convenient isos:

public export
pad : (n : Nat) -> Fin m -> Fin (n + m)
pad Z     k = k
pad (S n) k = FS (pad n k)

public export
sum : {a : Nat} -> Either (Fin a) (Fin b) -> Fin (a + b)
sum (Left x)  = weakenN b x
sum (Right x) = pad a x

public export
mus : {a : Nat} -> Fin (a + b) -> Either (Fin a) (Fin b)
mus {a = Z}   k      = Right k
mus {a = S n} FZ     = Left FZ
mus {a = S n} (FS l) = mapFst FS (mus l)

public export
prod : {b : Nat} -> Fin a -> Fin b -> Fin (a * b)
prod FZ     y = weakenN (mult (pred a) b) y
prod (FS x) y = pad b (prod x y)

public export
dorp : Fin (a * b) -> (Fin a, Fin b)
dorp = ? {- ...divmod... -}

[buzden]

Pretty sure these are the more convenient isos:

I agree with you and I rewrote correctness proofs of split functions as an inverse of appropriate functions.

However, I couldn't manage to call them as you suggest because there could be two different pairs of notions for sum and product for Fins:

• the sum and product of Fins as bounded Nats
• sum and product of Fins as indices.

These sums and products have different properties.

What I was originally talked about is the index-sum and index-product (this is what you name sum and prod in your example). If it has the signature of f : {...} -> Either (Fin a) (Fin b) -> Fin (a + b) then it has nice property of f (Right last) is last. The same for product. If index-product has signature of g : {...} -> Fin a -> Fin b -> Fin (a * b), then g last last is last. It's great.

When I was at first trying to express properties of my split functions through sum and product of Fins-as-bounded-Nats (I'll call then number-sum and number-product), I realised that signatures as above are not precise enough. E.g., if the signature of number-sum and number-product would be

(+) : {...} -> Fin a -> Fin b -> Fin (a + b)
(*) : {...} -> Fin a -> Fin b -> Fin (a * b)

it would lead to the following: the (Fin 4) 3 + the (Fin 3) 2 would be 5 of type Fin 7 and the (Fin 4) 3 * the (Fin 3) 2 would be 6 of type Fin 12. I.e. last + last wouldn't be last and the same for *.

Thus, I refined the signatures of number-sum and number-product to

(+) : {...} -> Fin (S a) -> Fin (S b) -> Fin (S $ a + b)
(*) : {...} -> Fin (S a) -> Fin (S b) -> Fin (S $ a * b)

With these signatures, examples from above would be nicer: the (Fin 4) 3 + the (Fin 3) 2 is 5 of type Fin 6 and the (Fin 4) 3 * the (Fin 3) 2 would be 6 of type Fin 7. I.e. signatures are precise, sum and product of lasts are lasts. But this leads to more complex signatures since they requires S ... in them.

---

Well, the question is the following. Actually, the original split functions and their properties now are expressed without number-sum and number-product. But the functions the these operations, and some properties of them are still in this PR. I feel myself that they can be useful sometime, but I'm not sure. So, should they leave or should I remove them?

[buzden]

Rebased over changes of #857.

[buzden]

I rebased again and added documentation comments to main functions.

[gallais]

This was fairly painful but I think the proof have cleaner types and are more maintainable now.
Of course a lot of these dances around congX would not be necessary if we had OTT.

Additionally I have renamed a lot of variables and definitions to have a more uniform
naming style (m, n for Nats, camelCase rather than snake_case, etc.).