Stream: Coq users

Topic: ✔ Partial auto

James Wood (Oct 03 2022 at 08:09):

I've got some code that looks a bit like the following. I want to start the proof by automatically applying the obvious combination of F0, F1, and F2, leaving just a goal F xs to be proved interactively. If it weren't for this difficult subgoal F xs, I'd register all of the Fn axioms as hints and use auto. However, auto is all-or-nothing, so this doesn't help. What should I do instead?

Axiom F : list nat -> Prop.

Axiom F0 : forall xs, F xs -> F (0 :: xs).
Axiom F1 : forall xs, F xs -> F (1 :: xs).
Axiom F2 : forall xs, F xs -> F (2 :: xs).

Goal forall xs, F (1 :: 0 :: 2 :: 1 :: xs).
  intro xs.

James Wood (Oct 03 2022 at 08:11):

I should add, like with hints, I want this collection of lemmas Fn to be open, i.e, to not have to list them out every time I want this automation.

James Wood (Oct 03 2022 at 15:50):

typeclasses eauto best_effort sounds promising, but I can't work out how to make it make the progress I want.

Paolo Giarrusso (Oct 03 2022 at 19:27):

the assumption is that (even in the full examples) all your hints are syntax-directed enough you never need to backtrack on the hint choice, so partial proofs are fine?

Paolo Giarrusso (Oct 03 2022 at 19:29):

I still don't know of an off-the-shelf solution, but that makes at least the specification well-behaved

Paolo Giarrusso (Oct 03 2022 at 22:04):

okay:

#[global] Hint Extern 0 (F (0 :: _)) => simple apply F0; (eauto || shelve) : core.
#[global] Hint Extern 0 (F (1 :: _)) => simple apply F1; (eauto || shelve) : core.
#[global] Hint Extern 0 (F (2 :: _)) => simple apply F2; (eauto || shelve) : core.

Goal forall xs, F (1 :: 0 :: 2 :: 1 :: xs).
  intro xs.
  unshelve eauto.
  (* Goal: F xs *)

Paolo Giarrusso (Oct 03 2022 at 22:05):

shelve tricks eauto into thinking you're done, as https://stackoverflow.com/a/46519832/53974 reminds me

Paolo Giarrusso (Oct 03 2022 at 22:09):

beware calling eauto in a hint is _usually_ a terrifying idea that leads to exponential blowup — because the parent invocation of eauto will run again on any goals left unsolved — but not here, since if eauto fails the goal is shelved. Using debug eauto shows the search is linear:

#[global] Hint Extern 0 (F (0 :: _)) => simple apply F0; (debug eauto || shelve) : core.
#[global] Hint Extern 0 (F (1 :: _)) => simple apply F1; (debug eauto || shelve) : core.
#[global] Hint Extern 0 (F (2 :: _)) => simple apply F2; (debug eauto || shelve) : core.

Goal forall xs, F (1 :: 0 :: 2 :: 1 :: xs).
  intro xs.
  unshelve debug eauto.

Paolo Giarrusso (Oct 03 2022 at 22:09):

gives:

1 depth=5
1 depth=5
1 depth=5
1 depth=5
1 depth=5
1.1 depth=5 (*external*) (simple apply F1; debug eauto || shelve)
1.1 depth=5 (*external*) (simple apply F2; debug eauto || shelve)
1.1 depth=5 (*external*) (simple apply F0; debug eauto || shelve)
1.1 depth=5 (*external*) (simple apply F1; debug eauto || shelve)

James Wood (Oct 04 2022 at 08:04):

Yes, that specification sounds right, and the solution looks good. I'll give it a try!

Notification Bot (Oct 04 2022 at 10:59):

James Wood has marked this topic as resolved.

Last updated: Oct 04 2023 at 20:01 UTC