Email Gateway (Aug 19 2022 at 11:36): Email Gateway (Aug 19 2022 at 11:36):From: Aleks Kissinger <aleks0@gmail.com>
Hi all,
This is mainly a question for the nominal folks, but I figured other
people might have some good suggestions as well. I'm looking to
formalise a nominal algebraic theory in Isabelle, which consists
(essentially) of a binder and an associative/commutative
multiplication operation. The types of theorems I want to prove
initially are things of the form "s = t", where s and t are elements
of such a nominal algebra A, presented by generators and relations.
So, there seem to be a handful of choices available for doing this, so
I'm trying to get an idea of what approach will yield the nicest
proofs, with the least overhead/faff. The two ideas I had in mind
were:
Forming a nominal_datatype and taking a quotient. This seems like
the obvious choice, but I have a few questions about it. Firstly, in
Nominal2, a nominal_datatype is already a quotient. Is this
quotient-of-a-quotient setup going to be a pain? If not, what things
need to be lifted to the quotient type in order to keep working modulo
alpha-equivalence as automatic as possible?
Forming the nominal_datatype, then defining a new equivalence
relation ~~ with the axioms of the algebra, along with any relations
between generators. Prove theorems of the form "s ~~ t". Essentially,
the the first half of the construction in #1, but don't bother with a
quotient type. This seems to come with its own set of problems. For
instance, things like "s ~~ t ==> P s ==> P t" would need to be
assumed for particular P, rather than being an axiom of HOL (as is the
case with "=").
Treating A as a "theory" rather than a presentation of a particular
algebra. That is, form a locale where the term formers are assumed as
functions, then assume relevant equalities, including equivariance
properties for the term formers. I think the latter should be tagged
[eqvt] so the nominal code knows it can apply them to try and
alpha-unify terms in various places. The main downside here is you
don't get all the nice scaffolding that is laid down by
nominal_datatype, but by having the correct assumptions/theorems in
context, a term built from these assumed functions could, at least in
theory, be handled in much the same way (though clearly things like
injectivity of constructors gets lost, once non-trivial equations are
assumed).
I'm pretty new to Isabelle, and especially Nominal/Nominal2. Any input
and pointers to relevant docs or examples would be much appreciated.
Many thanks,
Aleks
Email Gateway (Aug 19 2022 at 11:37):From: Christian Urban <christian.urban@kcl.ac.uk>
Hi Alex,
Email Gateway (Aug 19 2022 at 11:37):From: Dmitriy Traytel <traytel@in.tum.de>
I think the transferred attribute is supposed to do just that.
Dmitriy
Email Gateway (Aug 19 2022 at 11:37):From: Dmitriy Traytel <traytel@in.tum.de>
Oh, I see now that my reply applies to the development version only
(e.g. Isabelle/0cd62cb233e0). In Isabelle2013 this attribute is
implemented by legacy_transfer (i.e. not working with Lifting/Transfer).
Dmitriy
Email Gateway (Aug 19 2022 at 11:37):From: Makarius <makarius@sketis.net>
Reading this 2 or 3 times, I still don't understand what is meant -- too
many negations.
Isabelle has many different languages of different kind and purpose:
Isabelle/ML, Isabelle/Isar, Isabelle/Scala, Isabelle/Pure, Isabelle/HOL,
Isabelle/latex document source etc.
It does not make any sense to speak about "levels" here, and Isabelle/ML
vs. Isabelle/Isar are particularly difficult to arrange in 2-dimensional
topology. In reality it probably looks more like a Klein bottle.
To understand how Isabelle works, one needs to get basic terminology
right, and maybe spend some efforts to stop using wrong expressions.
Makarius
Email Gateway (Aug 19 2022 at 11:38):From: Makarius <makarius@sketis.net>
Using Isabelle/ML is definitely not trivial, but it is much easier than it
used to be several years ago, and the official documentation is
continously getting more and more complete, although rather thick now.
It is also much better than Coq, for example, where the reader of the
sources also needs to know some French, not just OCaml.
Getting basic terminology right is only the starting point, it is
necessary but not sufficient for what follows for those Isabelle users who
want to embark on building their own tools for the platform.
Makarius
Email Gateway (Aug 19 2022 at 11:39):From: Aleks Kissinger <aleks0@gmail.com>
Thanks for your feedback. A the moment, it looks like the best
solution is to keep the explicit congruence around. Simple proofs seem
to take approximately this shape:
theorem A ~~ B
proof -
have A A' by (* alpha-equivalence + reflexive *)
also have ... ~~ B' using (* some algebraic rule *) by blast
also have ... B by (* alpha-equivalence + reflexive *)
finally show ?thesis .
qed
Perhaps this can be improved, but this seems to work okay for my
purposes. The thing I have in mind is to write various tactics which
produce many such proof steps using some meta-reasoning (in this case,
a diagram representation and some rewriting techniques for the
expressions A and B).
Last updated: Apr 19 2024 at 01:05 UTC