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



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/
> 






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