§ Lean4 Dev Meeting

• Mathport uses matli4 to move tactics.
• Mathlib4 has syntax definitions ofr every single tactic that exists in mathlib.
• These only exist as syntax so far. We need to port this.
• The goal for this week is to have as many as possible knocked off.

§ Macro

• A tactic that expands to another tactic.
• Example: _ tactic. This expands into ({}), which shows you the current state.
• macro_rules need a piece of Syntax, and it expands into another tactic.

-- | do the iff.rfl as well.
macro_rules | `(tactic| rfl => `(tactic| exact Iff.rfl)

• Closed syntax categories: syntax rcasesPatLo := ....
• Open syntax categories: syntax X.

§ How to collate info?

• Use macro to define syntax + macro
• Use elab to define syntax + elaborator together.
• Add command to list all places where something was extended.
• Add information into docstrings.
• match_target.

§ Mapsto arrow

• (x: α) \mapsto e: maybe annoying to parse.
• \lambda (x: \alpha) \mapsto e: easy to parse, but mathematicians don't know what lambda is.

§ ext tactic

• implemented as a macro tactic, which uses an elab tactic.

§ colGt

• syntax "ext"
• Lean4 is whitespace sensitive, like python. colGt says that we can have the following syntax on a column that is greater than the current line.

ext
  x -- parsed as part of `x`.
  y -- parsed as part of `y`.
z -- is not parsed as part of `x y`.

• If in parens, we don't need colGt, because we want to allow something like:

ext (x
 y) -- should parse.

§ ppSpace

• Used when pretty printing a tactic.

§ Scoped syntax

• scoped syntax "ext_or_skip: .. .
• This declares a syntax that is valid only for the current section/namespace.
• Trailing percent ext_proof% is an indicator that it is a term macro / term elaboration.
• Protected: identifier cannot appear without prefixing namespaces.

§ Trivia

• {..} pattern matches on a struct.

§ Tactic development: Trace

• Create a new file Mathlib/Tactic/Trace.lean
• Move the syntax line from ./Mathlib/Mathport/Syntax.lean into Mathib/Tactic/Trace.lean.
• On adding a file, add it to Mathlib.lean. So we add import Mathlib.Tactic.Trace
• We also want to re-import the syntax into Mathlib/Mathport/Syntax.lean.
• We have now moved trace into its own file and hooked into the build system and extension.
• The first thing to do is to find out what the tactic even does.
• Go to trace at the mathlib docs.

-- Tactic.lean
import Lean
open Lean Meta Elab

syntax (name := trace) "trace " term : tactic

elab "foo" : tactic => do
  -- `TacticM Unit` expected
  logInfo "hi"

open Lean Meta Elab Tactic ~=
open Lean
open Lean.Meta
open Lean.Elab
open Lean.Elab.Tactic

• TacticM is a MonadRef, which is aware of source spans to report the errors. so we can write:

elab "foo" : tactic => do
  logInfo "hi"

• We can use withRef to control the current source span where errors are reported.

elab tk:"foo" val:term : tactic => do
  withRef tk (logInfo val)

• We want to evaluate the val:term, because otherwise, it literally prints the syntax tree for things like (2 + (by trivial)).
• Use elabTerm to elaborate the syntax into a term.
• set_option trace.Elab.definition true in ... which printso ut the declarations that are being sent to the kernel.
• elab is syntax + elab_rules together, just like macro is syntax + macro_rules together.
• Create a test file test/trace.lean. Import the tactic, and write some examples.
• Recompile, and check that the test works.
• How do we check that our port works?

§ Reducible

To clarify, @ [reducible ] marks the definition as reducible for typeclass
inference specifically. By default typeclass inference avoids reducing because
it would make the search very expensive.