Hi. What is the ~~best~~ fastest way of proving the equality of two permuted expressions in a commutative monoid, under the additional assumption that the underlying permutation is actually known?

So far, I'm just passing the desired equality to the simplifier alongside the associativity + commutativity laws, but (a) this does not benefit from the knowledge of what the permutation is, and (b) I sometimes have schematic entries in the expression, and the simplifier will generate lots of flex-flex pairs when proving the permutation. This seems unnecessary, and has moreover led to infinite loops in other places where e.g. `clarify`

would indefinitely succeed because it keeps renaming flex-flex pairs but not actually changing anything.

I considered applying the permutation explicitly using conversions, but was put off somewhat by the tedious nature of doing this (the number of 'atomic' conversions one has to apply is actually pretty large...) and the comment from the cookbook that conversions are "often much less efficient than the simplifier"

A third option which I pondered but didn't yet implement was to lift LHS and RHS to folds of multisets and then hope that there's a fast way of proving equality of two multisets. But here, too, I don't know if I should expect this to be any better than the raw simplifier approach.

Any experience / expectations / suggestions? Thanks!

Just for the schematics, doesn't using Subgoal.FOCUS fixes all the schematics avoiding all problems of possible unification?

I am pretty sure that it only fixes the forall-bound parameters, not the schematics

Maybe we are not talking about the same thing:

```
(*f is just for printing*)
ML \<open>
fun f ctxt (x:Subgoal.focus) = (@{print} (x); simp_tac ctxt 0)\<close>
schematic_goal "2*2 = ?a" for a :: nat
apply (tactic \<open>HEADGOAL (Subgoal.FOCUS_PREMS (fn _ => simp_tac @{context} 0) @{context})\<close>)
(*fails to do anything and cannot instantiate ?a*)
apply (tactic \<open>HEADGOAL (simp_tac @{context})\<close>)
(*succeeds*)
```

Yes, I was confusing it with `FOCUS_PARAMS`

, that does also not fix them. I never realized that `FOCUS_PREMS`

does, I rarely use that one

I don't see a difference between FOCUS and FOCUS_PREMS on this example (and in the code ` Thm.instantiate_cterm schematics concl`

is unconditional)

That is weird, because this:

```
schematic_goal "2 * 2 = ?a" for a :: nat
apply (tactic ‹HEADGOAL (Subgoal.FOCUS (fn {context=ctxt,...} =>
resolve_tac @{context} [refl] 1
) @{context})›)
```

does not solve the goal, while

```
schematic_goal "2 * 2 = ?a" for a :: nat
apply (tactic ‹HEADGOAL (Subgoal.FOCUS_PREMS (fn {context=ctxt,...} =>
resolve_tac @{context} [refl] 1
) @{context})›)
```

works (`FOCUS_PARAMS`

also works).

Hey! I went with pre-generating a bunch of equality theorems for 'picker'-permutations `(1,2,...,n) -> (i,1,2,...,)`

, and then building the desired permutations from those explicitly via conversions. That seems to be working OK.

Last updated: Dec 07 2023 at 16:21 UTC