Zulip Chat Archive

Stream: general

Topic: rewrite under a pi


Kevin Buzzard (Sep 27 2018 at 15:12):

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 (Sep 27 2018 at 15:15):

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

Mario Carneiro (Sep 27 2018 at 15:16):

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 (Sep 27 2018 at 15:17):

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

Mario Carneiro (Sep 27 2018 at 15:17):

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

Reid Barton (Sep 27 2018 at 15:18):

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 (Sep 27 2018 at 15:21):

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 (Sep 27 2018 at 15:21):

rw does not use Pi.congr or anything like it

Mario Carneiro (Sep 27 2018 at 15:21):

that's how simp works

Mario Carneiro (Sep 27 2018 at 15:22):

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

Reid Barton (Sep 27 2018 at 15:22):

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

Mario Carneiro (Sep 27 2018 at 15:23):

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 (Sep 27 2018 at 15:24):

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 (Sep 27 2018 at 15:25):

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 (Sep 27 2018 at 15:28):

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 (Sep 27 2018 at 15:34):

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 (Sep 27 2018 at 15:34):

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

Kevin Buzzard (Sep 27 2018 at 15:35):

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

Kevin Buzzard (Sep 27 2018 at 15:35):

I guess they'll have to ;-)

Mario Carneiro (Sep 27 2018 at 15:36):

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

Mario Carneiro (Sep 27 2018 at 15:36):

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

Kevin Buzzard (Sep 27 2018 at 15:36):

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 (Sep 27 2018 at 15:38):

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 (Sep 27 2018 at 15:39):

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

Mario Carneiro (Sep 27 2018 at 15:40):

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 (Sep 27 2018 at 15:42):

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


Last updated: Dec 20 2023 at 11:08 UTC