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.
