New conv tactic

Stream: new members

[Robert Maxton]

So, is there anything special to making a tactic that works in conv? Do I just put it in the converter.interactive namespace?

[Robert Maxton]

Specifically, I'm trying to write a tactic that takes a big chain of +s, turns it into a multiset.sum, and then collects like terms

[Robert Maxton]

and since I haven't done much tactic writing before I thought it'd be easiest to use it in a context where I can just hand my tactic the expression without having to "find" it first

[Robert Maxton]

(my specific use case is gathering scalar multiples of module elements, so the easiest way to find like terms is to just match against k • r, I think...?)

[Robert Maxton]

(If there's a better way to do this or an existing tactic I'm very open to that but this is what I came up with on my own)

[Eric Wieser]

I think strictly it's type should be conv unit rather than tactic unit, but they're the same type anyway

[Eric Wieser]

docs#conv

[Kyle Miller]

Robert Maxton said:

Specifically, I'm trying to write a tactic that takes a big chain of +s, turns it into a multiset.sum, and then collects like terms

Is the goal "collect like terms", or do you specifically want it written as a multiset.sum in the end?

[Robert Maxton]

Kyle Miller said:

Robert Maxton said:

Specifically, I'm trying to write a tactic that takes a big chain of +s, turns it into a multiset.sum, and then collects like terms

Is the goal "collect like terms", or do you specifically want it written as a multiset.sum in the end?

goal is to collect like terms

[Robert Maxton]

multiset.sum has the advantage of being already "orderless" -- I don't have to worry about associative rewrites

[Eric Wieser]

The advantage of list.sum is you'll only needadd_monoid not add_comm_monoid.

[Robert Maxton]

Well, whether that's an advantage or not is kind of contextual, no? For the use case that made me decide to try making this, the problem was that I was really frustrated with having to throw around somewhat-unreliable assoc_rwand add_comm just to factor large expressions, so building in the assumption that you can reorder terms in your sum is a plus in that case

[Eric Wieser]

My thinking was that it would be easier to start with the list tactic, then to build the multiset tactic on top of it

[Eric Wieser]

I think something like this works as a poor-man's list tactic:

simp only [←add_assoc],
refine (add_zero _).symm.trans _,
simp only [add_assoc],
change list.sum [_, _, _, _] -- need the right number of _

[Robert Maxton]

sorry, what's the intent of that tactic?

[Robert Maxton]

looks like it tries to cancel terms?

[Eric Wieser]

It changes a + b + c + d into [a, b, c, d].sum

[Eric Wieser]

Isn't that what you were asking for?

[Eric Wieser]

(I didn't actually test it)

[Robert Maxton]

Ah, right. Well, it's the first half of it anyway; the bit I want the conv for is actually stepping through the list looking for matching terms
I have a hacked together way to do multiset.sum but it's not particularly robust so I might swap it out for your list.sum anyway

[Robert Maxton]

but mostly I'm trying to figure out how Lean's tactic API works ^.^;

[Jireh Loreaux]

i actually just wonder whether something like noncomm_ring can do what you want immediately. (Given your other questions here I'm implicitly assuming that is your context.)

[Eric Wieser]

src#tactic.interactive.noncomm_ring is actually pretty unintelligent

[Robert Maxton]

well, for starters, what I want is more like noncomm_algebra anyway...

[Robert Maxton]

admittedly there's a certain formal similarity there but

[Kyle Miller]

Eric Wieser said:

The advantage of list.sum is you'll only needadd_monoid not add_comm_monoid.

My first thought about multset.sum was "What does that really give you? You still need to apply commutativity lemmas yourself if you want to change the order, so if you reassociate everything to be in a + (b + (c + ...)) form it doesn't seem to buy you anything." But, I think it does end up buying you something: it's like you're tagging a node in the expression with the fact that this particular additive monoid is commutative, so you don't need to look it up with typeclass search.

All list.sum records is that there's an addition with 0.

@Robert Maxton I'm curious, are you a Mathematica user? It's a long shot, but the fact you said "orderless" might be a tell.

[Robert Maxton]

oh yes, I am much more familiar with Mathematica

[Robert Maxton]

in fact I am doing this largely because Mathematica completely lacks any ability to meaningfully simplify similar products natively

[Robert Maxton]

it technically has "NonCommutativeMultiply", but it has no real definitions attached -- not even distributivity -- and unlike Lean, there's no good way to teach Simplify/FullSimplify anything new in a way that it'll actually use

[Robert Maxton]

as a result, Mathematica basically has no good way to handle symbolic operator algebras >.>

[Robert Maxton]

Kyle Miller said:

Eric Wieser said:

The advantage of list.sum is you'll only needadd_monoid not add_comm_monoid.

My first thought about multset.sum was "What does that really give you? You still need to apply commutativity lemmas yourself if you want to change the order, so if you reassociate everything to be in a + (b + (c + ...)) form it doesn't seem to buy you anything." But, I think it does end up buying you something: it's like you're tagging a node in the expression with the fact that this particular additive monoid is commutative, so you don't need to look it up with typeclass search.

All list.sum records is that there's an addition with 0.

Robert Maxton I'm curious, are you a Mathematica user? It's a long shot, but the fact you said "orderless" might be a tell.

That, and also that all the lemmas about multiset.sum already typecheck for "pulling something out of the multiset without paying attention to which entry it was"

[Robert Maxton]

my idea here is basically to use "dangerous" meta-def expression-based pattern-matching to do the factoring/gathering

[Robert Maxton]

and then prove equality after the fact using multiset.sum lemmas

[Kyle Miller]

I've used NonCommutativeMultiply for some category-theoretic manipulations. The next best thing is defining your own rewrite rules that do simplifications and wrapping those as functions (making use of the Flat attribute for the rules)

[Robert Maxton]

and so keep the assurance that it's provably true

[Kyle Miller]

It's very easy to get these things wrong in Mathematica, though... It's very happy to keep going in the face of total nonsense.

[Robert Maxton]

Kyle Miller said:

I've used NonCommutativeMultiply for some category-theoretic manipulations. The next best thing is defining your own rewrite rules that do simplifications and wrapping those as functions (making use of the Flat attribute)

yeaaaah, I'm going to be honest, I tried that and I just bounced, I did not see a good way of systematically canonicalizing something without basically rewriting Simplify myself

[Robert Maxton]

complete with probably-a-graph-search-algorithm

[Robert Maxton]

I guess if I just wrote a few rewrite rules and said "keep applying these until they stop changing the result", the way Lean ultimately does

[Robert Maxton]

but I'm a little spoiled by Mathematica's ability to make use of two-way relations in an intelligent way, at least for its built-in relations, I guess

[Kyle Miller]

I remember looking at https://github.com/NCAlgebra/NC at some point, but I've never really used it.

[Kyle Miller]

Robert Maxton said:

but I'm a little spoiled by Mathematica's ability to make use of two-way relations in an intelligent way, at least for its built-in relations, I guess

What are you referring to here? Its pattern language, or something else?

[Robert Maxton]

Kyle Miller said:

Robert Maxton said:

but I'm a little spoiled by Mathematica's ability to make use of two-way relations in an intelligent way, at least for its built-in relations, I guess

What are you referring to here? Its pattern language, or something else?

Hmm.... okay, upon reflection actually I don't have any good examples

[Robert Maxton]

in fact I can very easily think of instances where FullSimplify has insisted on barking up the wrong tree as far as reducing an expression goes
so nvm lol