Zulip Chat Archive
Stream: general
Topic: rewrite LHS is a mvar
Mario Carneiro (Mar 13 2018 at 12:57):
example (h : ∀ a : nat, a = 0) : 0 = 2 := by rw h -- rewrite tactic failed, lemma lhs is a metavariable example (h : ∀ a : nat, a = 0) : 0 = 2 := by rw ← h -- rewrite tactic failed, lemma lhs is a metavariable example (h : ∀ a : nat, 0 = a) : 0 = 2 := by rw h --ok example (h : ∀ a : nat, 0 = a) : 0 = 2 := by rw ← h -- rewrite tactic failed, did not find instance of the pattern in the target expression -- ?m_1
rewrite talks about LHS but apparently it doesn't take into account symmetry
Kevin Buzzard (Mar 13 2018 at 13:03):
example (h : ∀ a : nat, a = 0) : 0 = 2 := by rw h 2 -- succeeds!
Kevin Buzzard (Mar 13 2018 at 13:05):
oh this is more complicated than I thought. Of course that succeeds.
Kevin Buzzard (Mar 13 2018 at 13:07):
That first example is really hard. I can see why it fails. How should it have a clue what to set a?
Mario Carneiro (Mar 13 2018 at 13:08):
Actually, in my view none of them should fail. rw actually should not have any issues with the LHS being an arbitrary variable; it will just trigger very easily.
Kevin Buzzard (Mar 13 2018 at 13:08):
How is rw supposed to do the first one?
Kevin Buzzard (Mar 13 2018 at 13:09):
It has a tool for showing an arbitrary thing is 0, but it has to match 0 = 2
Kevin Buzzard (Mar 13 2018 at 13:09):
I think if I were rw I would let a be the first nat I found in the goal
Kevin Buzzard (Mar 13 2018 at 13:09):
which is 0
Kevin Buzzard (Mar 13 2018 at 13:09):
and then rewrite and get 0=2 and then decide I failed
Kevin Buzzard (Mar 13 2018 at 13:10):
Isn't that how it works? I just spent some time trying to figure this out.
Mario Carneiro (Mar 13 2018 at 13:10):
compare to when I wrap everything in id:
example (h : ∀ a : nat, id a = id 0) : id 0 = id 2 := by rw h -- ⊢ id 0 = id 2 example (h : ∀ a : nat, id a = id 0) : id 0 = id 2 := by rw ← h -- done example (h : ∀ a : nat, id 0 = id a) : id 0 = id 2 := by rw h -- done example (h : ∀ a : nat, id 0 = id a) : id 0 = id 2 := by rw ← h -- ⊢ id 0 = id 2
Kevin Buzzard (Mar 13 2018 at 13:10):
As I just said, I am unsurprised by the first one.
Kevin Buzzard (Mar 13 2018 at 13:10):
Why do you think it should work?
Mario Carneiro (Mar 13 2018 at 13:11):
rw should trigger on the first matching occurrence of the pattern. If the LHS is a metavar, that's just the first type correct subterm
Kevin Buzzard (Mar 13 2018 at 13:11):
and indeed this is a=0 for the first one
Kevin Buzzard (Mar 13 2018 at 13:12):
it matches id 0 so sets a=0
Kevin Buzzard (Mar 13 2018 at 13:12):
and now you're doomed
Mario Carneiro (Mar 13 2018 at 13:12):
No, that's intended behavior
Mario Carneiro (Mar 13 2018 at 13:12):
I'm not expecting it to solve the goal, but it shouldn't fail
Kevin Buzzard (Mar 13 2018 at 13:12):
Aah I see.
Mario Carneiro (Mar 13 2018 at 13:13):
the question is why I get a bunch of weird and inconsistent failures when I remove the id
Kevin Buzzard (Mar 13 2018 at 13:13):
example (h : ∀ a : nat, a = 0) : 0 = 2 := by rw ← h -- rewrite tactic failed, lemma lhs is a metavariable example (h' : ∀ a : nat, 0 = a) : 0 = 2 := by rw h' -- succeeds
Kevin Buzzard (Mar 13 2018 at 13:13):
I had imagined these were synonymous
Mario Carneiro (Mar 13 2018 at 13:14):
exactly my point
Mario Carneiro (Mar 13 2018 at 13:14):
there's a funny lhs metavar check that literally checks the left side even if that's the destination, not the source
Kevin Buzzard (Mar 13 2018 at 13:15):
I see. The issue is not that they fail, it's how they fail. I understand your point now.
Mario Carneiro (Mar 13 2018 at 13:17):
and the final example is even stranger - example (h : ∀ a : nat, 0 = a) : 0 = 2 := by rw ← h is using backwards rewrite to circumvent the buggy lhs metavar check, and instead hits a search bug, probably what the lhs metavar check was trying to avoid
Kevin Buzzard (Mar 13 2018 at 13:17):
example (h : ∀ a : nat, id 0 = id a) : id 0 = id 2 := by rw ← h -- ⊢ id 0 = id 2
Kevin Buzzard (Mar 13 2018 at 13:17):
I have no idea what to do with this one. It seems there are two reasonable ways to behave?
Mario Carneiro (Mar 13 2018 at 13:18):
I would argue that all the id examples are consistent
Kevin Buzzard (Mar 13 2018 at 13:18):
First I could spot the id 0 on the LHS and just replace it with id a
Mario Carneiro (Mar 13 2018 at 13:18):
Here, just like the forward rewrite version, it is rewriting id ?m -> id 0 and spots the first matching pattern id 0, so ?m := 0
Kevin Buzzard (Mar 13 2018 at 13:19):
oh ha ha I missed the \l
Kevin Buzzard (Mar 13 2018 at 13:19):
It's this one that confuses me:
Kevin Buzzard (Mar 13 2018 at 13:19):
example (h : ∀ a : nat, id 0 = id a) : id 0 = id 2 := by rw h -- done
Kevin Buzzard (Mar 13 2018 at 13:20):
Presumably it doesn't spot the id 0 in the goal and then announce that it's going to replace it with id ?m
Sebastian Ullrich (Mar 13 2018 at 13:20):
kabstract with a metavar will only match other metavars, it's probably trying to avoid that
Kevin Buzzard (Mar 13 2018 at 13:20):
instead it has to decide what to do with the a first
Mario Carneiro (Mar 13 2018 at 13:21):
why is that? As I said it seems inconsistent with the id ?m behavior. Is it being special cased? I feel like you would have to work hard to make that happen
Mario Carneiro (Mar 13 2018 at 13:23):
@Kevin Buzzard actually that's exactly what it does. It is rewriting id 0 -> id ?m, and spots the first matching pattern id 0, but ?m is unconstrained by this and the result is id ?m = id 2. The proof is finished with the automatic refl after rw
Kevin Buzzard (Mar 13 2018 at 13:24):
ha ha
Kevin Buzzard (Mar 13 2018 at 13:24):
yes I just noticed that this works too:
Kevin Buzzard (Mar 13 2018 at 13:24):
example (h : ∀ a : nat, 0 = a) : 2 = 0 := by rw h -- done
Kevin Buzzard (Mar 13 2018 at 13:24):
and here we really seem to have no option other than to leave the metavariable alone and make the match
Sebastian Ullrich (Mar 13 2018 at 13:26):
@Mario Carneiro It's using keyed matching, which uses structural equality for the head
Last updated: Dec 20 2023 at 11:08 UTC