rewrite under a pi

Stream: general

[Kevin Buzzard]

import data.real.basic

lemma quadroots {x : ℝ} : x ^ 2 - 3 * x + 2 = 0 ↔ x = 1 ∨ x = 2 := sorry

example : ∀ x : ℝ, ¬ (x ^ 2 - 3 * x + 2 = 0 → x = 1) :=
begin
  rw quadroots, -- fails
  sorry
end

I thought this would work. I have to intro x before it does. I know that rw can fail to rewrite under a lambda, but this is not a lambda, right? Can Lean also not rewrite under a pi?

[Mario Carneiro]

it cannot rewrite under a binder, because it needs to produce a substitution instance in the outer context

[Mario Carneiro]

To be clear, you can rewrite expressions that don't make use of the binder, like rewriting y to z in \lam x, x = y

[Mario Carneiro]

but since rw constructs an eq.rec term in the outer context it doesn't make sense to refer to x

[Mario Carneiro]

Think of it this way: rw quadroots is really rw [quadroots _]. What should go in for _?

[Reid Barton]

Interesting. I also encountered this exact question the other day--I expected rw to work in a similar situation, rewriting under a Pi, because it wasn't rewriting under a lambda. But I don't remember what ended up happening. It's possible I was in the "doesn't depend on x" situation.

[Reid Barton]

Can I think about it this way? I expect rw to apply something like "Pi.congr". But what is the argument to Pi.congr. It should just be an equality I intend to rewrite along, not something of the form \all x, f x = g x

[Mario Carneiro]

rw does not use Pi.congr or anything like it

[Mario Carneiro]

that's how simp works

[Mario Carneiro]

rw only uses eq.rec, i.e. the substitution property of equality

[Reid Barton]

Right, okay. But eq.rec still has that argument we have to provide

[Mario Carneiro]

so your goal has to have the form |- P a in the current context, and it is given an equality |- a = b, again in the current context (it may have metavariables but they have to be resolved in the current context), to produce |- P b

[Mario Carneiro]

In particular, it must be possible to write your goal as some function applied to the thing you want to rewrite, and this implies that it can't be a term that exists under a binder

[Mario Carneiro]

It's like you only know equality at one point and want to generalize to equality at all points - it doesn't work

[Mario Carneiro]

If you use a quantified equality as input to rw, it first applies some metavariables with the hope of matching them in the term, but before it has entered any binders. So that means you can always specify them yourself and give straight equations to rw with no loss of generality, unlike with simp where quantified equations are really more powerful

[Kevin Buzzard]

In my example, it's clear what I mean -- I want to rewrite "forall x, q(x)=0 -> ..." as "forall x, (x=1 or x=2) -> .."

[Kevin Buzzard]

There doesn't seem to be anything stopping that rewrite in theory

[Kevin Buzzard]

I can do it with intro, rw, revert. I'm not sure my users can though.

[Kevin Buzzard]

I guess they'll have to ;-)

[Mario Carneiro]

Of course, I follow. I'm just saying that's not how rw works

[Mario Carneiro]

the closest approximation to rw + binders is conv {rw}

[Kevin Buzzard]

Thank you Mario for your explanation. I find now I'm a more mature Lean user that when things like this happen I am now interested in understanding why they're failing (rather than banging my head against a table)

[Kevin Buzzard]

import data.real.basic

lemma quadroots {x : ℝ} : x ^ 2 - 3 * x + 2 = 0 ↔ x = 1 ∨ x = 2 := sorry

example : ∀ x : ℝ, ¬ (x ^ 2 - 3 * x + 2 = 0 → x = 1) :=
begin
  simp only [quadroots], -- WORKS!
  sorry
end

[Mario Carneiro]

right. simp uses a different algorithm, based on congruence lemmas, which has the advantage that you can rewrite under binders

[Mario Carneiro]

Rather than trying to match the goal all in one go like rw, it recurses into the term with things like funext that actually give you the opportunity to bubble those equalities into the inner context

[Kevin Buzzard]

rofl just noticed example is mathematically wrong ;-) [forall needs to go inside the brackets]