11.1. Basic navigation and rewriting🔗

As a first example, let us prove example (a b c : Nat) : a * (b * c) = a * (c * b) (examples in this file are somewhat artificial since other tactics could finish them immediately). The naive first attempt is to enter tactic mode and try rw [Nat.mul_comm]. But this transforms the goal into b * c * a = a * (c * b), after commuting the very first multiplication appearing in the term. There are several ways to fix this issue, and one way is to use a more precise tool: the conversion mode. The following code block shows the current target after each line.

The above snippet shows three navigation commands:

• lhs navigates to the left-hand side of a relation (equality, in this case). There is also a rhs to navigate to the right-hand side.

• congr creates as many targets as there are (nondependent and explicit) arguments to the current head function (here the head function is multiplication).

• rfl closes target using reflexivity.

Once arrived at the relevant target, we can use rw as in normal tactic mode.

The second main reason to use conversion mode is to rewrite under binders. Suppose we want to prove example (fun x : Nat => 0 + x) = (fun x => x). The naive first attempt is to enter tactic mode and try rw [Nat.zero_add]. But this fails with a frustrating

error: tactic 'rewrite' failed, did not find instance of the pattern
       in the target expression
  0 + ?n
⊢ (fun x => 0 + x) = fun x => x

The solution is:

where intro x is the navigation command entering inside the fun binder. Note that this example is somewhat artificial, one could also do:

or just

conv can also rewrite a hypothesis h from the local context, using conv at h.

11.2. Pattern matching🔗

Navigation using the above commands can be tedious. One can shortcut it using pattern matching as follows:

which is just syntax sugar for

Of course, wildcards are allowed:

11.3. Structuring conversion tactics🔗

Curly brackets and . can also be used in conv mode to structure tactics:

11.4. Other tactics inside conversion mode🔗

• arg i enter the i-th nondependent explicit argument of an application.

  example (a b c : Nat) : a * (b * c) = a * (c * b) := bya:Natb:Natc:Nat⊢ a * (b * c) = a * (c * b) conv =>a:Natb:Natc:Nat| a * (b * c) = a * (c * b) lhsa:Natb:Natc:Nat| a * (b * c) arg 2a:Natb:Natc:Nat| b * c rw [Nat.mul_comm]a:Natb:Natc:Nat| c * b

• args is an alternative name for congr.

• simp applies the simplifier to the current goal. It supports the same options available in regular tactic mode.

  def f (x : Nat) := if x > 0 then x + 1 else x + 2 example (g : Nat → Nat) (h₁ : g x = x + 1) (h₂ : x > 0) : g x = f x := byx:Natg:Nat → Nath₁:g x = x + 1h₂:x > 0⊢ g x = f x conv =>x:Natg:Nat → Nath₁:g x = x + 1h₂:x > 0| g x = f x rhsx:Natg:Nat → Nath₁:g x = x + 1h₂:x > 0| f x simp [f, h₂]x:Natg:Nat → Nath₁:g x = x + 1h₂:x > 0| x + 1 exact h₁All goals completed! 🐙

• enter [1, x, 2, y] iterate arg and intro with the given arguments.

• done fail if there are unsolved goals.

• trace_state display the current tactic state.

• whnf put term in weak head normal form.

• tactic => <tactic sequence> go back to regular tactic mode. This is useful for discharging goals not supported by conv mode, and applying custom congruence and extensionality lemmas.

  example (g : Nat → Nat → Nat) (h₁ : ∀ x, x ≠ 0 → g x x = 1) (h₂ : x ≠ 0) : g x x + x = 1 + x := byx:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0⊢ g x x + x = 1 + x conv =>x:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| g x x + x = 1 + x lhsx:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| g x x + x arg 1x:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| g x x rw [h₁]x:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| 1ax:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0⊢ x ≠ 0 . skipx:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| 1 . tactic =>ax:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0⊢ x ≠ 0 exact h₂All goals completed! 🐙

• apply <term> is syntax sugar for tactic => apply <term>.

  example (g : Nat → Nat → Nat) (h₁ : ∀ x, x ≠ 0 → g x x = 1) (h₂ : x ≠ 0) : g x x + x = 1 + x := byx:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0⊢ g x x + x = 1 + x conv =>x:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| g x x + x = 1 + x lhsx:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| g x x + x arg 1x:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| g x x rw [h₁]x:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| 1ax:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0⊢ x ≠ 0 . skipx:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| 1 . apply h₂All goals completed! 🐙