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.