Stream: Coq users

Topic: Using hypotheses in automation


view this post on Zulip Patrick Nicodemus (Apr 23 2023 at 17:07):

If you have a proof search tool like auto, it generally only focuses on the goal and works backward from there. Sometimes it seems like forward reasoning is preferable though. For example suppose I have the known theorem ~ n < m -> n >= m and I have a goal where this can be applied, i.e.

H : ~ n < m
--------------
n >= m

I already have the theorem n >= m -> ~n < m in a hint database because this seems like a more convenient way to work with the information.

So what are my options here?

  1. Add the hint ~ n < m -> n >= m to the hint database
  2. Add a loop which searches through the hypotheses at each stage in proof search for something matching ~ n < m and rewrite it to n >= m

The first one will add lots of wasted time in depth first search.
The second seems better but I am worried about the performance of adding a loop to search over hypotheses all the time.

view this post on Zulip Patrick Nicodemus (Apr 23 2023 at 17:07):

Maybe I am overly obsessing over performance and it is not a big deal. How do you handle this situation to simplify hypotheses into a convenient form?

view this post on Zulip Patrick Nicodemus (Apr 23 2023 at 17:09):

I have also considered adding autorewrite with arith_rewrite in * as a (very low priority) hint in auto but this also seems to be not very fast.

view this post on Zulip Michael Soegtrop (Apr 24 2023 at 07:45):

A few points on this:

view this post on Zulip Paolo Giarrusso (Apr 24 2023 at 08:34):

Michael: have you implemented custom automation, or gotten auto to help?

view this post on Zulip Michael Soegtrop (Apr 24 2023 at 16:00):

@Paolo Giarrusso : I get along with auto, eauto or typeclass eauto and some dedicated forwarding tactics which I run as extern hint at a certain cost level between likely cheap backward tactics and likely expensive backward tactics. For certain goal types I use reflexive tactics.


Last updated: Jun 18 2024 at 07:01 UTC