I have a problem with `auto.`

I am trying to prove the goal `a x0 x1 ≈ a x0 y0`

, where `≈`

is a certain setoid equivalence relation.

The key lemma I need to prove this goal is a hypothesis of the form

` b : Proper (forall_relation (λ a : obj[C], (equiv ==> equiv)%signatureT)) a`

, which says for all `x`

, `a x`

is a proper morphism, so this reduces the goal to `x1 ≈ y0`

. This is an assumption.

I could `apply b`

and this would solve the goal. However `auto`

does not recognize that the conclusion of `b`

matches the form of the goal, so it will not apply it automatically.

I wrote an Ltac script `unfold_proper`

which finds `b`

and unfolds these terms so it will be in a form `auto`

will recognize as an implication.

When I run `unfold_proper`

I get `b : ∀ (a0 : obj[C]) (x0 y : x ~{ C }~> a0), x0 ≈ y → a a0 x0 ≈ a a0 y`

. After this, `auto`

solves the goal.

So far so good. Now I want to add `unfold_proper`

as a `Hint Extern`

. But after doing this, `auto`

can no longer solve the goal.

```
(* debug auto: *)
* assumption. (*fail*)
* intro. (*fail*)
* simple apply H2. (*fail*)
* simple apply H1. (*fail*)
* simple apply H0. (*fail*)
* (*external*) (simple apply compose_respects) (in cat). (*fail*)
* (*external*) reflexivity (in cat). (*fail*)
* (*external*) unfold_proper (in cat). (*success*)
** assumption. (*fail*)
** intro. (*fail*)
** simple apply H2. (*fail*)
** simple apply H1. (*fail*)
** simple apply H0. (*fail*)
** (*external*) (simple apply compose_respects) (in cat). (*fail*)
** (*external*) reflexivity (in cat). (*fail*)
** (*external*) unfold_proper (in cat). (*fail*)
** (*external*) (progress simplify) (in cat). (*fail*)
** (*external*) (progress autorewrite with categories) (in cat). (*fail*)
** (*external*) functor_simpl (in cat). (*fail*)
** (*external*) apply_setoid_morphism (in cat). (*fail*)
** (*external*) (progress cbn in *) (in cat). (*fail*)
* (*external*) (progress simplify) (in cat). (*fail*)
* (*external*) (progress autorewrite with categories) (in cat). (*fail*)
* (*external*) functor_simpl (in cat). (*fail*)
* (*external*) apply_setoid_morphism (in cat). (*fail*)
* (*external*) (progress cbn in *) (in cat). (*fail*)
```

I find this strange. It runs ` (*external*) unfold_proper (in cat).`

at about the 8th step and succeeds. My expectation is that it should now automatically apply `b`

to the goal. But I don't see `b`

anywhere in the list of hypotheses that were tried, there is no `simple apply b`

, suggesting that even after `unfold_proper`

was run, `auto`

did not recognize the conclusion of `b`

as a match for the goal.

Does anyone have a suggestion as to why `unfold_proper; auto`

would solve the goal but `auto with cat`

would not, even though `cat`

contains `unfold_proper`

as a `Hint Extern`

and is able to successfully apply it? Obviously it is not a hint depth problem.

I assume that in `unfold_proper; auto`

, auto just applies `b`

; and that, unfold_proper modifies *an assumption* rather than the goal... I suspect auto already visited assumptions to compute which ones apply. The docs might agree, since hypotheses are added as hints at the beginning:

Implements a Prolog-like resolution procedure to solve the current goal. It first tries to solve the goal using the assumption tactic, then it reduces the goal to an atomic one using intros and introduces the newly generated hypotheses as hints. Then it looks at the list of tactics associated with the head symbol of the goal and tries to apply one of them. Lower cost tactics are tried before higher-cost tactics. This process is recursively applied to the generated subgoals.

To deal with this, maybe the Hint Extern could call `solve [unfold_proper; auto]`

, where `solve`

should fix some of the performance problems with nested auto calls.

Interesting, I have seen nested auto calls like this before but i did not understand the point.

Patrick Nicodemus has marked this topic as resolved.

Last updated: Oct 03 2023 at 20:01 UTC