James Wood (Oct 03 2022 at 08:09): 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.
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 *)
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.
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)
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 13 2024 at 01:02 UTC