Simplify Structure With One Argument In Tactic

Stream: new members

[Andrew Elsey]

Hi, essentially, I have a goal of the form

{to_a := a_2} + {to_a := a_1} + {to_a := a_0} = {to_a := a_2} + ({to_a := a_1} + {to_a := a_0}).

These are destructed structures (you can use induction or cases to get something similar) that extend "a" and have no arguments.

I can prove
a_2 + a_1 + a_0 = a_2 + (a_1 + a_0). What is the simplest way to change the goal and get rid of the bracket/structure cruft? Or, can I go from a_2 + a_1 + a_0 = a_2 + (a_1 + a_0) to the goal? I've tried using various tactics, split, constructor, injection seems to do the opposite of what I need. I am guessing there is a simple way to do this but for the life of me can't find the right tactic.

Thank you for your help!

[Yakov Pechersky]

When you defined your structure, add an [ext] attribute above it. That will autogenerate an extensionality lemma, which you can use via the ext tactic

[Andrew Elsey]

Yakov Pechersky said:

When you defined your structure, add an [ext] attribute above it. That will autogenerate an extensionality lemma, which you can use via the ext tactic

Thank you. Sorry, I should have mentioned, I do have that actually, however, I get this goal when I use ext :

(a + b + c).to_a.to_prod.fst = (a + (b + c)).to_a.to_prod.fst

which I can technically prove, but I have a proof of "a_2 + a_1 + a_0 = a_2 + (a_1 + a_0)" which I was specifically hoping to use. Is that a bad way to go about things or is there some way I can still remove the structure junk without ext?

[Greg Price]

Andrew Elsey said:

(a + b + c).to_a.to_prod.fst = (a + (b + c)).to_a.to_prod.fst

If you have a proof of a + b + c = a + (b + c), then you could rewrite using that proof as a premise.

Or is the issue about the difference between a_0 etc. and a etc.?

[Andrew Elsey]

Greg Price said:

Andrew Elsey said:

(a + b + c).to_a.to_prod.fst = (a + (b + c)).to_a.to_prod.fst

If you have a proof of a + b + c = a + (b + c), then you could rewrite using that proof as a premise.

Or is the issue about the difference between a_0 etc. and a etc.?

Don't think I can. To clarify, I have a proof of a.to_a + b.to_a + c.to_a = a.to_a + (b.to_a + c.to_a) but not a + b + c = a + (b + c), which is the ultimate goal. The "_0, _1, _2" stuff is just caused by destructing a, b, c

[Greg Price]

It may be helpful to post a #mwe. Then people can try out tweaks to your code and see exactly what's happening.

[Andrew Elsey]

Greg Price said:

It may be helpful to post a #mwe. Then people can try out tweaks to your code and see exactly what's happening.

I will do that in a bit. Thank you for the suggestion.

[Mario Carneiro]

You need lemmas saying (a + b).to_a = a.to_a + b.to_a and so on; these are probably true by rfl and @[simps] will automatically generate them

[Andrew Elsey]

Mario Carneiro said:

You need lemmas saying (a + b).to_a = a.to_a + b.to_a and so on; these are probably true by rfl and @[simps] will automatically generate them

I gave that a quick try and that actually worked really cleanly. After those lemmas all I needed to was cc. Thank you very much (and Greg and Yakov)!