Additional conv tactics.

def Mathlib.Tactic.Conv.convLHS : Lean.ParserDescr

conv_lhs => cs runs the conv tactic sequence cs on the left hand side of the target.

In general, for an n-ary operator as the target, it traverses into the second to last argument. It is a synonym for conv => arg -2; cs.

• conv_lhs at h => cs runs cs on the left hand side of hypothesis h.
• conv_lhs in pat => cs first looks for a subexpression matching pat (see also the pattern conv tactic) and then traverses into the left hand side of this subexpression. This syntax also supports the occs clause for the pattern.

def Mathlib.Tactic.Conv.convRHS : Lean.ParserDescr

conv_rhs => cs runs the conv tactic sequence cs on the right hand side of the target.

In general, for an n-ary operator as the target, it traverses into the last argument. It is a synonym for conv => arg -1; cs.

• conv_rhs at h => cs runs cs on the right hand side of hypothesis h.
• conv_rhs in pat => cs first looks for a subexpression matching pat (see the pattern conv tactic) and then traverses into the right hand side of this subexpression. This syntax also supports the occs clause for the pattern.

def Mathlib.Tactic.Conv.convRun_conv_ : Lean.ParserDescr

def Mathlib.Tactic.Conv.«convConvIn__=>_» : Lean.ParserDescr

conv in pat => cs runs the conv tactic sequence cs on the first subexpression matching the pattern pat in the target. The converted expression becomes the new target subgoal, like conv => cs.

The arguments in are the same as those as the in pattern. In fact, conv in pat => cs is a macro for conv => pattern pat; cs.

The syntax also supports the occs clause. Example:

conv in (occs := *) x + y => rw [add_comm]

def Mathlib.Tactic.Conv.dischargeConv : Lean.ParserDescr

• discharge => tac is a conv tactic which rewrites target p to True if tac is a tactic which proves the goal ⊢ p.
• discharge without argument returns ⊢ p as a subgoal.

def Mathlib.Tactic.Conv.elabDischargeConv : Lean.Elab.Tactic.Tactic

Elaborator for the discharge tactic.

def Mathlib.Tactic.Conv.convRefine_ : Lean.ParserDescr

Use refine in conv mode.

def Mathlib.Tactic.Conv.«command#conv_=>_» : Lean.ParserDescr

The command #conv tac => e will run a conv tactic tac on e, and display the resulting expression (discarding the proof). For example, #conv rw [true_and_iff] => True ∧ False displays False. There are also shorthand commands for several common conv tactics:

• #whnf e is short for #conv whnf => e
• #simp e is short for #conv simp => e
• #norm_num e is short for #conv norm_num => e
• #push c => e is short for #conv push c => e

def Mathlib.Tactic.Conv.withReducible : Lean.ParserDescr

with_reducible tacs executes tacs using the reducible transparency setting. In this setting only definitions tagged as [reducible] are unfolded.

def Mathlib.Tactic.Conv.«command#whnf_» : Lean.ParserDescr

The command #whnf e evaluates e to Weak Head Normal Form, which means that the "head" of the expression is reduced to a primitive - a lambda or forall, or an axiom or inductive type. It is similar to #reduce e, but it does not reduce the expression completely, only until the first constructor is exposed. For example:

open Nat List
set_option pp.notation false
#whnf [1, 2, 3].map succ
-- cons (succ 1) (map succ (cons 2 (cons 3 nil)))
#reduce [1, 2, 3].map succ
-- cons 2 (cons 3 (cons 4 nil))

The head of this expression is the List.cons constructor, so we can see from this much that the list is not empty, but the subterms Nat.succ 1 and List.map Nat.succ (List.cons 2 (List.cons 3 List.nil)) are still unevaluated. #reduce is equivalent to using #whnf on every subexpression.

def Mathlib.Tactic.Conv.«command#whnfR_» : Lean.ParserDescr

The command #whnfR e evaluates e to Weak Head Normal Form with Reducible transparency, that is, it uses whnf but only unfolding reducible definitions.

def Mathlib.Tactic.Conv.«command#simpOnly_=>__» : Lean.ParserDescr

• #simp => e runs simp on the expression e and displays the resulting expression after simplification.
• #simp only [lems] => e runs simp only [lems] on e.
• The => is optional, so #simp e and #simp only [lems] e have the same behavior. It is mostly useful for disambiguating the expression e from the lemmas.