Re: [mizar] Strong Mizar wish: linking to consider

[Markus Wenzel <wenzelm@informatik.tu-muenchen.de>]

On Sat, 9 Mar 2002, Freek Wiedijk wrote:

> Piotr Rudnicki wrote:
>
> >I may be biased, I do not like "then" at all and am quite
> >happy with using labels.

Interestingly, when I've started looking into the issue of human-readable
proofs severeal years ago the "then" element of Mizar was just another
funny detail to consider in the design of the Isar language.  Only much
later I realized that implicit reference to the most recent fact is a
fundamental principle in structured proof arrangement.

The "then" primitive of Isar (which is slightly different from Mizar)
essentially marks a turning point in the text, where the result of the
antecedent text is picked up to contribute to the succedent goal (to be
used eventually in its proof).  So a structured Isar proof body may be
understood as a sequence of chunks like this:

  <fact> then <goal>
    <proof>
  <fact> then <goal>
    <proof>
  <fact> then <goal>
    <proof>

In practice, significant parts of formal reasoning proceeds in such a
linear fashion.  Thus we are able to avoid the ``spaghetti code effect''
of excessive use of auxiliary pointers into the preceding text. In the
rare cases where non-linear references are required, explicit labels are
perfectly OK.

Isar even has further variants of "then", namely "moreover" /
"ultimately", which admit to structured chunks of proof texts at a larger
scale, diminishing the demand for labeled facts even more.


> Freek Wiedijk wrote:
>
> I thought of one more reason for this.  Because then "let
> ... such that ..." would be more equivalent to "let ...;
> assume ..." and "assume that ... and ..." would be more
> equivalent to "assume ...; assume ...".

Very good.  A key issue of clean language design is to look for
equivalences of language elements (and idioms), and try to derive more
complex concepts from a small number of primitives.  Thus one achieves
minimality and orthogonality of the design.

The derived "obtain" element of Isar is a good example here.  Being
defined in terms of existing language elements, there was never a question
how it would cooperate with the "then" primitive in the first place -- the
canonical behaviour of the underlying concepts are inherited directly.


	Markus

--------------------------------------------------------------------
Institut für Informatik, TU München, http://www4.in.tum.de/~wenzelm/
--- <>< ------------------------------------------------------------