rw of self

Stream: new members

[Damiano Testa]

While playing around with the question of this thread, I came across the funny behaviour below. I expected that rw could be used to rewrite a hypothesis with itself, but I was not able to make it work. Below is also an awkward way of doing it, by "duplicating a hypothesis". I can see that this is borderline self-referential, but is there a way to make the proof below work without duplicating a hypothesis?

Thanks!

import data.polynomial.basic

open polynomial

example {R : Type*} [semiring R] (h : (X : polynomial R) = X ^ 2) : (X : polynomial R) = X ^4 :=
begin
-- I would like to do this, but it does nothing...
--  rw [h] at h {occs := occurrences.pos [2]},
  have h' : X = X ^ 2 := h,
  rw [h] at h' {occs := occurrences.pos [2]},
  rw ← pow_mul at h',
  exact h',
end

[Damiano Testa]

Unsurprisingly, repeat { rw [h] at h {occs := occurrences.pos [2]} } times out.

[Johan Commelin]

hmm, I don't know if that's possible

[Riccardo Brasca]

Is occurrences.pos the same as nth_rewrite?

[Johan Commelin]

not exactly, but almost

[Damiano Testa]

Fair enough! The solution is not so bad, just feels clunky. I also suspect that these kind of rewrites would be more common when working with power series and finding better approximations, from earlier ones. Maybe also results like the contraction theorem... Btw, is the contraction theorem in mathlib?

[Johan Commelin]

you could do rw at pos [1] in the goal

[Damiano Testa]

maybe yes:

mathlib/src/topology/metric_space/contracting.lean:/-- Banach fixed-point theorem, contraction mapping theorem, emetric_space version.

[Damiano Testa]

Johan, I am not sure that I understand how to try what you suggested...

[Damiano Testa]

I got it! Thanks!

example {R : Type*} [semiring R] (h : (X : polynomial R) = X ^ 2) : (X : polynomial R) = X ^4 :=
begin
  rw [h] {occs := occurrences.pos [1]}, -- Johan's suggestion to work on the goal, instead
  rw [h] {occs := occurrences.pos [1]},

rw [h] at h {occs := occurrences.pos [2]},

  rw ← pow_mul,
  refl,
end

I like this, although I view it as a different workaround. In any case, this question mostly arose as a curiosity, than an actual issue.

[Johan Commelin]

what is the 3rd line doing?

[Damiano Testa]

It was a left-over from before. As I learned, it does absolutely nothing! I could replicate it as much as I wanted and it would still be useless! :grinning:

[Johan Commelin]

example {R : Type*} [semiring R] (a : R) (h : a = a ^ 2) : a = a ^ 4 :=
by { rw [h, h] {occs := occurrences.pos [1]}, rw ← pow_mul, refl }

[Damiano Testa]

Ah, I did not know that you could compress the rw with the optional parameters!