walker (Oct 24 2022 at 08:41): 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.
Julien Puydt (Oct 24 2022 at 08:42):Perhaps some //= placed at their apparition point might help?
walker (Oct 24 2022 at 08:44):But //= does not use external rewrite lemmas, at least not by default. How to fix that ?
walker (Oct 24 2022 at 08:46):actually //= is the reasaon I have 56 instead of 63.
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
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.
walker (Oct 24 2022 at 08:55):yes they are all about the exact same thing, thanks for the idea of multi rules.
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.
walker (Oct 24 2022 at 08:59):one question, so //basically solve the goal by applying only one hypothesis right?
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 ?
walker (Oct 24 2022 at 09:17):yup that was exactly what I wanted! thanks
Last updated: Feb 08 2023 at 04:04 UTC