I wonder how I could call `ring_simplify`

with an Ltac2 `constr list`

. Is there a better way than having a separate ring_simplify wrapper for 1..10 arguments?

You can probably hack your way around with a wrapper Ltac1 function + the Ltac2/Ltac1 FFI

ring is not a reasonable example of what you can / should do with Ltac1

ring is not a reasonable example of what you can / should do with Ltac1

Aren't ring and ring_simplify OCaml tactics meanwhile?

The issue with `ring_simplify`

is that it takes an arbitrary number of terms as argument. These are simplified together with the same variable indexing. If one `ring_simplifies`

ring equivalent terms separately, one might (and does) get different results. Only when one simplifies all equivalent terms together, there is a guarantee that they are equal after simplification.

I don't see a way to handle this with the FFI other than singling out the case for n=1,..,N for some small N. But this is not that bad - in case the Ltac2 list is larger than N it throws an error and it is trivial to extend and I don't expect N to get ever larger than 10. So I can live with this, it is just not very elegant.

No, you can use Ltac1 module to build the runtime equivalent of Ltac1 constr list out of Ltac2 lists. Then you pass this to an Ltac1 function that is just a wrapper around the list notation, and it should hopefully work.

(lists and constrs are the only exported Ltac1 type cast FFI currently)

Thanks, I found the tactic notation for ring_simplify now (I thought it was immediately an OCaml tactic). It should indeed be doable.

Last updated: Dec 05 2023 at 04:01 UTC