# Re: [isabelle] Parametricity as a poor man's dependent typing

• To: cl-isabelle-users at lists.cam.ac.uk
• Subject: Re: [isabelle] Parametricity as a poor man's dependent typing
• From: Joachim Breitner <breitner at kit.edu>
• Date: Fri, 10 Aug 2012 13:23:32 +0200
• References: <1330097248.5176.21.camel@kirk> <9D4D4BD4-C9A1-4E3E-AA44-50884345719C@loria.fr> <1330098760.5176.31.camel@kirk>

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.

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

--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.info.uni-karlsruhe.de/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.