rw (show ..., by omega)

Stream: new members

[Shing Tak Lam]

import tactic.omega

example (n p : ℕ) (hp : p ≠ 0) (h2 : 2 = p ^ n) (hp2 : p < 2) (hcont : ¬1 < p) :
  false :=
begin
  -- h2 : 2 = p ^ n,
  rw (show p = 1, by omega) at h2,
  -- h2 : 2 = p ^ n, still.
  rw (show p = 1, by sorry) at h2,
  -- h2 : 2 = 1 ^ n
  sorry
end

Why does the two rws have different behaviour? The first one does nothing (and there's no error). The second one actually does the rewrite that I expect.

[Shing Tak Lam]

separating the show into have ... rw ... works as expected...

import tactic.omega

example (n p : ℕ) (hp : p ≠ 0) (h2 : 2 = p ^ n) (hp2 : p < 2) (hcont : ¬1 < p) :
  false :=
begin
  have h : p = 1, by omega,
  rw h at h2,
  sorry
end

[Reid Barton]

Mysterious

[Rob Lewis]

I think the problem is that omega uses h2 in the proof of p = 1 for some reason, and this confuses rw.

[Rob Lewis]

You get the same behavior if you change your have line to a let. In a have, the dependency on h2 isn't there until after the rest of the proof is done.

[Shing Tak Lam]

I see.

lemma l (n p : ℕ) (hp : p ≠ 0) (h2 : 2 = p ^ n) (hp2 : p < 2) (hcont : ¬1 < p) :
  p = 1 :=
begin
  omega,
end

#print l

and it does seem like that it uses h2 in the proof (I think it just uses everything it can). So that makes sense. rw not producing an error was what confused me.

Thanks!

[Mario Carneiro]

I'm still not satisfied with this explanation. Why should it matter what is used in the proof that p = 1? I guess this might pose a problem for the revert/intro approach to rw at but that should still be happening after the theorem is already proven. Or is the issue perhaps that the expression show p = 1, by omega is elaborated in a context where h2 has already been reverted?

[Reid Barton]

I guess a minimal example is

example (h : 1 = 2) : true :=
begin
  rw h at h,
end

This has the same behavior: no error, but proof state is unchanged

[Rob Lewis]

I didn't fully debug this, but my guess is: first rw a at h elaborates a. Then it reverts h. Then it tries to build the eq.rec_on a ... term, but this doesn't type check because a no longer type checks. Then a bug in rw stops it from throwing an error. It could abstract the argument a, but it doesn't.

[Rob Lewis]

a elaborates fine, it's not that the revert happens before that.

[Rob Lewis]

But again, I only played with this for a minute, my guess could be wrong.