Formalization of a small part of the Parametricity Tutorial blog post

parametricity.coq

(* Developed using Coq 8.4pl5 *)

Require Import Coq.Setoids.Setoid.
Require Import Coq.Logic.ProofIrrelevance.
Require Import Coq.Logic.JMeq.

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.

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

Section Parametricity.

(*
 * Terms and types
 *
 * 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
 * We use a, b to range over type variables (see 'poly', below)
 *)

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

(*
 * Embedding relations into types
 *
 * We use A, B to range over relations
 *)

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

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).

(*
 * Projecting from the extended languages of types to source types
 *)

Variable left right : Typ -> Typ.

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.

(* Categorizing source types *)

Variable source : Typ -> Prop.
Hypothesis left_source : forall t, source t -> 
  left t = t.
Hypothesis right_source : forall t, source t ->
  right t = t.

(*
 * Type variables 
 *)

Hypothesis R_var : forall S T (A : RelOn S T) x y,
  forall (l_x : leftType x (embedRel A)) (r_x : rightType y (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 const_source : forall T, const T -> source T.

Corollary left_const : forall T, const T ->
  left T = T.
Proof.
  intros T Hconst.
  rewrite (left_source (const_source Hconst)) ; auto.
Qed.

Corollary right_const : forall T, const T ->
  right T = T.
Proof.
  intros T Hconst.
  rewrite (right_source (const_source Hconst)) ; auto.
Qed.

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 source_fn : forall S T,
  source S -> source T -> source (fn S T).

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.

Definition preserves_source (F : Typ -> Typ) := 
  forall T, source T -> source (F T).

Corollary left_preserves_source : forall F, preserves_source F ->
  forall T, source T -> left (F T) = F T.
Proof.
  intros ; apply left_source ; auto.
Qed.

Corollary right_preserves_source : forall F, preserves_source F ->
  forall T, source T -> right (F T) = F T.
Proof.
  intros ; apply right_source ; auto.
Qed.

Corollary leftType_para_source : forall f F, preserves_source F -> leftType f (para F) ->
  forall T, source T -> hasType f (F T).
Proof.
  unfold leftType ; intros f F HF Hf T HT.
  rewrite <- left_preserves_source ; auto.
  apply hasType_para with (F := fun T => (left (F T))).
  rewrite <- left_para. exact Hf.
Qed.

Corollary rightType_para_source : forall f F, preserves_source F -> rightType f (para F) ->
  forall T, source T -> hasType f (F T).
Proof.
  unfold rightType ; intros f F HF Hf T HT.
  rewrite <- right_preserves_source ; auto.
  apply hasType_para with (F := fun T => (right (F T))).
  rewrite <- right_para. exact Hf.
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))).

(* Type of the identity function *)
Definition idTyp := fun (a : Typ) => fn a a.

Fact source_idTyp : preserves_source idTyp.
Proof.
  intros T HT ; unfold idTyp ; apply source_fn ; auto.
Qed.

Example example_para_id : forall f
  (l_f : leftType f (para idTyp)) (r_f : rightType f (para idTyp)),
      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.

(*
 * Specializing the lemma to functional relations 
 *)

(* Functional relations *)
Definition FunRel S T f (t_f : hasType f (fn S T)) : RelOn S T :=
  fun x y (t_x : hasType x S) (t_y : hasType y T) => JMeq (hasType_app t_f t_x) t_y.

Lemma leftType_FunRel : forall S T f (t_f : hasType f (fn S T)) x,
      leftType x (embedRel (FunRel t_f)) 
  <-> hasType x S.
Proof.
  intros ; unfold leftType ; rewrite left_rel ; tauto.
Qed.

Lemma rightType_FunRel : forall S T f (t_f : hasType f (fn S T)) y,
      rightType y (embedRel (FunRel t_f)) 
  <-> hasType y T.
Proof.
  intros ; unfold rightType ; rewrite right_rel ; tauto.
Qed.

Lemma typing_irrelevance : forall x T (t_x1 : hasType x T) (t_x2 : hasType x T),
  JMeq t_x1 t_x2.
Proof.
  intros ; rewrite (proof_irrelevance _ t_x1 t_x2) ; auto.
Qed.

Lemma typing_irrelevance_eq : forall x y S T 
    (t_x1 : hasType x S) (t_y1 : hasType y T)
    (t_x2 : hasType x S) (t_y2 : hasType y T),
  JMeq t_x1 t_y1 ->
  JMeq t_x2 t_y2.
Proof.
  intros.
  rewrite <- (proof_irrelevance _ t_x1 t_x2).
  rewrite <- (proof_irrelevance _ t_y1 t_y2).
  auto.
Qed.

Corollary R_FunRel : forall S T f (t_f : hasType f (fn S T)),
  forall x y 
      (l_x : leftType x (embedRel (FunRel t_f)))
      (r_y : rightType y (embedRel (FunRel t_f))),
      R l_x r_y
  <-> JMeq (hasType_app t_f (fw (leftType_FunRel t_f x) l_x)) (fw (rightType_FunRel t_f y) r_y).
Proof.
  intros ; rewrite R_var ; unfold FunRel.
  split ; apply typing_irrelevance_eq.
Qed.

Corollary example_para_id_spec : forall f
    (l_f : leftType f (para idTyp)) 
    (r_f : rightType f (para idTyp)),
      R l_f r_f 
   -> forall S T g (t_g : hasType g (fn S T)),
      forall x (t_x : hasType x S) (HS : source S) (HT : source T),
        JMeq (hasType_app t_g (hasType_app (leftType_para_source source_idTyp l_f HS) t_x)) 
             (hasType_app (rightType_para_source source_idTyp r_f HT) (hasType_app t_g t_x)).
Proof.
  intros until 0 ; intro HR ; intros.
  rewrite example_para_id in HR.
  (* Instantiate the premise at the functional relation corresponding to function g *)
  assert (Hx : leftType x (embedRel (FunRel t_g))) by
    (unfold leftType ; rewrite left_rel ; auto).
  assert (Hgx : rightType (app g x) (embedRel (FunRel t_g))) by
    (unfold rightType ; rewrite right_rel ; exact (hasType_app t_g t_x)).
  assert (HRgx : R Hx Hgx) by
    (rewrite R_FunRel ; apply typing_irrelevance).
  pose (premise := HR _ _ _ _ _ Hx Hgx HRgx) ; clearbody premise.
  (* Derive conclusion from this instantiated premise *)
  rewrite R_var in premise ; unfold FunRel in premise.
  eapply typing_irrelevance_eq ; apply premise.
Qed.