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



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



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