I would like to define a different power function to be used on real number formulas, starting with the `ring`

and `ring_simplify`

tactics. I wish to just re send the `Add Ring`

command for `R`

, but I don't find where this `Add Ring`

is in the sources. Can somebody point me to the right place?

I think it's implicit in Add Field Rfield, in RealField.v

That seems logical, the Rfield structure contains a copy of RTheory

see also https://github.com/coq/coq/pull/10734

Add Field does force a Add Ring behavior. Each addition overwrites the effect of the previous one.

The `Add Field`

command that takes effect for final users that called `Require Import Reals.`

is actually found in `theories/Reals/RIneq.v`

line 2689.

I am frustrated that exponent iin power expressions is processed through full computation. As result, if my exponent is 10, it is expanded to a large ugly expression:

```
((R1 + R1) * (R1 + (R1 + R1) * (R1 + R1)))
```

I tried to replace `IZR`

by an inert function, which would have to be removed at post-processing time, but I don't manage to make the post-processing to work. And I was unable to find examples of such post-processing in the sources of Coq.

My code is visible here

https://github.com/ybertot/one_num_type/blob/main/add_ring_attempt.v

I must have made a mistake in my previous search. postprocessing is used in `theories/setoid_ring/ArithRing.v`

Last updated: Oct 13 2024 at 01:02 UTC