squeeze_simp

Stream: general

[Johan Commelin]

@Simon Hudon To what extend do you think sed and lean could cooperate to automatically turn every simp into a squeeze_simp, and then every squeeze_simp into a simp only? Can we automate Kenny?

[Simon Hudon]

But we like Kenny!

[Simon Hudon]

I was thinking along those lines but I was thinking of adding a feature to the emacs Lean mode. I'm not how I would do it for VS code though. Do you know how to script it?

[Johan Commelin]

I don't know anything about VScode

[Johan Commelin]

But couldn't this just be a CLI-only thing?

[Johan Commelin]

For other purposes the output of squeeze_simp is already very useful.

[Patrick Massot]

Can't we use a hole command here again?

[Mario Carneiro]

you still have to click on a hole command

[Johan Commelin]

Exactly

[Mario Carneiro]

indeed, you have to manually edit the file to put a hole in in the first place

[Johan Commelin]

I want sed to "click" on the hole command.

[Patrick Massot]

Oh you mean you want this for batch processing?

[Simon Hudon]

The difficult thing about using something like sed is detecting the end of the input squeeze_simp

[Simon Hudon]

But I guess we could output it in Lean

[Simon Hudon]

@Patrick Massot exactly

[Patrick Massot]

Sorry I read too quickly the beginning of this thread (I'm fighting dependent rw)

[Simon Hudon]

@Mario Carneiro has shown us how useful awk can be in these situations. Do you think if we output the beginning line and column number of the input, the ending line and column number of the input and the replacement, we can get awk to go in there and do the replacement? You'd probably also have to go from the last to the first if you want to do it in one go so that the line numbers don't get invalidated.

[Johan Commelin]

Sure, that should definitely be possible

[Johan Commelin]

I guess squeeze_simp can get access to its location in the file via some tactic_state magic, right?

[Johan Commelin]

Or you make squeeze_simp output a patch (-;

[Johan Commelin]

Then we can just commit it, and git takes care of the rest :lol:

[Simon Hudon]

I just looked into the patch file format. It seems like more work to format than to just do it ourselves

[Johan Commelin]

Ok, so how about your suggestion, with line+col numbers

[Simon Hudon]

I think the best bet is to use awk but I'll have to learn it

[Simon Hudon]

Right now I'm experimenting with emacs to see if I can get a nice first approximation

[Johan Commelin]

awk is not hard. Also, I wouldn't mind helping you.

[Johan Commelin]

We could use sed to squeeze_simpify a .lean file. After that, we run lean --make on the file, and capture the stdout.

[Johan Commelin]

If squeeze_simp can produce output of the form line:column:replacement_text I think we can take it from there.

[Simon Hudon]

I was thinking of a format like this:

84:23:
86:0:
--- BEGIN ---
simp only [perm_cons, multiset.cons_coe, iff_self, multiset.coe_eq_coe, multiset.quot_mk_to_coe'']
--- END ---

[Johan Commelin]

unix prefers to keep everything on 1 line.

[Simon Hudon]

In that case, how about line0:col0:line1:col1:replacement_text?

[Johan Commelin]

Looks good

[Johan Commelin]

Unless we want to anticipate multiline replacement texts

[Simon Hudon]

That's what I'm looking at now. The replacement is sometimes multiline but there's no real reason to be. I'll restrict it to one line and let the user reformat if needed

[Johan Commelin]

There is no "user" if we run this in batch mode over 25 files.

[Johan Commelin]

But we can write a smart awk script

[Johan Commelin]

It can try to reformat that line, breaking on suitable ,

[Simon Hudon]

That's tricky because it might not be alone on its line

[Johan Commelin]

I can compute the old line length, and the new one, etc...

[Johan Commelin]

It definitely makes a trivial thing a lot harder

[Simon Hudon]

Let's leave it for the "future work" section

[Simon Hudon]

It might become necessary to have a Lean code formatter which would make all of that good work redundant

[Johan Commelin]

Yep, sounds good

[Simon Hudon]

This proof engineering stuff is so funny. We're tweaking eternal truths :P

[Simon Hudon]

As impatient as I get with Lean and mathlib, it's pretty great that it finds my mistakes faster than my supervisor :D

[Bryan Gin-ge Chen]

Are there other "tactics with output" where this kind of tooling would also be useful? Maybe tidy?

[Mario Carneiro]

tidy already makes output

[Johan Commelin]

I'll be reading a bit of Milne to my kids... see you guys soon!

[Simon Hudon]

Have fun!

[Bryan Gin-ge Chen]

Indeed, what I mean is the output format being discussed here something we should also consider for e.g. tidy?

[Simon Hudon]

That could be useful. It might be more useful for tidy to have it tied into the IDE because you probably don't use tidyen masse

[Gabriel Ebner]

Where are you printing the replacement text? Trace messages?

[Simon Hudon]

Yes exactly

[Gabriel Ebner]

It's pretty easy to hook them up in vscode: in the extension, you just need to return a list of code actions. Then you can execute these replacements with ctrl+. (similar to holes, which are also implemented using code actions in the extension).

[Simon Hudon]

Emacs gives the line and column of the command issuing the trace. Does VS code also do the same?

[Gabriel Ebner]

A few suggestions for the format: it should not occur by accident (in a simp trace e.g.). And it would be nice to have a (textual) description for the replacement (vscode shows this in the dropdown). Ideally also the kind of code action, e.g. vscode can apply all quickfixes in a given file automatically.

[Gabriel Ebner]

We have access to the same position information, yes. However it only includes the start position of the tactic unfortunately.

[Simon Hudon]

Does it run them backward so that the line numbers remain valid?

[Gabriel Ebner]

Good question. I don't really know. If we do one-line replacements then it shouldn't matter too much.

[Simon Hudon]

In the parser cur_pos can give me an arbitrary position. I'm putting it at the end and it gives me a good approximation

[Mario Carneiro]

Ooh, this is nice. Can we just get a generic hook for writing things from lean?

[Sebastien Gouezel]

I got a strange squeeze_simp behavior, where the trace output does not has the same effect as the original one. The example is as follows (in a complete lattice):

theorem Inf_sup_Inf : Inf s ⊔ Inf t = Inf ((λp : α × α, p.1 ⊔ p.2) '' (set.prod s t)) :=
begin
  apply le_antisymm,
  { squeeze_simp,
    sorry },
  { sorry }
end

After squeeze_simp, the goal is

∀ (b x x_1 : α), x ∈ s → x_1 ∈ t → x ⊔ x_1 = b → Inf s ≤ b ∧ Inf t ≤ b

But if I copy the trace formula (hey, I never noticed that it looks like real math:) given by squeeze_simp, i.e.,

simp only [and_imp, set.mem_image, set.mem_prod, lattice.le_Inf_iff,
               exists_imp_distrib, lattice.sup_le_iff, prod.exists],

then I get the double goal

(∀ (b x x_1 : α), x ∈ s → x_1 ∈ t → x ⊔ x_1 = b → Inf s ≤ b) ∧
    ∀ (b x x_1 : α), x ∈ s → x_1 ∈ t → x ⊔ x_1 = b → Inf t ≤ b

Any idea for the reason of this behavior?

[Simon Hudon]

Can you open an issue and put up a MWE? I'll look into it.

[Sebastien Gouezel]

Done.

[Simon Hudon]

If you remove lattice.sup_le_iff from the list, you get the same effect as not having simp only. I don't get why squeeze_simp suggests it. I'll keep working on it

[Mario Carneiro]

I'm not sure it is worth trying for 100% fidelity in translating squeeze_simp to an appropriate simp only. The commands are complicated and almost nondeterministic, so I'm not at all surprised that there are edge cases where it doesn't work, and also suggested rewrites that don't need to be in the rewrite list. You should take the output of squeeze_simp as a base for revision rather than an actual reliable representation of what was used.