Zulip Chat Archive

Stream: general

Topic: rewrite occs


view this post on Zulip Scott Morrison (Mar 10 2018 at 21:06):

Can anyone help me understand why the 2nd example in the following doesn't work?

@[ematch] lemma baz (l : list ) : 1 :: l = 2 :: l := sorry
example : [1, 1, 2] = [2, 1, 2] :=
begin
rw [baz] {occs:=occurrences.pos [1]},
end
example : [1, 1, 2] = [1, 2, 2] :=
begin
rw [baz] {occs:=occurrences.pos [2]},
end

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:07):

I have been reading replace_fn.cpp and kabstract.cpp, to no avail: my understanding of what is going on there suggests the second example should still work.

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:10):

A related confusion is why in

example : [1, 1, 2] = [1, 2, 2] :=
begin
rw [baz],
end

the goal has become [2, 1, 2] = [1, 2, 2], and not [2, 1, 2] = [2, 2, 2]. That is, why did rewrite give up on the rhs?

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 21:18):

kabstract does not backtrack from unification: once l has been assigned [1, 2], it does not consider other values for it

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 21:19):

That is, it only finds occurrences of the same instantiation of the lhs

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 21:20):

(Don't ask me why :) )

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:22):

oh...

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:23):

I see, that ctx.unify call in kabstract is saving information about things it has seen before.

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:23):

It hadn't occurred to me that there were side effects there.

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:24):

That sucks (for my purposes)...

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:26):

So... if I really really wanted be be able to generate a list of all the rewrites of some expression e by some rule r (where we just rewrite in one place), is there any hope?

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:27):

It seems that just calling rw [r] at e {occs := occurrences.pos n} and gradually increasing n until it fails is doomed, because of this "feature" of kabstract.

view this post on Zulip Simon Hudon (Mar 10 2018 at 21:38):

if you want to hack a solution together, you might have to copy / paste the implementation of rw and reimplement kabstract. I think the key is to undo the assignment of meta variable. One way of to that is to traverse your expression and create new meta variables to replace the ones that you find.

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 21:38):

Yes. It just won't be very fast.

view this post on Zulip Simon Hudon (Mar 10 2018 at 21:40):

I assume with the new focus on Lean 4, that might be the one way to get the fixed tactic sooner than later.

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:41):

I see: reimplement kabstract in Lean?

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:42):

I was just trying to find the definition of type_context_old, and see if there was any hope of hacking on an extra option that would change this behaviour. But I agree it's exceedingly unlikely I could propose such a change.

view this post on Zulip Simon Hudon (Mar 10 2018 at 21:42):

yeah pretty much. Unless @Sebastian Ullrich agrees that the current semantics is wrong and is willing to fix it for you

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:43):

@Sebastian Ullrich ? :-)

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 21:43):

It's been that way since Lean 2, where it was even documented afair :)

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:43):

Okay!

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:43):

Looks like I will think about a really slow version of kabstract!

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:45):

(Context here is that I'm otherwise really happy with my rewrite_search tactic, based on greedily minimising edit distance. I have "real" examples where it successfully finds long (~10) chains of rewrites that complete a proof. Unfortunately sometimes it mysteriously fails, and this seems to be the issue.)

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 21:46):

It's not even clear to me what a different kabstract would look like. Would it introduce n lambdas and return n instantiated copies of e?

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 21:46):

@Scott Morrison I suppose repeatedly rewriting will not solve your problem? :)

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:47):

No -- I have lots of examples where the rewrite rule needs to be applied "inside" a bigger expression where the rewrite rule also applies.

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:47):

But after you do the outer rewrite the inner rewrite is no longer available.

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:48):

(rewrite_search is already trying repeated rewrites itself: I only discovered this problem because it was mysteriously failing.)

view this post on Zulip Kevin Buzzard (Mar 10 2018 at 21:48):

Scott -- has Mario made any suggestions on how to deal with your issues?

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:49):

Kevin -- I only raised this about 5 minutes ago, perhaps Mario is sleeping. :-)

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:51):

@Sebastian Ullrich, I guess I was thinking not actually to reimplement kabstract, but reimplement all of rewrite_core.

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:51):

(Reimplementing kabstract in Lean would not be helpful, because no tactics actually call it from Lean: only things in c++.)

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 21:53):

I'm not sure how you want to solve your issue with the current kabstract

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:53):

Or rather, to write something called all_rewrites, that takes an expr, and a list of lemmas, and returns list (expr \times expr), where the pairs are the result of using the lemma in one place, and the proof.

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:54):

It would work by recursively going down into the expr, and repeatedly calling unify ... oh, I see your point.

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:54):

Those calls to unify are _also_ going to be cached. :-(

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:54):

This is terrible. :-)

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 21:55):

Well, not if you create new mvars like Simon suggested

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:55):

I see; after every time you successfully find a match, you throw out the mvar you were passing to unify and make a new one.

view this post on Zulip Scott Morrison (Mar 10 2018 at 21:56):

(Thanks, Simon, sorry I was slow to understand exactly what you meant.)

view this post on Zulip Simon Hudon (Mar 10 2018 at 21:57):

No worries

view this post on Zulip Kevin Buzzard (Mar 10 2018 at 21:59):

Kevin -- I only raised this about 5 minutes ago, perhaps Mario is sleeping. :-)

Oh -- I knew that you had been discussing with Mario about what looked like a major refactoring job on the category theory library and I was just kind of assumed this might be something to do with the refactoring

view this post on Zulip Simon Hudon (Mar 10 2018 at 21:59):

I believe in rewrite, when you use ∀ x, f x = g x as your rewrite rule, you generate one mvar to instantiate x and you start matching. What you can do instead is create a unique local constant to instantiate x with (or as many as you have bound variable) and you create a table mapping those constants to mvars every time you attempt a match

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 22:00):

Btw, it might be easier to build something on top of tactic.ext_simplify_core. You basically get a very configurable term DFS where you can return subterm equality proofs pre or post visit and the tactic takes care of composing them into the complete proof.

view this post on Zulip Scott Morrison (Mar 10 2018 at 22:01):

Hmm... okay, on the 3rd reading I still don't understand that. :-) (Simon's comment about local constants.)

view this post on Zulip Mario Carneiro (Mar 10 2018 at 22:01):

I don't have any good suggestions for your rewrite issue. One possibility is to use conv or ext_simplify_core to recurse into all subterms and try rw on each of them

view this post on Zulip Kevin Buzzard (Mar 10 2018 at 22:02):

How do I do a rw in conv, by the way?

view this post on Zulip Scott Morrison (Mar 10 2018 at 22:02):

I don't actually know how conv is implemented under the hood: is it using ext_simplify_core anyway?

view this post on Zulip Kevin Buzzard (Mar 10 2018 at 22:02):

I don't mean a rw, I mean I want to replace something with something defeq

view this post on Zulip Kevin Buzzard (Mar 10 2018 at 22:03):

do I have to use whnf?

view this post on Zulip Scott Morrison (Mar 10 2018 at 22:03):

I really like these ideas. It hadn't occurred to me that I could think of conv as letting me recurse into all subterms in tactic mode.

view this post on Zulip Kevin Buzzard (Mar 10 2018 at 22:04):

I only just learnt how it worked really, it's all because of this push by Patrick to get some informal docs written.

view this post on Zulip Kevin Buzzard (Mar 10 2018 at 22:04):

I find them really enlightening

view this post on Zulip Scott Morrison (Mar 10 2018 at 22:04):

Is there any hope that I could build a pattern corresponding to the lhs of my rewrite rule, and pass that to conv, and thereby only visit the places where rw would work anyway? Or would this run into exactly the same unification caching problem?

view this post on Zulip Scott Morrison (Mar 10 2018 at 22:08):

Okay, answering my own question: no, you can't pass patterns to conv, it does indeed run into this same problem.

view this post on Zulip Scott Morrison (Mar 10 2018 at 22:11):

@Kevin Buzzard, here are two examples of using rw inside conv, solving the problem I started this thread with:

example : [1, 1, 2] = [2, 1, 2] :=
begin
conv { congr, rw [baz] },
end
example : [1, 1, 2] = [1, 2, 2] :=
begin
conv { congr, congr, skip, rw [baz] },
end

view this post on Zulip Scott Morrison (Mar 10 2018 at 22:14):

I think in the end ext_simplify_core is going to be the right solution. Since I want to build up a list of all the possible rewrites, I think it makes sense to build it up during the run of ext_simplify_core, rather than making multiple calls into conv, each one looking at a different piece of the expression.

view this post on Zulip Scott Morrison (Mar 10 2018 at 22:15):

(Please tell me if that doesn't make sense!)

view this post on Zulip Scott Morrison (Mar 10 2018 at 22:16):

Thank you, everyone, for the extremely helpful suggestions, as usual!

view this post on Zulip Simon Hudon (Mar 10 2018 at 22:18):

Thanks for the interesting challenges :smile:

view this post on Zulip Kevin Buzzard (Mar 10 2018 at 22:21):

I don't even understand what this thread is about. What is ematch? Did someone write some informal docs yet?

view this post on Zulip Kevin Buzzard (Mar 10 2018 at 22:22):

I really find life easier with docs. Then I have to ask fewer questions.

view this post on Zulip Mario Carneiro (Mar 10 2018 at 22:22):

I don't think the ematch attribute is relevant to simon's example

view this post on Zulip Andrew Ashworth (Mar 10 2018 at 22:27):

ematch: you can try reading Leo's paper.... https://link.springer.com/chapter/10.1007/978-3-540-73595-3_13

view this post on Zulip Andrew Ashworth (Mar 10 2018 at 22:28):

it's a little arcane unless you're really into the theory though

view this post on Zulip Andrew Ashworth (Mar 10 2018 at 22:33):

aha! something better: http://yices.csl.sri.com/papers/cav2007.pdf

view this post on Zulip Andrew Ashworth (Mar 10 2018 at 22:34):

seems the root paper at the bottom of all this is something from the 80s: https://people.eecs.berkeley.edu/~necula/Papers/nelson-thesis.pdf

view this post on Zulip Andrew Ashworth (Mar 10 2018 at 22:36):

that said, i'm not volunteering to read everything, digest it, and then write a simple introduction to ematch :)

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 11:52):

Oh thanks! I honestly behave like a computer. I looked at what Scott had posted, didn't understand the first word (ematch) and then just crashed and stopped reading (I was trying to get three kids to bed as well as reading chat). I see that this thread is well within my grasp now. Sorry for earlier noise.

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 11:56):

So Scott what are you actually trying to do in the long run here? What is the problem with just writing a tactic which tries every possible rw on some term using some set of terms which are equalities but with metavariables? Is that what you want? Isn't that exactly the sort of thing one can write a tactic for? Or is the point that you want to do it without writing a tactic?

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 12:03):

And a related question. Is Sebastian saying "there is something written in C++ which doesn't do what you want, but you could write a version in Lean which does do what you want but it would be slow"? And how does this contrast with Leo's Lean 4 plan -- goal #1 in fact -- of taking some stuff out of C++ and implementing it in Lean?

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 12:04):

How can this ever be a good idea? I don't understand the ramifications of this idea

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 12:07):

(deleted)

view this post on Zulip Gabriel Ebner (Mar 11 2018 at 12:10):

In Lean 4 it would be fast because you could compile it to C++ that runs as fast as the current kabstract code.

view this post on Zulip Simon Hudon (Mar 11 2018 at 19:35):

How will that work? Will Lean run the definitions of the current file in the VM and at the end compile the whole file to C++ to accelerate the verification of the next files?

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:08):

I don't mean a rw, I mean I want to replace something with something defeq

ooh I can use change.

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:08):

theorem H3 : 3 + 2 = 1 + 4 := begin
conv begin
to_lhs,
change 1 + 4,
end
end

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:10):

Great! Do you have a slightly more realistic example?

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:10):

I did have the other day!

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:10):

(not necessarily super realistic, like the ones I put in the conv doc)

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:10):

I had a goal of the form X=Y but Y had terms in it of the form \<a,_\>

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:12):

so I couldn't use show to replace X on LHS with something defeq because cut and paste wouldn't work for RHS. So I used conv and then realised I didn't know how to do show in conv mode and ended proving some auxiliary lemma with rfl and doing a rw. This way is much cooler :-)

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:12):

I was going to update the conv doc myself but then I realised you owned it rather than mathlib

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:12):

What?

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:13):

I don't own anything here

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:13):

My PR was merged into mathlib

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:13):

Please feel super free to update it

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:14):

wait I can't find it anywhere

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:14):

https://github.com/leanprover/mathlib/blob/master/docs/extras/conv.md

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:14):

or follow links from the main README

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:14):

Starting with link "extra Lean documentation"

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:14):

maybe I don't understand git. I thought I just pulled

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:15):

oh maybe I really don't understand git. I am pulling from my own fork not from mathlib

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:15):

(because it's no about mathlib)

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:15):

Do you have a git remote pointing to the main repo?

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:15):

git add remote upstream https://github.com/leanprover/mathlib.git

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:15):

$ git remote -v
leanprover  https://github.com/leanprover/mathlib.git (fetch)
leanprover  https://github.com/leanprover/mathlib.git (push)
origin  git@github.com:kbuzzard/mathlib.git (fetch)
origin  git@github.com:kbuzzard/mathlib.git (push)

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:16):

I need to pull harder somehow

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:16):

I am only pulling from origin

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:16):

Then git pull leanprover master

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:16):

you called leanprover what is traditionnaly called "upstream"

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:16):

great, I now have extras.

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:17):

Now git checkout -b docs-conv-change

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:18):

Do your modifications, git commit -a, git push. Then git will complain and tell you what to type instead of git push

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:18):

(with git push set-upstream in it)

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:18):

why won't it just push to my fork?

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:18):

then go to either upstream mathlib or your fork on Github and you'll be invited to open a PR

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:19):

Because it's a new branch

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:19):

a branch that is not on github yet

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:19):

(yeah, the word upstream is used in a slightly different sense in set-upstream)

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:28):

git push just pushed to my fork

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:28):

yes

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:28):

now you can PR

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:29):

except that you skipped creating a new branch...

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:29):

yeah :-/

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:29):

This is bad

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:29):

oh :-)

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:30):

You can't have several open PR with this non-branching strategy

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:30):

I have loads of my own WIPs all with no branch either.

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:30):

I will google and sort it out. Let's not spam here.

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:31):

Then you can't even PR since it would PR the WIP at the same time

view this post on Zulip Kevin Buzzard (Mar 12 2018 at 07:38):

Hmm. I can't deal with Mario's comments on my docs because travis hasn't finished building.

view this post on Zulip Mario Carneiro (Mar 12 2018 at 07:53):

I think you can more or less ignore travis builds for a doc change

view this post on Zulip Patrick Massot (Mar 12 2018 at 07:54):

Quoting Mario for @Kevin Buzzard

Re: PRs, I'm okay with docs of any kind. My recommendation is to try to write them with an authoritative locution style; I will let you know if you say false things. If you don't know something, leave it out, say you don't know in the doc, or ask about it here and then put in whatever you find out.

view this post on Zulip Mario Carneiro (Mar 12 2018 at 07:55):

(Of course, there is no guarantee that your PR won't (apparently) "break the build", since our current peculiar setup that pulls from a moving target lean nightly means that if Leo decides to break mathlib at the same time your PR will get the blame.)

view this post on Zulip Patrick Massot (Mar 12 2018 at 07:56):

I think you could edit a few sentences to conform to this recommendation

view this post on Zulip Mario Carneiro (Mar 12 2018 at 07:57):

I tried to respond to Kevin's parentheticals in the PR comments, so hopefully they will be addressed in the next revision


Last updated: May 18 2021 at 16:25 UTC