Repackaging `Nat.add`

Stream: lean4

[Siddhartha Gadgil]

The documentation for DiscrTree says "Moreover, it is the metaprogrammer's responsibility to re-pack applications such as
Nat.add a b into Add.add Nat inst a b".

Is there a convenient way to do this, or recognize this is needed? The function Nat.addis defined earlier, and then an instance of Add.add lets us repackage. So I am confused about what I should look for to know what the repackaged form is.

Thanks.

[Leonardo de Moura]

@Siddhartha Gadgil We can just replace the terms since Nat.add a b is definitionally equal to a + b.
Note that simp does the repackaging for us because we have simp theorems such as

@[simp] theorem add_eq : Nat.add x y = x + y := rfl
@[simp] theorem mul_eq : Nat.mul x y = x * y := rfl
@[simp] theorem sub_eq : Nat.sub x y = x - y := rfl

The uniform representation is important because of proof automation. To efficiently apply simp and other forms of proof automation, we use a "term indexing" data structure. For simp, we use a "discrimination tree", and it helps filter which simp theorems can be applied to a subterm. It is not feasible to sequentially try all of them. Most arithmetic-related simp theorems use x + y (i.e., HAdd.hAdd ... x y) to represent addition, and will only be tried in subterms of the same form.

[Siddhartha Gadgil]

Thanks. What I meant was in general how do we know what are all the valid replacements?