Page301.mmp fails on mmj2 version 2.5.3 - any ideas?

[David A. Wheeler]

I have a strange problem with mmj2's file "PA301.mmp" - anyone have
any idea what's up?

Background:
I'm doing a dry run of the mmj2 "PATutorial" files. However, when I try to
unify (control-U) file PA301.mmp, I get the following error instead of a unification:

E-PA-0348 Theorem sylClone Step 3: Invalid Ref = 200 on derivation proof step. Does not specify a valid statement in the Metamath file that was loaded. You can leave Ref blank to allow Unify to figure it out for you. Proof Text input reader last position: Source Id: Proof Text Line: 21 Column: 3

The error is on this line:
3:200 |- ( ph -> ( ps -> ch ) )
which refers back to this hypothesis:
h200 |- ( ps -> ch )

That should work, but it doesn't. Changing "3:200" to "3:h200" doesn't work either
(though that shouldn't be needed).

Anyone else seen this? Full file contents below.

--- David A. Wheeler

=======================================

$( <MM> <PROOF_ASST> THEOREM=sylClone LOC_AFTER=a2i
* Page301.mmp
Have a careful look at the "Step:Hyp:Ref" field at the start of each
proof step below. Notice especially how:
- Hypothesis Step Numbers are prefixed with 'h'
- Step Numbers are not in numeric order(!), but are unique
- Ref Labels are blank
- Trailing ":"s are optional, for your convenience
- Blanks are not permitted inside a "Step:Hyp:Ref" (making things
easier for the programmers)
- the final step "number" is "qed" (also for the convenience of
the programmer...)

OK, now press Ctrl-U and see what happens to the Step:Hyp:Ref fields.
(Use Edit/Undo -- twice -- to retry and look again.)

h1000 |- ( ph -> ps )
h200 |- ( ps -> ch )
h30 |- ( ch -> th )
3:200 |- ( ph -> ( ps -> ch ) )
4:3 |- ( ( ph -> ps ) -> ( ph -> ch ) )
qed:1000,4 |- ( ph -> ch )

*OK, proceed to the next Tutorial page (Page302.mmp)!
$)

[Mario Carneiro]

There was a change to the step format a while back to make it more permissive to syntax errors, but it changed the meaning of single colon statements from step:hyps to step:thm. So that means that you have to write 4:3: instead of 4:3 if you want "3" to be interpreted as a hypothesis and not a statement. Like so:

h1000              |- ( ph -> ps )
h200               |- ( ps -> ch )
h30                |- ( ch -> th )
3:200:              |- ( ph -> ( ps -> ch ) )
4:3:                |- ( ( ph -> ps ) -> ( ph -> ch ) )

qed:1000,4:         |- ( ph -> ch )

The hypothesis steps don't need the colons because they have no hypotheses (so h1000 will automatically be turned into h1000:: ).

Mario

--
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/E1ikeuB-0007Zn-I1%40rmmprod07.runbox.

[David A. Wheeler]

On December 26, 2019 10:26:28 PM EST, Mario Carneiro <di....@gmail.com> wrote:
>There was a change to the step format a while back to make it more
>permissive to syntax errors, but it changed the meaning of single colon
>statements from step:hyps to step:thm. So that means that you have to
>write
>4:3: instead of 4:3 if you want "3" to be interpreted as a hypothesis

Thanks, I had not noticed the change. We probably ought to change the tutorial files to match.

--- David A.Wheeler