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



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
 


-- 
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.