Skip to content

Instantly share code, notes, and snippets.

@edsko
Last active January 23, 2020 20:31
Show Gist options
  • Save edsko/8dbf6ddb88a772bfdc9f to your computer and use it in GitHub Desktop.
Save edsko/8dbf6ddb88a772bfdc9f to your computer and use it in GitHub Desktop.
Formalization of a small part of the Parametricity Tutorial blog post
(* 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment