Stream: Beginner Questions

Topic: Use polynomial or matrix

Hongjian Jiang (May 17 2024 at 09:30):

image.png
I try to prove the correctness of above lemma, and using matix as tool before, now i was thinking whether it is more convinent to use polomial staff to prove it?

Mathias Fleury (May 18 2024 at 07:57):

Without context on what the equations is supposed to mean, it is very hard to answer

Mathias Fleury (May 18 2024 at 08:00):

there are two questions you should ask yourself:

1. would the new way still follow the proof on paper or do you need to come up with a new proof?
2. if it still follows the proof on paper, is there a technical reason that one representation would be better than the other?
3. if there is no technical reason, then there is a question on usability which you usually test by converting a few of the easier lemmas
4. the grass is always greener somewhere else

Mathias Fleury (May 18 2024 at 08:04):

To give an example, image that you have a list of the objects where you use nth to map an index to one object. And you want to replace it by a function from nat => object:

1. this is only a technical difference, the proof would not change
2. it is easier as you do have to care about extending the list to add an object. But there is no natural domain (maximum index) anymore
3. The usability will improve a bit as you do not have to care about i < length xs anymore. And after porting some lemmas, you would probably realize auto is rather nicely automated for lists. So it is not that much better actually.

Hongjian Jiang (May 28 2024 at 16:47):

Thanks, Fleury. As your suggest, I go on use former way.

Hongjian Jiang (May 28 2024 at 16:48):

(deleted)

Hongjian Jiang (May 28 2024 at 16:51):

(deleted)

Last updated: Dec 21 2024 at 16:20 UTC