How to produce a `rcasesPat.ignore`

Stream: lean4

[Alex Meiburg]

Hi, I'm trying to write a tactic and still a bit of shaky on the metaprogramming. I want to produce an _ as an instance of TSyntax `Lean.Parser.Tactic.rcasesPat.ignore, but I can't figure out how to ... do that.

Quoting `(_) doesn't work because it gives me a `Lean.Parser.Term.hole (Lean.Syntax.atom info "_")

I tried (Lean.TSyntax.mk <| Lean.mkAtom "_") but that doesn't work, it turns into Tactic.rcasesPatLo (Tactic.rcasesPatMed ["_"]) [] and that doesn't work but I can't exactly understand why.

[Aaron Liu]

#check `(Lean.Parser.Tactic.rcasesPat.ignore| _)

[Alex Meiburg]

Okay, that taught me something. Hmm, but that is a ?m.130157 (Lean.TSyntax `Lean.Parser.Tactic.rcasesPat.ignore), and I don't understand why it isn't a Lean.TSyntax `Lean.Parser.Tactic.rcasesPat.ignore itself (or how to turn it into that).

I'm trying to follow the metaprogramming book and it's not clarifying much for me unfortunately

[Aaron Liu]

Alex Meiburg said:

Okay, that taught me something. Hmm, but that is a ?m.130157 (Lean.TSyntax `Lean.Parser.Tactic.rcasesPat.ignore), and I don't understand why it isn't a Lean.TSyntax `Lean.Parser.Tactic.rcasesPat.ignore itself (or how to turn it into that).

I'm trying to follow the metaprogramming book and it's not clarifying much for me unfortunately

That means it's in a monad (an arbitrary monad supporting enough hygiene) and you need to do ← `(Lean.Parser.Tactic.rcasesPat.ignore| _) to get it out (or you can use docs#Lean.Unhygienic.run)

[Alex Meiburg]

Ah, nice, ok that works. (I actually ended up using ← `(rcasesPat| _).) Do you understand why that is in a monad, but other syntactic objects aren't? Like If I do `this I just a Lean.Name without issue.

Also, how did you know that it was a monad - nothing in the type ?m.130157 (Lean.TSyntax `Lean.Parser.Tactic.rcasesPat.ignore) suggested monad to me, the mvar is just any Type → Type.

[Aaron Liu]

it's because you need a Bind ?m.130157 instance too

[Aaron Liu]

so monad

[Aaron Liu]

Alex Meiburg said:

Ah, nice, ok that works. (I actually ended up using ← `(rcasesPat| _).) Do you understand why that is in a monad, but other syntactic objects aren't? Like If I do `this I just a Lean.Name without issue.

`this isn't a syntax object, it's just a Lean.Name. All the syntax quotations come wrapped in a monad.

[Alex Meiburg]

More generally, is there documentation of how to use the ` command somewhere? I get that it's quotation, but this doc doesn't really explain anything.

[Alex Meiburg]

Aaron Liu said:

`` `this `` isn't a syntax object, it's just a `Lean.Name`. All the syntax quotations come wrapped in a monad.

Oh, wait what? That doc I just linked literally calls it a "a Syntax quotation"

[Aaron Liu]

` isn't a single command, there are multiple macros which all use backticks

[Alex Meiburg]

Ahhhh that's even worse! Is there no good documentation on this? How did you learn it?

[Aaron Liu]

Alex Meiburg said:

Oh, wait what? That doc I just linked literally calls it a "a Syntax quotation"

That's `(category| syntax) , which is a distinct thing

[Aaron Liu]

it produces a TSyntax `category

[Aaron Liu]

as opposed to a Name

[Aaron Liu]

Alex Meiburg said:

Ahhhh that's even worse! Is there no good documentation on this? How did you learn it?

I wrote a tactic

[Alex Meiburg]

Sure, that's what I'm trying to do too. But, when you ran into issues, did you find documentation that helped? Just soliciting help on Zulip? Did you find that trawling existing examples in Mathlib was sufficient?

[Aaron Liu]

After reading Metaprogramming in Lean, I decided to write a tactic, a dependent rewriting tactic which 𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 picked up and put in #26835

[Aaron Liu]

when I needed help I would click "go to source" on some of the metaprogramming definitions I use (like docs#Lean.Meta.matchEq?) and read there

[Aaron Liu]

I would also use loogle to find stuff

[Aaron Liu]

I used docs#Lean.Meta.kabstract as a model and replaced its guts with the functionality I wanted

[Alex Meiburg]

Okay. I guess I can't tell if I'm a bit slow, or if the docs are weak on this. :/

I'm certainly feeling slow.

I see now that some of the quotation is explained here: https://lean-lang.org/doc/reference/latest/Notations-and-Macros/Macros/#quotation

That doesn't make any reference to the fact, though, that there are multiple different ` operations.

[Alex Meiburg]

I can't be the only person who thinks that `(foo) and `foo meaning different things is very surprising!

[Aaron Liu]

I can't find anything about quoted names in the reference

[Aaron Liu]

I guess I'll just copy the docstring

[Aaron Liu]

Hierarchical names consist of a sequence of components, each of
which is either a string or numeric, that are written separated by dots (.).

Hierarchical names are used to name declarations and for creating
unique identifiers for free variables and metavariables.

You can create hierarchical names using a backtick:

`Lean.Meta.whnf

It is short for .str (.str (.str .anonymous "Lean") "Meta") "whnf".

You can use double backticks to request Lean to statically check whether the name
corresponds to a Lean declaration in scope.

``Lean.Meta.whnf

If the name is not in scope, Lean will report an error.

There are two ways to convert a String to a Name:

1. Name.mkSimple creates a name with a single string component.

2. String.toName first splits the string into its dot-separated
   components, and then creates a hierarchical name.

[Aaron Liu]

And here's a spot in metaprogramming in lean that tells you what the backtick means

[Kyle Miller]

Alex Meiburg said:

Do you understand why that is in a monad

Syntax quotations are monadic for hygiene reasons; they capture the current "macro scope" and annotate all the identifiers with it. It's explained in https://arxiv.org/abs/2001.10490v7

[Kyle Miller]

Since we're talking about names,
Alex Meiburg said:

but other syntactic objects aren't?

note that Name isn't a syntactic object. You need to use operations such as mkIdent to turn a Name into an Ident.

[Kyle Miller]

Re backticks having two meanings: at least they're both quotations of some sort. There's also some consistency in that double backtick means "quotation with checking".

[Kyle Miller]

Stepping back, is creating some syntax to feed rcases what you're sure you want to do?

docs#Lean.Elab.Tactic.RCases.rcases is the main interface to the "meta-level" tactic, and it takes a structured RCasesPatt

[Alex Meiburg]

This is the tactic I ended up with, which I'm happy enough with for now. (I'm using it my quantumInfo repo, I don't know how high the bar would be to get it in mathlib, or if that's remotely desirable.)

/--
Proves goals equating small matrices by expanding out products and simpliying standard Real arithmetic.
-/
syntax (name := matrix_expand) "matrix_expand"
  (" [" ((simpStar <|> simpErase <|> simpLemma),*,?) "]")?
  (" with " rcasesPat+)? : tactic

macro_rules
  | `(tactic| matrix_expand $[[$rules,*]]? $[with $withArg*]?) => do
    let id1 := (withArg.getD ⟨[]⟩).getD 0 (← `(rcasesPat| _))
    let id2 := (withArg.getD ⟨[]⟩).getD 1 (← `(rcasesPat| _))
    let rules' := rules.getD ⟨#[]⟩
    `(tactic| (
      ext i j
      repeat rcases (i : Prod _ _) with ⟨i, $id1⟩
      repeat rcases (j : Prod _ _) with ⟨j, $id2⟩
      fin_cases i
      <;> fin_cases j
      <;> simp [Matrix.conjTranspose_fin_two, Complex.ext_iff,
        Matrix.mul_apply, Fintype.sum_prod_type, Matrix.one_apply,
        $rules',* ]
      <;> try field_simp
      <;> try ring_nf))

I was synthesizing the rcases syntax because I wanted a default value for what to pass to an rcases in the macro.

[Alex Meiburg]

If I was writing this as something other than just expanding a macro into other tactics, I would use the actual rcases frontend, but for a script like this it seemed like the reasonable thing to do? I hope!

[Kyle Miller]

If it's easy enough to make correct syntax, then it seems fine to me!