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.

`typeclasses eauto best_effort`

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

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?

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

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

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!

James Wood has marked this topic as resolved.

Last updated: Jun 16 2024 at 02:41 UTC