conv in pat => cs runs the
conv tactic sequence
on the first subexpression matching the pattern
pat in the target.
The converted expression becomes the new target subgoal, like
conv => cs.
in are the same as those as the in
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]
#conv tac => e will run a conv tactic
e, and display the resulting
expression (discarding the proof).
#conv rw [true_and] => True ∧ False displays
There are also shorthand commands for several common conv tactics:
#whnf eis short for
#conv whnf => e
#simp eis short for
#conv simp => e
#norm_num eis short for
#conv norm_num => e
#push_neg eis short for
#conv push_neg => e
#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
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
#reduce is equivalent to using
#whnf on every subexpression.
#simp => eruns
simpon the expression
eand displays the resulting expression after simplification.
#simp only [lems] => eruns
simp only [lems]on
=>is optional, so
#simp only [lems] ehave the same behavior. It is mostly useful for disambiguating the expression
efrom the lemmas.