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 <http://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 <http://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 <http://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/aa78fe0e-a6e5-c2c5-bc8a-b18d4282796c%40gmx.net.
