*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Parametricity as a poor man's dependent typing*From*: Joachim Breitner <mail at joachim-breitner.de>*Date*: Fri, 24 Feb 2012 16:52:40 +0100*In-reply-to*: <9D4D4BD4-C9A1-4E3E-AA44-50884345719C@loria.fr>*Organization*:*References*: <1330097248.5176.21.camel@kirk> <9D4D4BD4-C9A1-4E3E-AA44-50884345719C@loria.fr>*Sender*: Joachim Breitner <msg at joachim-breitner.de>

Hi, hmm, not completely. But it seems there is more to do than just replace UNIV by S, e.g. every (ALL x :: 'a. P) would become (∀x∈S. P), and similarly for existential quantifiers. Then P S == ALL x. x ∈ S becomes P S == ∀x∈S. x ∈ S and things are sound again. I’m not deep into the theory of HOL enough to completely describe the required transformation though. "undefined" comes to mind, this needs to be replaced by "Some S". Greetings, Joachim Am Freitag, den 24.02.2012, 16:36 +0100 schrieb Stephan Merz: > 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/ > > > > > -- 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**

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

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

- Previous by Date: Re: [isabelle] Parametricity as a poor man's dependent typing
- Next by Date: [isabelle] Syntax, translations inside a locale
- Previous by Thread: Re: [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