Week 7 Lab: A definition that fails

Add a definition to a copy of set.mm, run mmj2's definition check, watch it reject one, and fix it. The corrected definition starts your definition exercise.

21 April 2027

Before the lab#

Have mmj2 loading set.mm as in the earlier labs, and a text editor open on a copy of set.mm that you are willing to break. mmj2 “does not update Metamath .mm databases”, so every definition today goes into the file by hand.

Read Appendix 4 of the Proof Explorer home page. Bring a draft of the definition you intend to submit for the definition exercise: a $a statement with a df- label and one line saying what it abbreviates.

In the lab#

First, a clean run. Add RunMacro,definitionCheck,ax-*,df-bi,df-clab,df-cleq,df-clel to your RunParms. The batch documentation says RunMacro runs a macro from the macro/ directory, that macros are on by default, and that definitionCheck with these arguments replaces the older SetMMDefinitionsCheckWithExclusions RunParm. Run it on the unchanged copy and keep the output: that is what a clean report looks like.

Second, a broken one. Change df-2 to the appendix’s self-referential 2 = ( 1 + 2 ), run the check again, and note what changed in the report. Teodor then hands round two definitions that are wrong in less obvious ways; run the check on each and write one line on what it objects to.

Third, yours. Restore df-2, add your own definition, and run the check. Fix it until the report is clean, then prove one small theorem from it in mmj2, in the usual way: a worksheet that unfolds the definition once.

Afterwards#

The passing definition is the good one for your definition exercise, and the version that failed is the bad one; keep both, and keep the reports, because what the check found is what the write-up explains.