## Stream: Isabelle/ML

### Topic: Equality in commutative monoids

#### Hanno Becker (Apr 12 2023 at 04:51):

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!

#### Mathias Fleury (Apr 12 2023 at 05:11):

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

#### Jan van Brügge (Apr 12 2023 at 08:04):

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

#### Mathias Fleury (Apr 12 2023 at 08:55):

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*)
(*succeeds*)
``````

#### Jan van Brügge (Apr 12 2023 at 09:48):

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

#### Mathias Fleury (Apr 12 2023 at 10:22):

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)

#### Jan van Brügge (Apr 15 2023 at 09:03):

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).

#### Hanno Becker (Apr 21 2023 at 11:08):

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