In Coq and Lean, the structure of inductive types, specifically the peano natural numbers starting at 0, *strongly* prefers 0-based indexing. The difference is stark enough that it's not really ever a discussion. You can do induction on nat, you can't do induction on positive nat (at least the version that is baked into the language doesn't give you this, you have to use a theorem that amounts to an index conversion under the hood). ZFC is more free in this regard because any definition is as good as any other from the point of view of the automation, but there is still friction associated with conversions.
My argument for 0-based matrices is at this point entirely one of uniformity. Changing 300 theorems with a silly index change is not an automatic job so it will be a lot of work, and the gain is small (and since I'm on Dijkstra's side in this argument, the gain is negative from my POV). Unlike Norm I don't think that rigid adherence to the textbook formulations of things is necessarily a good idea, as long as I think the author would agree that the reformulation is essentially equivalent (the "mathematician's equal"). It is easier to get this confirmation when you have actual practicing mathematicians on staff, as it were; there are a lot of mathematicians getting into lean these days and the 0-based thing hasn't caused one bit of dissent that I have heard. Here's the definition of a matrix: https://leanprover-community.github.io/mathlib_docs/find/matrix/src . It uses arbitrary finite sets, but further down the page you will see some theorems like https://leanprover-community.github.io/mathlib_docs/find/matrix.sub_left/src that specialize to the type "fin n", which is lean's version of our (0..^n). It is defined as {i : nat | i < n}, where nat is the inductive type of nonnegative integers. The type (1...n) would be the more cumbersome {i : nat | 0 < i /\ i <= n}, which has an extra conjunct that would have to be dealt with whenever you destructure the type (and working directly from the stated definition is much more common in lean than metamath). This is the sort of extra friction I am talking about - it's not just changing numbers in a few places. Mario On Wed, Sep 2, 2020 at 3:52 PM 'Stanislas Polu' via Metamath < [email protected]> wrote: > Wouldn’t they be clearly differentiated in a type theory setup? How does > coq/lean treat those? Are they the same concept or separated ones? > > -stan > > On Wed, Sep 2, 2020 at 8:51 PM 'fl' via Metamath < > [email protected]> wrote: > >> >> >> >> > I do not like the idea to regard words as vectors - these are two >> completely different concepts >> >> >> >> >> Simply do a computer program and you will realize soon that tuples can be >> concatenated at will. >> Length is a concept relevant to words and matrices. >> >> There is an abstract theory of words regarding them as elements of free >> structures. Concatenation is >> not at all an operation of its own. It's an operation similar to the >> others. >> >> Pretty sure that some transformation of matrices can be analyzed in terms >> of concatenation or subwords. >> >> No definitely it's the same concept. >> >> -- >> FL >> >> >> >> >> >> >> >> >> -- >> >> >> You received this message because you are subscribed to the Google Groups >> "Metamath" group. >> >> >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> >> >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/004ddf15-75e7-4bcb-90ec-94b021bfe12fn%40googlegroups.com >> <https://groups.google.com/d/msgid/metamath/004ddf15-75e7-4bcb-90ec-94b021bfe12fn%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> >> >> -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/CACZd_0wnkT5GnnRE7BuQKtuj0BTc5QWvGjQTotmKHTAE4t48fQ%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CACZd_0wnkT5GnnRE7BuQKtuj0BTc5QWvGjQTotmKHTAE4t48fQ%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSt%2ByKgLEpSfci1kCPtO0uwco6BOSTnuUoYFp9CNN3TUPQ%40mail.gmail.com.
