conv tactic

Stream: new members

[Bolton Bailey]

Several times in my lean project I have been faced with the situation of needing to rewrite an expression which involves a variable from a lambda encompassing that expression. My understanding is that this is called "rewriting under binders", and this page seems to say pretty explicitly that conv is the proper way of doing this. However, I am confused as to how this works. The "conversions" section in the lean reference manual https://leanprover.github.io/reference/tactics.html is simply blank (which is itself rather frustrating ) .

My understanding from reading the leanprover-community page is that applying the conv tactic would allow me to rewrite a particular section of a goal, even with a binder. However, this is not what happens in the mwe below. What am I doing wrong?

import data.mv_polynomial.basic

section

noncomputable theory

universes u

parameter {F : Type u}
parameter [field F]


@[derive decidable_eq]
inductive vars : Type
| X : vars
| Y : vars
| Z : vars


/-- Helper for converting mv_polynomial to single -/
def singlify : vars -> polynomial F
| x := ite (x = vars.X) polynomial.X 1

lemma helper_lemma : (λ (n : vars) (e : ℕ), singlify n ^ e) = (λ (n : vars) (e : ℕ), ite (n = vars.X) ((polynomial.X : polynomial F) ^ (e)) 1)
:=
begin
  funext,
  intros,
  rw singlify,
  rw ite_pow,
  rw one_pow,
end

lemma main_theorem (a₁ : vars →₀ ℕ) : a₁.prod (λ (n : vars) (e : ℕ), singlify n ^ e) = ((polynomial.X : polynomial F) ^ (a₁ vars.X))
:=
begin
  -- This method works, but requires me to create a whole new lemma which will only be used here.
  -- I would prefer to use conv, since that seems to be the canonical way, and it would make the proof more self contained.

  rw helper_lemma,
  rw finsupp.prod,
  rw finset.prod_ite,
  simp,
  rw finset.filter_eq',
  by_cases vars.X ∈ a₁.support,
  rw if_pos,
  rw finset.prod_singleton,
  exact h,
  rw if_neg,
  rw finset.prod_empty,
  have h1 : a₁ vars.X = 0,
  rw finsupp.not_mem_support_iff at h,
  exact h,
  rw h1,
  rw pow_zero,
  exact h,
end

lemma main_theorem_with_conv (a₁ : vars →₀ ℕ) : a₁.prod (λ (n : vars) (e : ℕ), singlify n ^ e) = ((polynomial.X : polynomial F) ^ (a₁ vars.X))
:=
begin
  conv
  begin
    to_lhs,
    congr,
    skip,
    funext,
    rw singlify,
    rw ite_pow,
    rw one_pow,
  end
  -- Goal is unchanged from the initial goal
end

end

[Kevin Buzzard]

Is simp only [singlify, ite_pow, one_pow], what you are looking for? simp can rewrite under binders.

[Kevin Buzzard]

PS creating a whole new lemma to help with other lemmas is exactly the mathlib philosophy. Better two short proofs than one longer one.

[Patrick Massot]

You should put a comma after end to see the new tactic state.

[Kevin Buzzard]

lemma helper_lemma : (λ (n : vars) (e : ℕ), singlify n ^ e) = (λ (n : vars) (e : ℕ), ite (n = vars.X) ((polynomial.X : polynomial F) ^ (e)) 1)
:= by simp [singlify, ite_pow, one_pow]

[Patrick Massot]

(right before your comment saying it doesn't work)

[Patrick Massot]

Kevin's answers are nice but the question "how to use conv" is still valid.

[Kevin Buzzard]

lemma main_theorem (a₁ : vars →₀ ℕ) : a₁.prod (λ (n : vars) (e : ℕ), singlify n ^ e) = ((polynomial.X : polynomial F) ^ (a₁ vars.X))
:=
begin
  -- This method works, but requires me to create a whole new lemma which will only be used here.
  -- I would prefer to use conv, since that seems to be the canonical way, and it would make the proof more self contained.

  simp only [singlify, ite_pow, one_pow],
  rw finsupp.prod,
  rw finset.prod_ite,
...