# Proving parametricity for Gallina functions

I have the following definitions

Definition nat'' {X : Type} := (X -> X) -> X -> X.
Definition nat' := forall (X : Type), @nat'' X.


And when I wanted to prove a certain property I ended up in the following situation:

  m : nat'
H : 0 = m nat S 0
X : Type
s : X -> X
z : X
============================
m X s z = z


which should be some kind of free theorem! Specifically, m: (forall X : Type), (X -> X) -> X -> X is a function that should behave parametrically for any instantiation of X, so by knowing that 0 = m nat S 0 I should be able to deduce that x = m X f x for any x : X and f : X -> X.

But I haven't seen such free theorems stated in Coq for Gallina terms. Is there an easy way to go about proving such a result without some deep embedding of a language and proving parametricity for this language?

• I believe that the logic of Coq admits ad-hoc models, where parametricity does not hold. Informally, we can envision a t : nat' in the model which behaves as zero when X is empty, and as one otherwise -- breaking parametricity. Such t is not definable in Coq, but present in some model. Hence, by soundness, we can't prove parametricity in Coq (unless we introduce new axioms). I can't justify this precisely since my knowledge of Coq models is quite limited -- hopefully others can provide more insight.
– chi
Commented Sep 3, 2018 at 11:03
• Interesting, @chi! I wasn't aware of this! Commented Sep 3, 2018 at 19:54
• Imagine you could write in Coq something like M = fun (T: Type) (x y: T) => if T = nat then x else y with type forall T, T -> T -> T, i.e. a Church-encoded boolean. (Coq rejects this, of course.) Then, M would be a boolean other than true and false, violating parametricity. I'd somehow expect that some model has something like M inside.
– chi
Commented Sep 3, 2018 at 21:01

My belief has always been that you cannot prove such free theorems from within Gallina about Gallina terms, but I don't have a definite reason why. I certainly can't imagine how this proof would work, given that there's no way to analyze functions like instances of nat' other than applying them.
• There's a construction in the HoTT book of a non-parametric function from excluded middle on hProps. Basically, you can decide for any type "is there exactly one non-identity isomorphism of this type?" because all proofs of existence of such a unique isomorphism are equal (if you assume function extensionality). Now you have a function of type forall T, T -> T which is negation on bool and identity on anything not equivalent to bool. Commented Sep 13, 2018 at 14:12