(** POPLmark challenge, Part 1A *)
Require Import Arith Binding.
Set Implicit Arguments.
(** * The type language *)
Inductive ty : Set :=
| Free : var -> ty
| Bound : nat -> ty
| Top : ty
| Arrow : ty -> ty -> ty
| Forall : ty -> ty -> ty.
(** This should be generated semi-automatically. *)
Notation "@ n" := (Free n) (at level 30).
Notation "# n" := (Bound n) (at level 30).
Infix "-->" := Arrow (right associativity, at level 31).
Notation "'All' t1 , t2" := (Forall t1 t2) (at level 32).
(** Define a type of contexts specialized to contain [ty]s. *)
Definition context : Set := context ty.
(** This should be generated automatically. *)
(** Syntactic notation for context binding *)
Notation "G ,, x <: t" := (Bind G x t) (left associativity, at level 40).
(** Look up a particular binding in a context *)
Notation "[ x <: t ] \in G" := (inContext x t G) (at level 50).
(** Check that a variable is in a context's domain *)
Notation "x \in G" := (inDom x G) (at level 50).
(** Substitution for type variables in types *)
Fixpoint subst (x : nat) (t b : ty) {struct b} : ty :=
match b with
| #x' =>
if eq_nat_dec x x'
then t
else b
| b1 --> b2 => (subst x t b1) --> (subst x t b2)
| All b1, b2 => All (subst x t b1), subst (S x) t b2
| _ => b
end.
(** This should be generated automatically. *)
(** Shorthand notation for substitution *)
Notation "{ x := t }" := (subst x t) (at level 33).
(** This should be generated automatically. *)
(** Well-formedness of types: all free variables are in the context's domain *)
Reserved Notation "G |-- t 'ok'" (at level 50).
(** This should be generated automatically. *)
Inductive wfTy : context -> ty -> Prop :=
| WF_Free : forall G x,
x \in G
-> G |-- @x ok
| WF_Top : forall G,
G |-- Top ok
| WF_Arrow : forall G t1 t2,
G |-- t1 ok
-> G |-- t2 ok
-> G |-- (t1 --> t2) ok
| WF_Forall : forall G t1 t2,
G |-- t1 ok
-> (forall x, ~(x \in G)
-> G,, x <: t1 |-- {O := @x}t2 ok)
-> G |-- (All t1, t2) ok
where "G |-- t 'ok'" := (wfTy G t).
(** This should be generated automatically. *)
Hint Constructors wfTy.
(** This should be generated automatically. *)
(** Well-formedness of contexts: no variables are repeated and every variable's associated type is well formed given the context up to that point *)
Notation "|-- G 'ok'" := (wfContext wfTy G) (at level 50).
(** This should be generated automatically. *)
(** * Subtyping judgment *)
Reserved Notation "G |-- t1 <: t2" (at level 50).
Inductive subTy : context -> ty -> ty -> Prop :=
| SA_Top : forall G t,
|-- G ok
-> G |-- t ok
-> G |-- t <: Top
| SA_Refl_TVar : forall G x,
|-- G ok
-> x \in G
-> G |-- @x <: @x
| SA_Trans_TVar : forall G x u t,
[x <: u] \in G
-> G |-- u <: t
-> G |-- @x <: t
| SA_Arrow : forall G s1 s2 t1 t2,
G |-- t1 <: s1
-> G |-- s2 <: t2
-> G |-- (s1 --> s2) <: (t1 --> t2)
| SA_All : forall G s1 s2 t1 t2,
G |-- t1 <: s1
-> (forall x, ~(x \in G)
-> G,, x <: t1 |-- {O := @x}s2 <: {O := @x}t2)
-> G |-- (All s1, s2) <: (All t1, t2)
where "G |-- t1 <: t2" := (subTy G t1 t2).
Hint Constructors subTy.
(** * Lemma A.1 (Reflexivity) *)
(** Lemma A.1 *)
Lemma reflexivity : forall G, |-- G ok
-> forall t, G |-- t ok
-> G |-- t <: t.
induction 2; eauto 6.
(** Prove by induction on the 2nd hypothesis, followed by logic programming up to depth 6. *)
Qed.
(** * Lemma A.2 (Permutation and Weakening) *)
(** "[D] is valid permutation of [G]." *)
Notation "G ~= D" := (permute wfTy G D) (at level 50).
(** This should be generated automatically. *)
(** Permutations don't affect well-formedness of types *)
Lemma permute_wfTy : forall G t,
G |-- t ok
-> forall D, G ~= D
-> D |-- t ok.
induction 1; intuition (eauto 10).
Qed.
(** Use this lemma automatically in logic programming. *)
Hint Resolve permute_wfTy.
(** The basic way to prove that a type remains well-formed in a modified context *)
Lemma preweaken_wfTy : forall G t,
G |-- t ok
-> forall D, (forall x, x \in G -> x \in D)
-> D |-- t ok.
induction 1; intuition eauto 7.
Qed.
Hint Resolve preweaken_wfTy.
(** The context of any correct typing judgment is well-formed. *)
Lemma subTy_wfContext : forall G s t,
G |-- s <: t
-> |-- G ok.
induction 1; auto.
Qed.
(** Two helper lemmas to deal with limitations in Coq's automated first-order reasoning *)
Lemma proj1_wfTy : forall G t P,
G |-- t ok /\ P
-> G |-- t ok.
intuition.
Qed.
Lemma proj2_wfTy : forall G t P,
P /\ G |-- t ok
-> G |-- t ok.
intuition.
Qed.
(** The two types in any correct typing judgment are well-formed. *)
Lemma subTy_wfTy : forall G s t,
G |-- s <: t
-> (G |-- s ok)
/\ (G |-- t ok).
Hint Resolve proj1_wfTy proj2_wfTy.
induction 1; intuition eauto 6.
Qed.
(** The combined form above was necessary to have a strong enough induction hypothesis, but we want to break it into two separate lemmas for easier use later. *)
Lemma subTy_wfTy1 : forall G s t,
G |-- s <: t
-> G |-- s ok.
generalize subTy_wfTy; firstorder.
Qed.
Lemma subTy_wfTy2 : forall G s t,
G |-- s <: t
-> G |-- t ok.
generalize subTy_wfTy; firstorder.
Qed.
Hint Resolve subTy_wfContext subTy_wfTy1 subTy_wfTy2.
Lemma permutation : forall G s t,
G |-- s <: t
-> forall D, G ~= D
-> D |-- s <: t.
induction 1; intuition; eauto; eauto 10.
Qed.
Lemma weakening : forall G s t,
G |-- s <: t
-> forall D, |-- G ++ D ok
-> G ++ D |-- s <: t.
Hint Extern 1 (_ ++ _,, _ <: _ |-- _ <: _) =>
match goal with
| [ |- ?G ++ ?D,, ?x <: ?t |-- _ <: _ ] =>
apply permutation with (G,, x <: t ++ D);
eauto 7
end.
(** This [Hint] command advises the automated proving machinery to try a special strategy if it encounters a subtyping goal where the context has the form (G ++ D,, x <: t): use the permutation lemma that we just proved to move around the parts of the context. *)
induction 1; intuition eauto.
Qed.
(** Weakening by a single binding *)
Lemma weakening1 : forall G s t,
G |-- s <: t
-> forall x u, |-- G,, x <: u ok
-> G,, x <: u |-- s <: t.
do 6 intro.
replace (G,, x <: u) with (G ++ (Empty _,, x <: u)); trivial.
intro.
apply weakening; auto.
Qed.
(** Weakening specialized to the form associated with the Narrowing lemma *)
Lemma narrowing_weakening : forall G t t',
G |-- t <: t'
-> forall x t'' D, |-- G,, x <: t'' ++ D ok
-> G,, x <: t'' ++ D |-- t <: t'.
intros.
eapply weakening; eauto.
eapply weakening1; eauto.
Qed.
Hint Resolve narrowing_weakening.
(** * Specialized proof automation tactics *)
(** ** Using injectivity of the [ty] constructors *)
Ltac ty_injections :=
repeat match goal with
| [ H : @ _ = @ _ |- _ ] => injection H; clear H; intros
| [ H : _ --> _ = _ --> _ |- _ ] => injection H; clear H; intros
| [ H : All _, _ = All _, _ |- _ ] => injection H; clear H; intros
end.
(** For instance, if we ever see a hypothesis [t1 --> t2 = s1 --> s2], we want to replace it with hypotheses [t1 = s1] and [t2 = s2]. *)
(** ** Replacing known subtypes of [Top] with [Top] *)
(** Slightly ugly form of the [Top_sub] lemma to follow, chosen to work properly with the [induction] tactic *)
Lemma Top_sub' : forall G T T',
G |-- T <: T'
-> T = Top
-> T' = Top.
induction 1; intuition; try discriminate.
Qed.
(** Any subtype of [Top] is [Top] *)
Lemma Top_sub : forall G T,
G |-- Top <: T
-> T = Top.
generalize Top_sub'; firstorder.
Qed.
(** Replace all types known to be [Top], clearing the now-irrelevant subtyping judgments that led us to do so. *)
Ltac discover_Top :=
repeat match goal with
| [ H : _ |-- Top <: _ |- _ ] =>
generalize (Top_sub H); clear H; intro
end.
(** ** The overall simplification tactic *)
Ltac ty_simpl :=
repeat progress (ty_injections; discover_Top; binding_simpl).
(** As long as we're modifying the goal, continue using injectivity, [Top]-replacement, and the [Binding] module's simplification tactic. *)
(** * Lemma A.3 (Transitivity and Narrowing) *)
(** Replacing a type binding in a context doesn't affect type well-formedness. *)
Lemma narrowing_wfTerm : forall G x t1 D t,
G,, x <: t1 ++ D |-- t ok
-> forall t2, G,, x <: t2 ++ D |-- t ok.
intros; eapply narrowing_wfTerm; eauto.
Qed.
(** This should be generated automatically. *)
Hint Resolve narrowing_wfTerm.
(** This should be generated automatically. *)
(** Here's the Narrowing part of the Transitivity/Narrowing lemma, with transitivity assumed for the current type. *)
Lemma narrowing' : forall Q,
(forall (G : context) (S T : ty),
(G |-- S <: Q) -> (G |-- Q <: T) -> G |-- S <: T) ->
forall (G G' : context) (M N : ty),
(G' |-- M <: N) ->
forall (x : var) (D : context) (P : ty),
G' = (G,, x <: Q ++ D) -> (G |-- P <: Q) -> G,, x <: P ++ D |-- M <: N.
induction 2; intros; ty_simpl;
(** We'll proceed by induction on the [G' |-- M <: N] derivation and simplify each case before... *)
try (apply SA_All;
[auto
| intros; rewrite <- weaken_bind_assoc; eauto]);
(** For the SA_All case, we give more detail of the proof, in particular, use the associativity of context operations to rewrite a context advantageously. *)
try match goal with
| [ _ : [_ <: _] \in _,, _ <: _ ++ _ |- _,, ?x0 <: _ ++ _ |-- @?x <: _ ] =>
destruct (var_eq_dec x x0); ty_simpl;
[eapply SA_Trans_TVar; eauto 6
| eauto]
end;
(** For the SA_Trans_TVar case, we proceed by case analysis on whether the two variables involved are equal. *)
eauto 6.
(** The remaining cases are solved automatically. *)
Qed.
Hint Resolve narrowing'.
(** Syntactic size function for types *)
Fixpoint tySize (t : ty) : nat :=
match t with
| Arrow t1 t2 => S (tySize t1 + tySize t2)
| Forall t1 t2 => S (tySize t1 + tySize t2)
| _ => 1
end.
(** This should be generated automatically. *)
(** Subsitution of a free variable doesn't change type size. *)
Lemma tySize_subst : forall x' b x, tySize({x := @x'}b) = tySize b.
induction b; simpl; intuition.
destruct (eq_nat_dec x n); auto.
Qed.
(** This should be generated automatically. *)
(** A syntactic induction principle for types that considers alpha-variation *)
Theorem ty_ind_syntactic : forall P : ty -> Prop,
(forall v : var, P (@ v)) ->
(forall n : nat, P (#n)) ->
P Top ->
(forall t : ty, P t -> forall t0 : ty, P t0 -> P (t --> t0)) ->
(forall t : ty, P t -> forall t0 : ty, (forall x, P ({0 := @x}t0)) -> P (All t, t0)) ->
forall t : ty, P t.
intros.
assert (forall n t, tySize t <= n -> P t).
clear t.
induction n.
destruct t; simpl; intros; wrong; omega.
destruct t; simpl; intros; auto.
apply H2; apply IHn; omega.
apply H3.
apply IHn; omega.
intro; apply IHn.
rewrite tySize_subst; omega.
eauto.
Qed.
(** This should be generated automatically. *)
(** A useful hint to get the Transitivity proof to take advantage of Narrowing *)
Lemma use_narrowing : forall G x t1 t2,
G ++ Empty _ |-- {0 := @x} t1 <: {0 := @x} t2
-> G |-- {0 := @x} t1 <: {0 := @x} t2.
trivial.
Qed.
Hint Resolve use_narrowing.
(** The big lemma! It's formulated using both seemingly pointless equalities, which are necessary to make [induction] work; and an implication for the second conjunct that assumes the first conjunct, to avoid the need to re-prove it. *)
Lemma transitivity_and_narrowing : forall Q,
(forall G S T Q', G |-- S <: Q'
-> Q' = Q
-> G |-- Q <: T
-> G |-- S <: T)
/\ ((forall G S T, G |-- S <: Q
-> G |-- Q <: T
-> G |-- S <: T)
-> forall G G' M N, G' |-- M <: N
-> forall x D P, G' = (G,, x <: Q ++ D)
-> G |-- P <: Q
-> G,, x <: P ++ D |-- M <: N).
induction Q using ty_ind_syntactic; split; eauto; induction 1; intuition; ty_simpl; eauto;
match goal with
| [ H : _ |-- _ --> _ <: _ |- _ ] =>
inversion H; subst; eauto
(** Here, we are inverting a proof of the form [G |-- t1 --> t2 <: s]. *)
| [ H : _ |-- All _, _ <: _ |- _ ] =>
inversion H; subst; eauto;
apply SA_All; intuition eauto;
match goal with
| [ H : forall x : var, _ /\ _, x : var |- _ ] =>
generalize (H x); intuition; eauto 7
(** We need to instantiate explicitly one part of the inductive hypothesis to make the conjunction inside accessible to automatic propositional reasoning. *)
end
end.
Qed.
Theorem transitivity : forall Q G S T,
G |-- S <: Q
-> G |-- Q <: T
-> G |-- S <: T.
generalize transitivity_and_narrowing; firstorder.
Qed.
Lemma narrowing : forall Q G M N x D P, G,, x <: Q ++ D |-- M <: N
-> G |-- P <: Q
-> G,, x <: P ++ D |-- M <: N.
intros.
generalize (transitivity_and_narrowing Q).
firstorder; eauto.
Qed.