Hi, I am trying to write a tactic that does the following:

- find an expression of some commutative monoid in a proof goal, call it
`original`

- compute a rearranged expression, call it
`new`

- replace
`original`

with`new`

; since`original = new`

, I suppose the simplifier can just prove it - remove the premise
`original = new`

from the premises.

so my question is, how do I achieve step 3 and 4? I asked previously so people say that the simplifier is complete in solving commutative monoid. A few pointers leading me to the right direction would be appreciated.

Do you know either where in the goal `original`

will appear or what `original`

will be? Otherwise this will be really hard

yes I know its type and it's in a fixed position (more or less). In general, finding `original`

shouldn't be difficult and deriving `new`

is dead easy

or in a big picture, I want to replace the goal `P original`

with `P new`

without adding anything to the context

You will have to create the term `original = new`

and prove that separately. Then you can use `unfold_thms_tac`

to replace all occurrences of `original`

by `new`

.

Last updated: Dec 07 2023 at 16:21 UTC