Stream: math-comp users

Topic: The equivalent of auto in ssreflect


view this post on Zulip walker (Oct 24 2022 at 08:41):

I have 56 goals that can be solved using combination of few rewrite lemmas + Induction hypothesis.
How can I automate that.

view this post on Zulip Julien Puydt (Oct 24 2022 at 08:42):

Perhaps some //= placed at their apparition point might help?

view this post on Zulip walker (Oct 24 2022 at 08:44):

But //= does not use external rewrite lemmas, at least not by default. How to fix that ?

view this post on Zulip walker (Oct 24 2022 at 08:46):

actually //= is the reasaon I have 56 instead of 63.

view this post on Zulip Enrico Tassi (Oct 24 2022 at 08:52):

If the lemmas are morally about the same thing, I suggest you craft a multi rule https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#multi-rule-rewriting

view this post on Zulip Enrico Tassi (Oct 24 2022 at 08:53):

I mean by rewrite //= !myrule. But note that you can use auto or any other Coq tactic in the middle of an ssr script.

view this post on Zulip walker (Oct 24 2022 at 08:55):

yes they are all about the exact same thing, thanks for the idea of multi rules.

view this post on Zulip Enrico Tassi (Oct 24 2022 at 08:57):

Another thing we often do is to load the context with more facts (via have & co), and this automatically powers // up.

view this post on Zulip walker (Oct 24 2022 at 08:59):

one question, so //basically solve the goal by applying only one hypothesis right?

view this post on Zulip Enrico Tassi (Oct 24 2022 at 09:13):

I'm a bit confused by the formatting of your message. Do you want have ? := trie_lookup_builder_a ?

view this post on Zulip walker (Oct 24 2022 at 09:17):

yup that was exactly what I wanted! thanks


Last updated: Feb 08 2023 at 04:04 UTC