Useful term elaborators

Stream: mathlib4

[Floris van Doorn]

We have some nice custom term elaborators, but I rarely use them, and don't know all of them. What are some term elaborators you use in practice, or think are underused? Note: you can write #help term to see all of them, but that list includes all notation, I believe.

[Floris van Doorn]

• I personally use exact?%, for the term-mode equivalent of by exact?
• I might start using congr(...) occasionally, to generate congruence lemmas for terms
• I believe there was a term elaborator that allows you to have metavariables in let/have tactics, but I don't remember the syntax and it's hard to search for it.

[Adam Topaz]

prod_assoc% is one that I wrote and probably has never been used. reassoc_of% is used in several category theory proofs.

[Eric Wieser]

eval% is another one, which is handy for things like have : 5! = eval% 5! := by rfl, though a norm_num version would be better

[Floris van Doorn]

@Kyle Miller I expect you wrote more term elaborators than the ones mentioned so far?

[Alex J. Best]

There is also the mod_cast term elab which basically runs norm_cast on the term before inserting, so one can do e.g simp [mod_cast foo] or similar

[Eric Wieser]

Should we add a % to its name?

[Floris van Doorn]

Also, that description doesn't seem to capture its actual behavior:

import Mathlib

example (n : Nat) : (mod_cast ((n : ℤ) : ℚ)) = 3 := by
  -- cast ⋯ ↑↑n = 3
  norm_cast
  -- cast ⋯ ↑n = 3

It also adds the cast in the statement, which presumably makes it useless in simp/rw. Searching for it in mathlib it seems to be (almost?) exclusively used in term mode.

[Alex J. Best]

My description is likely wrong, I haven't used it so much myself.

[Alex J. Best]

@Kim Morrison added this iirc?

[Kim Morrison]

I remember upstreaming it, but not writing it!

[Kyle Miller]

Mathlib term elaborators that I found (including ones already mentioned):

• proxy_equiv% t creates an equivalence _ ≃ t where _ stands for some sum of products of basic types.
• derive_fintype% t derives a Fintype t instance using proxy_equiv% t
• eval% t evaluates t and then reflects it back to an expression
• prod_assoc% uses the expected type (such as (α × β) × (γ × δ) ≃ α × (β × γ) × δ) and derives the equivalence
• congr(t) elaborates to a proof of an Eq, HEq, or Iff, where t is a pattern that can be full of $h "holes", where h is an Eq, HEq, or Iff, unifying and generalizing the congr/congrFun/congrArg functions
• Type* and Sort* add a fresh universe level variable u and elaborate to Type u and Sort u
• elementwise_of% w takes a lemma w of an equality of morphisms of concrete categories and creates an elementwise version
• reassoc_of% w takes a lemmas w of an equality of morphisms and creates a "reassoc" lemma
• clean% t elaborates t and then eliminates identity functions (type hints) from t
• delta% t elaborates t and head-delta-reduces it
• beta% t elaborates t and then head-beta-reduces it
• fbinop% is used to elaborate expressions involving products of container-like types

[Kyle Miller]

From core:

• ext_type% bool t and ext_iff_type% bool t create extensionality lemmas for t, where the bool (if true) flattens the structure
• eval_prec prec evaluates a precedence expression as a Nat
• eval_prec prio evaluates a priority expression as a Nat
• by_elab doSeq and by_elab fun expectedType? => do doSeq let you have an inline term elaborator
• with_annotate_term stx e annotates stx with terminfo for e (for hovers)
• mod_cast e runs the norm_cast machinery on e
• include_str "path" / "to" / "file" elaborates to a string literal containing the contents of the file
• show_term e elaborates e and shows the elaborated term
• by? ... is show_term by ...
• exact?% is by exact?
• json% jsonExpr lets you embed a JSON expression to get a docs#Lean.Json value
• `(...) syntax quotations
• let_fun x := v; b for "elaborate v and then elaborate b with x as a cdecl (value-free)". (have is implemented using this)
• let_delayed x := v; b elaborates as let x := v; b but elaborates b before elaborating v
• let_tmp x := v; b elaborates like let x := v; b but eliminates the let if x is unused in b
• haveI/letI are like have/let versions of let_tmp but that substitute the value of x into b
• type_of% e elaborates to the type of e
• ensure_type_of% ref msg e elaborates ref and e and ensures that e has the same type as ref has
• no_implicit_lambda% e elaborates e with the implicit lambda feature turned off
• clear% id; e elaborates e with id cleared from the local context
• let_mvar% ?m := v; e assigns the mvar ?m to v and elaborates e
• wait_if_type_mvar% ?m; e, wait_if_type_contains_mvar% ?m; e, and wait_if_contains_mvar% ?m; e are different variations of postponing depending on there being mvars in ?m
• no_error_if_unused% is allowed in match arms for Syntax match
• h ▸ e elaborates e and tries a number of tactics using the type of e and the expected type to rewrite using h to insert a cast

[Kyle Miller]

From Qq:

• q(...) and Q(..) quotations, with ~q(...) patterns

[Kyle Miller]

How I found these: I searched for : term, @[term_parser and @[builtin_term_parser

[Richard Copley]

Kyle Miller said:

exact?% is by exact?

I wish! It's by apply?

[Kim Morrison]

Richard Copley said:

Kyle Miller said:

exact?% is by exact?

I wish! It's by apply?

I think this would be reasonable to change. I'd merge the PR. :-)

[Richard Copley]

lean4#3974

[Thomas Murrills]

Eric Wieser said:

eval% is another one, which is handy for things like have : 5! = eval% 5! := by rfl, though a norm_num version would be better

#12353 introduces conv%, and along with it simp%, push_neg%, and norm_num%. (It also introduces ? variants of these as shortcuts for e.g. show_term …, so that it’s easy to check the result.)

There are some tentative choices made by that PR worth discussing, but probably in a separate thread. :)

[Mario Carneiro]

and a separate PR...

[Thomas Murrills]

To be clear, you mean you’d prefer the changes to the command syntax in a separate PR?

[Thomas Murrills]

(Or, well, that you think it would be better for them to be in a separate PR, not necessarily exclusively as a matter of personal preference.)

[Thomas Murrills]

Continued in #mathlib4 > conv% and changes to #conv (and friends). :)