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 <[email protected]>:
> 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
>
> --
> 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/E1jwGmg-0005Tc-Oi%40rmmprod06.runbox
> .
>
--
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/CAF7V2P8-tFgRKqJAspdFvxcvmW6B8iiM68%2B%3DZ8zx1VvBQWqJPA%40mail.gmail.com.
