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

```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) 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:
>
>> 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?
>

```

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