Email Gateway (Aug 18 2022 at 14:13): Email Gateway (Aug 18 2022 at 14:13):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
there are two ways of defining lattices in Isabelle:
The first approach makes the carrier set of the lattice explicit, as
e.g. in HOL/Algebra/Lattice.thy, the
second one (in HOL/Lattices.thy and HOL/Lattices/*) uses implicit
carrier sets (the UNIV-set of a type) and type-classes.
Is there a systematic/automatic way to go from theorems with the
implicit carrier set to corresponding theorems for an explicit carrier set?
My concrete problem is, that I have many theorems for the implicit
carrier-set, but the algorithms I want to verify require parametric
carrier sets, e.g.
I need the lattice of all subsets of control locations in the program,
that has some nice properties (e.g. finite-height) only, if there are
only finitely many
control locations.
However, because the set of control locations is a parameter of the
algorithm I want to verify, I cannot fix it in advance, and thus cannot
define a datatype of control locations, that
would be required to show that it's corresponding set-type is in the
lattice-typeclass.
Any ideas? Is the only way to redo the proofs of all necessary theorems
for explicit carrier sets?
Regards and thanks for any hints,
Peter
Email Gateway (Aug 18 2022 at 14:13):From: Lawrence Paulson <lp15@cam.ac.uk>
Unfortunately, I suspect that that will be necessary.
Larry Paulson
Email Gateway (Aug 18 2022 at 14:13):From: Alexander Krauss <krauss@in.tum.de>
Hi Peter,
My concrete problem is, that I have many theorems for the implicit
carrier-set, but the algorithms I want to verify require parametric
carrier sets, e.g.
[...]
Any ideas? Is the only way to redo the proofs of all necessary theorems
for explicit carrier sets?
The developer version contains a transfer tool (written by Amine Chaieb)
which may be helpful in situations like yours. Currently it is used for
lifting theorems between int and nat etc. But there is not really much
experience in using it, and it is not part of an official release, so
expect the unexpected! (and maybe redoing the proofs is less painful in
the end). Probably Amine or someone else can point you to an example of
how it can be used...
Alex
Email Gateway (Aug 18 2022 at 14:14):From: Clemens Ballarin <ballarin@in.tum.de>
Quoting Peter Lammich <peter.lammich@uni-muenster.de>:
there are two ways of defining lattices in Isabelle:
The first approach makes the carrier set of the lattice explicit, as
e.g. in HOL/Algebra/Lattice.thy, the
second one (in HOL/Lattices.thy and HOL/Lattices/*) uses implicit
carrier sets (the UNIV-set of a type) and type-classes.
In fact, there is a third, even more general way: don't use the HOL
equality, but an arbitrary equivalence relation.
HOL/Algebra/Lattice.thy explores this, based on work by Stephan Hohe.
Is there a systematic/automatic way to go from theorems with the
implicit carrier set to corresponding theorems for an explicit carrier set?
I believe that this is theoretically not possible in general. It
might be, if you restrict the kind of statements to a subset of
formulae -- for example, universal sentences only. I believe that
Peter Homeier addressed such issues in his quotient type work for HOL.
Clemens
Email Gateway (Aug 18 2022 at 14:14):From: Jeremy Avigad <avigad@cmu.edu>
Friends,
Below Alex is referring to a transfer method that Amine and I
developed while I was revising Isabelle's number theory library,
designed to help transfer theorems about the natural numbers to
equivalent statements about the nonnegative integers and vice-versa.
The idea is simple: whenever you have a bijection from a subset A of
one type (possibly the universal set) to a subset B of another, and
some functions and relations that respect the bijection, then any
theorem about A is equivalent to a theorem about B. (Similarly things
can be said about surjections rather than bijections, e.g. quotient
maps.) The transfer method simply applies carefully chosen rewrite
rules to translate theorems back and forth between such domains.
You can find the code for transfer in Transfer.ML, and the rules
designed specifically for transfer between nats and ints in
Nat_Transfer.thy of the developer version. They are put to use in
files like GCD.thy, Primes.thy, and UniqueFactorization.thy (the
latter two are in NumberTheory). It is pretty nifty: you give the
method a nat theorem and it returns the corresponding int theorem, or
vice-versa. It even works with higher-order constructs like summation,
etc.
But the methods are still in a prototype stage. Amine and I still need
to find time to polish them and put in rules for other higher-order
constructs, and improve the interface and document it. I'm not sure if/
when that will happen...
Unfortunately, this won't solve Peter's problem. The issue is that, in
general, one does not have bijections between parameterized structures
and types. This is what makes simple type theory simple: types can't
depend on parameters. (There is a trick due to John Harrison for
encoding natural numbers as types, and using polymorphism over type
variables, but it is limited.) Axiomatic type classes are simply stuck
in type-land.
If you really want to use structures that depend on parameters, here
are some options:
(1) (Re)do everything in locales, as Larry suggests.
(2) Give up on simple type theory and use a dependent type theory like
Coq (see e.g. Gonthier's finite group theory project).
(3) Give up on simple type theory and go the other direction, to set
theory. See, for example, Mizar's type system for an example of how
infrastructure for keeping track of types can be added on top of set
theory.
Tobias Nipkow, Brian Huffman, Amine Chaieb, and I once discussed ways
that one could embed Isabelle's type theory in a larger set-theoretic
framework, e.g. adding a type of sets and axioms that guarantee that
"small" types correspond to sets. If done right, that could yield a
consistent system (e.g. having the same logical strength as set
theory) where one could go back and forth between typed and set-
theoretic versions of theorems, and so, indirectly, from axiomatic-
type class versions to set-based locale versions. I still think that's
an idea worth exploring, if anyone is willing and able.
Best wishes,
Jeremy
Email Gateway (Aug 18 2022 at 14:14):From: "Dr. Brendan Patrick Mahony" <brendan.mahony@dsto.defence.gov.au>
This is an issue that has been of interest for some time.
If you want to do interesting mathematics (eg about lattices rather
than using lattices) you really should be using explicit carrier sets.
My intuitions suggest that the existing axclass - locale binding could
be strengthened to support moving seamlessly from "pure" mathematics
(on carrier set algebras) to "applied" mathematics (on type algebras).
A "carrier" locale could be associated with the "type" axclass and new
axclasses could be developed as specialised extensions of the
"carrier" locale (restrict to single type parameter, what else?). An
instance of the axclass is induced from an interpretation of the
locale with a universal carrier set.
We have a lattice development with this sort of structure, carrier
based development of sub-lattices, lattice morphisms, and other useful
approaches to proving lattice instances. A couple of linking theorems
then connect axclass and locale to make it easy to prove type lattice
instances.
It would be nice if the Isabelle axclass mechanism gave serious
support for this sort of approach.
IMPORTANT: This email remains the property of the Australian Defence Organisation and is subject to the jurisdiction of section 70 of the CRIMES ACT 1914. If you have received this email in error, you are requested to contact the sender and delete the email.
Email Gateway (Aug 18 2022 at 14:14):From: Lawrence Paulson <lp15@cam.ac.uk>
Yes, this would be an excellent research project for somebody who is
familiar with a variety of type theories and also has an intuitive
understanding of set theory. But finding such a person is probably
more difficult than finding somebody who is conversant in both Latin
and Klingon.
Larry
Email Gateway (Aug 18 2022 at 14:14):From: Gergely Buday <gbuday@gmail.com>
So it is a "challange". My question is whether having such a theory
makes it easy to tailor Isabelle to do such lifting between the two
kinds of theory development? How much programming work would this be
to have a usable framework?
Last updated: Apr 23 2024 at 20:15 UTC