Stream: Coq users

Topic: Alternative to auto that dont restore goal when failed

view this post on Zulip Daniel Hilst Selli (Nov 17 2021 at 21:29):

I'm trying to automate some proofs, I'm using a repeat (match goal with ...) loop but want to use hints instead, my problem is that auto will restore the goal if it can't completely proove it and I'm looking for something that goes as far as possible but leave the remaining goals so I can finish it manually. Is there any tatic like auto but that doesn't restore the goal when one of the subgoals fails?

view this post on Zulip MackieLoeffel (Nov 19 2021 at 06:46):

One trick is to use auto with a Hint Extern that shelves the goal. I.e. something like

Local Hint Extern 1000 => shelve : test_db.

Axiom P : Prop.
Axiom proof_of_P : P.

Goal P /\ True.
  unshelve auto with test_db.
  apply proof_of_P.

Last updated: Sep 23 2023 at 14:01 UTC