A translate tactic

Stream: mathlib4

[Yaël Dillies]

Thinking about it a bit more, if we had translate, to_additive could be described as

• additivise the statement of mul_thm to get the statement of add_thm
• run translate mul_thm on add_thm

[Eric Wieser]

It's basically just exact_mod_cast but with a different operator to coe

[Yaël Dillies]

And probably we'll want an additional argument to translate for it to know which dictionary to use.

[Eric Wieser]

Not sure what you mean by "dictionary"

[Yaël Dillies]

I'm thinking of a dictionary as a set of lemmas to allow translating between, eg:

• set → finset
• list → array
• multiplicative world → additive world
• order theory → order theory again (but everything dualised)
• algebra → algebra again (but a + b → b + a)
• algebra → algebra again (but a * b → b * a)

[Sky Wilshaw]

This sounds to me like some kind of natural isomorphism stuff.

[Yaël Dillies]

Yes, absolutely, a meta-theoretic one.

[Sky Wilshaw]

I'm quite surprised that this doesn't already exist! It sounds like a very natural abstraction, but I don't know how difficult implementing such a tactic would be.

[Eric Wieser]

My thinking is the way this would work, for two types A and B

• Start with a lemma about a type A
• Instantiate all the binders of a lemma with B_to_A x
• Apply A_to_B around the outside of the outer = in the statement if there is one (TODO: recurse into iffs)
• Push the former inwards, and the latter outwards until they cross and cancel. The dictionary containing these types of lemma would be keyed by (B_to_A, A_to_b) or similar
• End up with a lemma about the type B

[Sky Wilshaw]

When "pushing" in and out, that's where we'd use the lemmas mapping each operation over the isomorphism, presumably?

[Eric Wieser]

Yes, exactly

[Eric Wieser]

Things like docs#mul_opposite.op_mul or docs#of_add_add

[Yaël Dillies]

Note that in my explanation, I explicitly stated that translate shouldn't try to generate the statement. This is best done by specialised tools (the current to_additive dictionary) and might not have a single solution (in order theory there are exponentially many possible dualised statements).

[Yaël Dillies]

Also note that we want to support more relations than just =, and not only relations. Eg ⊆, ⊂, .nonempty

[Eric Wieser]

and might not have a single solution (in order theory there are exponentially many possible dualised statements).

Can you give an example?

[Yaël Dillies]

docs#monotone.comp involves three orders, and two out of the three can be meaningfully dualised. which results in 4 lemmas.

[Eric Wieser]

Can you split this thread at what you think is an appropriate point? Arrays are far behind us...

[Damiano Testa]

While this discussion is taking place, can I add to the list of wishes also automation to prove results about docs#polynomial.trailing_degree, from results about docs#polynomial.degree? :wink:

[Yaël Dillies]

Hmm actually it seems that I can't...

[Notification Bot]

19 messages were moved here from #mathlib4 > Array by Eric Wieser.

[Sky Wilshaw]

Eric Wieser said:

My thinking is the way this would work, for two types A and B

• Start with a lemma about a type A
• Instantiate all the binders of a lemma with B_to_A x
• Apply A_to_B around the outside of the outer = in the statement if there is one (TODO: recurse into iffs)

After applying your first three steps, would aesop be able to solve the resulting goal?

[Sky Wilshaw]

(after being taught the appropriate lemmas)

[Yaël Dillies]

Oh yeah, Damiano, nice one.

[Eric Wieser]

I don't see Aesop being more useful than simp only ... here, but I could be mistaken

[Yaël Dillies]

I think aesop is overkill here. We have a very well delimited domain.

[Sky Wilshaw]

simp only sounds like a reasonable thing to use to perform the 4th step.

[Sky Wilshaw]

This doesn't seem like a particularly difficult tactic to write given all of the infrastructure - I'd be interested in trying to write (at least a prototype version of) it.

[Eric Wieser]

Step 4 alone would be a useful thing to prototype

[Yaël Dillies]

To me, the first step (finding the correct coe_inj/coe_subset-like lemma and applying it) is the hardest.

[Sky Wilshaw]

It sounds like it to me too.

[Eric Wieser]

I think the tricky bit is building the lookup from "push this application inwards / outwards" to a list of the intended lemmas

[Yaël Dillies]

Note that we have to be picky about the lemmas we provide simp with in the last step, as coe_inj/coe_subset are simp lemmas and risk reverting the goal to the original statement!

[Eric Wieser]

I think there's a lot of overlap with the norm_cast push/pull/elim framework here

[Yaël Dillies]

I expect there to be wisdom to extract from norm_cast's implementation.

[Yaël Dillies]

Why am I even talking anymore? We clearly are the hive mind :laughing:

[Sky Wilshaw]

I may have some time tomorrow to look over this.

[Eric Wieser]

This also overlaps with the push_hom/pull_hom proposal

[Yaël Dillies]

Yes, there might be a pair of generic push/pull tactics to extract from this as well.

[Eric Wieser]

I think probably a good step would just be writing out a list of all the sorts of lemmas we'd want to be able to push / pull, perhaps for:

• order_dual
• mul_opposite
• add_monoid_hom

[Yaël Dillies]

I assume you mean functions rather than lemmas?

[Eric Wieser]

No, I mean lemmas. For the obvious push / pull actions in those areas, what lemmas would be valid things to apply

[Yaël Dillies]

Oh "(the sorts of lemmas we'd want) to be able to push", not "the sort of (lemmas we'd want to be able to push)". Linear language be cursed.

[Yaël Dillies]

@Mario Carneiro said:

Yaël Dillies said:

Regarding set and finset, I found that coe_inj.2 $ by { norm_cast, exact set.some_lemma } (or the coe_subset version thereof) was a reliable way of proving finset.some_lemma. By now, there are many lemmas in mathlib I proved that way. So I think it is a sensible heuristic for implementing such a tactic.

This is basically what the norm_cast tactic does, so I would say the tactic to do this already exists

I'm not sure, no. norm_cast only goes one direction, and what happens here is that you first need to apply some lemmas in the push_cast direction, then some others in the norm_cast one.

[Yaël Dillies]

Essentially, the diagram of possible cast normalisations is a square, and we're walking along three of its edges to deduce the fourth.

set.X  → finset.X
   ↑        ↑      norm_cast
set.X' → finset.X'

[Mario Carneiro]

In the vast majority of cases this is just something like ext; simp

[Mario Carneiro]

the ext "activates" the simp lemmas, indicating that you want to go around the square

[Mario Carneiro]

it would be a bad idea to go traversing that square without some explicit indication of such

[Mario Carneiro]

(unless you are in the context of a big closing tactic like aesop, where you can try stuff and roll back)

[Yaël Dillies]

Yes, I'm proposing we mark that information explicitly. And, no, ext won't cut it.

[Mario Carneiro]

I haven't seen a convincing example of that

[Yaël Dillies]

Can you read the entire thread? I feel like you're missing context.

[Mario Carneiro]

you yourself said that the proof is usually apply ext_lemma; simp or so

[Mario Carneiro]

(in the thread from which you got my quote)

[Yaël Dillies]

I never said this, no. I rather said rw ←norm_cast_lemma; norm_cast; simp

[Yaël Dillies]

docs#finset.coe_subset is not an extensionality lemma, for example.

[Mario Carneiro]

okay, either way it's a one liner already

[Mario Carneiro]

I don't see a motivation for writing a tactic here

[Yaël Dillies]

Well, it's a one-liner for the set/finset translation, but it's not for at least 4 of the other use cases I'm stating.

[Mario Carneiro]

Simp lemmas do most of the work in all of those examples

[Mario Carneiro]

to_additive is a lot of work to maintain and this sounds like it would be at least as complicated, if not more because you want it to apply to a bunch of very differently shaped domains

[Mario Carneiro]

The only thing that could feasibly cover all of those domains is a simp set, so we're back to norm_cast

[Mario Carneiro]

just make a macro for simp [up]; simp [left]; simp [down]

[Anne Baanen]

Another direction you might be interested in is to adapt locales (as seen in Isabelle). They seem to be quite good at implementing the kind of rewriting used by to_additive but in a more robust way. I don't know how effectively a basic implementation would mesh with existing Lean metaprogramming, but it's certainly worth mentioning as an alternative.

[Sky Wilshaw]

I was thinking that an easy way to deal with the non-uniqueness of a goal is to perfom the rewriting lemmas on the hypothesis and the goal. Then they'll both be normalised to the same form, and the user just needs to make sure they write the goal in the way they'd like.

[Sky Wilshaw]

It also makes translating "backwards" just as easy as translating "forwards".

[Jeremy Salwen]

Mario Carneiro said:

The only thing that could feasibly cover all of those domains is a simp set, so we're back to norm_cast

Are are you saying that norm_castitself could be used to do these sorts of simplifications for other domains like Array<->List? Or just that you could get similar behavior using simp sets?

[Mario Carneiro]

To use norm_cast directly you need to be using things that are marked as @[coe]

[Mario Carneiro]

but it's a wrapper for simp with specific simp sets so you can make your own simp sets to do something with non-coes

[Jeremy Salwen]

So we could have a macro which takes as arguments the appropriate simp sets. Where if you pass it the coe simp sets, it behaves like norm_cast, but if you pass it other simp sets it could handle other isomporphisms?

[Mario Carneiro]

yes

[Jeremy Salwen]

Ok that makes sense. I can give it a shot. From a software engineering perspective, does it make sense to try to modify the norm_cast implementation to allow you to control the simp sets it is using, or does it make more sense to implement something from scratch?

[Mario Carneiro]

I think you should start by doing it from scratch (or rather, copy and paste) to make sure that it actually works as intended

[Jeremy Salwen]

I implemented a prototype of this. I tested it for casting Array->List, but I wrote it in a way that it should be able to work for arbitrary isomorphisms: https://github.com/jeremysalwen/Lean4-Translate-Tactic

The basic idea is a construct a simp set that looks like

lemma Array.append_translated: @Array.append  = (λ {α} a b => List.toArray (List.append (a.data) (b.data))) := sorry
lemma Array.push_translated: @Array.push = (λ  {α} a v => List.toArray (a.data ++ [v])) := sorry
--- etc

This results in a more aggressive translation than simply pushing the casts up or down the expression, since (assuming we have all the appropriate lemmas) it will completely eliminate any Array operations from our expression, even if there are no casts in our original expression, or the functions are unapplied.

Since there are already existing lemmas that are similar to this, I wrote some code to transform the lemmas into this form, i.e. taking

theorem Array.push_data {α : Type u_1} (arr : Array α) (a : α) : (Array.push arr a).data = arr.data ++ [a]

And translating it to the Array.push_translatedlemma automatically. Right now it just applies this translation to any @[simp] lemmas that are candidates based on the operations in the lhs and rhs of the equation, but I think ideally we would tag the appropriate lemmas @[translate] so it would be more selective.

Thanks for your help, and also @Kyle Miller who helped a ton!

A few questions/notes:

1. The way I defined the simp sets was generating new defs and adding them to an array_to_string simp attribute I defined. I'm not sure if it would be better to just store things in SimpExtensions directly like norm_castand key things by type.
2. The isomorphism I translated isArray->List, which already has many existing lemmas that rewrite Array on the lhs to List on the rhs. However, I think in general we would want to translate in both directions. For some lemmas it seems like there would need to be more work needed to convert them to a form where we could rewrite them from right to left, e.g..:

theorem Array.getElem_eq_data_get {α : Type u_1} {i : Nat} (a : Array α) (h : i < Array.size a) :
a[i] = List.get a.data { val := i, isLt := h }

3. I wrote everything in a way that is up to the user to specify the forward coercion, the reverse coercion, etc, but nothing is validated that they are actually providing a proper isomorphism. I couldn't figure out if this is something that could be expressed easily (i.e. the user could provide an "isomorphism" object, and we could automatically generate the simp sets in either direction based on that).