Patrick Nicodemus (Oct 31 2022 at 01:02): Patrick Nicodemus (Oct 31 2022 at 01:02):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 catcontains unfold_proper as a Hint Extern and is able to successfully apply it? Obviously it is not a hint depth problem.
Paolo Giarrusso (Oct 31 2022 at 09:45):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.
Paolo Giarrusso (Oct 31 2022 at 09:50):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.
Patrick Nicodemus (Oct 31 2022 at 12:02):Interesting, I have seen nested auto calls like this before but i did not understand the point.
Notification Bot (Nov 01 2022 at 13:30):Patrick Nicodemus has marked this topic as resolved.
Last updated: Oct 03 2023 at 20:01 UTC