Zulip Chat Archive

Stream: new members

Topic: Simplify Structure With One Argument In Tactic


view this post on Zulip Andrew Elsey (Mar 30 2021 at 19:07):

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!

view this post on Zulip Yakov Pechersky (Mar 30 2021 at 19:11):

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

view this post on Zulip Andrew Elsey (Mar 30 2021 at 19:20):

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?

view this post on Zulip Greg Price (Mar 30 2021 at 19:24):

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.?

view this post on Zulip Andrew Elsey (Mar 30 2021 at 19:38):

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

view this post on Zulip Greg Price (Mar 30 2021 at 19:42):

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

view this post on Zulip Andrew Elsey (Mar 30 2021 at 19:43):

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.

view this post on Zulip Mario Carneiro (Mar 30 2021 at 20:40):

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

view this post on Zulip Andrew Elsey (Mar 30 2021 at 23:18):

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)!


Last updated: May 15 2021 at 00:39 UTC