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

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)”!

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

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