conv documentation

Stream: lean4

[Calvin Lee]

Lack of conv documentation and differences from lean3 came up in #general > Freeze of mathlib3 when attempting to forward port existing PRs. I have also seen some documentation of differences in #lean4 > conv navigation : Zoom out.
Is there anywhere that documentation exists for conv mode—or can be written? I would like to help document things and normalize behaviour if possible; since conv mode was very useful in lean3.

[Kevin Buzzard]

Please feel free to write an .md file explaining how conv works in lean 4. I'm sure the community will find somewhere to host it. In 2018 there were a few user-written documents on stuff like simp and conv, and they ended up on the community website. You can be inspired by the lean 3 version here https://leanprover-community.github.io/extras/conv.html

[Kevin Buzzard]

In fact perhaps it's time that document is updated to lean 4

[Kyle Miller]

@Calvin Lee I just went through all the conv tactics to collect a bit about how it works and what you can do with it. Here are my rough notes:

[Kyle Miller]

import Lean
import Mathlib.Tactic

/-!
# Research into `conv` mode, to help anyone who wants to write proper documentation.

Syntax:

conv: "conv" ("at" ident)? ("in" (occs)? term)? "=>" convSeq

occs: "(occs :=" ("*" <|> num+) ")"

convSeq: any sequence of conv tactics

`conv in (occs := ...) term => ...`
is short for
`conv => pattern (occs := ...) term; ...`
(the occs clause is optional)

Mathlib provides `conv_lhs` and `conv_rhs` variants to immediately do `lhs` or `rhs` as the
first tactic.
-/

/-!
`conv` sets up a special kind of tactic environment where you are shown `| lhs`
and the goal is actually `⊢ lhs = ?rhs`, where `?rhs` is a metavariable.
Each `conv` tactic uses the `lhs` to (partially) fill in the `?rhs` while also
(partially) solving for the goal (like the usual tactic environment).
At the end, this equality is used to rewrite `lhs` to `rhs`.

The idea is that if `lhs` starts with the entire original goal, then you can use
`conv` tactics to navigate into a subexpression of `lhs`, do some transformations, and then
at the end of the `conv` block you have `lhs = rhs`, which is used to convert the goal
from `lhs` to `rhs`.

What `conv` does at the very end of its tactic block is do `try rfl` to auto-solve
for the `?rhs` metavariable if it's still not solved for.
-/

example (a b c d : Nat) : a + b + c = a + b + d := by
  -- Rewrites the second occurrence of a + b
  conv in (occs := 2) a + b =>
    rw [add_comm]
  sorry

example (a b c d : Nat) : a + b + c = a + b + d := by
  -- Rewrites the both occurrences of a + b, using explicit `pattern` rather than
  -- `conv in (occs := *) a + b => ...`
  conv =>
    pattern (occs := *) a + b
    rw [add_comm]
  sorry

/-! # Conv tactics from Lean core -/

/-! ## Control

`done` checks that there are no `conv` goals remaining.

`skip` does nothing. It can be used to be the single tactic in an otherwise empty `conv` block.
It does *not* skip a `conv` goal.

`rfl` skips/closes a `conv` goal by using `rfl`. (Remember, the actual goal is `⊢ lhs = ?rhs`, so
this sets `?rhs := lhs` and uses `rfl` to prove `lhs = lhs`.)

`conv => convSeq` is a nested `conv`. It uses `conv` to change the current goal without closing it.
For example, this is how you can do a `conv`-targeted rewrite of the current expression and then
apply `conv` tactics to the result.

`all_goals convSeq` runs the `conv` tactics on every `conv` goal, collecting all the produced
subgoals (if any).

`any_goals convSeq` is like `all_goals` but succeeds if the tactic sequence succees for any
of the goals.

`case tag => convSeq` focuses on a goal with a given tag. Has the same syntax as the `case` tactic.
`case' tag => convSeq` is like `case` but does not auto-close the goal if the tactics
do not close it.

`next => convSeq` and `next x1 ... xn => convSeq` are like the `next` tactic, but they
auto-close the focused goal.

`· convSeq` focuses on the current goal and auto-closes it.

`focus => convSeq` focuses on the current goal. It does not auto-close the goal, unlike `next`.

`{ convSeq }` is like `next`.

`first | convSeq1 | convSeq2 | ...` tries each `conv` sequence one at a time until one
of them succeeds, or else fails.

`try convSeq` runs the `conv` sequence and succeeds even if it fails.
Same as `first | convSeq | skip`.

`repeat convSeq` repeatedly runs `convSeq` until it fails.

`( convSeq )` is for grouping. Useful when using `conv` tactic combinators.

`conv1 <;> conv2` is for trying `conv1` and then doing `conv2` if it fails.

`tactic => tacticSeq` converts the goal into `⊢ lhs = ?rhs` form and applies the tactic sequence.
The tactic does not have to solve the goal completely, and remaining goals are turned back
into `conv` goals. (Internal: there's also a `tactic' => tacticSeq` that does not remove the `conv`
annotations from the goal before applying the tactic sequence.)

### from Mathlib

`discharge => tacticSeq` takes a goal `| p` with `p` a proposition, uses the tactic sequence
to prove `⊢ p`, and then closes the goal to convert `p` to `True`.

`with_reducible convSeq` changes the transparency settings to `reducible` while evaluating the
`conv` sequence.

-/

/-! ## Navigation

`congr` (synonym: `args`) creates subgoals for every immediate subexpression of the expression.
You can use `rfl` to skip any of these subgoals.

`lhs` (synonym: `left`) traverses into the second-to-last argument of the expression.
(Implemented using `congr`.)

`rhs` (synonym: `right`) traverses into the last argument of the expression.
(Implemented using `congr`.)

`arg i` (and `arg @i`) traverses into the `i`th explicit argument (resp. the `i`th argument)
of the expression. (Implemented using `congr`.)

`ext` (synonym: `intro`) traverses into lambda, forall, and `let` expressions.
`ext x` gives the resulting binder the name `x`.
`ext x y z ...` applies `ext` once for each provided binder.

`enter [...]` is a compact way to describe a path to a subterm.
* `enter [i]` (where `i` is a natural number) is equivalent to `arg i`.
* `enter [@i]` is equivalent to `arg @i`.
* `enter [x]` (where `x` is an identifier) is equivalent to `ext x`.

Copying the docstring for `pattern`:
```quote
* `pattern pat` traverses to the first subterm of the target that matches `pat`.
* `pattern (occs := *) pat` traverses to every subterm of the target that matches `pat`
  which is not contained in another match of `pat`. It generates one subgoal for each matching
  subterm.
* `pattern (occs := 1 2 4) pat` matches occurrences `1, 2, 4` of `pat` and produces three subgoals.
  Occurrences are numbered left to right from the outside in.

Note that skipping an occurrence of `pat` will traverse inside that subexpression, which means
it may find more matches and this can affect the numbering of subsequent pattern matches.
For example, if we are searching for `f _` in `f (f a) = f b`:
* `occs := 1 2` (and `occs := *`) returns `| f (f a)` and `| f b`
* `occs := 2` returns `| f a`
* `occs := 2 3` returns `| f a` and `| f b`
* `occs := 1 3` is an error, because after skipping `f b` there is no third match.
```
-/

/-! ## Manipulation

`change t` changes the expression to `t` if the expression and `t` are definitionally equal.

`rw [thms...]` rewrites the expression using the given theorems. The syntax is similar to `rw`.

`erw [thms...]` rewrites the expression using the given theorems. The syntax is similar to `erw`.

`simp [thms...]` applies `simp` to rewrite the expression. The syntax is similar to `simp`.

`dsimp [thms...]` applies `dsimp` to rewrite the expression. The syntax is similar to `dsimp`.

`simp_match` simplifies `match` expressions.

`apply e` applies `e` to the goal (which remember is `⊢ lhs = ?rhs`) using the `apply` tactic.
Strange results may occur if the hypotheses of `e` are not equalities.

`refine e` applies `e` to the goal (which remember is `⊢ lhs = ?rhs`) using the `refine` tactic.
Strange results may occur if the placeholders in `e` are not equalities.

### from Std4

`exact e` closes the goal, where `e : lhs = ?rhs`.

### from Mathlib

The following apply their corresponding tactics in `conv` mode unless otherwise stated.

`abel` and `abel_nf`

`ring` and `ring_nf`

`norm_cast`

`norm_num1` and `norm_num`

`push_neg`

`apply_congr` applies a relevant `@[congr]` lemma

(category theory) `slice i j` reassociates as needed and focuses on the subexpression involving
the composition of morphisms `i` through `j`.

-/

/-! ## Reductions

`whnf` reduces the expression to weak-head normal form.

`zeta` applies zeta reduction to the expression (i.e., substitutes all `let` expressions
and expands all local variables).

`reduce` reduces the expression like the `#reduce` command.
(Documentation says "for debugging purposes only.")

`delta id1 id2 ...` applies delta reduction for the given constants (i.e., substitutes
the values of each constant). It is primitive: it ignores definitional equations and
uses the raw definition of each constant. Prefer using `unfold`.

`unfold id1 id2 ...` unfolds the definitions for the given constants using each
definitions equational lemmas. For recursive definitions, only one layer of unfolding
is performed.

-/

/-! ## Debugging, for internal use, or otherwise technical

`trace_state` prints the current goal state (runs the `trace_state` tactic)

`fail_if_success convSeq` fails if the `conv` sequence succeeds.

### from Std4

`guard_expr` and `guard_target`

`unreachable!`

### from Mathlib

`run_tac doSeq` evaluates the monadic value and runs it as a tactic using `tactic'`

-/

/-! ## Tactics and commands related to `conv`

`conv' ... => ...` is like `conv` but assumes the goal is already a `conv` goal.
Used internally to go back and forth between tactic mode and conv mode.

### from Mathlib

`conv_lhs ... => ...` and `conv_rhs ... => ...` are like `conv`, but they immediately use
`lhs` or `rhs` (respectively).

`#conv convTactic => e` is a command to apply the `convTactic` to the expression `e`, yielding
the converted expression (and dropping the generated proof).
This is used to implement `#simp`, `#whnf`, `#norm_num`, and `#push_neg`.

-/

[Kyle Miller]

This should include all the conv tactics in core, std4, and mathlib4

[Mario Carneiro]

tactic => and tactic' => are missing the arrows

[Calvin Lee]

Kyle Miller said:

This should include all the conv tactics in core, std4, and mathlib4

Can you elaborate on this a little bit?
Is there any reason how it is defined in three places? (i get core/otherwise, but is there any reason this tactic can't be mostly moved to std4 from mathlib4?)

[Kyle Miller]

conv itself is defined in one place, but it's extensible (just like the normal by tactic mode). You can define your own "conv tactics" that you can use from within conv. In the notes, all the conv tactics that come from std4 or mathlib4 are in "from XXX" sections.

[Kyle Miller]

I guess it's a bit confusing that the conv tactic (which is a tactic in the usual sense) has conv tactics, which are themselves not the usual sorts of tactics, but the conv tactic is not a conv tactic, yet there's a conv conv tactic for nested conv...

[Calvin Lee]

yep
this makes porting a bit clunky too (mentioned on the second thread i linked) because you can't do conv in in conv mode

[Kyle Miller]

Ah, but it's actually easy to extend nested conv syntax from outside core Lean. It's just a matter of someone actually doing it.

It's not so bad that to port you just need to add a pattern as the first line of the nested conv. (But also it'd be a nicer experience to have it in the conv syntax)

[Calvin Lee]

yes, so the way I ported this in my commit was for <pat> [<occs>] { <tacs...> } becomes conv => pattern (occs := <occs>) <pat>; <tacs...>
imo this would be easier if pattern (likewise arg, etc) would only change the conv view for its first argument
but i'm unsure if this is a deliberate design decision for lean4 conv.

[Kyle Miller]

What do you mean "for its first argument"? I thought Lean 4's conv works basically the same way as the Lean 3 one, but individual conv tactics might behave differently.

[Calvin Lee]

this is specifically about how for in lean3 "zooms out" after executing the next tactic, but pattern does not

[Kyle Miller]

It's not that for is zooming out, it's that it's running its tactic block in a sub-conv context. It's basically needing to do conv => pattern (occs := <occs>) <pat>; <tacs...> internally

[Kyle Miller]

So, it's not that the Lean 4 conv is designed differently, but rather there's no for-like conv tactic yet

[Kyle Miller]

#5786 is for adding it to mathlib. that's more expedient than trying to get it into core lean, but maybe it should find its way there at some point

[Kyle Miller]

We now have a ported version of the conv introduction and a conv guide. You can find these in the mathlib docs in the docs folder in the left sidebar.

[Scott Morrison]

@Kyle Miller, we should delete https://leanprover-community.github.io/extras/conv.html and replace the link to it from the community website sidebar with the link to your new doc!

[Mario Carneiro]

For example, enter [1,@2,x,3] is the same as arg 1, arg @2, ext x, arg 3.

The list of tactics should be separated by semicolons

[Mario Carneiro]

the link to the conv guide at the end of the introduction is broken

[Mario Carneiro]

The syntax for the conv tactic is

"conv" ("at" ident)? ("in" ("(occs :=" ("*" <|> num+) ")")? term)? "=>" convSeq

I think we also need a guide for reading syntax declarations, since I think we will want to use them a lot in documentation

[Kyle Miller]

Yeah, and this is mildly simplified from the actual one (strip off &, remove pp-directing-whitespace from strings, merge adjacent strings when sensible (like "(occs :="), inline some syntax definitions, strip off atomic(...)), so that guide could explain these conventions too

[Mario Carneiro]

FYI, if you actually use "(occs :=" in a syntax then it won't match (occs :=

[Mario Carneiro]

so you usually want to always split into tokens

[Kyle Miller]

Yeah, I'm aware, but I thought it was clearer like this for documentation.

[Kyle Miller]

Do the syntax tables have any sort of machine-readable representation? It'd be nice if we could generate some quasi-EBNF to document all the available term and tactic syntax.

[Mario Carneiro]

Unfortunately no; My best attempt is in the #help command but it can only show the initial token

[Mario Carneiro]

everything after that is stored in closures

[Mario Carneiro]

Well, there are still more radical things you can do parsing exprs

[Kyle Miller]

Is there at least an Expr with something that represents the parsers?

[Mario Carneiro]

yes

[Mario Carneiro]

it comes in two flavors though, the Parser and ParserDescr

[Mario Carneiro]

(also TrailingParser and TrailingParserDescr but these are basically the same)

[Mario Carneiro]

so you would need to parse both kinds

[Mario Carneiro]

and Parser can be arbitrary lean code so you would need to bottom out sometimes

[Kyle Miller]

I figure anything we can't explain can just be a link to its definition in the docs

[Mario Carneiro]

maybe I'll try my hand at this later

[Kyle Miller]

If it's not made out of >>, <|>, and a handful of other combinators, it's probably not worth interpreting the structure any further

[Mario Carneiro]

slice i j needs a (Mathlib) mark in the conv guide

[Mario Carneiro]

#simp et al should be shown on their own lines, since they are probably more interesting than #conv

[Kyle Miller]

I figured for those that there would be another guide for mathlib commands. It seems like an implementation detail that these have anything to do with conv

[Mario Carneiro]

Oh I suppose that's true

[Mac Malone]

Mario Carneiro said:

Well, there are still more radical things you can do parsing exprs

Fyi, I am currently in the process of completing a library that does just this.

[Mac Malone]

Currently, it can compile/transpile the parsers/syntaxes of the entire Lean grammar. The main TODOs are adding configuration options and debugging the test use case (which are parsers for the Lean grammar that does not need an Environment to parse Lean).