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!

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)%R`

is non trivial to prove whereas `(2 + n != 0)%N`

simply reduces to `true = true`

by computation.

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.

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