rewrite_strat stack overflows on trivial goals

[JasonGross]

Description of the problem

Require Import Coq.Setoids.Setoid.

Axiom mul_0_r : forall n : nat, n * 0 = 0.
Local Hint Rewrite mul_0_r : mydb.
Goal forall x, x * 0 = 0.
  intros.
  rewrite_strat (topdown (try (hints mydb))). (* stack overflow *)

What's going on here? I could have sworn that rewrite_strat wasn't this dysfunctional....

Coq Version

8.16

[JasonGross]

Seems to have something to do with try.

[SkySkimmer]

topdown @rewstrategy := fix @ident. (choice @rewstrategy (progress (subterms @ident))) ; try @ident
so when the strategy does nothing but doesn't fail it's non terminating
Stack overflow is at least as reasonable as not terminating IMO

[JasonGross]

Perhaps, but repeat idtac doesn't loop

Maybe a better definition would be
topdown @rewstrategy := fix @ident. try ((choice (progress @rewstrategy) (progress (subterms @ident))) ; @ident)
?

[SkySkimmer]

repeat idtac doesn't loop because repeat has an implicit progress

A lot of strategies already imply progress IIUC so adding useless progress might not be very efficient. Also the parentheses aren't balanced so I'm not 100% sure what you intend.

[JasonGross]

Parentheses fixed, sorry.

As far as efficiency goes, this is easy fix by making iterated progress a no-op: have the return state of each tactic be | Failure of exn | Id | Success of (progress_kind * new_goal * proof) where progress_kind is either "definitely made progress" or "unknown if progress". Then progress only does something interesting on "unknown if progress", turning it either into "definitely progress made" or Failure. Similarly, try just turns Failure into Id, while sequencing with anything non-Id turns "definitely progress" into "unknown if progress".

But I guess I don't have global vision about whether or not it's better to bake in progress vs try. I lean towards baking in try for anything that looks like a looping construct?

[JasonGross]

I do think the design should make it relatively hard to trigger infinite loops / stack overflows, if feasible. The user never wants to write code that does this, so if we can make more expressions mean something that is not "stack overflow" without needing special cases, that seems better