more auto in ExampleR.v

[awalterschulze]

ExampleR.v has a lot of easy concrete proofs, but the proofs end up being very long.

We can use

Create HintDb lang.

Hint Extern 1 =>
  match goal with
  | [ H : _ `elem` _ |- _ ] =>
    inversion H; clear H
  end || listerine || subst: lang.

See https://stackoverflow.com/questions/44767744/coq-why-do-i-need-to-manually-unfold-a-value-even-though-it-has-a-hint-unfold for how I learned out how to hack this.

Then we can solve a lot of the theorems using auto 1000 with lang..

But when we get to Lemma test_notelem_x11star_0, we run into star which is recursive and auto ends up running seemingly forever.

I think we could possibly tweak the number in extern to only try inversion on star_lang as a last resort to make the recursion more unlikely and that why stop the seemingly infinite recursion that occurs in test_notelem_x11star_0. Then it might be possible to automate all of these proofs into being very short proofs as @Nielius was pushing for.

Or maybe there is an even better way?

• Here is a nice reference on Hint Constructors, which I didn't end up using http://adam.chlipala.net/cpdt/html/LogicProg.html
• Not so useful, but helped me with syntax: https://github.com/coq/coq/blob/master/test-suite/success/Hints.v#L191

[paulcadman]

Thanks for all the information - I want to learn about this.

[awalterschulze]

This was a good read, really well written, with lots of basic examples, that not only explain how to use auto, but how auto works on an intuitive level and also covers all the Hint variants http://adam.chlipala.net/cpdt/html/LogicProg.html

[awalterschulze]

Here is an example of how to use more auto with lists https://github.com/awalterschulze/regex-reexamined-coq/pull/137

[Nielius]

I also liked the UseAuto section of Software Foundations Vol 2.. It especially had a good discussion (if I recall correctly) of some of the limitations of auto and eauto, that you can easily solve by doing some kind of preprocessing (like wreckit) or by using intuition.

[awalterschulze]

Yes so far that link is a pretty good read. Here is a quote.

""" Note that proof search tactics never perform any rewriting step (tactics rewrite, subst), nor any case analysis on an arbitrary data structure or property (tactics destruct and inversion), nor any proof by induction (tactic induction). So, proof search is really intended to automate the final steps from the various branches of a proof. """

This is worrying as we do typically require a lot of inversion, because when we have or, it turns into nor, which turns into not, which have to unfold and then we have to intro and then we have a "goal" in the hypothesis, which we would like to invert, using inversion, but this is not part of auto's repertoire

So I don't know how possible it is to use auto for ExampleR.v But we can might combine it with some Hint Externs' that do, do inversion.

[Nielius]

Their solution to that problem is to have a few tactics (jauto and iauto) that do auto or eauto together with some pre- and post-processing:

We are going to study four proof-search tactics: auto, eauto, iauto and jauto. The tactics auto and eauto are builtin in Coq. The tactic iauto is a shorthand for the builtin tactic try solve [intuition eauto]. The tactic jauto is defined in the library LibTactics, and simply performs some preprocessing of the goal before calling eauto. The goal of this chapter is to explain the general principles of proof search and to give rule of thumbs for guessing which of the four tactics mentioned above is best suited for solving a given goal.

Proof search is a compromise between efficiency and expressiveness, that is, a tradeoff between how complex goals the tactic can solve and how much time the tactic requires for terminating. The tactic auto builds proofs only by using the basic tactics reflexivity, assumption, and apply. The tactic eauto can also exploit eapply. The tactic jauto extends eauto by being able to open conjunctions and existentials that occur in the context. The tactic iauto is able to deal with conjunctions, disjunctions, and negation in a quite clever way; however it is not able to open existentials from the context. Also, iauto usually becomes very slow when the goal involves several disjunctions.

[awalterschulze]

I am still reading, but here was another interesting note

It is very important to understand that the hypothesis ∀ n m, P m → m ≠ 0 → P n is eauto-friendly, whereas ∀ n m, m ≠ 0 → P m → P n really isn't. Guessing a value of m for which P m holds and then checking that m ≠ 0 holds works well because there are few values of m for which P m holds. So, it is likely that eauto comes up with the right one. On the other hand, guessing a value of m for which m ≠ 0 and then checking that P m holds does not work well, because there are many values of m that satisfy m ≠ 0 but not P m.

[awalterschulze]

Another Note: Hint UnFold only works in the goal

the Hint Unfold mechanism only works for unfolding definitions that appear in the goal. In general, proof search does not unfold definitions from the context.

[awalterschulze]

Now to reply to @Nielius

It seems iauto and jauto are not in the standard library. We haven't pulled in any dependencies into this project yet, so that could be interesting or disrupting, not sure.

Maybe lets try to puzzle things out with auto and eauto and Extern Hints for a bit first, while we are learning.