change with

[patrick-nicodemus]

This is something I have posted about on Zulip but I thought I should create a formal issue for it.

I think the Coq API should expose a change with tactic that, from a goal G with type T, creates a new (sealed?) goal G' with type T' such that T, T' are convertible.

I personally am interested in writing tactics to help write definitions, not just proofs, and I want the definitions to be as simple as possible to facilitate reasoning about them. I think inserting a lot of casts into a definition would decrease its readability, and so I don't view
refine {{ _ : lp:T' }} G GL as a good solution.

We can already do this by doing

Ltac change_with_ltac T T' := change T with T'.

so just exposing something like this directly would be a good start.