Define a polymorphic type in coq

Question

So i was doing an exercise for learning coq. and I was trying to defind a type according to this encoding: forall X.(X -> X) -> X -> X;`and this is from Alonzo Church(he proposed an encoding for natural number) as below:

0 , f:x:x

1 , f:x:fx

2 , f:x:f(fx)

3 , f:x:f(f(fx))

.....

n , f:x:fnx:

My code is like below:

Definition nat := forall X : Type, (X -> X) -> X -> X.

And the exercise require me to define expressions zero,one,two and three that encode the corresponding numbers as elements of nat: Below is what I thought it will be

Definition zero : nat :=
  fun (X : Type) (f : X -> X) (x : X) => x.
Definition one : nat := 
  fun (X : Type) (f : X -> X) (x : X) => f x.
Definition two : nat :=
  fun (X : Type) (f : X -> X) (x : X) => f (f x).
Definition three : nat :=
  fun (X:Type)(f: X -> X)(x: X) => f ( f ( f x )).

My question is I need to prove that the plus n one = succ n. and the n is my defined type Nat

I have a succ function defined as below:

Definition succ (n : nat) : nat :=
fun (X : Type) (f : X -> X) (x : X) => f (n X f x).

my plus function defined as below:

Definition plus (n m : nat) : nat :=
fun (X : Type) (f : X -> X) (x : X) => (n X f (m X f x)).

The thing is when I tried to prove plus n one = succ n, I stuck in the middle and have no idea how to prove. code as below:

Theorem plus_succ: forall (n : nat),
  plus n one = succ n.
Proof.
  intros.

1 subgoal n : nat ______________________________________(1/1) plus n one = succ n

and there's no way I can do inversion or any other tactic...(I am new to Coq, I've learnt list,poly,induction and tactics so far)

So that brings me to the thought that probably one, two or maybe all of my definition I defined above are not accurate. Tons of appreciation if anyone can help me or give me some hints! Thankssss!

kyo dralliam kyo dralliam · Accepted Answer · 2021-03-06T23:21:35

Using Church encodings in Coq is not a bad idea per-se, but you won't be able to say much about the inhabitants of this type (beside constructing some of them as you did).

The first issue is that inhabitants of this Church encoding are functions, and you will be able to show that two functions are equal in pure Coq only if they compute to the same value (up to unfolding, beta-reductions, reductions of match and fixes). This is not the case for plus n one and succ n: you have on the lhs fun X f x => f (n X f x) and on the rhs fun X f x => n X f (f x). What you could hope to prove is forall (X : type) (f : X -> X) (x : X), f (n X f x) = n X f (f x), and you would then need to use functional extensionality, an axiom stating that the equality between functions is determined by the value of the functions at each point of their domain (see Coq.Logic.FunctionalExtensionality in the stdlib for more details on that point). This axiom is frequently assumed, but it is not innocent either (e.g. it does block computations).

The second issue you will run into is that you expect the inhabitants of nat = forall X, (X -> X) -> X -> X to be functions parametric in their first argument X : Type, but there is nothing actually enforcing that. Indeed, you can construct non-parametric inhabitants if you assume additional axioms, for instance excluded-middle. In pure Coq (without any axiom), there are results due to Bernardy and Lasson that show that indeed all inhabitants of your type nat are parametric, however you cannot internalize this result. And without parametricity, you have no bullets to prove equations such as f (n X f x) = n X f (f x).

So your troubles come from these two issues:

in absence of functional extensionality, the equalities that you can prove between functions are quite limited, and
you are not able in pure Coq to express internally that a quantification over types is parametric.

If you want to learn more about these issues on parametricity and what can still be achieved using Church encodings (or variants of these), I would recommend having a look at Chlipala's Parametric Higher-Order Abstract Syntax.

Define a polymorphic type in coq

1 Answers