rewrite occs

Stream: general

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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?

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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

[Sebastian Ullrich]

(Don't ask me why :) )

[Scott Morrison]

oh...

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

That sucks (for my purposes)...

[Scott Morrison]

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?

[Scott Morrison]

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.

[Simon Hudon]

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.

[Sebastian Ullrich]

Yes. It just won't be very fast.

[Simon Hudon]

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

[Scott Morrison]

I see: reimplement kabstract in Lean?

[Scott Morrison]

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.

[Simon Hudon]

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

[Scott Morrison]

@Sebastian Ullrich ? :-)

[Sebastian Ullrich]

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

[Scott Morrison]

Okay!

[Scott Morrison]

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

[Scott Morrison]

(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.)

[Sebastian Ullrich]

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?

[Sebastian Ullrich]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Kevin Buzzard]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Sebastian Ullrich]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

This is terrible. :-)

[Sebastian Ullrich]

Well, not if you create new mvars like Simon suggested

[Scott Morrison]

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.

[Scott Morrison]

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

[Simon Hudon]

No worries

[Kevin Buzzard]

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

[Simon Hudon]

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

[Sebastian Ullrich]

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.

[Scott Morrison]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Scott Morrison]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

do I have to use whnf?

[Scott Morrison]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

I find them really enlightening

[Scott Morrison]

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?

[Scott Morrison]

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

[Scott Morrison]

@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

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Simon Hudon]

Thanks for the interesting challenges :smile:

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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?

[Kevin Buzzard]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

(deleted)

[Gabriel Ebner]

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

[Simon Hudon]

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?

[Kevin Buzzard]

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

ooh I can use change.

[Kevin Buzzard]

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

[Patrick Massot]

Great! Do you have a slightly more realistic example?

[Kevin Buzzard]

I did have the other day!

[Patrick Massot]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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 :-)

[Kevin Buzzard]

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

[Patrick Massot]

What?

[Patrick Massot]

I don't own anything here

[Patrick Massot]

My PR was merged into mathlib

[Patrick Massot]

Please feel super free to update it

[Kevin Buzzard]

wait I can't find it anywhere

[Patrick Massot]

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

[Patrick Massot]

or follow links from the main README

[Patrick Massot]

Starting with link "extra Lean documentation"

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Patrick Massot]

(because it's no about mathlib)

[Patrick Massot]

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

[Patrick Massot]

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

[Kevin Buzzard]

$ 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)

[Kevin Buzzard]

I need to pull harder somehow

[Kevin Buzzard]

I am only pulling from origin

[Patrick Massot]

Then git pull leanprover master

[Patrick Massot]

you called leanprover what is traditionnaly called "upstream"

[Kevin Buzzard]

great, I now have extras.

[Patrick Massot]

Now git checkout -b docs-conv-change

[Patrick Massot]

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

[Patrick Massot]

(with git push set-upstream in it)

[Kevin Buzzard]

why won't it just push to my fork?

[Patrick Massot]

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

[Patrick Massot]

Because it's a new branch

[Patrick Massot]

a branch that is not on github yet

[Patrick Massot]

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

[Kevin Buzzard]

git push just pushed to my fork

[Patrick Massot]

yes

[Patrick Massot]

now you can PR

[Patrick Massot]

except that you skipped creating a new branch...

[Kevin Buzzard]

yeah :-/

[Patrick Massot]

This is bad

[Kevin Buzzard]

oh :-)

[Patrick Massot]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Patrick Massot]

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.

[Mario Carneiro]

(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.)

[Patrick Massot]

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

[Mario Carneiro]

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