simp/dsimp infinite recursion

Stream: lean4

[Parth Shastri]

opaque A : Prop → Prop
opaque B : Prop → Prop
opaque C : Prop → Prop

abbrev AB p := A (B p)
abbrev ABC p := AB (C p)

@[simp] theorem A_B : A (B p) = AB p := rfl
@[simp] theorem AB_C : AB (C p) = ABC p := rfl

example : ABC p := by dsimp
-- error: maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)

Removing the @[simp] theorems results in the following error, which shows that dsimp did not simplify at all:

error: unsolved goals
p : Prop
⊢ ABC p

The same behavior is observed when using example : A (B (C p)) := by dsimp.

[Kind Bubble]

(deleted)

[Reid Barton]

abbrev makes a transparent definition, so dsimp will see that ABC p is the same as AB (C p) and use AB_C to rewrite it back to ABC p.

[Parth Shastri]

If I remove A_B then the error no longer occurs. Also, I did not mark ABC with @[simp]. Removing A_B and adding @[simp] to ABC does result in the infinite recursion that you describe, but the fact that it does not occur without @[simp] suggests that this isn't the cause of the issue.

[Yaël Dillies]

Have you tried set_option trace.simplify.rewrites true (or whatever the Lean 4 equivalent of it is) to see what simp rewrites with?

[Reid Barton]

set_option trace.Meta.Tactic.simp true in

[Reid Barton]

Yeah sorry, it actually matches A_B first to rewrite to AB (C p)

[Reid Barton]

I don't understand why it takes two of these lemmas to make a loop, but neither lemma seems sensible when AB and ABC are abbrevs