Stream: Isabelle/ML

Topic: Equality in commutative monoids


view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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*)
  apply (tactic \<open>HEADGOAL (simp_tac @{context})\<close>)
   (*succeeds*)

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip 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 2024 at 16:22 UTC