*To*: Joachim Breitner <mail at joachim-breitner.de>*Subject*: Re: [isabelle] Parametricity as a poor man's dependent typing*From*: Stephan Merz <Stephan.Merz at loria.fr>*Date*: Fri, 24 Feb 2012 16:36:46 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <1330097248.5176.21.camel@kirk>*References*: <1330097248.5176.21.camel@kirk>

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 On 24 Feb 2012, at 16:27, Joachim Breitner wrote: > 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? > > -- > Joachim "nomeata" Breitner > mail at joachim-breitner.de | nomeata at debian.org | GPG: 0x4743206C > xmpp: nomeata at joachim-breitner.de | http://www.joachim-breitner.de/ >

**Follow-Ups**:**Re: [isabelle] Parametricity as a poor man's dependent typing***From:*Joachim Breitner

**References**:**[isabelle] Parametricity as a poor man's dependent typing***From:*Joachim Breitner

- Previous by Date: [isabelle] Parametricity as a poor man's dependent typing
- Next by Date: Re: [isabelle] Parametricity as a poor man's dependent typing
- Previous by Thread: [isabelle] Parametricity as a poor man's dependent typing
- Next by Thread: Re: [isabelle] Parametricity as a poor man's dependent typing
- Cl-isabelle-users February 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list