Any comments on my draft presentation Schwabhauser4.6.pptx?

[David A. Wheeler]

I'd love to hear comments on my draft presentation
"Proving Geometric Proof Schwabhäuser 4.6 in Metamath Proof Explorer":

https://dwheeler.com/misc/Schwabhauser4.6.pptx

This presentation focuses on Schwabhäuser theorem (“Satz”) 4.6
as formalized by Thierry Arnoux in MPE theorem tgbtwnxfr ; it shows how
to recreate this proof using mmj2. My thanks to Thierry for his hard work!

I'd be especially interested in tips that would reduce what
you'd need to know or guess to create this proof beyond what's already
stated in Schwabhäuser.

--- David A. Wheeler

[Thierry Arnoux]

Hi David,

This looks very good!

It's nice to have a step-by-step explanation of how the proof is built. I think you got it right.

A few remarks:

Maybe I would rephrase the text in slide 12: It's true you need to prove that x exists, but actually at the point in time you use the theorem you already have ` E. x e. A ` as a hypothesis, so I would rather write Set variable x is a point you know exists, and you need to use in the construction.
You could see it as an intermediate construction point. It shall not appear in the result ` ch `.

Also maybe slide 4, ` .~ ` shall be named a "relation" rather than an "operator" (` I ` and ` .- ` are indeed operators, they return classes).

Slide 4, you have too many parentheses in ( ph -> ( B e. P ) ), you don't need them around B e. P!

Slide 7, To convert “XX=YY” into “XX e. (AA I BB)”, I'm not sure why you double the letters here. You could maybe write "to transfer the membership between X and Y which are known to be equal"?

I think slide 7 gives a very good overview of the proof, the rest is mainly glue around it :-) It's very nice that you went through all the steps, this could serve as a good introduction.

BR,
_
Thierry

[Alexander van der Vekens]

Hi David,

great work. I really like this presentation, because it is very precise, specific and complete, and it gives an illustrative impression of Metamath and mmj2.

I have only one remark:

* Slides 1 and 2: You do not "prove a geometric proof" - you either "formalize a geometric proof" or "formally prove a specific geometry theorem".

The rest seems to be perfect (I have to admit, however, that I did not go through slides 13-30 in detail...).

Regards,

Alexander

[David A. Wheeler]

On Wed, 15 Jul 2020 13:48:22 -0700 (PDT), "'Alexander van der Vekens' via Metamath" <meta...@googlegroups.com> wrote:
> Hi David,
> great work. I really like this presentation, because it is very precise,
> specific and complete, and it gives an illustrative impression of Metamath
> and mmj2.

Thanks! I intend to eventually create a per-slide voiceover & turn this into a Youtube video.

> I have only one remark:
> * Slides 1 and 2: You do not "prove a geometric proof" - you either
> "formalize a geometric proof" or "formally prove a specific geometry
> theorem".

You're absolutely right! Fixed.

--- David A. Wheeler

[David A. Wheeler]

My thanks to everyone for their constructive criticism on my draft
prresentation on Schwabhauser 4.6! I've fixed everything I know
about, and added another slide to briefly explain the key theorems/axiom
the proof depends on.

The new draft video is here:
https://youtu.be/sNXgTh-8OhQ

Any last-minute comments before I post it "officially"?

--- David A. Wheeler

[Marnix Klooster]

Hi David,

Thanks for this!

First, the middle main bullet on slide 7 should use congruence instead of  = , I think?

Second, I had a bit of a hard time following what was being used exactly.

Specifically, I had to find a copy of the book to find out that "IFS" stands for "inner five segments [configuration]", i.e., a triangle  acd  with  b  on  ac , together with a congruent  a'c'd'  with  b' .

But working through the proof, it seems that all that is _really_ being used, is that  abc ~ a'b'c'  implies  ab ~ a'b'  and  bc ~ b'c' (which directly follows from the definition of congruence).

So (1) using IFS here seems kind of heavy and indirect machinery; but given that the goal is to follow the book closely, (2) a definition would help (with picture? e.g. Abb. 11 from page 34, but without the dotted lines).

 

Thanks again!

-Marnix 

Op vr 17 jul. 2020 05:11 schreef David A. Wheeler <dwhe...@dwheeler.com>:

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1jwGmg-0005Tc-Oi%40rmmprod06.runbox.

[Marnix Klooster]

Hi all,

Not a comment on David's nice and helpful presentation, but to show (again) my "dream" of a more calculational proof format: I'm hoping to one day have an mmj2 equivalent, some intelligent editor, that allows me to write something like the proof below, and have a Metamath proof of this same statement auto-generated from it.

The idea is that this tool would automatically apply any relevant transitivity, commutativity, identity, hypothesis/scope manipulation, "windowing/Leibniz", and substitution rules.

Anyway, I just wrote this out by hand of course since I have no implementation yet, so this will have bugs. But it shows the concept: This proof contains all essential information for this proof.

To me this is a lot more readable than a 4-page MPE proof...

-Marnix

```

* |- ( ph  ->  <" A B C ">  .~  <" D E F "> )  $==>  $...

* [imagine all the other hypotheses here]

* |- ( ph  ->  $... )

     B  e.  ( A I C )

$==> "by 4.5 (tgcgrxfr)"

     E. e  e.  P  ( e  e.  ( D I F )  /\  <" A B C ">  .~  <" D e F "> )

<->  "by hypothesis"

     E. e  e.  P  ( e  e.  ( D I F )  /\  <" D E F ">  .~  <" D e F "> )

->    "by subproof"

     * |- ( e  e.  ( D I F ) -> $... )

     

          <" D E F ">  .~  <" D e F ">

     $==> "by (cgr3simp1) and (cgr3simp2)"

          ( D  .-  E )  =  ( D  .-  e )  &&. ( F  .-  E )  =  ( F  .-  e )

     $==> "by 4.2 (tgifscgr) using hypothesis"

          ( e  .-  E ) = ( e  .-  e ) )

     $==> "by A3 (axtgcgrid)"

          e = E

          

     E. e  e.  P  ( e  e.  ( D I F )  /\  e = E )

<->   "using 1-point rule"

     ( E e.  P  /\  E  e.  ( D I F ) )

<->  "by hypothesis"

     E  e.  ( D I F )

```

Op vr 17 jul. 2020 05:11 schreef David A. Wheeler <dwhe...@dwheeler.com>:

My thanks to everyone for their constructive criticism on my draft

[David A. Wheeler]

On Fri, 17 Jul 2020 16:20:24 +0200, Marnix Klooster <marnix....@gmail.com> wrote:
> Thanks for this!
>
> First, the middle main bullet on slide 7 should use congruence instead of
> = , I think?

Yes! Thanks for telling me. Fixed.

> Second, I had a bit of a hard time following what was being used exactly.
>
> Specifically, I had to find a copy of the book to find out that "IFS"
> stands for "inner five segments [configuration]", i.e., a triangle acd
> with b on ac , together with a congruent a'c'd' with b' .

Okay, I've added text that explains what IFS means earlier.

> But working through the proof, it seems that all that is _really_ being
> used, is that abc ~ a'b'c' implies ab ~ a'b' and bc ~ b'c' (which
> directly follows from the definition of congruence).

> So (1) using IFS here seems kind of heavy and indirect machinery; ...

Well, we also need to prove bd ~ b'd'. But that's not really the point (ha?).
The point was to try to follow the original proof "relatively closely",
to show how to use an informal proof to help create a formal proof.
We need to use something like IFS since that's what the book used.

> but given
> that the goal is to follow the book closely, (2) a definition would help
> (with picture? e.g. Abb. 11 from page 34, but without the dotted lines).

You read my mind! You must have seen the first draft video.
The second draft video adds a new slide 8 that includes a figure that
basically does that. (It's the "obvious" way to illustrate IFS.)
I'll add some tic marks so the new figure is easier to follow.

My goal was, in part, to show how to "translate" an informal proof
into Metamath. There are no doubts many ways to prove something :-).

--- David A. Wheeler

[David A. Wheeler]

Thank you *everyone* for your helpful comments on my draft video
showing how to (re)prove Schwabhauser 4.6!

Version #3 is now available for your amusement:
https://youtu.be/3R27Qx69jHc

I'm hoping that everything is fine & then I will officially release this version.
However, it's "unlisted" in case someone finds any (more) issues in it.
Please let me know of any issues soon!

--- David A. Wheeler