missing tactic port

Stream: mathlib4

[Arien Malec]

I have a ported file that depends on a local tactic with a meta

meta def rbtree.default_lt : tactic unit :=
`[apply has_lt.lt]

used like this: (lt : α → α → Prop . rbtree.default_lt)

What's the Lean4 approach for a default parameter value?

[Arien Malec]

So, digging, it looks like has_lt is now spelled LT but subbing the seeming equivalent statement lt : α → α → Prop := by apply LT.lt gets invalid auto tactic

[Arien Malec]

I'm just not sure if the goal is for the the comparator to be pluggable, or if the goal is to implicitly constrain α to be of class LT?

[Arien Malec]

Or maybe the goal is: if I have an lt, use that, otherwise require the α to be of typeclass LT and use the native lt?

[Scott Morrison]

This tactic is only used to supply an auto_param. In Lean 4, you can use tactics in the default value, instead of using an autoparam.

[Scott Morrison]

i.e. replace . rbtree.default_lt in the structure definition with := by apply LT.lt?

[Scott Morrison]

Oh, hmm, you tried that. What's your branch?

[Arien Malec]

PR mathlib4#611, arienmalec/port_rbtree_init

[Jireh Loreaux]

@Arien Malec : that's mathlib4#611, not #611

[Arien Malec]

Gotcha -- Zulip defaults to mathlib PRs..

[Jireh Loreaux]

For now, yes. If you look in the "Organization Settings" menu you can see how the various linkifiers are expanded.

[Kevin Buzzard]

More details:

def RBTree (α : Type u)
    (lt : α → α → Prop := by apply LT.lt) :
    Type u :=
  { t : RBNode α // t.WellFormed lt }

(in file Mathlib.Data.RBTree.Init on the branch above) gives error invalid auto tactic, identifier is not allowed on LT.lt

[Arien Malec]

@Ruben Van de Velde notes that Std has an RBMap so probably the call here is to deprecate RBTree and unwind the dependencies in the port. (The RBMap implementation punts on the fancy autoparam stuff, and just has you pass a comparator...

[Arien Malec]

From what I could see, the dependencies in mathlib are through data.tree, and all data.tree does is allow conversion from an rbtree

[Arien Malec]

It also blocks data.list.defsbut all that's done there is convert to an rbtree

[Arien Malec]

Also used in ring2 which is separately ported.

[Scott Morrison]

Yes, sorry, should have thought to say this earlier. I don't think this file should be ported at all. :-)

[Arien Malec]

Hmm. all data.tree seems to do is be used in tactics and testing -- not sure how it even got pulled into one of the dependency graphs.

[Arien Malec]

When I look at the graph from data.tree it's basically everything, but comes in through the tactic metaverse.

[Arien Malec]

eg, linarith via cancel_denoms which is the only direct dependency.

[Arien Malec]

I'm doing the --exclude-tactics thing but maybe things are getting pulled in transitively...

leanproject import-graph --from data.tree --exclude-tactics data.tree.pdf --port-status

[Scott Morrison]

Yes, I made a change so that when --exclude-tactics deletes a tactic node in the graph, it adds all "grandparent" edges.

[Scott Morrison]

Perhaps this was a bad idea and has led you astray. :-)

[Scott Morrison]

Perhaps just port as mostly empty file: just a comment to say that the code is no longer needed because it was only use in tactics, which are being reimplemented.

[Arien Malec]

I think it might be better to remove nodes that have only a single edge from tactic/meta

[Scott Morrison]

It's not really clear what the algorithm should be. What is there are theory files that are genuinely needed, but only imported in matlib3 transitively via tactics files?

[Mario Carneiro]

well, we'd have to run that "needed" script again...

[Mario Carneiro]

you could try removing all tactic files including their edges in and out from the graph, but I suspect that there is quite a lot of "cheating" with declarations being transitively pulled in for stuff like data.list.basic, which is used by a downstream file which only does e.g. import tactic.linarith

[Mario Carneiro]

Regarding this particular file, I suggest the following course of action:

Mario Carneiro said:

I think a suitable "port" of the data.rbtree is: make a list of all the theorems about rbtree that don't yet exist in Std.Data.RBMap, open an issue for them on std4, and then remove everything from the module except for #aligns if possible (if the types are too different, just leave them unaligned). Std.Data.RBMap intends to completely replace that directory.

[Arien Malec]

Have pushed part 2, with deprecate statements as well.

[Arien Malec]

Will go through the RBMap theorems

[Arien Malec]

Looks like Std heavily covers the well-formed invariants associated with insert/delete, but mathlib additionally covers the behavior or searching and ordering

[Mario Carneiro]

yes, you should translate the mathlib statements to something about RBMap, then put them in the mathlib4 file for now (it's okay to comment out / sorry the proofs if the originals don't work) and open an issue to move them to std4

[Mario Carneiro]

we don't want to just delete the file if that means some theorems get lost without there being a replacement or an issue tracking said replacement

[Arien Malec]

No theorems in init.lean; insert.lean covers the wellfoundedness work that's already in Std, so it's basic.lean, find.lean and min_max.lean that want to be saved.

[Mario Carneiro]

Could you translate the statements into actual lean 4 theorems with sorry? That's the equivalent of porting work for these files

[Arien Malec]

K