Best way to define things

[r00nk]

Hello again everyone, amateur mathematician here. 
In my spare time I've been working on proving one of the 100 theorems, the 
friendship theorem, and I've gotten myself struck in a bit of a pickle. Namely,
I'm defining a good chunk of graph theory and am trying to find a clean way to 
do so without trampling over similar definitions already found in set.mm.

I've got the proof done on paper and the theorem stated in set.mm as such;

$( (Start of r0nks mathbox) $)

$( simple graphs $)

  $c USGrph $.

  $( Extend class notation with undirected simple graphs. $)
  cusg $a class USGrph $.

  $( Undirected Simple Graph. This definition is loosely based on the UMGrph definition $)
  ${
    $d e v x $.
    df-usgra $a |- USGrph = { <. v , e >. | e : dom e -1-1->
       { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 } } $.
  $}

  $c FRNDGrph $.

  $( Extend class notation with friendship graphs. $)
  cfrng $a class FRNDGrph $.

  ${
    $d x y z v e $.
    df-cfrng $a |- FRNDGrph = { <. v , e >. | ( <. v , e >. e. USGrph ) /\ 
       ( A. x e. v A. y e. v E! z ( ( ( z , x ) e. e ) /\ 
       ( ( z , y ) e. e ) ) ) }  $. 
  $}

  $( The friendship theorem. If G is a friendship graph, then there is an element in G adjacent to all other elements in G. $)
  ${
    $d x y z $.
    frndshp $p |- ( <. v , e >. e. FRNDGrph ) -> ( E x ( ( x e. v ) /\ 
			    ( VDeg ` x = card ` ( v / x ) )  $= ? $.
  $}

$( (end of r0nks mathbox) $)

As you can see, the USGrph definition I made is based on Mario Carnerio's UMGrph
definition. In the actual theorem I'm proving, I'm also using his VDeg function.

I'm currently in need of a definition for path, and so I'm working on creating
one. The thing is, there's already a definition for eulerian path (df-eupa), and
part of that definition is the definition for path. So I could just copy and 
paste that part of the definition, but then we'd have repeated definitions. I
could change df-eupa to use my definition instead, but that's someone else's 
mathbox. 

What's the policy on tinkering with others mathboxes? Also, should one use 
pieces of other pieces math boxes to prove parts of the 100 list? I understand 
that they're sort of unofficial additions, so is it a bad idea to build off of 
them?

[David A. Wheeler]

On Sun, 15 Jan 2017 19:21:55 -0800 (PST), r00nk <samuelsh...@gmail.com> wrote:
> Hello again everyone, amateur mathematician here.
> In my spare time I've been working on proving one of the 100 theorems, the

> friendship theorem...

That's fantastic! With 2 more theorems Metamath will match Coq:
http://us.metamath.org/mm_100.html

> and I've gotten myself struck in a bit of a pickle. Namely,
> I'm defining a good chunk of graph theory and am trying to find a clean way to

> do so without trampling over similar definitions already found in set.mm...

Mathboxes are staging areas, and there are many reasons something could be staged.
Sometimes it simply provides an opportunity for others to comment on them, and/or
improve them.

I think you're doing exactly the right thing - post to the mailing list for discussion.

> What's the policy on tinkering with others mathboxes?

I can't speak to "policy", but I think it should not be done without coordinating
with the other person. People often have unpushed changes in their local repositories
that no one else knows about yet.

> Also, should one use
> pieces of other pieces math boxes to prove parts of the 100 list?
> I understand that they're sort of unofficial additions,
> so is it a bad idea to build off of them?

If person X needs material from person Y's mathbox, then that is
an *excellent* argument for moving the material into the main body.
Again, I think you should coordinate with the other person -
maybe they're making changes as well.

Since Mario definitely reads this mailing list, I think you've done that :-).

I look forward to the proof!

--- David A. Wheeler

[Mario Carneiro]

On Sun, Jan 15, 2017 at 10:21 PM, r00nk <samuelsh...@gmail.com> wrote:

As you can see, the USGrph definition I made is based on Mario Carnerio's UMGrph
definition. In the actual theorem I'm proving, I'm also using his VDeg function.

I'm currently in need of a definition for path, and so I'm working on creating
one. The thing is, there's already a definition for eulerian path (df-eupa), and
part of that definition is the definition for path. So I could just copy and 
paste that part of the definition, but then we'd have repeated definitions. I
could change df-eupa to use my definition instead, but that's someone else's 
mathbox.

This is fine. The definition of a path will follow the theorems about df-eupa for the most part, so it won't be hard to prove; later I can redefine df-eupa to refer to your more general path definition to avoid duplication.

 

What's the policy on tinkering with others mathboxes? Also, should one use 
pieces of other pieces math boxes to prove parts of the 100 list? I understand 
that they're sort of unofficial additions, so is it a bad idea to build off of 
them?

My only concern with df-umgra is that it doesn't use the structure framework used everywhere else. However it's perfectly functional right now so I think it should be okay to import to the main body, with the caveat that it may change in the future to extensible structures.

The general policy on mathbox use is that it is not permitted to use one mathbox from another, but this is actually a constraint for maintainers, not users, which are free to use anything for their proofs. It simply means that if one mathbox wants to reference another, the referred material needs to be moved to main, and this is in fact one of the major forces that gets things out of a mathbox. As it applies to your specific case, this means that konigsberg and associated theorems needs to be moved to main soon, and then there will be no problems with referencing it.

Mario

[Alexander van der Vekens]

Hi r00nk (Samuel?),
after I started to prove the friendship theorem some weeks ago, I detected your post, and therefore I want to synchronize our work. For this, I created the topic "Friendship Theorem" (https://groups.google.com/d/topic/metamath/j3EjD6ibhvo/discussion).

My main question is: Did you proceed with your efforts to prove the friendship theorem?

If yes, did you obtain any results yet, and is your approach expedient?

I plan to follow a different approach (see topic "Friendship Theorem"). It would be great if you can contribute to the discussion in my topic.

Regards,
Alexander