2
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – chi Sep 3 '18 at 11:03
  • $\begingroup$ Interesting, @chi! I wasn't aware of this! $\endgroup$ – Mathias Vorreiter Pedersen Sep 3 '18 at 19:54
  • $\begingroup$ 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. $\endgroup$ – chi Sep 3 '18 at 21:01
4
$\begingroup$

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.

As you mentioned, you can (in principle) do a parametricity proof for a deeply-embedded language.

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – Jason Gross Sep 13 '18 at 14:12
2
$\begingroup$

There are plugins for Coq to prove such parametricity theorems. E.g. https://github.com/parametricity-coq/paramcoq which has been superseded by https://template-coq.github.io/template-coq/

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.