WittVector saga

Stream: mathlib4

[Damiano Testa]

The file RingTheory.WittVector.IsPoly is available for porting. A large portion of this file develops gost_calc and ghost_simp, but never uses these tactics. I am willing to try to port these tactics: which one do you think is the simplest file that uses the tactics?

ping @Johan Commelin @Rob Lewis, as the listed authors of the file.

[Johan Commelin]

Probably src/ring_theory/witt_vector/mul_p.lean. It is only 81 lines.

[Damiano Testa]

Ok, I'll port what is not tactic in is_poly and will then use mul_p as a guinea pig for developing the tactics.

[Damiano Testa]

I created !4#4851, porting RingTheory.WittVector.IsPoly. There are only a couple of sorrys left and all the tactic material commented out. If anyone feels like fixing the, possibly easy, sorrys, please, go ahead!

[Damiano Testa]

In the meanwhile, I will take a look at ring_theory/witt_vector/mul_p.lean and see whether I can implement the tactics ghost_calc and ghost_simp of RingTheory.WittVector.IsPoly.

[Damiano Testa]

Looks like src/ring_theory/witt_vector/verschiebung.lean might be a better test for the tactics: mul_p does not use any new tactic!

Also, since the tactics ghost_calc and ghost_simp are not actually used in the file RingTheory.WittVector.IsPoly, it is probably a better idea to port the whole file without any tactics and then implement the tactics once the file is ported.

[Damiano Testa]

The file RingTheory.WittVector.IsPoly is ready for review! For the moment, I commented out all meta code, fixed all the sorries and created a new "Attributes" file. The attributes currently do nothing other than allowing @[attribute] to work. Moreover, as far as I understand, attributes cannot be defined in the file where they are used, so it was either a matter of creating a new file or of putting the attributes in an earlier file.

[Johan Commelin]

@Damiano Testa thanks! I kicked it on the queue

[Damiano Testa]

Great! Seems to have been approved twice!

[Xavier Roblot]

I am currently working on RingTheory.WittVector.Frobenius and it is using ghost_simp and ghost_calc a a few places. Are these tactics being ported or should I try to do without them?

[Damiano Testa]

Yes, my plan was to port them, but only once they started being needed. I guess that now is the time, but I probably won't have much time until Monday...

[Damiano Testa]

The attributes should "work", in the sense that I registered them, but I left the tactics unported, since they were not used in the file where they were defined (which was ...Witt...IsPoly.

[Xavier Roblot]

Great! I'll do the parts of this file that doesn't need these tactics in the meantime.

[Damiano Testa]

I have been trying to port the ghost tactics, but have had little success. Also, over the coming two weeks, I will have little Lean time and lots of administrative chores. I have not given up on porting these tactics, but realistically, I won't have them working before sometime in July.

@Xavier Roblot @Moritz Firsching

[Damiano Testa]

If someone else wants to take over, feel free to do so.

[Xavier Roblot]

I guess this can wait a bit. Thanks for working on this!

[Johan Commelin]

Anyone with meta skills who wants to take a look at these tactics? If needed, I can try to explain the maths side of things.
In the near future these tactics will probably block the longest unported chain.

[Moritz Doll]

as for ghost_simp, is it something along the lines of the following?

macro_rules
| `(tactic| ghost_simp $[[$simpArgs,*]]?) =>
  let args := simpArgs.map (·.getElems) |>.getD #[]
  `(tactic|
    intro
    simp (config := {decide := false}) only [ghost_simps, ← sub_eq_add_neg, $args,*] )

(essentially c&p from zify)

[Johan Commelin]

@Scott Morrison and I did a hacking session this morning (after Kyle pushed some stuff last night).
The result is https://github.com/leanprover-community/mathlib4/pull/4897

[Johan Commelin]

It seems that ghost_calc and ghost_simp are now working quite well

[Scott Morrison]

And happily we discovered that the @[is_poly] attribute is no longer required: it used to generate additional instance declarations, but type class search can now generated these unaided. A Lean 4 win!

[Xavier Roblot]

So I have been using the new tactics (thanks!) for the port of RingTheory.WittVector.Frobenius #4887 but I am getting some errors while using ghost_calc

failed to synthesize instance
  IsPoly₂ p fun {R} [CommRing R] x y ↦ frobeniusFun (x * y)

failed to synthesize instance
  IsPoly₂ p fun {R} [CommRing R] x y ↦ frobeniusFun x * frobeniusFun y

The goal here is

 ∀ (x y : 𝕎 R), frobeniusFun (x * y) = frobeniusFun x * frobeniusFun y

I have been looking at functions around docs#WittVector.mulIsPoly₂ but I have been not successful so far...

[Thomas Murrills]

Nice!! !4#5520 is nearly there, with ghost_calc also still giving one last error here even with the new work—hopefully there's now a much smaller gap to cross! :) The issue is synthesizing IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x.

It seems lean is struggling to find its way up to IsPoly₂ then back down to IsPoly via IsPoly₂.diag. For a simpler example, consider

#synth IsPoly p fun _ _ x => -x + -x -- fails

Interestingly,

#synth IsPoly p fun _ _ x => -x + x -- succeeds, and relies on IsPoly₂.comp via negIsPoly, idIsPolyI')
#synth IsPoly p fun _ _ x => x + -x -- fails

This instance is constructable "by hand" as e.g. #check @IsPoly₂.diag p _ (IsPoly₂.comp (h := fun _ _ => (·+·)) (f := fun _ _ => (-·)) (g := fun _ _ => (-·))), so we have all the instances—we just can't see them via TC search. I'm not sure what the solution is here, though.

(I've marked this PR help-wanted in case anyone wants to take over, and won't be working on it any further for the next several hours.)

[Johan Commelin]

@Xavier Roblot you'll have to make all occurences of IsPoly into instances instead of theorems. In particular:
https://github.com/leanprover-community/mathlib4/pull/4887/files#diff-e4a6458fbec116d2b2426060db7aa7cce13c4fa07f890a20cdccf142040607afR235

[Thomas Murrills]

(Hmm, thinking about it, one option is to help lean along by introducing

instance diag_comp_isPoly {h f g} [IsPoly₂ p h] [IsPoly p f] [IsPoly p g] :
    IsPoly p fun _R _Rcr x => h (f x) (g x) := @IsPoly₂.diag _ _ IsPoly₂.comp

though I'm a bit wary of introducing instances like this. Lean then has no problem synthesizing any of the above (including the "real-world" instance), although there's still some work to be done later on in that theorem even when including this.)

[Xavier Roblot]

#4887 is ready now

[Johan Commelin]

@Xavier Roblot left a review and a bors d+

[Johan Commelin]

@Thomas Murrills it could be that Scott and I decided a bit too quickly that TC could handle all of this. For now I suggest that you add the required instance by hand in the proof that needs it. Together with a porting note.

[Johan Commelin]

We can then port 3 more files, and look at the total damage.

[Thomas Murrills]

Ok, sounds good!

[Thomas Murrills]

I'll take back the help-wanted :)

[Thomas Murrills]

Ok, !4#5520 builds and just needs to lint; it's now awaiting-review and awaiting-CI :)

[Kyle Miller]

Johan Commelin said:

It seems that ghost_calc and ghost_simp are now working quite well

I'm happy to see that the ghost_calc implementation actually made it through the infer_instances like I hoped it would, and it figures that it still needed a little tweaking beyond that point :smile:

[Thomas Murrills]

Ok, I got WittVector.Identities building (waiting for CI on !4#5527)! :) This was a bit of a difficult one for TC search unfortunately; ghost_calc was used only twice but needed all instances provided.

There was also another issue to report: simp only [] was necessary before ghost_calc in both cases for it to recognize the goal—otherwise it errors with ghost_calc expecting target to be an equality of `WittVector`s. From manual inspection it seems as though it's just performing beta reduction.

[Thomas Murrills]

Ah, I see @Johan Commelin already merged it, nice! :D (and that I left a stray LibrarySearch import in there, whoops. Thanks for catching that!!)

[Thomas Murrills]

Also, just to record this publicly somewhere for when we get the chance, else I'll forget: I think frobenius_zmodp in WittVector.Frobenius ought to be frobenius_zmodP

[Johan Commelin]

Yeah, maybe ghost_calc should just start of with a simp only [].

[Johan Commelin]

Thomas Murrills said:

Also, just to record this publicly somewhere for when we get the chance, else I'll forget: I think frobenius_zmodp in WittVector.Frobenius ought to be frobenius_zmodP

Probably consistent. But I still find those capital ps very weird.

[Thomas Murrills]

They are a bit weird! But I think better than the alternative, which might consist of staring at something like charp for 30 seconds before realizing it's not a word :upside_down:

[Thomas Murrills]

(I also personally probably don't find them as weird simply because I don't have the mathlib3 history, and my eyes automatically look for the upperCamelCase boundaries for semantic content. so a string of lowercases stands out more.)

[Johan Commelin]

Ideally we would come up with names that didn't hardcode variable conventions into them

[Kyle Miller]

Thomas Murrills said:

There was also another issue to report: simp only [] was necessary before ghost_calc in both cases for it to recognize the goal—otherwise it errors with ghost_calc expecting target to be an equality of `WittVector`s. From manual inspection it seems as though it's just performing beta reduction.

If you change getTarget'' to getTarget' it might be enough

[Kyle Miller]

I chose the more conservative one first. One prime does whnf

[Johan Commelin]

aha, yeah, I think we want a bit more whnf