Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Equality for set-based reasoning using thestru...

view this post on Zulip Email Gateway (Aug 23 2022 at 08:57):

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,

I have a technical question for those who are well versed in
the formalizaton of applied mathematics in Isabelle/HOL using set-based
reasoning in HOL-Algebra (or similar).

I am curious as to what is the canonical approach for dealing with the
equality of algebraic structures (e.g. monoids). Suppose, a given monoid
undergoes a sequence of transformations, the result of these
transformations being an identical monoid (isomorphisms are not good
enough).

I am aware of two different solutions, but I am not certain whether there
exist (better) alternatives and which solution would be preferred/more
canonical?

  1. (Partial) equivalence relation. For example,

locale monoid_eq = monoid G + monoid F for G F +
assumes "carrier G = carrier F"
and "x ∈ carrier G ⟹ y ∈ carrier G ⟹ x ⊗⇘G⇙ y = x ⊗⇘F⇙ y"
and "𝟭⇘G⇙ = 𝟭⇘F⇙"

It should also be possible to define a partial quotient type based on
monoid_eq. However, I can imagine that this could result in a substantial
amount of boilerplate code (one would wish to transfer the entire
HOL-Algebra to the new type(s)).

  1. Augmentation of the monoid locale with an additional condition that
    mimics the restriction of the domain of the operation ⊗ to the carrier set
    via undefined. Once this is done, one can use the standard HOL's equality.

Here, I present more background information and describe my own experiences
with the aforementioned approaches.

Having tried the second solution in a reasonably sizeable development, I
found it to be very unwieldy. There seems to be a need to propagate this
type of condition to almost every derived structure and function operating
on such structures. At some point, I found myself spending more time
dealing with 'undefined' than doing work towards the development of the
theory that I was trying to develop.

Having recently tried the first solution, it seems to be more manageable:
it is not difficult to transfer results among the members of the same
equivalence class in an ad-hoc manner. Nonetheless, it does feel a little
bit odd to have to deal with two different notions of the concept of
equality and I have never seen anyone using this approach before.
Therefore, I decided to make an attempt to seek advice from the list.

Kind Regards,
Mikhail Chekhov

Last updated: Nov 21 2024 at 12:39 UTC