Formalization of a small part of the Parametricity Tutorial blog post

parametricity.coq

Require Import Coq.Setoids.Setoid.

Set Implicit Arguments.

(* Auxiliary *)

Lemma simplify_eq : forall (A : Type) (P : A -> A -> Prop),
  (forall x x', x = x' -> P x x') <-> (forall x, P x x).
Proof.
  split ; intro H ; auto.
  intros x x' Heq ; rewrite Heq ; auto.
Qed.

Lemma swap_arg2 : forall (X A B : Prop),
  (A -> X -> B) <-> (X -> A -> B).
Proof.
  tauto.
Qed.

Lemma swap_arg3 : forall (X A B C : Prop),
  (A -> B -> X -> C) <-> (X -> A -> B -> C).
Proof.
  tauto.
Qed.

Lemma dup_arg : forall (X A : Prop),
  (X -> X -> A) <-> (X -> A).
Proof.
  tauto.
Qed.

Section Parametricity.

Variables Term Typ : Set.
Variable hasType : Term -> Typ -> Prop.

(*
 * We use S, T to range over types
 * We use x, y to range over terms
 * We (sometimes) use f, g to range over terms that are functions
 *)

Definition RelOn (S T : Typ) := 
  forall (x y : Term), hasType x S -> hasType y T -> Prop.

Variable left right : Typ -> Typ.

Inductive Rel : Type := 
  EmbedRel : forall S T, RelOn S T -> Rel.

Variable rel : Rel -> Typ.

Definition embedRel (S T : Typ) (A : RelOn S T) : Typ := rel (EmbedRel A).

(*
 * We use A, B to range over relations
 * We use a, b to range over type variables (see 'poly', below)
 *)

Hypothesis left_rel : forall S T (A : RelOn S T),
  left (embedRel A) = S.
Hypothesis right_rel : forall S T (A : RelOn S T),
  right (embedRel A) = T.

Variable R : forall (T : Typ), RelOn (left T) (right T).

(* Convenience *)

Definition leftType (t : Term) (T : Typ) : Prop := 
  hasType t (left T).
Definition rightType (t : Term) (T : Typ) : Prop := 
  hasType t (right T).

Lemma leftType_rel : forall S T (A : RelOn S T) x,
  leftType x (rel (EmbedRel A)) -> hasType x S.
Proof.
  unfold leftType ; setoid_rewrite left_rel ; auto.
Qed.

Lemma rightType_rel : forall S T (A : RelOn S T) x,
  rightType x (rel (EmbedRel A)) -> hasType x T.
Proof.
  unfold rightType ; setoid_rewrite right_rel ; auto.
Qed.

(* Type variables *)

Hypothesis R_var : forall S T (A : RelOn S T) x y,
  forall (l_x : leftType x (rel (EmbedRel A))) (r_x : rightType y (rel (EmbedRel A))),
      R l_x r_x 
  <-> A x y (leftType_rel l_x) (rightType_rel r_x).

(* Constant types *)

Variable const : Typ -> Prop.

Variable Int Bool : Typ.
Hypothesis const_Int : const Int.
Hypothesis const_Bool : const Bool.

Hypothesis left_const : forall T, const T ->
  left T = T.
Hypothesis right_const : forall T, const T ->
  right T = T.

Hypothesis R_const : forall T x y, const T -> 
  forall (l_x : leftType x T) (r_y : rightType y T),
      R l_x r_y
  <-> x = y.

Example example_const : forall x (l_x : leftType x Int) (r_x : rightType x Int),
      R l_x r_x
  <-> x = x.
Proof.
  intros ; apply (R_const const_Int).
Qed.

(* Functions *)

Variable fn : Typ -> Typ -> Typ.
Variable app : Term -> Term -> Term.

Hypothesis hasType_app : forall S T f x (l_f : hasType f (fn S T)) (l_x : hasType x S), 
  hasType (app f x) T.

Hypothesis extensionality : forall S T f g,
  hasType f (fn S T) -> hasType g (fn S T) -> (
      (forall x, hasType x S -> app f x = app g x) 
  <-> f = g
).

Hypothesis left_fn : forall A B,
  left (fn A B) = fn (left A) (left B).
Hypothesis right_fn : forall A B,
  right (fn A B) = fn (right A) (right B).

Corollary leftType_app : forall S T f x (l_f : leftType f (fn S T)) (l_x : leftType x S), 
  leftType (app f x) T.
Proof.
  unfold leftType.
  intros ; apply hasType_app with (S := left S) ; auto.
  rewrite <- left_fn ; auto.
Qed.

Corollary rightType_app : forall S T f x (l_f : rightType f (fn S T)) (l_x : rightType x S), 
  rightType (app f x) T.
Proof.
  unfold rightType.
  intros ; apply hasType_app with (S := right S) ; auto.
  rewrite <- right_fn ; auto.
Qed.

Hypothesis R_fn : forall S T f g (l_f : leftType f (fn S T)) (r_g : rightType g (fn S T)),
      R l_f r_g
  <-> (forall (x y : Term) (l_x : leftType x S) (r_y : rightType y S), 
         R l_x r_y -> R (leftType_app l_f l_x) (rightType_app r_g r_y)).

Example example_fn : forall f (l_f : leftType f (fn Int Bool)) (r_f : rightType f (fn Int Bool)),
      R l_f r_f
  <-> f = f.
Proof.
  intros.
  rewrite R_fn.
  setoid_rewrite (R_const const_Int).
  setoid_rewrite (R_const const_Bool).
  (* The last step follows from extensionality but its a bit painful to prove *)
  unfold leftType in *.
  unfold rightType in *.
  rewrite left_fn in l_f.
  rewrite right_fn in r_f.
  rewrite (left_const const_Int) in *.
  rewrite (right_const const_Int) in *.
  rewrite (left_const const_Bool) in *.
  rewrite (right_const const_Bool) in *.
  setoid_rewrite swap_arg3 ; rewrite simplify_eq.
  setoid_rewrite dup_arg.
  rewrite (extensionality l_f r_f).
  tauto.
Qed.

(* Parametric polymorphism over types of kind star *)

Variable para : (Typ -> Typ) -> Typ.

Hypothesis hasType_para : forall f F, hasType f (para F) ->
  forall T, hasType f (F T).

Hypothesis left_para : forall F,
  left (para F) = para (fun a => left (F a)).
Hypothesis right_para : forall F,
  right (para F) = para (fun a => right (F a)).

Corollary leftType_para : forall f F, leftType f (para F) ->
  forall T, leftType f (F T).
Proof.
  unfold leftType ; intros.
  apply hasType_para with (F := (fun a => left (F a))).
  rewrite <- left_para ; auto.
Qed.

Corollary rightType_para : forall f F, rightType f (para F) ->
  forall T, rightType f (F T).
Proof.
  unfold rightType ; intros.
  apply hasType_para with (F := (fun a => right (F a))).
  rewrite <- right_para ; auto.
Qed.

Hypothesis R_para : forall f g (F : Typ -> Typ)
  (l_f : leftType f (para F)) (r_g : rightType g (para F)), 
      R l_f r_g 
  <-> (forall S T (A : RelOn S T), R (leftType_para l_f (embedRel A)) (rightType_para r_g (embedRel A))).

Example example_para_id : forall f
  (l_f : leftType f (para (fun a => fn a a))) (r_f : rightType f (para (fun a => fn a a))),
      R l_f r_f
  <-> (forall S T (A : RelOn S T) x y (l_x : leftType x (embedRel A)) (r_y : rightType y (embedRel A)),
         R l_x r_y -> R (leftType_app (leftType_para l_f (embedRel A)) l_x) 
                        (rightType_app (rightType_para r_f (embedRel A)) r_y)).
Proof.
  intros.
  rewrite R_para.
  setoid_rewrite R_fn.
  tauto.
Qed.