LambdaProj.Proofs
Lemma wf_rcd_lookup : forall l R T,
well_formed_ty R ->
Tlookup l R = Some T ->
well_formed_ty T.
Proof with eauto.
induction R; intros; try solve_by_invert.
inversion H. unfold Tlookup in H0.
destruct (eqb l s)...
inversion H0. subst...
Qed.
Lemma wf_subtype : forall S T,
S <: T ->
well_formed_ty T /\ well_formed_ty S.
Proof with eauto.
induction 1; try (destruct IHsubtype1; destruct IHsubtype2)...
split... inversion H. inversion H5...
Qed.
Lemma wf_has_type : forall Gamma t T,
Gamma |- t : T ->
well_formed_ty T.
Proof with eauto.
induction 1...
- (* T_App *)
inversion IHhas_type1...
- (* T_Proj *)
eapply wf_rcd_lookup...
- (* T_Sub *)
apply wf_subtype in H0.
destruct H0...
Qed.
Lemma step_preserves_record_tm : forall tr tr',
record_tm tr ->
tr --> tr' ->
record_tm tr'.
Proof.
intros * Hrt Hstp.
inversion Hrt; subst; inversion Hstp; subst; eauto.
Qed.
Lemma rcd_types_match : forall R' R l T,
R' <: R ->
Tlookup l R = Some T ->
exists T', Tlookup l R' = Some T' /\ T' <: T.
Proof with eauto using wf_rcd_lookup.
intros * Hsub. generalize dependent T.
induction Hsub; intros Ti Hget; try solve_by_invert.
- (* S_Refl *)
exists Ti...
- (* S_Trans *)
destruct (IHHsub2 Ti) as [Ui Hui]... destruct Hui.
destruct (IHHsub1 Ui) as [Si Hsi]... destruct Hsi.
exists Si...
- (* S_RcdDepth *)
rename l0 into k.
unfold Tlookup. unfold Tlookup in Hget.
destruct (eqb l k)...
+ (* l = k -- we're looking up the first field *)
inversion Hget. subst. exists S...
- (* S_RcdPerm *)
exists Ti. split.
+ (* lookup *)
unfold Tlookup. unfold Tlookup in Hget.
destruct (eqb_spec l l1)...
* (* l = l1 -- we're looking up the first field *)
destruct (eqb_spec l l2)...
(* l = l2 -- contradictory *)
destruct H0.
subst...
+ (* subtype *)
inversion H. subst. inversion H5. subst...
Qed.
Lemma lookup_field_in_value : forall r R l T,
value r ->
empty |- r : R ->
Tlookup l R = Some T ->
exists v, tlookup l r = Some v /\ empty |- v : T.
Proof with eauto.
remember empty as Gamma.
intros * Hval Htyp. generalize dependent T.
induction Htyp; intros; subst; try solve_by_invert.
- (* T_Sub *)
apply (rcd_types_match S) in H0...
destruct H0 as [Si [HgetSi Hsub]].
eapply IHHtyp in HgetSi...
destruct HgetSi as [vi [Hget Htyvi]]...
- (* T_RCons *)
simpl in H0. simpl. simpl in H1.
destruct (eqb l l0).
+ (* l is first *)
injection H1 as H1. subst. exists t...
+ (* l in tail *)
eapply IHHtyp2 in H1...
inversion Hval...
Qed.
Lemma sub_inversion_arrow : forall S T1 T2,
S <: <{{ T1 -> T2 }}> ->
exists S1 S2, S = <{{ S1 -> S2 }}> /\ T1 <: S1 /\ S2 <: T2.
Proof with eauto.
intros * Hs.
remember <{{ T1 -> T2 }}> as T.
generalize dependent T2. generalize dependent T1.
induction Hs; intros; try solve_by_invert.
- (* S_Refl *)
inversion H; subst; try congruence.
inversion H2; subst.
exists T1, T2...
- (* S_Trans *)
apply IHHs2 in HeqT. destruct HeqT as [S1 [S2 [HeqS [Hsub1 Hsub2]]]].
apply IHHs1 in HeqS. destruct HeqS as [S3 [S4 [HeqR [Hsub3 Hsub4]]]].
exists S3, S4...
- (* S_Arrow *)
inversion HeqT; subst...
Qed.
Lemma typing_inversion_abs : forall Gamma x S1 t2 T,
Gamma |- \x:S1, t2 : T ->
exists S2, <{{ S1 -> S2 }}> <: T
/\ (x |-> S1; Gamma) |- t2 : S2.
Proof with eauto.
intros * H.
remember <{ \x:S1, t2 }> as t.
induction H; inversion Heqt; subst; intros; try solve_by_invert.
- (* T_Abs *)
assert (Hwf := wf_has_type _ _ _ H0).
exists T12...
- (* T_Sub *)
destruct IHhas_type as [S2 [Hsub Hty]]...
Qed.
Lemma abs_arrow : forall x S1 s2 T1 T2,
empty |- \x:S1, s2 : (T1 -> T2) ->
T1 <: S1 /\ (x |-> S1) |- s2 : T2.
Proof with eauto.
intros * Hty.
apply typing_inversion_abs in Hty.
destruct Hty as [S2 [Hsub Hty]].
apply sub_inversion_arrow in Hsub.
destruct Hsub as [U1 [U2 [Heq [Hsub1 Hsub2]]]].
inversion Heq; subst...
Qed.
Lemma canonical_forms_of_arrow_types : forall Gamma s T1 T2,
Gamma |- s : (T1 -> T2) ->
value s ->
exists x S1 s2, s = <{ \x:S1, s2 }>.
Proof with eauto.
intros * Ht.
remember <{{T1 -> T2}}> as T.
generalize dependent T2. generalize dependent T1.
induction Ht; intros; subst; try solve_by_invert.
- (* T_Abs *)
inversion H...
- (* T_Sub *)
apply sub_inversion_arrow in H.
destruct H as [S1 [S2 [Heq Hsub]]]...
Qed.
Theorem progress : forall t T,
empty |- t : T ->
value t \/ exists t', t --> t'.
Proof with eauto.
intros * Ht.
remember empty as Gamma.
revert HeqGamma.
induction Ht; intros HeqGamma; subst...
- (* T_Var *)
inversion H.
- (* T_App *)
right.
destruct IHHt1; subst...
+ (* t1 is a value *)
destruct IHHt2; subst...
* (* t2 is a value *)
destruct (canonical_forms_of_arrow_types empty t1 T1 T2)
as [x [S1 [t12 Heqt1]]]...
subst. exists <{ t12 [x:=t2] }>...
* (* t2 steps *)
destruct H0 as [t2' Hstp]. exists <{ t1 t2' }> ...
+ (* t1 steps *)
destruct H as [t1' Hstp]. exists <{ t1' t2 }>...
- (* T_Proj *)
right. destruct IHHt...
+ (* rcd is value *)
destruct (lookup_field_in_value t R l T)
as [t' [Hget Ht']]...
+ (* rcd_steps *)
destruct H0 as [t' Hstp]. exists <{ t' --> l }>...
- (* T_RCons *)
destruct IHHt1...
+ (* head is a value *)
destruct IHHt2...
* (* tail steps *)
right. destruct H2 as [tr' Hstp].
exists <{ l = t :: tr' }>...
+ (* head steps *)
right. destruct H1 as [t' Hstp].
exists <{ l = t' :: tr}>...
Qed.
Lemma weakening : forall Gamma Gamma' t T,
inclusion Gamma Gamma' ->
Gamma |- t : T ->
Gamma' |- t : T.
Proof.
intros * H Ht.
generalize dependent Gamma'.
induction Ht; eauto using inclusion_update.
Qed.
Lemma weakening_empty : forall Gamma t T,
empty |- t : T ->
Gamma |- t : T.
Proof.
intros *.
eapply weakening.
discriminate.
Qed.
Lemma substitution_preserves_typing : forall Gamma x U t v T,
(x |-> U; Gamma) |- t : T ->
empty |- v : U ->
Gamma |- t [x:=v] : T.
Proof.
intros * Ht Hv.
remember (x |-> U; Gamma) as Gamma'.
generalize dependent Gamma.
induction Ht; intros Gamma' G; simpl; eauto.
- (* T_Var *)
rename x0 into y.
destruct (eqb_spec x y) as [Hxy|Hxy]; subst.
+ (* x = y *)
rewrite update_eq in H.
injection H as H. subst.
apply weakening_empty. assumption.
+ (* x <> y *)
apply T_Var; [|assumption].
rewrite update_neq in H; assumption.
- (* T_Abs *)
rename x0 into y. subst.
destruct (eqb_spec x y) as [Hxy|Hxy]; apply T_Abs; try assumption.
+ (* x = y *)
subst. rewrite update_shadow in Ht. assumption.
+ (* x <> y *)
subst. apply IHHt.
rewrite update_permute; auto.
- (* rcons *)
apply T_RCons; eauto.
inversion H0; subst; simpl; auto.
Qed.
Theorem preservation : forall t t' T,
empty |- t : T ->
t --> t' ->
empty |- t' : T.
Proof with eauto.
intros * HT. generalize dependent t'.
remember empty as Gamma.
induction HT;
intros t' HE; subst;
try solve [inversion HE; subst; eauto].
- (* T_App *)
inversion HE; subst...
+ (* ST_AppAbs *)
destruct (abs_arrow _ _ _ _ _ HT1) as [HA1 HA2].
apply substitution_preserves_typing with T0...
- (* T_Proj *)
inversion HE; subst...
destruct (lookup_field_in_value _ _ _ _ H2 HT H)
as [vi [Hget Hty]].
rewrite H4 in Hget. inversion Hget. subst...
- (* T_RCons *)
inversion HE; subst...
eauto using step_preserves_record_tm.
Qed.