Email Gateway (Aug 22 2022 at 17:21): Email Gateway (Aug 22 2022 at 17:21):From: Paulo Emílio de Vilhena <pevilhena2@gmail.com>
Dear all,
I’ve noticed an interesting behavior on locales and duplicate facts: it is
possible to have duplicate facts (same name and result) for the same locale
on different files, but if one tries to make an interpretation of this
locale on a context that imports both files, Isabelle realizes the
duplication and reports an error. This can get even more subtle: if you
prove a lemma for a locale B and prove that A is a sublocale of B, so if
the fact was already given earlier for A, one gets the same problem only
when trying to instantiate the locale A.
If someone decides to work on this issue, I’m available to help.
Cheers,
Paulo.
Email Gateway (Aug 22 2022 at 17:31):From: Lawrence Paulson <lp15@cam.ac.uk>
Would any locale experts like to tackle this problem? It can be demonstrated by visiting HOL/Algebra/IntRing.thy and adding Divisibility to the list of imports. Suddenly you get failures all over the place, starting at the line
interpretation int: abelian_group 𝒵
The problem is that Divisibility adds some duplicate names to the locale, such as l_cancel, r_cancel, Units_m_closed.
Larry
Email Gateway (Aug 22 2022 at 17:32):From: Makarius <makarius@sketis.net>
At the bottom of it is a generally looming danger with theory merges:
"containers" from either theory might be incompatible and fail to merge.
This happens so rarely in practice, that users often think of a merge as
total.
There might be workarounds for locale interpretation, but I can't say on
the spot how it works in detail.
Spontaneously, I would say it is a mistake in the HOL-Algebra library to
use such hidden duplicates. Wasn't it part of the project at Cambridge
to clean up fact names in this part?
Makarius
Email Gateway (Aug 22 2022 at 17:33):From: Lawrence Paulson <lp15@cam.ac.uk>
The name clashes come about in pretty obscure ways. Theory Group proves certain lemmas in the locale group. Theory Divisibility creates a new locale, monoid_cancel, assuming the exact same lemmas as axioms and with the same names. Then it goes on to prove
sublocale group ⊆ monoid_cancel
by standard simp_all
There is still no sign of anything wrong, although already (I think) locale group now has conflicting names and can't be instantiated any more. The name clash should be flagged at this point.
Larry
Email Gateway (Aug 22 2022 at 17:33):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
The problem is not just the sublocale declaration. For example, the lemma Units_m_closed
in Divisibility is put into the locale monoid, but the same lemma has been proven in the
same locale in theory Group. This is not detected in theory Divisibility because the names
for the two theorems in the background theory are different due to the different theory
names. The problem only manifests when an interpretation tries to interpret the monoid
locale because this notes the theorem twice. There is no workaround in Isabelle2017 for this.
For the l_cancel problem, there is a workaround, but it needs two theories.
In theory 1, import only Group, but not Divisibility and add an interpretation of the
locale monoid under a suitable qualifier q.
In theory 2, import theory 1 and Divisibility. Interpret the locale monoid_cancel with
a different qualifier q'. Then interpret group with qualifier q.
In step 2, the first interpretation ensures that the locale roundup algorithm will not
attempt to interpret monoid_cancel during the second interpretation. The drawbacks of this
solution are:
a. The theorems that divisibility adds to monoid are not available in either theory.
b. The definitions and theorems from monoid_cancel must be reference with qualifier q'
instead of q.
Best,
Andreas
Last updated: Apr 26 2024 at 16:20 UTC