Is the issue here the ability to translate to Lean more easily? On the flip side, there has been some interest in translation from set.mm to Mathematica, which would be more difficult with 0-based matrices.
Why there is a need for words in the development of matrices? Is any of this already being done in set.mm? Is there literature that develops matrices using words? Norm On Wednesday, September 2, 2020 at 6:08:26 PM UTC-4 di.... gmail.com wrote: > 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 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 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f016fb42-418a-4f6c-89f7-6b423a982710n%40googlegroups.com.
