Aesop: ordering norm rules with penalties

Stream: lean4

[Alex Keizer]

I'm trying to guide aesop to use a more specific normalization rule before it tries to use a general rule. I thought I could give the general rule a higher penalty, but it seems to not actually affect which rule gets applied.

Consider the following MWE

import Aesop

structure Foo where
  x : Int

def Foo.neg (foo : Foo) : Foo :=
  ⟨-foo.x⟩

instance : Neg Foo := ⟨Foo.neg⟩

instance : OfNat Foo 1 := ⟨Foo.mk 1⟩

def Foo.negOne : Foo := ⟨-1⟩


@[aesop norm 10]
theorem Foo.desugar_neg (foo : Foo) : -foo = foo.neg :=
  rfl

@[aesop norm 1]
theorem Foo.desugar_negOne : (-1 : Foo) = Foo.negOne :=
  rfl


example : (-1 : Foo) = z := by
  aesop
  -- ⊢ Foo.neg 1 = z

Here, I want to rewrite the constant -1 differently from a generic occurence of -foo, so desugar_negOne is the more specific rule, while desugar_neg is the general rule. However, whatever I try, the goal in the last example always becomes Foo.neg 1, i.e., the generic rule got applied. Only if I remove the aesop attribute from desugar_neg entirely, does the second rule fire and the goal becomes Foo.negOne as desired.

Am I misunderstanding how the norm penalty works / should work?

[Jannis Limperg]

Equations are added as simp rules and are applied in a simplifier pass, so we can't use the same semantics for penalties as for other types of rules. However, the simplifier supports priorities, which Aesop could (and should) set and which would solve this particular issue. I'll implement this. As a workaround, you can write @[simp 10] for the negOne lemma.

[Alex Keizer]

Thanks, that indeed fixes my problem!