Equality in commutative monoids · Isabelle/ML

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.

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

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

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

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

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

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.

Stream: Isabelle/ML

Topic: Equality in commutative monoids