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



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
Description: This is a digitally signed message part



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