[isabelle] Parametricity for functions which ignore arguments
Dmitriy and I are struggling with a proof about parametricity of a constant in
Isabelle/HOL. Suppose we have a natural functor 'a F and a parametric function foo
bnf_axiomatization 'a F
consts foo :: "'a F => ('a => 'c G) => 'c G"
foo_param: "!!A. rel_fun (rel_F A) (rel_fun (rel_fun A (rel_G B)) (rel_G B)) foo foo"
where 'b G is some type expression for which rel_G is the appropriate relator (G can be a
BNF, too, if this helps in any way).
Further, we know that for given x :: 'a F and y :: 'b F with "rel_F A x y", the function
foo ignores its second argument, i.e.,
!!f g. foo x f = foo x g
!!f g. foo y f = foo y g
Can we deduce from all of the above that "rel_G C (foo x f) (foo y g)" for any f and g?
And if so, how?
Intuitively, the reasoning goes as follows. Parametricity expresses that foo cannot create
values of type 'c out of nothing. By its type signature, it can only create such values by
using the second argument. However, for the given arguments x and y, we know that foo x
and foo y ignore their second arguments, so foo cannot create a value in 'c. That is, foo
must return a value of type 'c G which does not contain any 'c values at all. Therefore,
there exist values a and b such that rel_G C a b for any relation C. Hence,
rel_fun A (rel_G C) (%_. a) (%_. b)
and therefore foo x f = foo x (%_. a) `rel_G C` foo y (%_. b) = foo y g.
Is there a flaw in our intuitive reasoning? If not, how could this be formally expressed
This archive was generated by a fusion of
Pipermail (Mailman edition) and