rewrite tactic failed, lemma is not an equality nor a iff

Stream: new members

[Kevin Kappelmann]

Hi, I am having some rewriting issues. When I try to rewrite an obtained equality without explicitly re-stating the type, the rewriter fails returning rewrite tactic failed, lemma is not an equality nor a iff. However, when I explicitly re-state the type, the rewriter succeeds. Here is an example:

import algebra.archimedean

variables {α : Type*} [discrete_linear_ordered_field α] [floor_ring α]

variables (a b c : α)

lemma my_eq_lemma (a b : α) {c : α} (fract_c_not_zero : fract c ≠ 0) :
a + (fract c)⁻¹ * (b + ⌊c⌋ * a) = (fract c)⁻¹ * (a * c + b) := sorry

example (hyp : fract c ≠ 0) : a + (fract c)⁻¹ * (b + ⌊c⌋ * a) = (fract c)⁻¹ * (a * c + b) :=
begin
have my_eq, from my_eq_lemma a b hyp, -- my_eq : a + (fract c)⁻¹ * (b + ↑⌊c⌋ * a) = (fract c)⁻¹ * (a * c + b)
rw my_eq -- rewrite tactic failed, lemma is not an equality nor a iff
end

example (hyp : fract c ≠ 0) : a + (fract c)⁻¹ * (b + ⌊c⌋ * a) = (fract c)⁻¹ * (a * c + b) :=
begin
have my_eq : a + (fract c)⁻¹ * (b + ⌊c⌋ * a) = (fract c)⁻¹ * (a * c + b), from my_eq_lemma a b hyp,
rw my_eq -- works
end

I would like to avoid re-stating the type as in my actual use case, the type is even longer. Any ideas? simp only [my_eq] also does not seem to work.

[Kevin Kappelmann]

Oops, gimme a second, some typos in the example.
Edit: Fixed it.

[Floris van Doorn]

If I replace the line by have my_eq := my_eq_lemma a b hyp the small example work for me. Does this work in the actual use case?
I don't know what is going on though.

[Patrick Massot]

That's a nice one. Using set option pp.all true shows 100% same tactic state in both example

[Kevin Buzzard]

I would like to avoid re-stating the type as in my actual use case, the type is even longer. Any ideas?

You can take short cuts with change / show sometimes -- e.g. show _ = 0 works fine if you're just trying to simplify the right hand side to something definitionally equal.

[Floris van Doorn]

They are different with the option set_option pp.instantiate_mvars false.

This gives a clue of what is going on. If you say have my_eq, from my_eq_lemma a b hyp then you are doing two steps: first you add a new fact whose type and definition are metavariables, and then you provide the definition, while with the have my_eq := ... notation this is one step. Somehow the type of my_eq is not updated (enough) when doing two steps.

Probably the rewrite tactic needs to call instantiate_mvars on the type of the expression it is rewriting with.

[Kevin Kappelmann]

If I replace the line by have my_eq := my_eq_lemma a b hyp the small example work for me. Does this work in the actual use case?
I don't know what is going on though.

Ahw, that does work, yeah! :)

[Edward Ayers]

Interestingly, have my_eq : a + _ = _, from my_eq_lemma a b hyp, works but have my_eq : a_ = _, from my_eq_lemma a b hyp, doesn't work for me. The error being rewrite tactic failed, lemma lhs is a metavariable

[Edward Ayers]

So I think the problem is that rw x is not instantiating the metavariables on x before trying to rewrite with it.

[Edward Ayers]

ah floris beat me

[Edward Ayers]

Seems a shame that rw doesn't automatically try to instantiate mvars.

[Kevin Kappelmann]

I keep on running into this issue btw. Another example:

lemma rat_num_lt_denom (q : ℚ) (q_lt_one : q < 1) : q.num < q.denom :=
begin
have one_times_denom_eq_denom, from one_mul q.denom,
rw ←one_times_denom_eq_denom, -- rewrite tactic failed, lemma is not an equality nor a iff
sorry
end

I just use the := workaround anytime I have this issue at the moment.

[Mario Carneiro]

you should always use := for tactic have unless you have a particular reason to do it in two stages

[Mario Carneiro]

despite the visual resemblance it's two tactics and that causes some information to not get around

[Mario Carneiro]

That said, this is a bug in rw

[Kevin Kappelmann]

I should use it because of this bug or is there any other reason?

[Mario Carneiro]

it has more information available for elaboration in one place, so you (usually) get a more accurate result

[Mario Carneiro]

it's also probably slightly faster