Remove instance from abbrev type

Stream: mathlib4

[Moritz R]

In Clausal FOL, one defines clauses to be multisets of literals.
However when doing

/-- A Clause (over Function symbols F and variables alpha) is a multiset of Literals. -/
abbrev Clause (F : ℕ → Type*) (α : Type*) := Multiset (Literal F α)

clauses inherit the subset-with-counts-ordering of Multisets. This is very unfortunate, since
clauses are typically ordered by extending the order on literals by the Dershowitz-Manna ordering extension which is already in mathlib (but not an instance for multisets ofc).
I tried making my abbrev a def, however i find myself basically duplicating the whole mathlib library on multisets, just to avoid this instance.

Is there any way i can kill the existing ordering instance for Clause?

[Yury G. Kudryashov]

AFAIK, no. You can try to write a metaprogram that will copy API for you.

[Edward van de Meent]

You can write attribute [-instance] foo, i believe...

[Edward van de Meent]

But then you won't get the order on Multiset either

[Moritz R]

Edward van de Meent said:

But then you won't get the order on Multiset either

If I modify the ordering behaviour of the multiset type, then the chances that anything ever gets merged into any library instantly drop to 0.
For good reason

[Moritz R]

I stumbled across this very recent work on Lean by Leo.
In particular the sentence

**We are decoupling whether a declaration is available for type class resolution from its transparency status**

looks like it might become a possibility to have this as a feature soon?

[Moritz R]

I hope someone in the know can comment on this

[Matthew Ballard]

See how far moving the instances to a separate file gets you

[Violeta Hernández]

I'd argue that you should just make a new def for what you're doing, and create maps to convert between multisets and clauses.

[Moritz R]

Matthew Ballard schrieb:

See how far moving the instances to a separate file gets you

How should moving the instance to a separate file and then importing that help in any way?

[Moritz R]

Violeta Hernández schrieb:

I'd argue that you should just make a new def for what you're doing, and create maps to convert between multisets and clauses.

Well the conversion map would just be the typed identity function in both directions.
If i now want to use all the nice api on multisets, like .cons, +, insert, singleton, 0, member
i need to define these via the conversion on Clause F alpha. But now i have zero lemmas about them and tactics like simp and grind will prove nothing about them. So then i have to copy all the theorems about these definitions (the proofs become exacts ofc).

[Moritz R]

How is this different to saying "duplicate all the code"?

[Yury G. Kudryashov]

You can use metaprogramming to do this for you.

[Yury G. Kudryashov]

But Lean is becoming more and more insistent on instances being canonical for a type.

[Moritz R]

Yury G. Kudryashov schrieb:

You can use metaprogramming to do this for you.

I dislike the thought of having a whole library of invisible lemmas. Is there any examples i can look at?

[Aaron Liu]

for example docs#commandDeclare_uint_theorems__

[Yury G. Kudryashov]

to_additive generates half of theorems about groups. You can have something like

#multiset2clause Multiset.cons Multiset.cons_inj_left -- more names

[Moritz R]

If i would do this automatically i would want all of the lemmas from Multiset to transfer. This is in the hundreds of theorems.

[Moritz R]

And this gets pretty complicated pretty quickly, since proofs and statements will expect the wrong <= instance to be there

[Moritz R]

and some stuff might even be proven using the wrong <= only in the proof, not in the statement

[Jovan Gerbscheid]

Note that the to_additive machinery is now fully extensible. So you can make your own attribute to_clause and use it in the same way that to_additive is used.

(Unfortunately, you'll need to copy around 60 lines of code from Mathlib.Tactic.Translate.ToAdditive. This may be reduced in the future)

[Jovan Gerbscheid]

On the other hand, how bad would it be to scope the order instance on Multiset? That would probably be an easy solution.

[Violeta Hernández]

Moritz R said:

Violeta Hernández schrieb:

I'd argue that you should just make a new def for what you're doing, and create maps to convert between multisets and clauses.

Well the conversion map would just be the typed identity function in both directions.
If i now want to use all the nice api on multisets, like .cons, +, insert, singleton, 0, member
i need to define these via the conversion on Clause F alpha. But now i have zero lemmas about them and tactics like simp and grind will prove nothing about them. So then i have to copy all the theorems about these definitions (the proofs become exacts ofc).

This is what we do elsewhere in the library (docs#OrderDual, docs#Tropical, docs#Lex) and I think it works well. If you teach simp about how your casting functions interact with the functions defined on the aliased type, it can get a lot done.

[Violeta Hernández]

An alternative would just be to use the type of multisets and keep Multiset.IsDershowitzMannaLT as a non-instance relation. Depending on what you're doing this might be easier.

[Eric Wieser]

I think the best option would be to write

structure Clause (F : ℕ → Type*) (α : Type*) where literals : Multiset (Literal F α)

[Eric Wieser]

Then you can add the order instance you want by pulling back across literals

[Moritz R]

Violeta Hernández schrieb:

An alternative would just be to use the type of multisets and keep Multiset.IsDershowitzMannaLT as a non-instance relation. Depending on what you're doing this might be easier.

All of mathlibs order lemmas only fire on seeing a LT instance. Having an ordering without a LT instance is extremely painful

[Moritz R]

This both applies to my definition of clauses and to Multiset.IsDershowitzMannaLT in Mathlib

[Moritz R]

Jovan Gerbscheid schrieb:

On the other hand, how bad would it be to scope the order instance on Multiset? That would probably be an easy solution.

I think this would be reasonable. Then Mathlib could also have a scoped instance for Multiset.IsDershowitzMannaLT and i can have my orderings on Clause.

[Aaron Liu]

this dershowitz manna ordering extension seems similar to docs#Relation.CutExpand

[Moritz R]

oh indeed, CutExpand seems to be equivalent to the (currently private) oneStep relation defined in the dershowitz file

[Moritz R]

and the DM ordering is proven to be the transitive closure of oneStep

[Violeta Hernández]

I wonder if we could get an AI or something to look for files duplicating work in Mathlib...

[Violeta Hernández]

Violeta Hernández ha dicho:

An alternative would just be to use the type of multisets and keep Multiset.IsDershowitzMannaLT as a non-instance relation. Depending on what you're doing this might be easier.

We make use of the equivalent (?) Multiset.cutExpand on the CGT repo without making it an instance, and it seems to work fine.

[Moritz R]

No, cutexpand isn't an ordering yet, as it isn't transitive

[Violeta Hernández]

How nice or painful it is to work with an unbundled relation largely depends on how many properties it has. I'd say that a well-founded partial order that doesn't interact with any of the algebraic structure on the type should not be too difficult to keep unbundled.

[Moritz R]

I don't see how using mathlibs lemmas about Linear orders has to do with bundling

[Jovan Gerbscheid]

The point is that if you're working with e.g. a PartialOrder then it is easier to do so unbundled, compared to when using e.g. a LinearOrder, simply because there is less stuff that you're missing. And there are some lemmas/type classes that work in the unbundled setting, such as Std.Refl and Std.isTotal, which allow you to work with unbundled orders comfortably.