Require Export Coq.Lists.List.
Require Import Coq.Program.Equality.
Require Export SysFWellscoped.
Require Import Coq.Program.Tactics.
Import CommaNotation.
Ltac inv H := inversion H; try clear H; try subst.
Ltac autorevert x :=
try (match goal with
| [y : ?Y |- ?claim] =>
try (match x with y => idtac end; fail 1);
match goal with [z : _ |- _] =>
match claim with context[z] =>
first
[ match Y with context[z] => revert y; autorevert x end
| match y with z => revert y; autorevert x end]
end
end
end).
Definition ctx n := fin n -> ty n.
Reserved Notation "'SUB' Delta |- A <: B"
(at level 68, A at level 99, no associativity).
Inductive sub {n} (Delta : ctx n) : ty n -> ty n -> Prop :=
| SA_top A :
SUB Delta |- A <: top
| SA_Refl x :
SUB Delta |- var_ty x <: var_ty x
| SA_Trans x B :
SUB Delta |- (Delta x) <: B -> SUB Delta |- var_ty x <: B
| SA_arrow A1 A2 B1 B2 :
SUB Delta |- B1 <: A1 -> SUB Delta |- A2 <: B2 ->
SUB Delta |- arr A1 A2 <: arr B1 B2
| SA_all (A1: ty n) (A2: ty (S n)) B1 B2 :
SUB Delta |- B1 <: A1 -> @sub (S n) ((B1, Delta) >> ⟨↑⟩) A2 B2 ->
SUB Delta |- all A1 A2 <: all B1 B2
where "'SUB' Delta |- A <: B" := (sub Delta A B).
Hint Constructors sub.
Lemma sub_refl n (Delta: ctx n) A : SUB Delta |- A <: A.
Proof. revert Delta. induction A; intuition; constructor; eauto. Qed.
Lemma sub_weak m n (Delta1: ctx m) (Delta2: ctx n) A1 A2 A1' A2' (xi: fin m -> fin n) :
SUB Delta1 |- A1 <: A2 ->
(forall x, (Delta1 x)⟨xi⟩ = Delta2 (xi x)) ->
A1' = A1⟨xi⟩ -> A2' = A2⟨xi⟩ ->
SUB Delta2 |- A1' <: A2' .
Proof.
intros H. autorevert H. induction H; intros; subst; asimpl; econstructor; eauto.
- eapply IHsub2; try reflexivity.
auto_case; [|now asimpl]. rewrite <- H1. now asimpl.
Qed.
Lemma sub_weak1 n (Delta : ctx n) A A' B B' C :
SUB Delta |- A <: B -> A' = A⟨↑⟩ -> B' = B⟨↑⟩ -> SUB ((C, Delta) >> ⟨↑⟩) |- A' <: B'.
Proof. intros. eapply sub_weak; eauto. intros x. now asimpl. Qed.
Definition transitivity_at {n} (B: ty n) := forall m Gamma (A : ty m) C (xi: fin n -> fin m),
SUB Gamma |- A <: B⟨xi⟩ -> SUB Gamma |- B⟨ xi⟩ <: C -> SUB Gamma |- A <: C.
Lemma transitivity_proj n (Gamma: ctx n) A B C :
transitivity_at B ->
SUB Gamma |- A <: B -> SUB Gamma |- B <: C -> SUB Gamma |- A <: C.
Proof. intros H. specialize (H n Gamma A C id). now asimpl in H. Qed.
Hint Resolve transitivity_proj.
Lemma transitivity_ren m n B (xi: fin m -> fin n) : transitivity_at B -> transitivity_at B⟨xi⟩.
Proof. unfold transitivity_at. intros. eapply H; asimpl in H0; asimpl in H1; eauto. Qed.
Lemma sub_narrow n (Delta Delta': ctx n) A C :
(forall x, SUB Delta' |- Delta' x <: Delta x) ->
(forall x, Delta x = Delta' x \/ transitivity_at (Delta x)) ->
SUB Delta |- A <: C -> SUB Delta' |- A <: C.
Proof with asimpl;eauto.
intros H H' HH. autorevert HH. induction HH; intros; eauto.
- destruct (H' x); eauto. rewrite H0 in *. eauto.
- constructor; eauto.
eapply IHHH2.
+ auto_case; try apply sub_refl.
eapply sub_weak; try reflexivity. eapply H. now asimpl.
+ auto_case. destruct (H' f); eauto using transitivity_ren.
rewrite H0. now left.
Qed.
Corollary sub_trans' n (B : ty n): transitivity_at B.
Proof with asimpl;eauto.
unfold transitivity_at.
autorevert B. induction B; intros...
- depind H...
- depind H... depind H0...
- depind H... depind H1...
- depind H... depind H1...
econstructor... clear IHsub0 IHsub3 IHsub1 IHsub2.
eapply IHB2; eauto.
+ asimpl in *. eapply sub_narrow; try eapply H0.
* auto_case. apply sub_refl.
eapply sub_weak with (xi := ↑); try reflexivity; eauto. now asimpl.
* intros [x|]; try cbn; eauto. right. apply transitivity_ren. apply transitivity_ren. eauto.
+ asimpl in H1_0. auto.
Qed.
Corollary sub_trans n (Delta : ctx n) A B C:
SUB Delta |- A <: B -> SUB Delta |- B <: C -> SUB Delta |- A <: C.
Proof. eauto using sub_trans'. Qed.
Lemma sub_substitution m m' (sigma : fin m -> ty m') Delta (Delta': ctx m') A B:
(forall x , SUB Delta' |- sigma x <: (Delta x)[sigma] ) ->
SUB Delta |- A <: B -> SUB Delta' |- subst_ty sigma A <: subst_ty sigma B.
Proof.
intros eq H. autorevert H. induction H; try now (econstructor; eauto).
- intros. asimpl. eapply sub_refl.
- intros. asimpl. eauto. cbn in *. eauto using sub_trans.
- intros. asimpl. econstructor; eauto.
asimpl. eapply IHsub2.
auto_case; asimpl; cbn; eauto using sub_refl.
eapply sub_weak; try reflexivity. eapply eq.
all: now asimpl.
Qed.
Require Import Coq.Program.Equality.
Require Export SysFWellscoped.
Require Import Coq.Program.Tactics.
Import CommaNotation.
Ltac inv H := inversion H; try clear H; try subst.
Ltac autorevert x :=
try (match goal with
| [y : ?Y |- ?claim] =>
try (match x with y => idtac end; fail 1);
match goal with [z : _ |- _] =>
match claim with context[z] =>
first
[ match Y with context[z] => revert y; autorevert x end
| match y with z => revert y; autorevert x end]
end
end
end).
Definition ctx n := fin n -> ty n.
Reserved Notation "'SUB' Delta |- A <: B"
(at level 68, A at level 99, no associativity).
Inductive sub {n} (Delta : ctx n) : ty n -> ty n -> Prop :=
| SA_top A :
SUB Delta |- A <: top
| SA_Refl x :
SUB Delta |- var_ty x <: var_ty x
| SA_Trans x B :
SUB Delta |- (Delta x) <: B -> SUB Delta |- var_ty x <: B
| SA_arrow A1 A2 B1 B2 :
SUB Delta |- B1 <: A1 -> SUB Delta |- A2 <: B2 ->
SUB Delta |- arr A1 A2 <: arr B1 B2
| SA_all (A1: ty n) (A2: ty (S n)) B1 B2 :
SUB Delta |- B1 <: A1 -> @sub (S n) ((B1, Delta) >> ⟨↑⟩) A2 B2 ->
SUB Delta |- all A1 A2 <: all B1 B2
where "'SUB' Delta |- A <: B" := (sub Delta A B).
Hint Constructors sub.
Lemma sub_refl n (Delta: ctx n) A : SUB Delta |- A <: A.
Proof. revert Delta. induction A; intuition; constructor; eauto. Qed.
Lemma sub_weak m n (Delta1: ctx m) (Delta2: ctx n) A1 A2 A1' A2' (xi: fin m -> fin n) :
SUB Delta1 |- A1 <: A2 ->
(forall x, (Delta1 x)⟨xi⟩ = Delta2 (xi x)) ->
A1' = A1⟨xi⟩ -> A2' = A2⟨xi⟩ ->
SUB Delta2 |- A1' <: A2' .
Proof.
intros H. autorevert H. induction H; intros; subst; asimpl; econstructor; eauto.
- eapply IHsub2; try reflexivity.
auto_case; [|now asimpl]. rewrite <- H1. now asimpl.
Qed.
Lemma sub_weak1 n (Delta : ctx n) A A' B B' C :
SUB Delta |- A <: B -> A' = A⟨↑⟩ -> B' = B⟨↑⟩ -> SUB ((C, Delta) >> ⟨↑⟩) |- A' <: B'.
Proof. intros. eapply sub_weak; eauto. intros x. now asimpl. Qed.
Definition transitivity_at {n} (B: ty n) := forall m Gamma (A : ty m) C (xi: fin n -> fin m),
SUB Gamma |- A <: B⟨xi⟩ -> SUB Gamma |- B⟨ xi⟩ <: C -> SUB Gamma |- A <: C.
Lemma transitivity_proj n (Gamma: ctx n) A B C :
transitivity_at B ->
SUB Gamma |- A <: B -> SUB Gamma |- B <: C -> SUB Gamma |- A <: C.
Proof. intros H. specialize (H n Gamma A C id). now asimpl in H. Qed.
Hint Resolve transitivity_proj.
Lemma transitivity_ren m n B (xi: fin m -> fin n) : transitivity_at B -> transitivity_at B⟨xi⟩.
Proof. unfold transitivity_at. intros. eapply H; asimpl in H0; asimpl in H1; eauto. Qed.
Lemma sub_narrow n (Delta Delta': ctx n) A C :
(forall x, SUB Delta' |- Delta' x <: Delta x) ->
(forall x, Delta x = Delta' x \/ transitivity_at (Delta x)) ->
SUB Delta |- A <: C -> SUB Delta' |- A <: C.
Proof with asimpl;eauto.
intros H H' HH. autorevert HH. induction HH; intros; eauto.
- destruct (H' x); eauto. rewrite H0 in *. eauto.
- constructor; eauto.
eapply IHHH2.
+ auto_case; try apply sub_refl.
eapply sub_weak; try reflexivity. eapply H. now asimpl.
+ auto_case. destruct (H' f); eauto using transitivity_ren.
rewrite H0. now left.
Qed.
Corollary sub_trans' n (B : ty n): transitivity_at B.
Proof with asimpl;eauto.
unfold transitivity_at.
autorevert B. induction B; intros...
- depind H...
- depind H... depind H0...
- depind H... depind H1...
- depind H... depind H1...
econstructor... clear IHsub0 IHsub3 IHsub1 IHsub2.
eapply IHB2; eauto.
+ asimpl in *. eapply sub_narrow; try eapply H0.
* auto_case. apply sub_refl.
eapply sub_weak with (xi := ↑); try reflexivity; eauto. now asimpl.
* intros [x|]; try cbn; eauto. right. apply transitivity_ren. apply transitivity_ren. eauto.
+ asimpl in H1_0. auto.
Qed.
Corollary sub_trans n (Delta : ctx n) A B C:
SUB Delta |- A <: B -> SUB Delta |- B <: C -> SUB Delta |- A <: C.
Proof. eauto using sub_trans'. Qed.
Lemma sub_substitution m m' (sigma : fin m -> ty m') Delta (Delta': ctx m') A B:
(forall x , SUB Delta' |- sigma x <: (Delta x)[sigma] ) ->
SUB Delta |- A <: B -> SUB Delta' |- subst_ty sigma A <: subst_ty sigma B.
Proof.
intros eq H. autorevert H. induction H; try now (econstructor; eauto).
- intros. asimpl. eapply sub_refl.
- intros. asimpl. eauto. cbn in *. eauto using sub_trans.
- intros. asimpl. econstructor; eauto.
asimpl. eapply IHsub2.
auto_case; asimpl; cbn; eauto using sub_refl.
eapply sub_weak; try reflexivity. eapply eq.
all: now asimpl.
Qed.
Inductive value {m n}: tm m n -> Prop :=
| Value_abs A s : value(abs A s)
| Value_tabs A s : value(tabs A s).
Reserved Notation "'TY' Delta ; Gamma |- A : B"
(at level 68, A at level 99, no associativity,
format "'TY' Delta ; Gamma |- A : B").
Definition dctx m n := fin m -> ty n.
Inductive has_ty {m n} (Delta : ctx m) (Gamma : dctx n m) : tm m n -> ty m -> Prop :=
| T_Var x :
TY Delta;Gamma |- var_tm x : (Gamma x)
| T_abs (A: ty m) B (s: tm m (S n)):
@has_ty m (S n) Delta (A, Gamma) s B ->
TY Delta;Gamma |- abs A s : arr A B
| T_app A B s t:
TY Delta;Gamma |- s : arr A B -> TY Delta;Gamma |- t : A ->
TY Delta;Gamma |- app s t : B
| T_tabs A B s :
@has_ty (S m) n ((A, Delta) >> ⟨↑⟩) (Gamma >> ⟨↑⟩) s B ->
TY Delta;Gamma |- tabs A s : all A B
| T_Tapp A B A' s B' :
TY Delta;Gamma |- s : all A B ->
SUB Delta |- A' <: A -> B' = subst_ty (A'..) B ->
TY Delta;Gamma |- tapp s A' : B'
| T_Sub A B s :
TY Delta;Gamma |- s : A -> SUB Delta |- A <: B ->
TY Delta;Gamma |- s : B
where "'TY' Delta ; Gamma |- s : A" := (has_ty Delta Gamma s A).
Hint Constructors has_ty.
Reserved Notation "'EV' s => t"
(at level 68, s at level 80, no associativity, format "'EV' s => t").
Inductive eval {m n} : tm m n -> tm m n -> Prop :=
| E_appabs A s t : EV app (abs A s) t => s[ids; t..]
| E_Tapptabs A s B : EV tapp (tabs A s) B => s[B..; ids]
| E_appFun s s' t :
EV s => s' ->
EV app s t => app s' t
| E_appArg s s' v:
EV s => s' -> value v ->
EV app v s => app v s'
| E_TyFun s s' A :
EV s => s' ->
EV tapp s A => tapp s' A
where "'EV' s => t" := (eval s t).
Definition empty {X} : fin 0 -> X :=
fun x => match x with end.
Lemma can_form_arr {s: tm 0 0} {A B}:
TY empty;empty |- s : arr A B -> value s -> exists C t, s = abs C t.
Proof.
intros H.
depind H; intros; eauto.
all: try now (try destruct x0; try inversion H1).
inversion H0; subst; eauto. inversion x.
Qed.
Lemma can_form_all {s A B}:
TY empty;empty |- s : all A B -> value s -> exists C t, s = tabs C t.
Proof.
intros H.
depind H; intros; eauto.
all: try now (try destruct x0; try inversion H1).
inv H0; subst; eauto. inversion x.
Qed.
Theorem ev_progress s A:
TY empty;empty |- s : A -> value s \/ exists t, EV s => t.
Proof.
intros. depind H; eauto; try (left; constructor).
- inversion x.
- right. edestruct IHhas_ty1 as [? | [? ?]]; try reflexivity.
+ edestruct (can_form_arr H H1) as [? [? ?]]; subst.
eexists. econstructor.
+ eexists. econstructor. eauto.
- right. edestruct IHhas_ty as [? | [? ?]]; try reflexivity.
+ edestruct (can_form_all H H1) as [? [? ?]]; subst. eexists. econstructor.
+ eexists. econstructor. eauto.
Qed.
Lemma context_renaming_lemma m m' n n' (Delta: ctx m') (Gamma: dctx n' m') (s: tm m n) A (sigma : fin m -> fin m') (tau: fin n -> fin n') Delta' (Gamma' : dctx n m):
(forall x, (Delta' x)⟨sigma⟩ = Delta (sigma x)) ->
(forall (x: fin n) , (Gamma' x)⟨sigma⟩ = (Gamma (tau x))) ->
TY Delta'; Gamma' |- s : A -> TY Delta; Gamma |- s⟨sigma;tau⟩ : A⟨sigma⟩.
Proof.
intros H H' ty. autorevert ty.
induction ty; intros; asimpl in *; subst; try now (econstructor; eauto).
- rewrite H'. constructor.
- constructor. apply IHty; eauto. auto_case.
- econstructor. apply IHty; eauto.
+ auto_case; try now asimpl. rewrite <- H. now asimpl.
+ intros. asimpl. rewrite <- H'. now asimpl.
- eapply T_Tapp with (A0 := A⟨sigma⟩) .
asimpl in IHty. eapply IHty; eauto.
eapply sub_weak; eauto.
now asimpl.
- econstructor. eauto.
eapply sub_weak; eauto.
Qed.
Lemma context_morphism_lemma m m' n n' (Delta: ctx m) (Delta': ctx m') (Gamma: dctx n m) (s: tm m n) A (sigma : fin m -> ty m') (tau: fin n -> tm m' n') (Gamma' : dctx n' m'):
(forall x, SUB Delta' |- sigma x <: (Delta x)[sigma]) ->
(forall (x: fin n) , TY Delta'; Gamma' |- tau x : subst_ty sigma (Gamma x)) ->
TY Delta; Gamma |- s : A -> TY Delta'; Gamma' |- s[sigma;tau] : A[sigma].
Proof.
intros eq1 eq2 ty. autorevert ty.
induction ty; intros; subst; asimpl; try now (econstructor; eauto).
- eapply eq2.
- constructor. eapply IHty; eauto.
auto_case; asimpl.
+ assert (subst_ty sigma (Gamma f) = ((Gamma f)[sigma]⟨id⟩)) as -> by (now asimpl) .
eapply context_renaming_lemma; eauto; now asimpl.
+ econstructor.
- constructor. eapply IHty; eauto.
+ auto_case.
* asimpl.
specialize (eq1 f).
eapply sub_weak1 with (C := A[sigma]) in eq1; eauto. asimpl in eq1. eapply eq1.
* asimpl. econstructor. apply sub_refl.
+ intros x. asimpl.
assert ((Gamma x) [sigma >> ⟨↑⟩] = (Gamma x)[sigma]⟨↑⟩) by (now asimpl).
auto_unfold in *. rewrite H.
eapply context_renaming_lemma.
* intros. now asimpl.
* intros. now asimpl.
* eapply eq2.
- eapply T_Tapp with (A0 := subst_ty sigma A) .
asimpl in IHty. eapply IHty; eauto.
eapply sub_substitution; eauto.
now asimpl.
- econstructor.
+ eapply IHty; eauto.
+ eapply sub_substitution; eauto.
Qed.
Lemma ty_inv_abs m n Delta Gamma A A' B C (s: tm m (S n)):
TY Delta;Gamma |- abs A s : C -> SUB Delta |- C <: arr A' B ->
(SUB Delta |- A' <: A /\
exists B', TY Delta; A .: Gamma |- s : B' /\ SUB Delta |- B' <: B).
Proof.
intros H. depind H; intros.
- inv H0. split; eauto.
- eauto using sub_trans.
Qed.
Lemma ty_subst m n (Gamma: dctx m n) (Delta: ctx n) Delta' s A:
(forall x, SUB Delta' |- Delta' x <: Delta x) ->
TY Delta; Gamma |- s : A -> TY Delta'; Gamma |- s : A.
Proof.
intros eq H. autorevert H. induction H; eauto; intros.
- econstructor; eauto. asimpl. eapply IHhas_ty. auto_case; eauto using sub_refl.
eapply sub_weak; try reflexivity. apply eq. intros x. now asimpl.
- econstructor; eauto.
replace A with (A[ids]) by (now asimpl). replace A' with (A'[ids]) by (now asimpl).
eapply sub_substitution; eauto. intros x.
asimpl. econstructor. eauto.
- econstructor; eauto. eapply sub_substitution with (sigma := ids) in H0; eauto.
asimpl in H0. eapply H0. intros x. econstructor. asimpl. eapply eq.
Qed.
Lemma ty_inv_tabs {m n} {Delta Gamma A A' B C} (s : tm (S m) n):
TY Delta;Gamma |- tabs A s : C -> SUB Delta |- C <: all A' B ->
(SUB Delta |- A' <: A /\ exists B',
TY (A'.:Delta) >> ren_ty ↑; Gamma >> ren_ty ↑ |- s : B' /\ SUB (A' .: Delta) >> ren_ty ↑ |- B' <: B).
Proof.
intros H. depind H; intros.
- inv H0. split; eauto.
eexists. split; eauto.
eapply ty_subst; eauto. auto_case.
apply sub_refl. eapply sub_weak; try reflexivity; eauto.
- eauto using sub_trans.
Qed.
Theorem preservation m n Delta Gamma (s: tm m n) t A :
TY Delta;Gamma |- s : A -> EV s => t ->
TY Delta;Gamma |- t : A.
Proof.
intros H_ty H_ev. autorevert H_ev.
induction H_ev; intros; eauto using ty.
all: try (now (depind H_ty; eauto)).
- depind H_ty; [|eauto].
+ depind H_ty1; subst.
* replace B with (B[ids]) by (now asimpl).
eapply context_morphism_lemma; eauto.
-- intros. asimpl. repeat constructor. apply sub_refl.
-- intros [|]; intros; cbn; asimpl; eauto.
* pose proof (ty_inv_abs _ _ _ _ _ _ _ _ _ H_ty1 H) as (?&?&?&?).
eapply T_Sub; eauto.
replace x with (x[var_ty]) by (now asimpl).
eapply context_morphism_lemma; eauto.
-- intros. asimpl. repeat constructor. apply sub_refl.
-- intros [|]; intros; cbn; asimpl; eauto.
- depind H_ty; eauto.
+ depind H_ty.
* asimpl in H_ty.
eapply context_morphism_lemma; try eapply H_ty; eauto.
-- auto_case.
++ asimpl. constructor. apply sub_refl.
++ now asimpl.
-- intros x. asimpl. constructor.
* pose proof (ty_inv_tabs _ H_ty H) as (?&?&?&?).
eapply T_Sub; eauto. asimpl in *.
eapply context_morphism_lemma; eauto.
-- auto_case; asimpl; eauto. asimpl. constructor. apply sub_refl.
-- intros z. unfold funcomp. asimpl. constructor.
-- eapply sub_substitution; eauto.
auto_case; asimpl.
constructor. apply sub_refl.
Qed.