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