abab9579 (Sep 21 2022 at 13:05): abab9579 (Sep 21 2022 at 13:05):I am yet to approach circumstances where small-scale reflection would be helpful, other than being able to use rewrite with lemmas.
I suspect it is me not knowing how to use them properly.
Could you explain how to use small-scale reflection effectively? Explanation with a concrete example would be great!
Pierre Roux (Sep 21 2022 at 13:48):Maybe is it linked to the fact that you are using a lot of real numbers / abstract ring / other algebraic structure not offering effective computation. Small scale reflection is probably more useful when manipulating things like natural numbers / integers / booleans / other things equipped with computation.
To take an example in a nearby stream, (2 + n%:R != 0)%Ris non trivial to prove whereas (2 + n != 0)%N simply reduces to true = true by computation.
abab9579 (Sep 21 2022 at 13:55):I see. I am curious, does the computational benefit also translate to structures like finite groups? Saw lots of work done towards that part in math-comp libs.
Pierre Roux (Sep 21 2022 at 14:01):If you manipulate a finite group of a given order maybe but if it is more abstract (a finite group of some order n : nat) probably not that much. However you may still manipulate natural numbers and boolean in the process and enjoy their computational behavior.
Last updated: Feb 08 2023 at 04:04 UTC