Idiomatic Mizar

The idiomatic way to define a new gadget, well, suppose we had our definition found in a textbook schematically as:

We would define a gadget in three steps:

1. Define a structure GadgetStr consisting of the stuff and structure
2. Define a attr Gadget-like which encodes the properties
3. Define a mode Gadget is Gadget-like GadgetStr

When defining a new attribute (say, hairy) for a Gadget, we schematically define it as:

definition
  :: Any preliminary loci declarations here...
  let IT be Gadget;
  attr IT is hairy means
  :Def:
  :: ...
end;

This is a nod towards using it in defining functors and modes.

Principle 1: consistency. Honestly, the best policy is to be consistent with what you're working with.

For example, I want to define the semi-direct product of two groups. I look at the definition of the product of two groups in GROUP_7, and define it similarly semidirect_product (G1, G2, phi) (or something similar).

When defining the Hall \(\pi\) subgroups, I look at how the Sylow \(p\) Subgroups were defined in GROUP_10 and adopt analogous naming conventions like the_hall_pi-subgroups_of_primes (Pi, G).

Principle 2: readability. If there is nothing analogous existing in the Mizar Math library, then try to be faithful to the notation in the literature provided it is well understood. For example, the classical matrix groups \(GL(n,\mathbb{F})\) or \(SL(n,\mathbb{F})\) and so on. We could encode these as GL(n, F), SL(n, F), etc.

Care must be taken with this principle: finite group theory has a lot of whacky notation which mystifies the entire subject. It would be better to define the signalizer(A) instead of |/|(A) or some other approximation of И(A).

Use xboole_0 definition 10 to prove X = Y by proving X c= Y and Y c= X. This is the idiomatic way to prove the claim. Avoid TARSKI:2 if possible.

There are times when it is unclear whether we should define a new mode or a new attribute, and the rule of thumb is to prefer defining attributes and registering them (as opposed to using redefinitions).

There's an entire article justifying this practice:

• Artur Kornilowicz,
  "Registrations vs Redefinitions in Mizar".
  Eprint

The rule presented in the paper:

If the result type of a functor and the mother type of a mode to which the original type of the functor and the mode is redefined is an expandable type, then such redefinitions are replaceable by a functorial registration in the case of functors and by a conditional registration in the case of modes.

To be explicit, there are two cases:

1. When a redefine func can be replaced by a registration: if we redefine a functor to have the type an expandable mode, then we can replace the redefinition with a functor registration (provided the original definition of the functor has the same "mother type" [base type] as the desired type of the redefinition)
   • In this case, a functorial registration suffices.
2. When a redefine mode can be replaced by a registration: when the original definition of the mode has the same "mother mode" [base type] as the new redefinition's type
   • In this case, a conditional registration suffices.

Programmers have the idiom to make code private by default, and for good reason.

But in Mizar, it's better to make everything public by default.

• Examples should be public theorems, not private lemmas.

The only exceptions I have found:

• If I have a confusingly long proof of a theorem A implies B & C, I may have a private lemma proving half (A implies C, for example). This is just to clarify the proof for myself.