Add inverse to Data.Fin.quotRem and properties

[Taneb]

It would be nice to be able to demonstrate that Fin (x * y) is isomorphic to Fin x × Fin y. This would be useful for proving, for example, in agda-categories that FinSetoids is cartesian, or in something that I'm working on, that you can combine two finite state machines in various way

The inverse function can be implemented as:

combine : ∀ {n k} → Fin k → Fin n → Fin (n ℕ.* k)
combine x zero = inject+ _ x
combine x (suc y) = raise _ (combine x y)

With one direction of inverse proof as:

 : ∀ {n k} x (y : Fin n) → quotRem k (combine x y) ≡ (x , y)
quotRem-combine {suc n} {k} x 0F rewrite splitAt-inject+ k (n ℕ.* k) x = refl
quotRem-combine {suc n} {k} x (suc y) rewrite splitAt-raise k (n ℕ.* k) (combine x y) = cong (Data.Product.map₂ suc) (quotRem-combine x y)

But I haven't been able to prove the other direction

[MatthewDaggitt]

Without looking at much, @uzytkownik opened a recent PR (#1402) with some results about quotRem in. They might be relevant?

[MatthewDaggitt]

In fact I think they implemented exactly the results you're looking for!

[Taneb]

Ah! I hadn't seen that. The types match roughly what I had in mind, but the proofs seem very complicated... I'm going to hunt around for a simper proof

[Taneb]

Finding a simpler proof turned out to be way easier than expected. I'll make a PR this evening

[gallais]

Can we please make combine take its arguments in the same order as _*_?
So combine : Fin n → Fin k → Fin (n ℕ.* k) rather than Fin k → Fin n → ...

[Taneb]

Can we please make combine take its arguments in the same order as _*_?
So combine : Fin n → Fin k → Fin (n ℕ.* k) rather than Fin k → Fin n → ...

I have no objections to this. I was going with consistency with quotRem, which reverses them. Maybe that should also change?

[JacquesCarette]

I have a horrible proof in pi-dual that I meant to clean up and add too. A nice proof is better!

I would suggest adding remQuot (and combine') instead of changing the ones that are there. quotRem outputs things in the 'right' order given its name!

[Taneb]

Before doing anything with reversing multiplications, here's my proof of the other side of the inverse:

combine-quotRem : ∀ {n} k (i : Fin (n ℕ.* k)) → uncurry combine (quotRem {n} k i) ≡ i
combine-quotRem {suc n} k i with splitAt k i | P.inspect (splitAt k) i
... | inj₁ j | P.[ eq ] = begin
  join k (n ℕ.* k) (inj₁ j)      ≡˘⟨ cong (join k (n ℕ.* k)) eq ⟩
  join k (n ℕ.* k) (splitAt k i) ≡⟨ join-splitAt k (n ℕ.* k) i ⟩
  i                              ∎
  where open ≡-Reasoning
... | inj₂ j | P.[ eq ] = begin
  raise {n ℕ.* k} k (uncurry combine (quotRem {n} k j)) ≡⟨ cong (raise k) (combine-quotRem {n} k j) ⟩
  join k (n ℕ.* k) (inj₂ j)                             ≡˘⟨ cong (join k (n ℕ.* k)) eq ⟩
  join k (n ℕ.* k) (splitAt k i)                        ≡⟨ join-splitAt k (n ℕ.* k) i ⟩
  i                                                     ∎
  where open ≡-Reasoning