# Can't automate lemme that works manually in Coq

(It seems like my previous question had too much irrelevant information, so I tried to digress the details. I'm not sure if this is still the same problem, but I'll delete another question if the same solution works for both.)

I am trying to explain some custom lists and predicates:

``````Inductive alphabet := A.

Definition sentence : Type := list alphabet.

Variable pred1 : sentence -> Prop.

Variable pred2 : sentence -> Prop.

Variable conclusion : Prop.
```

```

Now, with the following hypotheses:

``````Hypothesis H1 : forall (X : sentence),
pred1 X -> pred2 (X ++ X).

Hypothesis H2 : forall X,
pred2 X -> conclusion.
```

```

I want to prove

``````Example manual : pred1 [A] -> conclusion.
```

```

This is obviously true, as it `conclusion`

follows when someone `sentence`

has `pred2`

, and `pred1`

for anyone `sentence`

implies that repetition of it `sentence`

has `pred2`

. Written proof would be

``````intro. eapply H2. apply H1. exact H. Qed.
```

```

Please note that in the proof of use only `intro`

, `apply`

, `eapply`

and `exact`

. This means that the proof must provide direct automation as long as `H1`

it is `H2`

available in context. For example, the semi-automatic version

``````Example semiauto : pred1 [A] -> conclusion.
pose proof H1. pose proof H2. eauto. Qed.
```

```

works as you expected. Now try the fully automated version with prompts:

``````Hint Resolve H1 H2.

Example auto : pred1 [A] -> conclusion.
eauto.
intro.
eauto.
eapply H2.
eauto.
apply H1.
eauto. Qed.
```

```

This is strange. `eauto`

occurs not only at the beginning, but also at every step, except for the last. Why is this happening?

Some guesswork: the follow-up `H1`

includes a shape `X ++ X`

that could cause unification problems. Perhaps Coq does some implicit cleanup with help `H1`

when it's explicitly injected into the context, but not when it's just at the DB hint.

Any ideas?

+3

source to share

The problem is transparency `sentence`

.

Based on Anton Trunov's answer, if you look very closely, you will notice that the difference between `Print HintDb core`

and `Create HintDb foo. Print HintDb foo.`

is what `Print HintDb core`

says

``````Unfoldable variable definitions: none
Unfoldable constant definitions: none
```

```

but `Create HintDb foo. Print HintDb foo.`

says

``````Unfoldable variable definitions: all
Unfoldable constant definitions: all
```

```

I've built the following simplified version of your example:

``````Require Import Coq.Lists.List.
Import ListNotations.
Definition sentence := list nat.
Variable pred1 : sentence -> Prop.
Variable pred2 : sentence -> Prop.
Hypothesis H1 : forall (X : sentence),
pred1 X -> pred2 (X ++ X).
Create HintDb foo.
Hint Resolve H1 : foo.
Hint Resolve H1 : bar.
Hint Resolve H1.
Example ex1 : pred1 [0] -> exists X, pred2 X.
eexists.
debug eauto.
```

```

Here we have that `eauto`

both `eauto with bar`

(and `eauto with bar nocore`

, which removes the underlying database from consideration `eauto`

) both fail, but `eauto with foo`

(and `eauto with foo nocore`

) succeeds. This suggests that the issue is transparency. After playing around a bit, I found that it `eauto`

would work if we write

``````Hint Transparent sentence.
```

```

Also, even without it, it `eauto`

works fine if I explicitly pass the `X`

expanded type to the variable :

``````Example ex2 : pred1 [0] -> exists X : list nat, pred2 X.
```

```

I'm not entirely sure why Coq behaves this way ... maybe it refuses to unify evars with terms that are of different types (if it `?X`

has a type `sentence`

, when it `X ++ X`

has a type `list`

), or maybe it is a meta-unification override ... Me opened a bugtracker issue about this lack of documentation / bad behavior .

+2

source

A possible workaround here is to add hints to the new user database:

``````Create HintDb my_hints.
Hint Resolve H1 H2 : my_hints.
```

```

Now we can finish the proof:

``````Example auto : pred1 [A] -> conclusion.
eauto with my_hints. Qed.
```

```

One more thing: the Coq reference manual tells ( ยง8.9.1 ) us that

You can query the database of prompts using the command `Create HintDb`

. If a hint is added to an unknown database, it will be automatically created.

But if we omit a part `Create HintDb my_hints.`

, the tactic `eauto`

won't work. It looks like the same thing happens when hints are added to the default hints database `core`

.

0

source

All Articles