Simp/Rewrite type of constructor

Stream: lean4

[Joey Eremondi]

I'm trying to automate a long but tedious proof, and most cases are straightforward constructor applications, but there are some cases where it's only apparent that a constructor can be applied after some simp rules have been applied.

I'm wondering, is there either

• A version of constructor that rewrites the type of the constructor according to e.g. some simp lemmas, or
• A version of constructor that applies a constructor, then produces as goals the equalities that must be satisfied for the constructor application to be type-correct

[Henrik Böving]

Sounds to me like Aesop is the type of tactic that you want.

[Kyle Miller]

It could be helpful having some examples. Is it that indices aren't defeq?

[Joey Eremondi]

Kyle Miller said:

It could be helpful having some examples. Is it that indices aren't defeq?

Yes exactly, the indices are propositionally equal but not definitionallly.

[Kyle Miller]

This tactic doesn't exist, but I've been thinking about what it would take to make it.

One issue that comes to mind is that, if you're able to create equalities, then usually every constructor is applicable (barring universe constraints). If you can name which constructor you want to apply, then I think it shouldn't be too much work to make a tactic that lets you apply it and create side goals for equalities.

[Kyle Miller]

It could be that you have to specify a discharger tactic (with perhaps simp as the default discharger), and it takes the first constructor such that the discharger is able to prove all the generated equalities.