Use the fin from ExtLib

[elefthei]

This is another annoying compatibility thing -- the Fin.t from ExtLib has many useful lemmas like

  Theorem fin_case : forall n (f : fin (S n)),
      f = F1 \/ exists f', f = FS f'.

But if we decide to use it we would have to change fin everywhere.

[YaZko]

By compatibility you just mean that importing Extlib too eagerly can shadow the standard library's Fin that we use?

Independently from that, there are a few options:

• Live as we live, if you need more lemmas we can define them locally
• Indeed use Extlib's fin type. I'm not too fond of that, I would rather like to cut out completely the dependency on Extlib, and they use the same definition of fin types as the standard library
• Depend on stdpp that defines additional lemmas for the standard library's fin type (and would take PRs)
• On a side note, people tend to recommend the alternate fin n := {k : nat | k < n}, we notably used it in the toy compiler for itrees, we could also consider that.

That being said, I'm almost certain that we will merge @nchappe 's branch for general indexing of choices sooner or later, in which case fin types will be a lot less present, so I would be in favor of the first bullet unless you're actually feeling like it's painful to work with currently.

[elefthei]

Ah ok these all make a lot of sense. Let's keep the standard library fin then and maybe we'll end up adding a dependency to stdpp in the future.