Stream: Beginner Questions

Topic: How can I simplify the following lemmas?

Hernán Rajchert (Feb 01 2023 at 23:05):

I have a typedef Assets and instantiations for zero, plus, semigroup_add, ab_semigroup_add and some others. And I have the following code

type_synonym Accounts = "AccountId ⇀ Assets"

fun mergeAccounts :: "Accounts ⇒ Accounts ⇒ Accounts" where
"mergeAccounts acc1 acc2 = (λaccId. combine_options (+) (acc1 accId) (acc2 accId))"

lemma mergeAccountsAssoc : "mergeAccounts (mergeAccounts a b) c = mergeAccounts a (mergeAccounts b c)"
proof -
  let ?l = "mergeAccounts (mergeAccounts a b) c"
  let ?r = "mergeAccounts a (mergeAccounts b c)"
  have "⋀x. ?l x = ?r x"
    by (simp add: Groups.semigroup_add_class.add.assoc combine_options_assoc)
  thus ?thesis
    by simp
qed

lemma mergeAccountsComm : "mergeAccounts a b = mergeAccounts b a"
proof -
  let ?l = "mergeAccounts a b"
  let ?r = "mergeAccounts b a"

  have "⋀x. ?l x = ?r x"
    by (simp add: Groups.ab_semigroup_add_class.add.commute combine_options_commute)
  thus ?thesis
    by simp
qed

It works, but is rather verbose. Is there a way to simplify this? I was trying to use the is keyword to avoid the formula repetition but I wasn't able to locate the documentation (searching "is" by text is hard :sweat_smile: ).

Also, not sure if this applies, but should I transfer the goal or make a subgoal? I struggled trying to solve the problem at the initial level and it was trivial once I started using the let ?l, let ?r.

Lukas Stevens (Feb 03 2023 at 14:00):

The is keyword works by providing a term (with potential wildcards _) that matches the goal according to higher-order pattern unification. After the is you can use the matched variables to refer to subterms of the goal. In you case it would be (is "?l = ?r").

Lukas Stevens (Feb 03 2023 at 14:01):

I don't know what transfer has to do with your problem. Transfer is used to rewrite the goal in accordance with transfer relations, e.g. transforming a goal that talks about nats to a goal talking about non-negative ints.

Wolfgang Jeltsch (Feb 03 2023 at 16:44):

Hernán Rajchert said:

I was trying to use the is keyword to avoid the formula repetition but I wasn't able to locate the documentation (searching "is" by text is hard :sweat_smile: ).

You can look up is in the index at the end of The Isabelle/Isar Reference Manual. :smile:

Also, not sure if this applies, but should I transfer the goal or make a subgoal?

Without having had a deeper look at your code, I would say you shouldn’t use transfer here, because you managed with bare simplification. The transfer method takes you to a lower level of abstraction (the representations of assets in your case), but you should reason on a higher level of abstraction if possible.

Hernán Rajchert (Feb 03 2023 at 19:13):

Thanks! I was missing the parenthesis around the is keyword :man_facepalming:

And actually I didn't even needed to add the ?l ?r bindings, I simplified the proofs to

lemma mergeAccountsAssoc : "mergeAccounts (mergeAccounts a b) c = mergeAccounts a (mergeAccounts b c)"
  by (simp add: Groups.semigroup_add_class.add.assoc combine_options_assoc)

lemma mergeAccountsComm : "mergeAccounts a b = mergeAccounts b a"
  by (simp add: Groups.ab_semigroup_add_class.add.commute combine_options_commute)

I still wonder why sledgehammer didn't find the solution to the lemma but did find it for the intermediatehave.

Wolfgang Jeltsch (Feb 03 2023 at 19:24):

Hernán Rajchert said:

I still wonder why sledgehammer didn't find the solution to the lemma but did find it for the intermediatehave.

Don’t rely too much on Sledgehammer. Experimentation can also be fruitful. For example, if your proof consists of two steps, which both are solved using simp, as is the case with your code above, you might just be able to merge them into one step that uses simp. It is, of course, possible that this won’t work, since simp applies available simplification rules as it sees fit, without reconsidering bad choices. Another trick is to try to merge two blast invocations into one or a simp and a blastinvocation into an auto invocation.

By the way, there is also try, which invokes several proof-finding and disproving tools, including Sledgehammer, and there is also try0, which is invoked by try and finds you invocations of the simple proof methods (which I prefer), like simp, blast, auto, and fastforce. For try0 to be successful, you might want to pass to it facts it should consider via the simp, intro, elim, and dest parameters.

Last updated: Apr 26 2024 at 16:20 UTC