On Sun, Oct 20, 2019 at 5:19 AM 'Alexander van der Vekens' via Metamath < [email protected]> wrote:
> Thank you, Norm, for this background information. I see the risk of a > misuse of additional variables, and I also had concerns about using the > primes ', " (which can be confused with the grave accent grave ` ). > > My initial intend was to use special variables for special cases. > > One of these cases (replacing a setvar variable in a definition by a class > variable in a corresponding theorem) is described in my initial posting: ` > def $e |- I = ( p e. L |-> V ) $. ` , ` defval $p |- ( ( ph /\ .p. e. L ) > -> ( I ` .p. ) = ... ` . If P is not used elsewhere, it can be used instead > of .p., but if it is already used, it is a littel bit strange to use P' in > this case: ` defval $p |- ( ( ph /\ P' e. L ) -> ( I ` P' ) = ... ` . > I would just use P for this, and plan around it so that I don't have to use P elsewhere. It's not especially important that all variables be one-letter abbreviations of something; consistency across multiple statements is more important. Another case would be the need for class variables of the same kind, e.g. > "Let ` M e. ( Base `` A ) `and ` M' e. ( Base `` A ) ` be two matrices ... > ". Here, the "prime" solution is adequate, but could cause the difficulties > explained by Norm. > As Norm suggested, this could be M and N. This is what "variable pairs" are about. A third case is the usage of setvar variables in antecedents/hypotheses, > see, for example, ~ gsumcom3: > > gsumcom3.n $e |- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) ) > > Here, j and k should be replaced by J and K or, if J and K are already in > use, by J' and K'. I often thought that there is a theorem which could help > me proving my theorem, until I find out that it requires setvar variables > in its hypotheses, but in my case there is a class expression at this place > - I have to revise/reprove the concerned theorem, or I have to perform a > transfomation of the class (expression) into a setvar. Maybe it is not a > good idea to allow free setvar variables in hypotheses/antecedents at all, > because these could always cause such problems. But this is a different > topic. > It is almost always the case that set variables in an antecedent are there because they have to be. It's not an equivalent theorem if you replace j with J here, it is stronger, and often not true. In the deduction style, something like |- ( A. x e. A ps -> ch ) can be rewritten as $e |- ( ( ph /\ x e. A ) -> ps ) $a |- ( ph -> ch ) You can easily convert between ( ( ph /\ x e. A ) -> ps ) and ( ph -> A. x e. A ps ) using ralrimiva and r19.21bi. They are equivalent as hypotheses. By contrast, $e |- ( ( ph /\ X e. A ) -> ps ) $a |- ( ph -> ch ) is equivalent to |- ( ( X e. A -> ps ) -> ch ) which is not at all equivalent and is usually useless, because it is unlikely that the hypothesis X e. A holds so it can't be used in the proof. As a concrete example, in which I am running out of adequate available > variables, are theorems about matrices having polynomials as entries. For > these theorems, I use the following capitel letters as class variables with > fixed meaning (in addition I also use symbols-as-class-variables for > certain operations): > > - ` R ` : represents a ring. > - ` B = ( Base `` R ) ` is its base set > - ` P = ( Poly1 `` R ) ` is the polynomial algebra over (the ring) ` R > ` > - ` K = ( Base `` P ) ` is its base set > - ` Y = ( var1 `` R ) ` is its variable > - ` E = ( .g `` ( mulGrp `` P ) ) ` is its exponentiation > > > - ` A = ( N Mat R ) ` is the algebra of N x N matrices over (the ring) > ` R `. > - ` M = ( Base `` A ) ` is its base set > - ` C = ( N Mat P ) ` is the algebra of N x N matrices over (the > polynomial ring) ` P `. > - ` D = ( Base `` C ) ` is its base set > - ` Q = ( Poly1 `` A ) ` is the polynomial algebra over (the matrix > ring) ` A `. > - ` L = ( Base `` Q ) ` is its base set > - ` X = ( var1 `` A ) ` is its variable > - Z: Zero (if .0. is already used) > - O: One ( if .1. is already used) > - T: Transformation (e.g. of a matrix consisting of polynomials into a > polynomial with matrix coefficients) > - F: diverse auxiliary mappings > - I,J: integers (indices, sum variables, etc) > > That means only 7 letters are remaining: CGHSUVW. Usually, V and W are > used for arbitrary classes, indicating that certain classes are sets (e.g. > ` ( X e. V -> ... ) `), so only 5 capital letters are actually remaining: > CGHSU. This means there is no large choice for concrete objects like > matrices and polynomials to be represented. > Do all of these appear simultaneously in the same theorem? You can still achieve consistent naming while double-booking some of the letters, as long as they don't appear together in the same statement (and even in this case it might be worth it to sacrifice some consistency locally due to a naming conflict). V and W can certainly be double-booked, they can be used for vector spaces or individual vectors, and other letters can be used as arbitrary classes if necessary - that's a pretty low priority naming convention. Maybe a mechanism for local class variables (only visible/usable within the > scope in which they are defined) could be helpful, but this would be a too > heavy conceptual change of the metamath system, at least for the moment. > > As a conclusion, I would propose *not *to provide additional class > variables in general at the moment. As a first step, it may be helpful to > provide a table listing all class variables (including the > symbols-as-class-variables) and explainig for which mathematical concept > they are used commonly/frequently. We can put this table into section > "convention", adding the advice to use the shown variables for the > indicated concept whenever possible/adequate. My list shown above could be > a part of such a table... > While I am okay with using such a table as documentation, it should not be considered binding. The "conventions" I am talking about re: naming are all locally defined, generally within a single section, and I wouldn't want to tie peoples' hands with a rigid global convention, especially if it paints people into a corner, as you seem to be. I've never had issues with needing many variable names, but this may be a consequence of my laissez-faire attitude to variable name assignments. As long as you have at most 26 variables, you can make it work (and with symbol variables it's even more than that). I think it's too late for local variables in metamath. I agree with the sentiment, but the verifier support is spotty and the metamath language doesn't lend itself well to this style without a whole lot of verbosity. Insert plug for MM0 that anticipated this problem and uses local variables everywhere, so that you can actually have variables with *names* like "pos" or "start" or "len". Mario -- 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/CAFXXJSshFcMUTw9Xqh4MKo1CJYx-kuzfqW%2BMi9GErDY3KG5XQQ%40mail.gmail.com.
