*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Parametricity as a poor man's dependent typing*From*: Joachim Breitner <mail at joachim-breitner.de>*Date*: Fri, 24 Feb 2012 16:27:28 +0100*Organization*:*Sender*: Joachim Breitner <msg at joachim-breitner.de>

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/

**Attachment:
signature.asc**

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

**Re: [isabelle] Parametricity as a poor man's dependent typing***From:*Tobias Nipkow

- Previous by Date: [isabelle] post-doc position at MSR/INRIA centre
- Next by Date: Re: [isabelle] Parametricity as a poor man's dependent typing
- Previous by Thread: [isabelle] post-doc position at MSR/INRIA centre
- 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