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/CAGDRuAj%3DEeAXVyaUvrsfZs8q%2B7JOFoCVXZkABLyUCmhApDVMpg%40mail.gmail.com.
