Hi, I was looking at Fin from https://github.com/coq/coq/blob/master/theories/Vectors/Fin.v#L37 and I'm wondering why it's called `t`

instead of `fin`

? I even see that some of the docs refer to it as fin even:

(** [fin n] is a way to represent \[1 .. n\]

Are the docs out of sync with the type name or am I missing something.

I am merely speculating, but I guess it's implied that this type should always be referred to with the module name. `t`

is short for `type`

, I guess? So instead of `Fin.fin`

or `Fin.type`

one just writes `Fin.t`

for short.

ah that makes sense, I've seen that before but I didn't make the connection in this case since the docs referred to it as fin rather than Fin.t or t. Thanks

This convention is the same as (and probably inherited from) OCaml.

Note, that use of Fin.t is not recommended: https://github.com/coq/coq/blob/master/theories/Vectors/Fin.v#L14-L25 You may save you a lot of troubles by using a more comfortable representation of bounded integers.

Let me step in to express another point of view. One can work with the `Fin.t`

type but as a dependent type, it requires mastering *dependent elimination*, which is not a quick learning path for beginners. That I agree with. It is however a *rewarding learning path* because you will understand a lot while struggling with this type, and the associated type of vectors.

In another context, LaTeX is neither a quick learning path for typesetting beginners. Does this mean it should not be recommended to typeset publications in mathematics or computer science?

Btw, K. Buzzard uses similar arguments to make to case for `Lean`

over `Coq`

for would be formalizing mathematicians.

It's just a matter of objective. In most cases, `Fin.t`

and `Vector.t`

are terrible choices. Indeed, to learn about dependent elimination, they can be good examples. Since we had no clue that @Thomas Dziedzic was in that particular case, better warn.

@Pierre Roux I agree with you that they are difficult to use but it would also be nice if we could put more resources such tutorial, tactics, and anything that we feel will help beginners than outright telling them that it is difficult. I feel the difficult part is the fun :) Now I am a bit comfortable using dependent types after learning tricks like small-inversion but it would be also nice if could add it as a tactic to Coq [1]. Another painful thing which I still don't understand is how to get rid of the "Abstracting over the terms ...." error. Just my 2 cents.

[1] https://github.com/coq/coq/pull/16097

@Mukesh Tiwari you fix these errors by debugging the type error in the code generated by the tactic

Hi @Mukesh Tiwari , we have been working towards building a real documentation for Coq and its platform based on (online) interactive tutorial and how-to. The project will be announced in more details soon, as we are currently still finalizing the repo and the Coq enhancement proposal.

You are making a really good point that didn't cross our minds during preparation and that we'll make sure to remember. This project should also be the opportunity to make all those tricks accessible in a same place, and I hope should make the whole schmilblick easier to learn.

PS: Also, if you were to notice that a tutorial does not to mention such a point, it would be easy to add through a PR

Last updated: Jun 13 2024 at 19:02 UTC