Stream: Coq users

Topic: simp all using Equations


view this post on Zulip Yannick Forster (Oct 16 2020 at 14:29):

Hi all, I want to do call the simp tactic from the Equations plugin to simplify all possible occurrences of a function defined using Equations in the goal. Is it possible, or do I have to pass the names of all functions manually?

view this post on Zulip Matthieu Sozeau (Oct 16 2020 at 16:36):

Currently the simp tactic is just an alias to autorewrite and it's not possible to give "all" databases to it (like auto with *), but that's surely a good feature request :)

view this post on Zulip Maxime Dénès (Oct 16 2020 at 16:38):

I thought we agreed that auto with * was a disaster

view this post on Zulip Maxime Dénès (Oct 16 2020 at 16:39):

but I guess you could instead have a dictionary of equations

view this post on Zulip Matthieu Sozeau (Oct 16 2020 at 17:34):

Yes, you don't want a with *, but rather a way to refer to all the equations (and maybe even have more fine grained set-like operations on databases)

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 18:15):

Does Ltac2 have first-class databases?

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 18:17):

it would be nice to have APIs to get lists of hint databases, and then access their properties.

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 18:17):

oh, and possibly iterate over hints.

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 18:18):

would this require rewriting the underlying internals? plugins to iterate over hints exist, so it’s at least not impossible in OCaml

view this post on Zulip Matthieu Sozeau (Oct 16 2020 at 21:39):

I think the main issue if any is to persist this state indeed, which should ideally just be a set of global names. I guess Ltac2 would fit here indeed. @Pierre-Marie Pédrot ?


Last updated: Feb 06 2023 at 12:04 UTC