Email Gateway (Aug 18 2022 at 19:14): Email Gateway (Aug 18 2022 at 19:14):From: Joachim Breitner <mail@joachim-breitner.de>
Dear Isabelle list,
when doing Group Theory in Isabelle, for example in the Free Groups
submission to AFP, I keep proving facts that are “obvious” to the
mathematician and where I would expect a type system to do the work for
me, but I was told that this cannot be done in Isabelle because it does
not support dependent types. This leads to code as in
http://afp.sourceforge.net/browser_info/devel/HOL/Free-Groups/PingPongLemma.html
(unfortunately, the lines have no anchors, but search for “The following
lemmas establish all” and see how I defined mems).
Note how almost all these lemmas would be trivial if we had “X = UNIV”
and “carrier G = UNIV”, or put differently, if these were types of their
own. But they are not, these are sets, although I do _not_ use any
property of their elements and I do _not_ anywhere require elements of
the set’s carrier type that are not in the set.
I was wondering if a parametricity argument as follows is sound, and if
it is, if it can somehow be used in Isabelle to simplify the proofs
(Syntax somewhat liberal, I hope I get the idea across):
If for a free type variable 'a, “P(UNIV :: 'a)” holds,
and given “S ≠ Ø”,
we know “P S” holds.
Assume this ideas was provided as a lemma attribute. Then I could much
more easily prove, for example,
lift_is_hom':
[[ group G; f ∈ gens -> carrier G; carrier G = UNIV :: 'a ]]
==> G.lift g ∈ hom (free_group X) G
and obtain the result that I want,
lift_is_hom:
[[ group G ; f ∈ gens -> carrier G ]]
==> G.lift g ∈ hom (free_group X) G
by something like
lift_is_hom = lift_is_hom'[parametricity 'a "carrier G", simp].
Greetings,
Joachim
PS: I posed a related question in December 2010 and Alexander Krauss
dangled a possible solution:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-December/msg00040.html
did anything come out of this already?
signature.asc
Email Gateway (Aug 18 2022 at 19:14):From: Stephan Merz <Stephan.Merz@loria.fr>
But suppose
P S == ALL x. x : S
Then you have
P (UNIV :: 'a set)
for any type 'a but not P S for an arbitrary non-empty set S. Or am I completely off-track?
Stephan
Email Gateway (Aug 18 2022 at 19:14):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
hmm, not completely. But it seems there is more to do than just replace
UNIV by S, e.g. every (ALL x :: 'a. P) would become (∀x∈S. P), and
similarly for existential quantifiers. Then
P S == ALL x. x ∈ S
becomes
P S == ∀x∈S. x ∈ S
and things are sound again. I’m not deep into the theory of HOL enough
to completely describe the required transformation though. "undefined"
comes to mind, this needs to be replaced by "Some S".
Greetings,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 19:14):From: Tobias Nipkow <nipkow@in.tum.de>
Unfortunately, Alex Krauss is not pursuing this angle anymore. I don't
think there is a general parametricity theorem for HOL, but I am sure
one could transform a certain class of HOL proofs and raise the
theorem from a type to a set. But it takes some work to automate this.
Tobias
Am 24/02/2012 16:27, schrieb Joachim Breitner:
Dear Isabelle list,
when doing Group Theory in Isabelle, for example in the Free
Groups submission to AFP, I keep proving facts that are “obvious”
to the mathematician and where I would expect a type system to do
the work for me, but I was told that this cannot be done in
Isabelle because it does not support dependent types. This leads to
code as in
http://afp.sourceforge.net/browser_info/devel/HOL/Free-Groups/PingPongLemma.html(unfortunately, the lines have no anchors, but search for “The following
lemmas establish all” and see how I defined mems).Note how almost all these lemmas would be trivial if we had “X =
UNIV” and “carrier G = UNIV”, or put differently, if these were
types of their own. But they are not, these are sets, although I do
_not_ use any property of their elements and I do _not_ anywhere
require elements of the set’s carrier type that are not in the
set.I was wondering if a parametricity argument as follows is sound,
and if it is, if it can somehow be used in Isabelle to simplify the
proofs (Syntax somewhat liberal, I hope I get the idea across):If for a free type variable 'a, “P(UNIV :: 'a)” holds, and given “S
≠ Ø”, we know “P S” holds.Assume this ideas was provided as a lemma attribute. Then I could
much more easily prove, for example,lift_is_hom': [[ group G; f ∈ gens -> carrier G; carrier G = UNIV
:: 'a ]] ==> G.lift g ∈ hom (free_group X) Gand obtain the result that I want,
lift_is_hom: [[ group G ; f ∈ gens -> carrier G ]] ==> G.lift g ∈
hom (free_group X) Gby something like
lift_is_hom = lift_is_hom'[parametricity 'a "carrier G", simp].
Greetings, Joachim
PS: I posed a related question in December 2010 and Alexander
Krauss dangled a possible solution:This is a notorious problem, and there is no satisfactory
solution. From 2011 on I'll be working on an infrastructure to
deal with this (basically recovering what type systems do on the
level of reasoning), but I am not expecting to have something
usable for quite some time.https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-December/msg00040.html
did anything come out of this already?
Email Gateway (Aug 19 2022 at 08:14):From: Joachim Breitner <breitner@kit.edu>
Hi,
I thought more about using parametricity to ease working with
definitions that only make sense on a set of values, and where lots of
lemmata will have such a set membership as an assumption. Right now I am
wondering if the transfer package can be of some help here.
So I start with some abstract set:
axiomatization a_set :: "nat set" where ne: "a_set ≠ {}"
and I want to prove something like
lemma goal: assumes "list_all (λx. x ∈ a_set) xs"
and "∀x ∈ a_set. f x ∈ a_set"
shows "list_all (λx. x ∈ a_set) (map f xs)"
where "map" is just an example for a possibly much more complicated
polymophic expression.
To make working with closed functions on the set easier, I create a type
and set it up for the transfer package:
typedef (open) a_type = a_set using ne by auto
setup_lifting type_definition_a_type
The idea is that if I can do some calculation on this type that’s
related to a calculation on a_set, then the result will also be in the
set:
lemma untransfer: "list_all2 cr_a_type x y ⟹ list_all (λx. x∈a_set) x"
by (induct rule: list_all2_induct, auto simp add:cr_a_type_def Rep_a_type)
And indeed I can prove the goal:
lemma goal: assumes "list_all (λx. x ∈ a_set) xs"
and "∀x ∈ a_set. f x ∈ a_set"
shows "list_all (λx. x ∈ a_set) (map f xs)"
proof-
have "list_all2 cr_a_type xs (map Abs_a_type xs)" (is "list_all2 _ _ ?xs'")
using assms(1)
by (auto simp add:list_all2_def cr_a_type_def set_zip list_all_length Abs_a_type_inverse)
moreover
have "fun_rel cr_a_type cr_a_type f (λ x. Abs_a_type (f (Rep_a_type x)))" (is "fun_rel _ _ _ ?f'")
using assms(2)
by (auto simp add:cr_a_type_def Abs_a_type_inverse Rep_a_type)
ultimately
have "list_all2 cr_a_type (map f xs) (map ?f' ?xs')"
by -(rule fun_relD[OF fun_relD[OF map_transfer]])
thus ?thesis
by (rule untransfer)
qed
Note that everything related to the actual operation I am doing on f and
x is just mechanical application of transfer rules. Also the first two
steps are what the lifting package does all the time. So it seems that
this pattern can be automated.
The main problem seems to be that this only works well for a
globally-defined set "a_set". Trying to make goal abstract in "a_set"
using a context fails
context fixes S :: "nat set" assumes ne:"S ≠ {}"
begin
typedef (open) S_type = S using ne by auto
setup_lifting type_definition_a_type
(* ... *)
with
Illegal variables in representing set: "S"
The error(s) above occurred in typedef "S_type".
So one question is: Is it fundamentally not possible (i.e. unsound) to
define a type within a context that depends on a parameter? Or is
theoretically acceptable as long as the type does not escape the
context, i.e. only lemmas are available to the outside that do not
mention this type?
Greetings,
Joachim
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC