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