Stream: Coq users

Topic: Why is the fin type named `t`?


view this post on Zulip Thomas Dziedzic (Apr 19 2024 at 12:05):

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.

view this post on Zulip k32 (Apr 19 2024 at 12:08):

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.

view this post on Zulip Thomas Dziedzic (Apr 19 2024 at 12:11):

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

view this post on Zulip Yann Leray (Apr 19 2024 at 12:23):

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

view this post on Zulip Pierre Roux (Apr 19 2024 at 15:14):

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.

view this post on Zulip Dominique Larchey-Wendling (Apr 20 2024 at 06:41):

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.

view this post on Zulip Pierre Roux (Apr 22 2024 at 07:35):

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.

view this post on Zulip Mukesh Tiwari (Apr 22 2024 at 09:51):

@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

view this post on Zulip Paolo Giarrusso (May 05 2024 at 12:22):

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

view this post on Zulip Thomas Lamiaux (May 06 2024 at 00:15):

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