Check if a previously-stated theorem proves a particular subgoal?

Using Coq
1

For example, for a coq file that looks like:

Theorem mini : forall a:nat, a + 0 = a.
Proof. auto. Qed.

Theorem main : forall a:nat, a + 0 = a /\ a + 1 > a.
Proof.
    split.
    ...

Then is there some tactic that can search through the current context to see that this first subgoal has already been solved previously in “Theorem mini” and then runs “apply mini”?

I know I can do an explicit search with “Search (forall a:nat, a+0 = a)”!

2

A not entirely automatic solution is to register theorems as “hints” which can be looked up with auto or eauto.

Theorem mini : forall a:nat, a + 0 = a.
Proof. auto. Qed.

Create HintDb myarith discriminated.  (* Create a hint database "myarith". *)
Hint Resolve mini : myarith.  (* Add the theorem mini to the hint database "myarith" *)

Theorem main : forall a:nat, a + 0 = a /\ a + 1 > a.
Proof.
    split; auto with myarith.  (* Use the hint database myarith to discharge some goals. *)

See also the reference manual on hints: https://coq.inria.fr/refman/proof-engine/tactics.html#coq:cmd.create-hintdb

auto by default uses the database core so you could also do Hint Resolve mini : core. and later auto., which is fine in self-contained projects, but probably less acceptable in libraries.

3 Likes
3

I’d add to @Lyxia’s answer, that auto can chain theorems, which is great but can also slow it down, especially if you want to add all theorems as hints (which you’d have to for what you ask). In the worst case, the complexity of auto is exponential in the search depth.

To limit that, you can use trivial, or call auto N with N the maximum search depth.

To learn much more on auto, the relevant chapter in Software Foundations is pretty good.

1 Like