Implementing an advanced change tactic

Stream: general

[Patrick Johnson]

Sometimes I want to change a part of an assumption or the goal with another expression, providing a proof that they are equal. Tactics convert, convert_to, congr, congr' and change may help sometimes, but they are not flexible enough for my use case.

I would like to have a tactic ch that changes a part of an expression with another expression and creates a new goal to prove that the two expressions are equal. Example:

example {a b : ℕ} : 0 ≤ (a + 1) * b * (a + 1) :=
begin
  ch _ + 1 = _ * 1 at ⊢,
end

The goals become:

a b: ℕ
⊢ a + 1 = ?m_1 * 1

a b: ℕ
⊢ 0 ≤ ?m_1 * 1 * b * (?m_1 * 1)

a b: ℕ
⊢ ℕ

The tactic looks at _ + 1 and tries to resolve _. If there was additional b + 1 in the goal expression, the tactic would throw an error, because the match would be ambiguous. After resolving _ to a, it produces a new goal asking to prove that a + 1 = ?m_1 * 1 for some natural number ?m_1. Underscores on the LHS resolve to fixed expressions, while underscores on the RHS become metavariables. The tactic can also be applied at multiple locations.

This is my attempt to implement it:

import tactic
open tactic
open tactic.interactive
setup_tactic_parser

meta def tactic.interactive.ch
  (eq : parse texpr) (l : parse location) : tactic unit := do
  h ← i_to_expr eq,
  p ← tactic.assert `this h,
  tactic.swap,
  simp none none tt [simp_arg_type.expr ``(%%p)] [] l,
  clear [`this],
  tactic.swap

It does not support underscores at all and simp is not good enough for this purpose, because, for example, it will fail if we try to replace x with x * 1. The better approach would be to rewrite it manually (by using eq.rec to explicitly specify what parts we want to rewrite). Any suggestions on how to proceed?

[Junyan Xu]

example {a b : ℕ} : 0 ≤ (a + 1) * b * (a + 1) :=
begin
  rw (_ : _ + 1 = _ * 1),

/-
tactic failed, there are unsolved goals
state:
2 goals
a b : ℕ
⊢ 0 ≤ ?m_1 * 1 * b * (?m_1 * 1)

a b : ℕ
⊢ a + 1 = ?m_1 * 1
-/
end

[Patrick Johnson]

That's nice, but somewhat too verbose. I tried to make a single tactic for rw [...], swap, but I'm not sure how to construct a parse rw_rules term:

meta def tactic.interactive.ch (p : parse texpr) (l : parse location) : tactic unit := do
  rw p l, -- term `p` has type `parse texpr` but is expected to have type `parse rw_rules`
  tactic.swap

[Patrick Johnson]

I would also like the tactic to handle the following case:

example : ∃ (n : ℕ), n = 0 :=
begin
  ch ∀ (x : ℕ), x = x * 1,
end

Goals:

x: ℕ
⊢ x = x * 1

⊢ ∃ (n : ℕ), n * 1 = 0 * 1

[Eric Wieser]

Can you do the rw trick above but for simp_rw to solve that one?

[Patrick Johnson]

Apparently not.

[Junyan Xu]

Lean doesn't allow you to rewrite by x = x + 1, but if you switch the sides it works, but not without a call of the have or suffices tactic:

import tactic
example : ∃ (n : ℕ), n + 1 = 0 + 1 :=
begin
  suffices h : ∀ n : ℕ, n + 1 = n,
  simp_rw h,
  /-
  tactic failed, there are unsolved goals
  state:
  2 goals
  h : ∀ (n : ℕ), n + 1 = n
  ⊢ ∃ (n : ℕ), n = 0

  ⊢ ∀ (n : ℕ), n + 1 = n
  -/
end

There's also the conv mode.
If you want to dig into tactic writing, the metaprogramming / tactics stream would be the place to get help from.