Proposal to add new attributes

[AdamSobieski]

Introduction

Hello. I would like to propose some attribute concepts for mathlib and to also broach a subtopic of drawing illustrations and animations with Lean.

Motivating Use Cases

As the motivating use cases include enhancing the Loogle search engine and the Lean VS Code extension, I am proposing these attribute concepts for mathlib.

Education

Enhancing the automated and adaptive generation of educational multimedia documents from formal proofs is a motivating use case for this proposal.

Documentation

Enhancing the automated generation of multimedia documentation from formal proofs is a motivating use case for this proposal.

Loogle Search Engine

Enhancing Loogle search engine capabilities is a motivating use case for this proposal.

Intellisense and Tooltips

Enhancing VS Code Intellisense and tooltip capabilities is a motivating use case for this proposal.

In theory, users could type a key, chord, or sequence to commence a text-entry mode where they could enter a natural-language title (see: @[title]) of sought content, possibly then making use of an on-screen menu (see: @[title] and @[description]), perhaps then pressing the Tab key to select a recommendation, to retrieve a Lean object identifier which would be entered into the Lean content.

@[title], @[description], and @[usage] attributes could, perhaps alongside other attributes to be determined, be used to provide that content to display when users hover over a thing in VS Code.

Attribute Concepts

Some preliminary attribute concepts are offered for discussion.

Here is a sketch showing some of these interrelated attributes in use together:

@[originator (value := "Gottfried Wilhelm Leibniz", date := "...")]
@[transcriber (value := "Alice Smith", date := "...")]
@[transcriber (value := "Robert Jones", date := "...")]
@[title (lang := "en", value: = "the natural language name of the theorem")]
@[title (lang := "fr", value := "le nom en langage naturel du théorème")]
@[title (lang := "de", value := "der natürlichsprachliche Name des Theorems")]
@[title (lang := "es", value := "el nombre en lenguaje natural del teorema")]
@[description (lang := "en", value := "...")]
@[description (lang := "fr", value := "...")]
@[description (lang := "de", value := "...")]
@[description (lang := "es", value := "...")]
theorem ...

@[originator]

@[originator] attributes would allow indicating one or more historical or contemporary originators.

@[transcriber]

@[transcriber] attributes would allow indicating one or more transcribers who formalized the content into Lean.

@[title]

@[title] attributes would allow attaching one or more natural-language titles to a declaration.

@[description]

@[description] attributes would allow attaching one or more natural-language descriptions to a declaration.

@[usage]

@[usage] attributes would allow attaching one or more example usages to a declaration.

If examples could be named, could be provided with optional identifiers, then a @[usage] attribute on a declaration could refer to certain examples by their identifiers. Examples showcasing usage could be shown in a tooltip when that thing was hovered over. Multiple examples showcasing usage could be presented via a clickable carousel, or the examples' source code locations could be navigated to via hyperlink.

Alternatively, attributes could be placed on unnamed examples to indicate that they are intended to showcase another named thing's usage.

@[seealso]

@[seealso] attributes would allow attaching one or more hyperlinks to related content to a declaration.

@[illustration]

@[illustration] attributes would allow referencing existing illustrations or animations, e.g., by href, and providing functions with which to procedurally generate illustrations and animations.

Lean and Drawing

Towards enabling the procedural generation of illustrations and animations, drawing capabilities could be provided for Lean in either mathlib or another project.

With respect to producing illustrations for LaTeX documents, software options include [1]: PGF/TikZ, PSTricks, and the default graphics packages. Other graphics packages included in LaTeX include: pgfplots, Xy-pic, ePiX, MetaPost, MetaFun, and Mfpic. Independent GUI wrappers and software tools which create images suitable for inclusion in LaTeX documents include: LaTeXPiX, TPX, Xfig, Asymptote, Inkscape, Ipe, Knitr/Sweave, KtikZ,QtikZ, and GeoCobra.

A comparable library is OCaml-Canvas. Here is an excerpt from a source-code example:

let c = Canvas.createOnscreen ~title:"Hello world"
            ~pos:(300, 200) ~size:(300, 200) () in

  Canvas.setFillColor c Color.orange;
  Canvas.fillRect c ~pos:(0.0, 0.0) ~size:(300.0, 200.0);

  Canvas.setStrokeColor c Color.cyan;
  Canvas.setLineWidth c 10.0;
  Canvas.clearPath c;
  Canvas.moveTo c (5.0, 5.0);
  Canvas.lineTo c (295.0, 5.0);
  Canvas.lineTo c (295.0, 195.0);
  Canvas.lineTo c (5.0, 195.0);
  Canvas.closePath c;
  Canvas.stroke c;

  Canvas.setFont c "Liberation Sans" ~size:36.0
    ~slant:Font.Roman ~weight:Font.bold;

  Canvas.setFillColor c (Color.of_rgb 0 64 255);
  Canvas.setLineWidth c 1.0;
  Canvas.save c;
  Canvas.translate c (150.0, 100.0);
  Canvas.rotate c (-. Const.pi_8);
  Canvas.fillText c "Hello world !" (-130.0, 20.0);
  Canvas.restore c;

  Canvas.show c;

In addition to a "canvas" object, a "theme" or "style" object could be provided as an additional parameter for drawing-related functions. Such a parameter could simply be a dictionary of property names and values. Attributes could both override and provide default values for such dictionaries of property names and values.

A simple, hopefully clarifying, data structure for looking up properties' values with such overriding and default-value dictionaries is sketched below in C#:

public class NestableDictionary<K, V> : IReadOnlyDictionary<K, V>
{
   private IReadOnlyDictionary<K, V> first;  // provided overrides
   private IReadOnlyDictionary<K, V> middle; // style or theme content
   provide IReadOnlyDictionary<K, V> last;   // provided default values

   public V this[K key]
   {
      get
      {
         try
         {
            return first[key];
         }
         catch (KeyNotFoundException)
         {
            try
            {
               return middle[key];
            }
            catch (KeyNotFoundException)
            {
               return last[key];
            }
         }
      }
   }

   public bool TryGetValue(K key, out V value)
   {
       if (first.TryGetValue(key, out value)) return true;
       if (middle.TryGetValue(key, out value)) return true;
       if (last.TryGetValue(key, out value)) return true;
       value = default(V);
       return false;
   }

   ...
}

See Also

leanprover/lean4#4905

Conclusion

Thank you for any comments, questions, or feedback.