Mingli, you wrote: > So far the learning curve is a little bit steep because a lot of conventions are not documented?
We are striving to keep documentation up-to-date and to document our conventions. For the moment, documentation is not very centralized: there is the website (e.g., http://us2.metamath.org/mpeuni/mmset.html), the github pages (like README.md and CONTRIBUTING.md), the help of the metamath program (obtained by typing MM> help [command]), the statement ~conventions in set.mm (http://us2.metamath.org/mpeuni/conventions.html#uniprg) for set.mm-specific conventions, searching within this google group. Can you keep a log of what seems undocumented to you, and share it here once you've verified it is undocumented, so that we can add it ? Thanks in advance. Benoît On Friday, February 11, 2022 at 2:04:43 PM UTC+1 [email protected] wrote: > Hi, Thierry and Benoit, > > I had read the lines in set.mm > > ``` > $c class $. > > $( Add 'class' as a typecode. $) > $( $j syntax 'class'; $) > ``` > > So I guess the class notion is a kind of syntax sugar. I did not know mmj > can simplify the development, that is why I want to understand how this > mechanism works. > Right now, I know mmj and the webpage is more important for development. > > Thanks > > Mingli > > On Fri, Feb 11, 2022 at 7:55 PM Thierry Arnoux <[email protected]> wrote: > >> Hi Mingli, >> You're trying to understand how a proof is stored and verified. >> >> There's absolutely nothing wrong with that, but I just wanted to state >> that it's not mandatory that you understand those. >> >> I think when I first started with Metamath, I focused on understanding >> simple proofs on the website, or on MMJ2 (both are similar), created my >> first proofs and let the tool (MMJ2) store and verified the proof for me. I >> consider the compressed proof format like a kind of "binary executable" >> which we don't absolutely need to understand and read. >> >> MMJ2 and the website both hide some steps of the proof (syntactical >> steps) and allows you focus on the more important ones (logical steps). >> >> 1. So the question here is: cdr, ccrg, cfield, df-field are all $a, and >> only elin2 is a $p, where are the $f or $ e? >> >> Like all proofs in set.mm, the proof you chose is provided in compressed >> format. That format favors space over readability, so as few information as >> possible is included. >> >> The $f and $e hypotheses which are "in scope" are known, so they do not >> need not repeated in the statement list in parentheses. That format is >> described in appendix B. of the Metamath Book, which states: >> >> *If the statement being proved has m mandatory hypotheses,** integers 1 >> through m correspond to the labels of these hypotheses in the** order >> shown by the show statement ... / full command, i.e., the RPN** order of >> the mandatory hypotheses.* >> >> Here is the output of that command: >> >> 67962 isfld $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) ) $= >> ... $. >> Its mandatory hypotheses in RPN order are: >> cR $f class R $. >> >> So there is a single mandatory hypothesis, which is `cR`, referred to by >> a `A` in the compressed proof (here A encodes to integer 1). >> >> MM> show proof isfld /all >> 1 cA=cR $f class R >> 2 cB=cdr $a class DivRing >> 3 cC=ccrg $a class CRing >> 4 cX=cfield $a class Field >> 5 elin2.x=df-field $a |- Field = ( DivRing i^i CRing ) >> 6 isfld=elin2 $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) ) >> ``` >> >> 2. But where does step 1 come from? and when the verifier reads cdr in >> step 2, what does it happen? >> It seems I should understand how class notions take effect precisely? >> >> ...and that's where the `cR` comes from, since `A` is the first character >> of the compressed proof (ABCDEF). >> >> What happens is that the statement with a single "class R" is stored on >> the proof stack. >> >> >> Here is how I would describe the rest of the verification process: >> >> Next, `B` is read, which refers to `cdr`. This pushes "class DivRing" on >> the stack, which now contains "class R / class DivRing". >> >> And so on until step 5, where the stack contains "class R / class DivRing >> / class CRing / class Field / |- Field = ( DivRing i^i CRing )". >> >> Then, at step 6, `elin2` in invoked, which requires 4 variables : A, X, B >> and C, and an hypothesis ~elin2.x of the form `|- X = ( B i^i C ) `. >> >> All 5 items are popped from the stack, in the order in which they are >> declared: >> >> - A, which is substituted by R >> - B, substituted by DivRing >> - C, substituted by CRing >> - X, substituted by Field >> - |- X = ( B i^i C ), substituted by Field = ( DivRing i^i CRing ). >> The verifier checks that this substitution matches. >> >> Finally, the statement of elin2 is pushed on the stack: |- ( A e. X <-> ( >> A e. B /\ A e. C ) ) >> >> Which, when substituted, results in |- ( R e. Field <-> ( R e. DivRing /\ >> R e. CRing ) ). >> >> That is the final and only expression remaining on the proof stack, and >> the verifier finally verifies that this matches with the statement of >> ~isfld. >> >> And that's it! Luckily this was a very short proof! >> >> >> In practice, if you had used MMJ2 or checked the website proof of isfld >> <http://us2.metamath.org:88/mpeuni/isfld.html>, you can see that that >> proof only has 2 steps: 1-4 are hidden, and only 5-6 are shown. >> >> That's because steps 1-4 only deal with "syntactically" building the >> expressions which will later be used in substitutions, not deriving new >> true statements. >> >> >> I hope this helps and clarifies!... >> >> BR, >> _ >> Thierry >> >> >> On 11/02/2022 15:54, Mingli Yuan wrote: >> >> Hi, Benoit and others, thanks for your reply. Let me keep a weekly pace >> to learn metamath step by step. >> I still stick to Alex's assignment :-) - try to complete the proofs he >> left in the first reply. >> Yes and of course, I was blocked by questions. I record the learning >> process and give comments and questions as below. >> It is a little bit long and preliminary, but maybe the next newcomers can >> learn faster and easier. >> >> I had read the manual - *metamath* by Norm, and I understood the RPN >> notion and the stack. >> Also I checked several examples, e.g., >> >> ```metamath >> $( A field is a commutative division ring. (Contributed by Mario >> Carneiro,17-Jun-2015.) $) >> isfld $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) ) $= >> ( cdr ccrg cfield df-field elin2 ) ABCDEF $. >> ``` >> >> The proof here starts with cdr which is a class notion, and I understand >> here is one abstract layer based on the class notion. >> And based on the abstract layer we can set up more advanced math. In my >> understanding, it also means if we grasp several rules >> above the layer we can safely ignore the detail beneath the layer. Those >> are the assumptions I started to explore. >> >> I copy the definitions of field and elin2 for reference >> >> ```metamath >> $c DivRing $. >> $c Field $. >> >> $( Extend class notation with class of all division rings. $) >> cdr $a class DivRing $. >> >> $( Class of fields. $) >> cfield $a class Field $. >> >> $( Define class of all division rings. A division ring is a ring in which >> the set of units is exactly the nonzero elements of the ring. >> (Contributed by NM, 18-Oct-2012.) $) >> df-drng $a |- DivRing = { r e. Ring | >> ( Unit ` r ) = ( ( Base ` r ) \ { ( 0g ` r ) } ) } $. >> >> $( A _field_ is a commutative division ring. (Contributed by Mario >> Carneiro, >> 17-Jun-2015.) $) >> df-field $a |- Field = ( DivRing i^i CRing ) $. >> ``` >> >> ``` >> ${ >> elin2.x $e |- X = ( B i^i C ) $. >> $( Membership in a class defined as an intersection. (Contributed by >> Stefan O'Rear, 29-Mar-2015.) $) >> elin2 $p |- ( A e. X <-> ( A e. B /\ A e. C ) ) $= >> ( wcel cin wa eleq2i elin bitri ) ADFABCGZFABFACFHDLAEIABCJK $. >> $} >> ``` >> >> In order to understand how proof of isfld works, I use below command to >> show >> >> ``` >> MM > show proof isfld /renumber /lemmon >> 1 df-field $a |- Field = ( DivRing i^i CRing ) >> 2 1 elin2 $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) ) >> ``` >> >> and >> >> ``` >> MM> show proof isfld >> 5 elin2.x=df-field $a |- Field = ( DivRing i^i CRing ) >> 6 isfld=elin2 $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) ) >> ``` >> >> My questions here are: >> >> 1. In the manual by Norm, a simple example was given at page 137, it >> pushes several $f or $ e into the stack, >> and when it meets assertions, it will match and substitute. >> >> Considering proof >> >> ```metamath >> ( cdr ccrg cfield df-field elin2 ) ABCDEF $. >> ``` >> >> So the question here is: cdr, ccrg, cfield, df-field are all $a, and only >> elin2 is a $p, where are the $f or $ e? >> >> 2. Fortunately, I check the manual and found a /all option and mention >> about syntax construction, so we have >> >> ``` >> MM> show proof isfld /all >> 1 cA=cR $f class R >> 2 cB=cdr $a class DivRing >> 3 cC=ccrg $a class CRing >> 4 cX=cfield $a class Field >> 5 elin2.x=df-field $a |- Field = ( DivRing i^i CRing ) >> 6 isfld=elin2 $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) ) >> ``` >> >> But where does step 1 come from? and when the verifier reads cdr in step >> 2, what does it happen? >> It seems I should understand how class notions take effect precisely? >> >> 3. If we could ignore the class notions here as an abstraction layer, >> maybe we can understand the proof as process below >> >> ``` >> 1. cdr a label and class of DivRing, left it in scope >> 2. ccrg a label and class of CRing, left it in scope >> 3. cfield a label and class of Field, left it in scope >> 4. df-field construct class by defined constructions and assigned >> it to label Field, left it in scope >> 5. elin2.x matched by Field >> 6. elin2 takes effect by elin2 and QED. >> ``` >> >> I know this understanding is only roughly true but not precisely. >> >> Thanks in advance. >> >> Mingli >> >> >> >> >> >> >> >> >> On Tue, Feb 8, 2022 at 8:23 AM Benoit <[email protected]> wrote: >> >>> Sorry, I'm a bit late to the party. As has been noted, you also need >>> bilinearity of the associated symmetric form. Without it, you are simply >>> defining homogeneous functions of degree two. >>> >>> Also, quadratic forms should be defined in set.mm on (left) modules for >>> wider applicability (even if some results might be funny over >>> noncommutative rings). >>> >>> As for the first point, the associated symmetric form is probably >>> important enough that a definition would be useful. Here is a proposal (I >>> do not remember the names of the components of an extensible structure, so >>> I put mnemonic ones): >>> >>> $( Define the function associating with a function ` q ` from a magma to >>> a group its "associated binary form". For its value, see ... It is >>> symmetric as soon as the magma and the group are commutative (with no >>> condition on q), see ... It is bilinear when the magma and the group are >>> respectively a module and its ring of scalars and ` q ` is a quadratic form >>> (this is actually part of the definiton of a quadratic form, see ~df-qform >>> ). $) >>> df-assocbiform $a assoc_bi_form = ( m e. Magma , g e. Group |-> >>> ( q e. ( ( Base `g ) ^m ( Base ` m ) ) |-> >>> ( x , y e. ( Base ` m ) |-> ( ( q ` ( x ( >>> Plus ` m ) y ) ) >>> >>> >>> ( Plus ` g ) >>> ( ( >>> Opposite ` g ) ` ( ( q ` x ) ( Plus ` g ) ( q ` y ) ) ) ) ) ) ) $. >>> >>> If homogeneous functions are to be defined, then maybe (restricting to >>> the case domain=codomain): >>> df-homog $a Homog = ( x e. ScalSet |-> ( d e. NN0 |-> { f e. ( ( Base ` >>> x ) ^m ( Base ` x ) ) | >>> A. a e. ( Base ` x ) A. s e. ( Base ` >>> ( Scalar ` x ) ) ( f ` ( s ( scalmul ` x ) a ) ) = ( s^d ( scalmul ` x ) ( >>> f ` a ) ) } ) ) $. >>> (s^d is probably defined somewhere in set.mm but I do not know the >>> syntax, and ScalSet is the class of "sets with a magma of scalars", or >>> "M-sets" if M is said magma, sometimes "sets with operators", as in group >>> actions). >>> >>> Then, quadratic forms can be defined by: >>> df-qform $a QForm = ( m e. LMod |-> { q e. ( ( Homog ` m ) ` 2 ) | ( ( M >>> assoc_bi_form ( Scalar ` M ) ) ` q ) e. ( BilinForm ` m ) } ) $. >>> >>> It remains to define the class of bilinear forms on a module: >>> df-bilinform $a BilinForm = ( m e. LMod |-> { q e. ( ( Base ` ( Scalar >>> `m ) ) ^m ( ( Base ` m ) X. ( Base ` m ) ) ) | [ the two partial functions >>> are linear forms ] } ) $. >>> >>> If notation becomes too heavy, one can use "local variables" in the form >>> " [ z / ( Base ` x ) ] ... " as is done in a few other definitions in >>> set.mm, if I recall correctly. >>> >>> Benoît >>> >>> >>> On Monday, February 7, 2022 at 2:59:21 AM UTC+1 [email protected] >>> wrote: >>> >>>> Thanks, Thierry, Mario and Alex, I will follow your advice, and take >>>> the exercise. :-) >>>> >>>> The community is so friendly! I will ask if I am blocked. >>>> >>>> Mingli >>>> >>>> >>>> On Mon, Feb 7, 2022 at 8:00 AM vvs <[email protected]> wrote: >>>> >>>>> I don't see why you are so eager to say "types are not quite sets" >>>>>> >>>>> >>>>> I am not, I think. I don't really care. I'm trying to avoid being >>>>> biased but fall in that trap over and over again. >>>>> >>>>> But I know that such people exist >>>>> <https://en.wikipedia.org/wiki/Type_theory#Differences_from_Set_Theory> >>>>> and I don't know why someone should insist that they are wrong just >>>>> because >>>>> somebody else have a different opinion. This is also a philosophical >>>>> difference, not just a practical one. But even from a practical point of >>>>> view everyone have their own definition of feasibility. We can walk >>>>> backwards or even upside down, that's certainly possible, but not >>>>> everyone >>>>> will find this quite feasible. And when I'm not sure what solution is >>>>> feasible in this particular case, I prefer to reason conservatively. But >>>>> maybe I'm overreacting sometimes. >>>>> >>>>> >>>>>> Type theory thinking can still be useful without the trappings of >>>>>> type theory itself, and in fact type theory simulated in set theory has >>>>>> some advantages over pure type theory in that you can bend the rules >>>>>> when >>>>>> it is advantageous to do so. >>>>>> >>>>> >>>>> And not everyone will like it. Should we say that there is only one >>>>> single truth? >>>>> >>>>> >>>>>> In lean, there is a concept called "defeq", or definitional equality, >>>>>> and it is strictly stronger than regular equality: there are things that >>>>>> are propositionally equal but not defeq, like x + (y + z) and (x + y) + >>>>>> z. >>>>>> You can prove these two are equal, but if you have a type family indexed >>>>>> in >>>>>> natural numbers and an element in F ((x + y) + z) you can't just treat >>>>>> it >>>>>> as an element of F (x + (y + z)). In metamath you can; since the values >>>>>> are >>>>>> equal the sets are equal so any element of one is also an element of the >>>>>> other. Defeq is simply not a thing in metamath, and this is very freeing. >>>>>> >>>>> >>>>> Ok. But this is starting to sound like a preaching :) And don't take >>>>> me wrong. If you feel so strongly about this issue I won't continue to >>>>> try >>>>> to dissuade you. Probably this discussion already turned into >>>>> bikeshedding >>>>> and I should stop arguing and do something useful instead :) I'm sorry. >>>>> >>>>> -- >>>>> 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/14ce5c0a-44e9-4ee8-b6be-ac2d67848ac8n%40googlegroups.com >>>>> >>>>> <https://groups.google.com/d/msgid/metamath/14ce5c0a-44e9-4ee8-b6be-ac2d67848ac8n%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/c9b002d5-1182-4ddc-b4cd-8e6502a2ad66n%40googlegroups.com >>> >>> <https://groups.google.com/d/msgid/metamath/c9b002d5-1182-4ddc-b4cd-8e6502a2ad66n%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/CAGDRuAjAUAtf9Mvz%3D7TRK3%3DtjAHPp1e0%2BWEmX61n4%2BUuqT%3DsFw%40mail.gmail.com >> >> <https://groups.google.com/d/msgid/metamath/CAGDRuAjAUAtf9Mvz%3D7TRK3%3DtjAHPp1e0%2BWEmX61n4%2BUuqT%3DsFw%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/f7a1053b-1363-4457-880a-8c00ea1b47d1n%40googlegroups.com.
