Skip to content

Instantly share code, notes, and snippets.

@edsko

edsko/parametricity.coq

Last active January 23, 2020 20:31
Download ZIP

Revisions

  1. edsko revised this gist May 11, 2015. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion parametricity.coq
    View file
    Original file line number Diff line number Diff line change
    @@ -294,7 +294,7 @@ Proof.
    Qed.

    Example example_para_id : forall f
    (l_f : leftType f (para (fun a => fn a a))) (r_f : rightType f (para idTyp)),
    (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)
  2. edsko revised this gist May 11, 2015. 1 changed file with 2 additions and 0 deletions.
    2 changes: 2 additions & 0 deletions parametricity.coq
    View file
    Original file line number Diff line number Diff line change
    @@ -1,3 +1,5 @@
    (* Developed using Coq 8.4pl5 *)

    Require Import Coq.Setoids.Setoid.
    Require Import Coq.Logic.ProofIrrelevance.
    Require Import Coq.Logic.JMeq.
  3. edsko revised this gist May 10, 2015. 1 changed file with 4 additions and 7 deletions.
    11 changes: 4 additions & 7 deletions parametricity.coq
    View file
    Original file line number Diff line number Diff line change
    @@ -344,18 +344,15 @@ Proof.
    auto.
    Qed.

    Lemma R_FunRel : forall S T f (t_f : hasType f (fn S T)),
    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.
    rewrite <- (proof_irrelevance _ (leftType_rel l_x) (fw (leftType_FunRel t_f x) l_x)).
    rewrite <- (proof_irrelevance _ (rightType_rel r_y) (fw (rightType_FunRel t_f y) r_y)).
    tauto.
    intros ; rewrite R_var ; unfold FunRel.
    split ; apply typing_irrelevance_eq.
    Qed.

    Corollary example_para_id_spec : forall f
    @@ -380,4 +377,4 @@ Proof.
    (* Derive conclusion from this instantiated premise *)
    rewrite R_var in premise ; unfold FunRel in premise.
    eapply typing_irrelevance_eq ; apply premise.
    Qed.
    Qed.
  4. edsko revised this gist May 10, 2015. 1 changed file with 162 additions and 19 deletions.
    181 changes: 162 additions & 19 deletions parametricity.coq
    View file
    Original file line number Diff line number Diff line change
    @@ -1,4 +1,6 @@
    Require Import Coq.Setoids.Setoid.
    Require Import Coq.Logic.ProofIrrelevance.
    Require Import Coq.Logic.JMeq.

    Set Implicit Arguments.

    @@ -29,22 +31,34 @@ Proof.
    tauto.
    Qed.

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

    Variables Term Typ : Set.
    Variable hasType : Term -> Typ -> Prop.
    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.

    Variable left right : Typ -> Typ.

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

    @@ -53,10 +67,11 @@ 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)
    * 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),
    @@ -83,10 +98,20 @@ Proof.
    unfold rightType ; setoid_rewrite right_rel ; auto.
    Qed.

    (* Type variables *)
    (* 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 (rel (EmbedRel A))) (r_x : rightType y (rel (EmbedRel A))),
    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).

    @@ -98,10 +123,21 @@ Variable Int Bool : Typ.
    Hypothesis const_Int : const Int.
    Hypothesis const_Bool : const Bool.

    Hypothesis left_const : forall T, const T ->
    Hypothesis const_source : forall T, const T -> source T.

    Corollary left_const : forall T, const T ->
    left T = T.
    Hypothesis right_const : forall T, const 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),
    @@ -129,6 +165,9 @@ Hypothesis extensionality : forall S T f g,
    <-> 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,
    @@ -206,13 +245,54 @@ Proof.
    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 (fun a => fn a a))) (r_f : rightType f (para (fun a => fn a a))),
    (l_f : leftType f (para (fun a => fn a a))) (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)
    @@ -224,17 +304,80 @@ Proof.
    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.

    Lemma 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.
    rewrite <- (proof_irrelevance _ (leftType_rel l_x) (fw (leftType_FunRel t_f x) l_x)).
    rewrite <- (proof_irrelevance _ (rightType_rel r_y) (fw (rightType_FunRel t_f y) r_y)).
    tauto.
    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.
  5. edsko created this gist May 10, 2015.
    240 changes: 240 additions & 0 deletions parametricity.coq
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,240 @@
    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.