Stream: Ltac2

Topic: Calling ring_simplify with a list of terms


view this post on Zulip Michael Soegtrop (Mar 18 2021 at 17:13):

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?

view this post on Zulip Pierre-Marie Pédrot (Mar 18 2021 at 20:40):

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

view this post on Zulip Pierre-Marie Pédrot (Mar 18 2021 at 20:42):

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

view this post on Zulip Michael Soegtrop (Mar 19 2021 at 09:35):

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.

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 10:50):

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.

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2021 at 10:51):

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

view this post on Zulip Michael Soegtrop (Mar 19 2021 at 13:43):

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: Jan 31 2023 at 09:01 UTC