Rocoma.Recipes_typing
Declare Scope ty_scope.
Delimit Scope ty_scope with ty.
Reserved Notation "[ Γ , a , b ⊢ s :- U ]" (format "[ Γ , a , b ⊢ s :- U ]").
Reserved Notation "[ ⊢ s :- U ]" (format "[ ⊢ s :- U ]").
Definition ctx := var -> type.
Definition empty_ctx: ctx := fun _ => Void.
Definition fv_plage (lo hi : nat) (s : term) :=
forall i, lo <= i < hi -> var_not_free i s.
Lemma fv_plage_eq a f :
fv_plage a a f.
Proof.
by move=> i h; exfalso; lia.
Qed.
forall i, lo <= i < hi -> var_not_free i s.
Lemma fv_plage_eq a f :
fv_plage a a f.
Proof.
by move=> i h; exfalso; lia.
Qed.
Shrinking the forbidden window weakens the property.
Lemma fv_plage_mono a b a1 b1 f :
a <= a1 -> b1 <= b ->
fv_plage a b f ->
fv_plage a1 b1 f.
Proof.
move=> ?? h i ?.
apply h.
by lia.
Qed.
a <= a1 -> b1 <= b ->
fv_plage a b f ->
fv_plage a1 b1 f.
Proof.
move=> ?? h i ?.
apply h.
by lia.
Qed.
Shifting window.
Lemma fv_plage_shift a b f n :
fv_plage a b f ->
fv_plage (a + n) (b + n) f.[ren (+n)].
Proof.
move=> h i hi.
have->: i = n + (i - n) by lia.
apply var_not_free_add.
apply h.
by lia.
Qed.
fv_plage a b f ->
fv_plage (a + n) (b + n) f.[ren (+n)].
Proof.
move=> h i hi.
have->: i = n + (i - n) by lia.
apply var_not_free_add.
apply h.
by lia.
Qed.
Two adjacent windows merge.
Lemma fv_plage_glue a b c f :
fv_plage a b f ->
fv_plage b c f ->
fv_plage a c f.
Proof.
move=> h1 h2 i hi.
case (boolP (i < b))=> hb.
- apply h1. by lia.
- apply h2. by lia.
Qed.
Lemma fv_plage_upn_cut_in a b k n f :
a <= k -> k <= b ->
fv_plage a b f ->
fv_plage a (b + n) f.[upn k (ren (+n))].
Proof.
move=> hak hkb h j hj.
case (boolP (j < k))=> hjk.
- apply var_not_free_upn_lt=>//.
apply h. by lia.
- case (boolP (j < k + n))=> hjkn.
+ apply var_not_free_upn_mid; by lia.
+ have e: j = (j - n) + n by lia.
rewrite e.
apply var_not_free_upn_ge; first by lia.
apply h. by lia.
Qed.
Lemma fv_plage_upn_cut_below a b k n f :
k <= a ->
fv_plage a b f ->
fv_plage (a + n) (b + n) f.[upn k (ren (+n))].
Proof.
move=> hka h j hj.
have->: j = (j - n) + n by lia.
apply var_not_free_upn_ge; first by lia.
apply h. by lia.
Qed.
Inductive has_type (Γ : ctx) (a b: nat) : recipe -> type -> Prop :=
| ty_var x U :
Γ x = U ->
[ Γ, a, b ⊢ Var x :- U ]
| ty_zero U :
U = Void ->
[ Γ, a, b ⊢ Zero :- U ]
| ty_top U :
U = Void ->
[ Γ , a , b ⊢ Top :- U ]
| ty_imp s f U :
U = Void ->
fv_plage a b f ->
[ Γ, a, b ⊢ s :- U ] ->
[ Γ, a, b ⊢ Imp s f :- U ]
| ty_and s t U :
[ Γ, a, b ⊢ s :- U ] ->
[ Γ, a, b ⊢ t :- U ] ->
[ Γ, a, b ⊢ And s t :- U ]
| ty_app s t U V :
[ Γ, a, b ⊢ s :- Arr U V ] ->
[ Γ, a, b ⊢ t :- U ] ->
[ Γ, a, b ⊢ App s t :- V ]
| ty_tapp s T U :
fv_plage a b T ->
[ Γ, a, b ⊢ s :- TArr U ] ->
[ Γ, a, b ⊢ TApp s T :- U ]
| ty_lam s U V :
[ U .: Γ, a, b ⊢ s :- V ] ->
[ Γ, a, b ⊢ Lam s U :- Arr U V ]
| ty_tlam s U :
[ Γ, a.+1, b.+1 ⊢ s :- U ] ->
[ Γ, a, b ⊢ TLam s :- TArr U ]
| ty_tall s U :
U = Void ->
[ Γ, a.+1, b.+1 ⊢ s :- U ] ->
[ Γ, a, b ⊢ TAll s :- U ]
| ty_box s U :
closed s ->
[ Γ, 0, b ⊢ s :- U ] ->
[ Γ, a, b ⊢ Box s :- U ]
| ty_neu s U :
[ Γ, a, b ⊢ s :- U ] ->
[ Γ, a, b ⊢ Neu s :- U ]
where "[ Γ , a , b ⊢ s :- U ]" := (has_type Γ a b s U) : ty_scope.
Notation "[ ⊢ s :- U ]" := (has_type empty_ctx 0 0 s U) : ty_scope.
Open Scope ty_scope.
Ltac tac_has_type :=
match goal with
| h: has_type _ _ _ _ _ |- _ => inv h
end.
Definition ctx_insertion (n: nat) (Γ: ctx) (U: type) :=
fun (i: nat) =>
if i < n then Γ i else
if eqn i n then U
else Γ (i.-1).
Ltac inv_ctx_insertion :=
match goal with
| h: [ (ctx_insertion _ _ _), _, _ ⊢ _ :- _ ] |- _ => inv h
end.
Lemma ctx_insertion0 Γ U :
ctx_insertion 0 Γ U = U .: Γ .
Proof.
rewrite /ctx_insertion.
by f_ext=> -[]//=.
Qed.
Lemma shift_ctx_insertion W n Γ U :
W .: ctx_insertion n Γ U =
ctx_insertion n.+1 (W.:Γ) U.
Proof.
rewrite /ctx_insertion.
f_ext=> -[] //= x.
have->: (x.+1 < n.+1) = (x < n) by lia.
case (boolP (x < n))=> // xn;
case (boolP (eqn x n))=> //= xn2.
have{xn xn2}xn: x > n by lia.
case: x xn=>//.
Qed.
Lemma has_type_det Γ a b s U V :
[ Γ, a, b ⊢ s :- U ] ->
[ Γ, a, b ⊢ s :- V ] ->
U = V.
Proof.
move=> h.
move: h V.
elim=>{Γ U a b}//=.
- by move=> > <- > h; inv h.
- by move=> > -> > h; inv h.
- by move=> > -> > h; inv h.
- move=> > -> ??? > h3. by inv h3.
- move=> > ??? h4 > h5. inv h5. by apply h4.
- move=> > ? h2 ?? > h5. inv h5. specialize (h2 _ H1). by congruence.
- move=> > ? h2 > h3 > h4. inv h4. specialize (h3 _ H3). by congruence.
- move=> > ? > h3 > h4. inv h4. specialize (h3 _ H2). by congruence.
- move=> > ? > h3 > h4. inv h4. specialize (h3 _ H0). by congruence.
- move=> > ?? > ? > h4. by inv h4.
- move=> > ?? h > h3. inv h3. by apply h.
- move=> > ? h2 > h3. inv h3. specialize (h2 _ H0). by congruence.
Qed.
Lemma has_type_neu r Γ U a b :
[ Γ, a, b ⊢ r :- U ] -> [ Γ, a, b ⊢ neu r :- U ].
Proof.
elim: r Γ U a b =>/=;
try first [ by move=> *; tac_has_type; constructor; eauto
| by move=> *; tac_has_type; eauto using has_type].
move=> *. tac_has_type. constructor.
by apply closed_sneu.
by eauto.
Qed.
Lemma neu_eq_same_type s t Γ U a b :
[ Γ, a, b ⊢ s :- U ] ->
neu s = neu t ->
[ Γ, a, b ⊢ t :- U ].
Proof.
elim: s t Γ U a b.
- move=> x t > ? /= h.
by have->: t = Var x by elim: t h=>//.
- move=> t > hty /= h. inv hty.
case (inversion_neu_top h)=> ->; by constructor.
- move=> t > hty /= h. inv hty.
case (inversion_neu_top h)=> ->; by constructor.
- move=> s h1 t h2 r > hty /= h. inv hty.
have[ss [tt [?[??]]]]:= inversion_neu_and h.
subst.
constructor; by [apply h1| apply h2].
- move=> s h1 t h2 r > hty /= h. inv hty.
have[ss [tt [?[??]]]]:= inversion_neu_app h.
subst.
apply ty_app with U; by [apply h1| apply h2].
- move=> s h1 S r > hty /= h. inv hty.
have[ss [??]]:= inversion_neu_tapp h.
subst.
constructor=>//.
by apply h1.
- move=> s h1 V r > hty /= h. inv hty.
have[ss [??]]:= inversion_neu_lam h.
subst.
constructor.
by apply h1.
- move=> s h1 f r > hty /= h. inv hty.
have[ss [??]]:= inversion_neu_imp h.
subst.
constructor=>//.
by apply h1.
- move=> s h1 r > hty /= h. inv hty.
have[ss [??]]:= inversion_neu_tlam h.
subst.
constructor=>//.
by apply h1.
- move=> s h1 r > hty /= h. inv hty.
have[ss [??]]:= inversion_neu_tall h.
subst.
constructor=>//.
by apply h1.
- move=> s h1 r > hty /= h. inv hty.
have[ss [??]]:= inversion_neu_neu h.
subst.
constructor=>//.
by apply h1.
- move=> s h1 r > hty /= h. inv hty.
have[ss [??]]:= inversion_neu_box h.
subst.
constructor=>//.
simpl in h.
by apply neu_eq_closed with s.
by apply h1.
Qed.
Lemma upn_miss_var n m x θ :
x <> n ->
n < m ->
upn m θ x <> TVar n.
Proof.
move=> h1 h2.
rewrite upnP.
case (boolP (x < m))=> xm.
- move=> h. injection h. by lia.
- move=> h.
destruct (θ (x - m))=>//=.
asimpl in h.
injections.
by lia.
Qed.
Lemma fv_plage_upn_gen a b (θ : var -> term) f :
fv_plage a b f ->
fv_plage a b f.[upn b θ].
Proof.
move=> h j hj.
apply var_not_free_upn_lt_gen.
- by lia.
- by apply h.
Qed.
Lemma has_type_hsubst_upn r Γ U a b θ :
[ Γ, a, b ⊢ r :- U ] ->
[ Γ, a, b ⊢ r.|[upn b θ] :- U ].
Proof.
elim: r Γ U a b θ=>//=.
- by move=> > h1 > h2 > h; inv h; apply ty_and; [apply h1|apply h2].
- move=> s h1 t h2 Γ U a b θ h; inv h.
apply ty_app with U0; by [apply h1|apply h2].
- move=> s h1 T Γ U a b θ h; inv h.
apply ty_tapp; by [apply fv_plage_upn_gen|apply h1].
- by move=> > h1 > h; inv h; apply ty_lam; apply h1.
- move=> s h1 f Γ U a b θ h; inv h.
apply ty_imp=>//; by [apply fv_plage_upn_gen|apply h1].
- move=> s h1 Γ U a b θ h; inv h.
rewrite fold_up_upn; apply ty_tlam; by apply h1.
- move=> s h1 Γ U a b θ h; inv h.
rewrite fold_up_upn; apply ty_tall=>//; by apply h1.
- by move=> > h1 > h; inv h; apply ty_neu; apply h1.
- move=> s h1 Γ U a b θ h; inv h.
apply ty_box; by [apply closed_unaffectedh|apply h1].
Qed.
Lemma has_type_swap_a s Γ a a' b U :
b <= a -> b <= a' ->
[ Γ, a, b ⊢ s :- U ] ->
[ Γ, a', b ⊢ s :- U ].
Proof.
elim: s Γ a a' b U=>/=.
- by move=> > ?? h; inv h; apply ty_var.
- by move=> > ?? h; inv h; apply ty_zero.
- by move=> > ?? h; inv h; apply ty_top.
- move=> s h1 t h2 Γ a a' b U ?? h; inv h.
apply ty_and; by [apply h1 with a|apply h2 with a].
- move=> s h1 t h2 Γ a a' b U ?? h; inv h.
apply ty_app with U0; by [apply h1 with a|apply h2 with a].
- move=> s h1 T Γ a a' b U ?? h; inv h.
apply ty_tapp; last by apply h1 with a.
by move=> i ?; exfalso; lia.
- move=> s h1 W Γ a a' b U ?? h; inv h.
by apply ty_lam; apply h1 with a.
- move=> s h1 f Γ a a' b U ?? h; inv h.
apply ty_imp=>//; last by apply h1 with a.
by move=> i ?; exfalso; lia.
- move=> s h1 Γ a a' b U ?? h; inv h.
apply ty_tlam; apply h1 with a.+1; by [lia|lia|].
- move=> s h1 Γ a a' b U ?? h; inv h.
apply ty_tall=>//; apply h1 with a.+1; by [lia|lia|].
- move=> s h1 Γ a a' b U ?? h; inv h.
by apply ty_neu; apply h1 with a.
(* ty_box resets the counter: the premise does not mention a *)
- by move=> > h1 > ?? h; inv h; apply ty_box.
Qed.
Corollary has_type_hsubst_0 s U θ :
[ ⊢ s :- U ] -> [ ⊢ s.|[θ] :- U ].
Proof.
move=> h.
have:= @has_type_hsubst_upn s empty_ctx U 0 0 θ.
rewrite upn0. by apply.
Qed.
fv_plage a b f ->
fv_plage b c f ->
fv_plage a c f.
Proof.
move=> h1 h2 i hi.
case (boolP (i < b))=> hb.
- apply h1. by lia.
- apply h2. by lia.
Qed.
Lemma fv_plage_upn_cut_in a b k n f :
a <= k -> k <= b ->
fv_plage a b f ->
fv_plage a (b + n) f.[upn k (ren (+n))].
Proof.
move=> hak hkb h j hj.
case (boolP (j < k))=> hjk.
- apply var_not_free_upn_lt=>//.
apply h. by lia.
- case (boolP (j < k + n))=> hjkn.
+ apply var_not_free_upn_mid; by lia.
+ have e: j = (j - n) + n by lia.
rewrite e.
apply var_not_free_upn_ge; first by lia.
apply h. by lia.
Qed.
Lemma fv_plage_upn_cut_below a b k n f :
k <= a ->
fv_plage a b f ->
fv_plage (a + n) (b + n) f.[upn k (ren (+n))].
Proof.
move=> hka h j hj.
have->: j = (j - n) + n by lia.
apply var_not_free_upn_ge; first by lia.
apply h. by lia.
Qed.
Inductive has_type (Γ : ctx) (a b: nat) : recipe -> type -> Prop :=
| ty_var x U :
Γ x = U ->
[ Γ, a, b ⊢ Var x :- U ]
| ty_zero U :
U = Void ->
[ Γ, a, b ⊢ Zero :- U ]
| ty_top U :
U = Void ->
[ Γ , a , b ⊢ Top :- U ]
| ty_imp s f U :
U = Void ->
fv_plage a b f ->
[ Γ, a, b ⊢ s :- U ] ->
[ Γ, a, b ⊢ Imp s f :- U ]
| ty_and s t U :
[ Γ, a, b ⊢ s :- U ] ->
[ Γ, a, b ⊢ t :- U ] ->
[ Γ, a, b ⊢ And s t :- U ]
| ty_app s t U V :
[ Γ, a, b ⊢ s :- Arr U V ] ->
[ Γ, a, b ⊢ t :- U ] ->
[ Γ, a, b ⊢ App s t :- V ]
| ty_tapp s T U :
fv_plage a b T ->
[ Γ, a, b ⊢ s :- TArr U ] ->
[ Γ, a, b ⊢ TApp s T :- U ]
| ty_lam s U V :
[ U .: Γ, a, b ⊢ s :- V ] ->
[ Γ, a, b ⊢ Lam s U :- Arr U V ]
| ty_tlam s U :
[ Γ, a.+1, b.+1 ⊢ s :- U ] ->
[ Γ, a, b ⊢ TLam s :- TArr U ]
| ty_tall s U :
U = Void ->
[ Γ, a.+1, b.+1 ⊢ s :- U ] ->
[ Γ, a, b ⊢ TAll s :- U ]
| ty_box s U :
closed s ->
[ Γ, 0, b ⊢ s :- U ] ->
[ Γ, a, b ⊢ Box s :- U ]
| ty_neu s U :
[ Γ, a, b ⊢ s :- U ] ->
[ Γ, a, b ⊢ Neu s :- U ]
where "[ Γ , a , b ⊢ s :- U ]" := (has_type Γ a b s U) : ty_scope.
Notation "[ ⊢ s :- U ]" := (has_type empty_ctx 0 0 s U) : ty_scope.
Open Scope ty_scope.
Ltac tac_has_type :=
match goal with
| h: has_type _ _ _ _ _ |- _ => inv h
end.
Definition ctx_insertion (n: nat) (Γ: ctx) (U: type) :=
fun (i: nat) =>
if i < n then Γ i else
if eqn i n then U
else Γ (i.-1).
Ltac inv_ctx_insertion :=
match goal with
| h: [ (ctx_insertion _ _ _), _, _ ⊢ _ :- _ ] |- _ => inv h
end.
Lemma ctx_insertion0 Γ U :
ctx_insertion 0 Γ U = U .: Γ .
Proof.
rewrite /ctx_insertion.
by f_ext=> -[]//=.
Qed.
Lemma shift_ctx_insertion W n Γ U :
W .: ctx_insertion n Γ U =
ctx_insertion n.+1 (W.:Γ) U.
Proof.
rewrite /ctx_insertion.
f_ext=> -[] //= x.
have->: (x.+1 < n.+1) = (x < n) by lia.
case (boolP (x < n))=> // xn;
case (boolP (eqn x n))=> //= xn2.
have{xn xn2}xn: x > n by lia.
case: x xn=>//.
Qed.
Lemma has_type_det Γ a b s U V :
[ Γ, a, b ⊢ s :- U ] ->
[ Γ, a, b ⊢ s :- V ] ->
U = V.
Proof.
move=> h.
move: h V.
elim=>{Γ U a b}//=.
- by move=> > <- > h; inv h.
- by move=> > -> > h; inv h.
- by move=> > -> > h; inv h.
- move=> > -> ??? > h3. by inv h3.
- move=> > ??? h4 > h5. inv h5. by apply h4.
- move=> > ? h2 ?? > h5. inv h5. specialize (h2 _ H1). by congruence.
- move=> > ? h2 > h3 > h4. inv h4. specialize (h3 _ H3). by congruence.
- move=> > ? > h3 > h4. inv h4. specialize (h3 _ H2). by congruence.
- move=> > ? > h3 > h4. inv h4. specialize (h3 _ H0). by congruence.
- move=> > ?? > ? > h4. by inv h4.
- move=> > ?? h > h3. inv h3. by apply h.
- move=> > ? h2 > h3. inv h3. specialize (h2 _ H0). by congruence.
Qed.
Lemma has_type_neu r Γ U a b :
[ Γ, a, b ⊢ r :- U ] -> [ Γ, a, b ⊢ neu r :- U ].
Proof.
elim: r Γ U a b =>/=;
try first [ by move=> *; tac_has_type; constructor; eauto
| by move=> *; tac_has_type; eauto using has_type].
move=> *. tac_has_type. constructor.
by apply closed_sneu.
by eauto.
Qed.
Lemma neu_eq_same_type s t Γ U a b :
[ Γ, a, b ⊢ s :- U ] ->
neu s = neu t ->
[ Γ, a, b ⊢ t :- U ].
Proof.
elim: s t Γ U a b.
- move=> x t > ? /= h.
by have->: t = Var x by elim: t h=>//.
- move=> t > hty /= h. inv hty.
case (inversion_neu_top h)=> ->; by constructor.
- move=> t > hty /= h. inv hty.
case (inversion_neu_top h)=> ->; by constructor.
- move=> s h1 t h2 r > hty /= h. inv hty.
have[ss [tt [?[??]]]]:= inversion_neu_and h.
subst.
constructor; by [apply h1| apply h2].
- move=> s h1 t h2 r > hty /= h. inv hty.
have[ss [tt [?[??]]]]:= inversion_neu_app h.
subst.
apply ty_app with U; by [apply h1| apply h2].
- move=> s h1 S r > hty /= h. inv hty.
have[ss [??]]:= inversion_neu_tapp h.
subst.
constructor=>//.
by apply h1.
- move=> s h1 V r > hty /= h. inv hty.
have[ss [??]]:= inversion_neu_lam h.
subst.
constructor.
by apply h1.
- move=> s h1 f r > hty /= h. inv hty.
have[ss [??]]:= inversion_neu_imp h.
subst.
constructor=>//.
by apply h1.
- move=> s h1 r > hty /= h. inv hty.
have[ss [??]]:= inversion_neu_tlam h.
subst.
constructor=>//.
by apply h1.
- move=> s h1 r > hty /= h. inv hty.
have[ss [??]]:= inversion_neu_tall h.
subst.
constructor=>//.
by apply h1.
- move=> s h1 r > hty /= h. inv hty.
have[ss [??]]:= inversion_neu_neu h.
subst.
constructor=>//.
by apply h1.
- move=> s h1 r > hty /= h. inv hty.
have[ss [??]]:= inversion_neu_box h.
subst.
constructor=>//.
simpl in h.
by apply neu_eq_closed with s.
by apply h1.
Qed.
Lemma upn_miss_var n m x θ :
x <> n ->
n < m ->
upn m θ x <> TVar n.
Proof.
move=> h1 h2.
rewrite upnP.
case (boolP (x < m))=> xm.
- move=> h. injection h. by lia.
- move=> h.
destruct (θ (x - m))=>//=.
asimpl in h.
injections.
by lia.
Qed.
Lemma fv_plage_upn_gen a b (θ : var -> term) f :
fv_plage a b f ->
fv_plage a b f.[upn b θ].
Proof.
move=> h j hj.
apply var_not_free_upn_lt_gen.
- by lia.
- by apply h.
Qed.
Lemma has_type_hsubst_upn r Γ U a b θ :
[ Γ, a, b ⊢ r :- U ] ->
[ Γ, a, b ⊢ r.|[upn b θ] :- U ].
Proof.
elim: r Γ U a b θ=>//=.
- by move=> > h1 > h2 > h; inv h; apply ty_and; [apply h1|apply h2].
- move=> s h1 t h2 Γ U a b θ h; inv h.
apply ty_app with U0; by [apply h1|apply h2].
- move=> s h1 T Γ U a b θ h; inv h.
apply ty_tapp; by [apply fv_plage_upn_gen|apply h1].
- by move=> > h1 > h; inv h; apply ty_lam; apply h1.
- move=> s h1 f Γ U a b θ h; inv h.
apply ty_imp=>//; by [apply fv_plage_upn_gen|apply h1].
- move=> s h1 Γ U a b θ h; inv h.
rewrite fold_up_upn; apply ty_tlam; by apply h1.
- move=> s h1 Γ U a b θ h; inv h.
rewrite fold_up_upn; apply ty_tall=>//; by apply h1.
- by move=> > h1 > h; inv h; apply ty_neu; apply h1.
- move=> s h1 Γ U a b θ h; inv h.
apply ty_box; by [apply closed_unaffectedh|apply h1].
Qed.
Lemma has_type_swap_a s Γ a a' b U :
b <= a -> b <= a' ->
[ Γ, a, b ⊢ s :- U ] ->
[ Γ, a', b ⊢ s :- U ].
Proof.
elim: s Γ a a' b U=>/=.
- by move=> > ?? h; inv h; apply ty_var.
- by move=> > ?? h; inv h; apply ty_zero.
- by move=> > ?? h; inv h; apply ty_top.
- move=> s h1 t h2 Γ a a' b U ?? h; inv h.
apply ty_and; by [apply h1 with a|apply h2 with a].
- move=> s h1 t h2 Γ a a' b U ?? h; inv h.
apply ty_app with U0; by [apply h1 with a|apply h2 with a].
- move=> s h1 T Γ a a' b U ?? h; inv h.
apply ty_tapp; last by apply h1 with a.
by move=> i ?; exfalso; lia.
- move=> s h1 W Γ a a' b U ?? h; inv h.
by apply ty_lam; apply h1 with a.
- move=> s h1 f Γ a a' b U ?? h; inv h.
apply ty_imp=>//; last by apply h1 with a.
by move=> i ?; exfalso; lia.
- move=> s h1 Γ a a' b U ?? h; inv h.
apply ty_tlam; apply h1 with a.+1; by [lia|lia|].
- move=> s h1 Γ a a' b U ?? h; inv h.
apply ty_tall=>//; apply h1 with a.+1; by [lia|lia|].
- move=> s h1 Γ a a' b U ?? h; inv h.
by apply ty_neu; apply h1 with a.
(* ty_box resets the counter: the premise does not mention a *)
- by move=> > h1 > ?? h; inv h; apply ty_box.
Qed.
Corollary has_type_hsubst_0 s U θ :
[ ⊢ s :- U ] -> [ ⊢ s.|[θ] :- U ].
Proof.
move=> h.
have:= @has_type_hsubst_upn s empty_ctx U 0 0 θ.
rewrite upn0. by apply.
Qed.
Lemma tsubst_ext_one (T : term) (σ1 σ2 : var -> term) d :
var_not_free d T ->
(forall x, x <> d -> σ1 x = σ2 x) ->
T.[σ1] = T.[σ2].
Proof.
rewrite /var_not_free => hT hσ.
have e : forall σ : var -> term, T.[σ] = T.[subst_var2 d (ids d.+1) >> σ]
by move=> σ; rewrite -subst_comp hT.
rewrite (e σ1) (e σ2).
f_equal; f_ext=> x.
rewrite /subst_var2 /scomp /funcomp.
case: (boolP (x == d))=> ex; asimpl.
- apply: hσ.
by lia.
- apply: hσ.
by apply/eqP.
Qed.
Lemma up_ext_one (σ1 σ2 : var -> term) d :
(forall x, x <> d -> σ1 x = σ2 x) ->
forall x, x <> d.+1 -> up σ1 x = up σ2 x.
Proof.
move=> hσ [|y] hy.
- by asimpl.
- have hy' : y <> d by lia.
by asimpl; rewrite (hσ _ hy').
Qed.
Same on a recipe, when d lies in the forbidden window.
Lemma has_type_hsubst_ext s Γ U a b d (σ1 σ2 : var -> term) :
a <= d -> d < b ->
(forall x, x <> d -> σ1 x = σ2 x) ->
[ Γ, a, b ⊢ s :- U ] ->
s.|[σ1] = s.|[σ2].
Proof.
elim: s Γ U a b d σ1 σ2=>/=.
- by move=> *.
- by move=> *.
- by move=> *.
- move=> s h1 t h2 Γ U a b d σ1 σ2 had hdb hσ h; inv h.
f_equal; by [apply h1 with Γ U a b d|apply h2 with Γ U a b d].
- move=> s h1 t h2 Γ U a b d σ1 σ2 had hdb hσ h; inv h.
f_equal; by [apply h1 with Γ (Arr U0 U) a b d|apply h2 with Γ U0 a b d].
- move=> s h1 T Γ U a b d σ1 σ2 had hdb hσ h; inv h.
f_equal.
+ by apply h1 with Γ (TArr U) a b d.
+ apply tsubst_ext_one with d=>//.
by apply H1; lia.
- move=> s h1 W Γ U a b d σ1 σ2 had hdb hσ h; inv h.
f_equal.
by apply h1 with (W .: Γ) V a b d.
- move=> s h1 f Γ U a b d σ1 σ2 had hdb hσ h; inv h.
f_equal.
+ by apply h1 with Γ Void a b d.
+ apply tsubst_ext_one with d=>//.
by apply H2; lia.
- move=> s h1 Γ U a b d σ1 σ2 had hdb hσ h; inv h.
f_equal.
apply h1 with Γ U0 a.+1 b.+1 d.+1; by [lia|apply up_ext_one|].
- move=> s h1 Γ U a b d σ1 σ2 had hdb hσ h; inv h.
f_equal.
apply h1 with Γ Void a.+1 b.+1 d.+1; by [lia|apply up_ext_one|].
- move=> s h1 Γ U a b d σ1 σ2 had hdb hσ h; inv h.
f_equal.
by apply h1 with Γ U a b d.
- move=> s h1 Γ U a b d σ1 σ2 had hdb hσ h; inv h.
f_equal.
apply h1 with Γ U 0 b d; by [lia|].
Qed.
Definition ren_dec (d : nat) : var -> var := fun x => if x < d then x else x.-1.
Lemma upn_T_vs_dec (T : term) d :
forall x, x <> d -> upn d (T .: ids) x = ren (ren_dec d) x.
Proof.
move=> x hx.
Check ren_dec.
rewrite upnP /ren_dec /=.
case: ifPn=> hxd //.
have [k hk]: exists k, x - d = k.+1 by exists (x - d).-1; lia.
rewrite hk /=.
by asimpl; f_equal; lia.
Qed.
Corollary hsubst_T_is_ren s Γ U a b d T :
a <= d -> d < b ->
[ Γ, a, b ⊢ s :- U ] ->
s.|[upn d (T .: ids)] = s.|[ren (ren_dec d)].
Proof.
move=> had hdb h.
apply has_type_hsubst_ext with Γ U a b d=>//.
by apply upn_T_vs_dec.
Qed.
Definition complete (r: recipe) :=
closed r /\ [ ⊢ r :- Void ].
Lemma fv_has_ty s n U Γ Δ a b :
(forall i, i < n -> Γ i = Δ i) ->
fv n s ->
[ Γ, a, b ⊢ s :- U ] ->
[ Δ, a, b ⊢ s :- U ].
Proof.
elim: s n U Γ Δ a b; try by (intros; subst; constructor).
{ move=> x n > h hfv ht. constructor. inv ht.
rewrite h=>//.
case (boolP (x < n))=>// h1.
exfalso.
move: hfv.
rewrite /fv; asimpl.
rewrite upnP ifF /=; last by lia.
have e: n + (x - n).+1 %coq_nat = x.+1 by lia.
move=> h2; injection h2=> {}h2.
by lia. }
{ by move=> > ?? ht; inv ht; constructor. }
{ by move=> > ?? ht; inv ht; constructor. }
{ move=> > hs > ht n ? Γ > h /fv_and [] ?? ht2.
inv ht2. constructor.
by apply hs with n Γ.
by apply ht with n Γ. }
{ move=> s hs t ht n U Γ > h /fv_app [] h1 h2 ht2.
inv ht2. econstructor.
by apply (hs n (Arr U0 U) Γ).
by apply (ht n U0 Γ). }
{ move=> s hs S n U Γ > h /fv_tapp [h1 ht2].
inv ht2. constructor=>//. by apply hs with n Γ. }
{ move=> s hs U n V Γ > h0 /fv_lam h ht.
inv ht. constructor=>//.
by apply hs with n.+1 (U .: Γ)=>// -[]. }
{ move=> s hs f n U Γ > h /fv_imp h1 ht2.
inv ht2. constructor=>//. by apply hs with n Γ. }
{ move=> s hs n U Γ > h /fv_tlam h1 ht2.
inv ht2. constructor=>//. by apply hs with n Γ. }
{ move=> s hs n U Γ > h /fv_tall h1 ht2.
inv ht2. constructor=>//. by apply hs with n Γ. }
{ move=> s hs n U Γ > h /fv_neu h1 ht2.
inv ht2. constructor=>//. by apply hs with n Γ. }
{ move=> s hs n U Γ > h /fv_box h1 ht2.
inv ht2. constructor=>//. by apply hs with n Γ. }
Qed.
Corollary closed_has_ty_contr s Γ V a b :
closed s ->
[ Γ, a, b ⊢ s :- V ] ->
[ empty_ctx, a, b ⊢ s :- V ].
Proof.
exact: fv_has_ty.
Qed.
Corollary closed_has_ty_weak s Γ V a b :
closed s ->
[ empty_ctx, a, b ⊢ s :- V ] ->
[ Γ, a, b ⊢ s :- V ].
Proof.
exact: fv_has_ty.
Qed.
Lemma has_type_hshift_cut_in s Γ a b U k n :
[ Γ, a, b ⊢ s :- U ] ->
a <= k -> k <= b ->
[ Γ, a, b + n ⊢ s.|[upn k (ren (+n))] :- U ].
Proof.
move=> h.
elim: h k n=> {Γ a b s U}.
- by move=> > <- *; constructor.
- by move=> > -> *; constructor.
- by move=> > -> *; constructor.
- move=> Γ a b s f U -> hfv hs ih k n h1 h2 /=.
constructor=>//.
+ by apply fv_plage_upn_cut_in.
+ by apply ih.
- move=> Γ a b s t U hs ihs ht iht k n h1 h2 /=.
constructor; by [apply ihs | apply iht].
- move=> Γ a b s t U V hs ihs ht iht k n h1 h2 /=.
apply ty_app with U; by [apply ihs | apply iht].
- move=> Γ a b s T U hfv hs ih k n h1 h2 /=.
constructor.
+ by apply fv_plage_upn_cut_in.
+ by apply ih.
- move=> Γ a b s U V hs ih k n h1 h2 /=.
constructor. by apply ih.
- move=> Γ a b s U hs ih k n h1 h2 /=.
rewrite fold_up_upn.
constructor.
Print ssrnat.
rewrite -addSn.
by apply ih; lia.
- move=> Γ a b s U -> hs ih k n h1 h2 /=.
rewrite fold_up_upn.
constructor=>//.
rewrite -addSn.
by apply ih; lia.
- move=> Γ a b s U hc hs ih k n h1 h2 /=.
constructor.
+ by apply closed_unaffectedh.
+ by apply ih; lia.
- move=> Γ a b s U hs ih k n h1 h2 /=.
constructor. by apply ih.
Qed.
Lemma has_type_hshift_cut_below s Γ a b U k n :
[ Γ, a, b ⊢ s :- U ] ->
k <= a -> k <= b ->
[ Γ, a + n, b + n ⊢ s.|[upn k (ren (+n))] :- U ].
Proof.
move=> h.
elim: h k n=> {Γ a b s U}.
- by move=> > <- *; constructor.
- by move=> > -> *; constructor.
- by move=> > -> *; constructor.
- move=> Γ a b s f U -> hfv hs ih k n h1 h2 /=.
constructor=>//.
+ by apply fv_plage_upn_cut_below.
+ by apply ih.
- move=> Γ a b s t U hs ihs ht iht k n h1 h2 /=.
constructor; by [apply ihs | apply iht].
- move=> Γ a b s t U V hs ihs ht iht k n h1 h2 /=.
apply ty_app with U; by [apply ihs | apply iht].
- move=> Γ a b s T U hfv hs ih k n h1 h2 /=.
constructor.
+ by apply fv_plage_upn_cut_below.
+ by apply ih.
- move=> Γ a b s U V hs ih k n h1 h2 /=.
constructor. by apply ih.
- move=> Γ a b s U hs ih k n h1 h2 /=.
rewrite fold_up_upn.
constructor.
rewrite -!addSn.
by apply ih; lia.
- move=> Γ a b s U -> hs ih k n h1 h2 /=.
rewrite fold_up_upn.
constructor=>//.
rewrite -!addSn.
by apply ih; lia.
- move=> Γ a b s U hc hs ih k n h1 h2 /=.
constructor.
+ by apply closed_unaffectedh.
(* ty_box resets a to 0: the cut moves inside the window *)
+ apply has_type_hshift_cut_in=>//; by lia.
- move=> Γ a b s U hs ih k n h1 h2 /=.
constructor. by apply ih.
Qed.
Lemma has_type_hshift Γ a b u U n :
[ Γ, a, b ⊢ u :- U ] ->
[ Γ, a + n, b + n ⊢ u.|[ren (+n)] :- U ].
Proof.
move=> h.
have->: (ren (+n) : var -> term) = upn 0 (ren (+n)) by rewrite upn0.
by apply has_type_hshift_cut_below.
Qed.
Lemma __has_type_eq_ab_refuted :
~ (forall Γ a b s U, [ Γ, a, a ⊢ s :- U ] -> [ Γ, b, b ⊢ s :- U ]).
Proof.
move=> h.
have h0: [ empty_ctx, 0, 0 ⊢ Box (Imp Top (TVar 0)) :- Void ]
by repeat constructor.
specialize (h empty_ctx 0 1 _ _ h0).
inv h. inv H1.
have e: 0 <= 0 < 1 by lia.
by have := H4 0 e.
Qed.
Lemma has_type_lower_b s Γ a b U b1 :
[ Γ, a, b ⊢ s :- U ] ->
b1 <= b ->
[ Γ, a, b1 ⊢ s :- U ].
Proof.
move=> h.
elim: h b1=> {Γ a b s U}.
- by move=> > <- *; constructor.
- by move=> > -> *; constructor.
- by move=> > -> *; constructor.
- move=> Γ a b s f U -> hfv hs ih b1 h1.
constructor=>//.
+ apply fv_plage_mono with a b; by [lia|].
+ by apply ih.
- move=> Γ a b s t U hs ihs ht iht b1 h1.
constructor; by [apply ihs | apply iht].
- move=> Γ a b s t U V hs ihs ht iht b1 h1.
apply ty_app with U; by [apply ihs | apply iht].
- move=> Γ a b s T U hfv hs ih b1 h1.
constructor.
+ apply fv_plage_mono with a b; by [lia|].
+ by apply ih.
- move=> Γ a b s U V hs ih b1 h1.
constructor. by apply ih.
- move=> Γ a b s U hs ih b1 h1.
constructor. by apply ih; lia.
- move=> Γ a b s U -> hs ih b1 h1.
constructor=>//. by apply ih; lia.
- move=> Γ a b s U hc hs ih b1 h1.
constructor=>//. by apply ih.
- move=> Γ a b s U hs ih b1 h1.
constructor. by apply ih.
Qed.
Lemma has_type_lower_1 s Γ U :
[ Γ, 1, 1 ⊢ s :- U ] -> [ Γ, 0, 0 ⊢ s :- U ].
Proof.
move=> h.
apply has_type_swap_a with 1=>//.
by apply has_type_lower_b with 1.
Qed.
Lemma has_type_hsubst1 s Γ U T :
[ Γ, 1, 1 ⊢ s :- U ] -> [ Γ, 0, 0 ⊢ s.|[T/] :- U ].
Proof.
move=> h.
apply has_type_swap_a with 1=>//.
have->: (T .: ids : var -> term) = upn 0 (T .: ids) by rewrite upn0.
apply has_type_hsubst_upn.
by apply has_type_lower_b with 1.
Qed.
Corollary has_type_lower_b0 s Γ a b U :
[ Γ, a, b ⊢ s :- U ] ->
[ Γ, a, 0 ⊢ s :- U ].
Proof.
move=> h.
by apply has_type_lower_b with b.
Qed.
Lemma has_type_beta_gen Γ W U n t s a b :
closed t ->
[ empty_ctx, a, b ⊢ t :- U ] ->
[ ctx_insertion n Γ U, a, b ⊢ s :- W ] ->
[ Γ, a, b ⊢ s.[t//n] :- W ].
Proof.
elim: s Γ W U n t a b;
try (by move=>*; inv_ctx_insertion; econstructor; eauto).
- move=> x Γ W U n t > ?? h2 /=.
rewrite /subst_var. inv h2. rewrite /ctx_insertion.
case (lt_eq_lt_dec x n) => [[]|] xn /=.
+ constructor.
by rewrite ifT; [|lia].
+ subst.
have->: n < n = false by lia.
have->: eqn n n = true by lia.
by apply closed_has_ty_weak.
+ constructor.
rewrite !ifF; try by lia.
by f_equal; lia.
- move=> s h1 Z Γ W U n u > ? h3 h4 /=.
inv h4.
rewrite upn1 subst_var_lemma.
have->: u.[ren (+1)] = u.
{ have->: ren (+1) = upn 0 (ren (+1)) by [].
by apply fv_unaffected_lift. }
rewrite addn1.
constructor.
rewrite shift_ctx_insertion in H2.
by apply (h1 _ _ _ _ u) in H2.
- move=> s h1 Γ W U n u a b ? h3 h4 /=. inv_ctx_insertion.
rewrite subst_var_hsubst.
constructor.
apply h1 with U=>//.
+ by apply closed_unaffectedh.
+ rewrite -(addn1 a) -(addn1 b).
by apply has_type_hshift.
- move=> s h1 Γ W U n u a b ? h3 h4 /=. inv_ctx_insertion.
rewrite subst_var_hsubst.
constructor=>//.
apply h1 with U=>//.
+ by apply closed_unaffectedh.
+ rewrite -(addn1 a) -(addn1 b).
by apply has_type_hshift.
- move=> s h1 Γ W U n u a b ? h3 h4 /=. inv_ctx_insertion.
constructor=>//.
+ by rewrite closed_subst.
+ rewrite closed_subst=>//.
apply closed_has_ty_weak=>//.
by apply closed_has_ty_contr with (ctx_insertion n Γ U).
Qed.
Lemma has_type_beta s t U V Γ a b :
closed t ->
[ U .: Γ, a, b ⊢ s :- V ] ->
[ empty_ctx, a, b ⊢ t :- U ] ->
[ Γ, a, b ⊢ s.[t/] :- V ].
Proof.
move=> *.
rewrite -subst_var_0.
apply has_type_beta_gen with U=>//.
by rewrite ctx_insertion0.
Qed.
Lemma has_type_fall m s Γ a :
[ Γ, a + m, a + m ⊢ s :- Void ] ->
[ Γ, a, a ⊢ fall m s :- Void ].
Proof.
elim: m a=> [|? ih] ? /= h.
- by rewrite addn0 in h.
- apply ty_tall, ih=>//.
by rewrite addSnnS.
Qed.
[ Γ, 1, 1 ⊢ s :- U ] -> [ Γ, 0, 0 ⊢ s :- U ].
Proof.
move=> h.
apply has_type_swap_a with 1=>//.
by apply has_type_lower_b with 1.
Qed.
Lemma has_type_hsubst1 s Γ U T :
[ Γ, 1, 1 ⊢ s :- U ] -> [ Γ, 0, 0 ⊢ s.|[T/] :- U ].
Proof.
move=> h.
apply has_type_swap_a with 1=>//.
have->: (T .: ids : var -> term) = upn 0 (T .: ids) by rewrite upn0.
apply has_type_hsubst_upn.
by apply has_type_lower_b with 1.
Qed.
Corollary has_type_lower_b0 s Γ a b U :
[ Γ, a, b ⊢ s :- U ] ->
[ Γ, a, 0 ⊢ s :- U ].
Proof.
move=> h.
by apply has_type_lower_b with b.
Qed.
Lemma has_type_beta_gen Γ W U n t s a b :
closed t ->
[ empty_ctx, a, b ⊢ t :- U ] ->
[ ctx_insertion n Γ U, a, b ⊢ s :- W ] ->
[ Γ, a, b ⊢ s.[t//n] :- W ].
Proof.
elim: s Γ W U n t a b;
try (by move=>*; inv_ctx_insertion; econstructor; eauto).
- move=> x Γ W U n t > ?? h2 /=.
rewrite /subst_var. inv h2. rewrite /ctx_insertion.
case (lt_eq_lt_dec x n) => [[]|] xn /=.
+ constructor.
by rewrite ifT; [|lia].
+ subst.
have->: n < n = false by lia.
have->: eqn n n = true by lia.
by apply closed_has_ty_weak.
+ constructor.
rewrite !ifF; try by lia.
by f_equal; lia.
- move=> s h1 Z Γ W U n u > ? h3 h4 /=.
inv h4.
rewrite upn1 subst_var_lemma.
have->: u.[ren (+1)] = u.
{ have->: ren (+1) = upn 0 (ren (+1)) by [].
by apply fv_unaffected_lift. }
rewrite addn1.
constructor.
rewrite shift_ctx_insertion in H2.
by apply (h1 _ _ _ _ u) in H2.
- move=> s h1 Γ W U n u a b ? h3 h4 /=. inv_ctx_insertion.
rewrite subst_var_hsubst.
constructor.
apply h1 with U=>//.
+ by apply closed_unaffectedh.
+ rewrite -(addn1 a) -(addn1 b).
by apply has_type_hshift.
- move=> s h1 Γ W U n u a b ? h3 h4 /=. inv_ctx_insertion.
rewrite subst_var_hsubst.
constructor=>//.
apply h1 with U=>//.
+ by apply closed_unaffectedh.
+ rewrite -(addn1 a) -(addn1 b).
by apply has_type_hshift.
- move=> s h1 Γ W U n u a b ? h3 h4 /=. inv_ctx_insertion.
constructor=>//.
+ by rewrite closed_subst.
+ rewrite closed_subst=>//.
apply closed_has_ty_weak=>//.
by apply closed_has_ty_contr with (ctx_insertion n Γ U).
Qed.
Lemma has_type_beta s t U V Γ a b :
closed t ->
[ U .: Γ, a, b ⊢ s :- V ] ->
[ empty_ctx, a, b ⊢ t :- U ] ->
[ Γ, a, b ⊢ s.[t/] :- V ].
Proof.
move=> *.
rewrite -subst_var_0.
apply has_type_beta_gen with U=>//.
by rewrite ctx_insertion0.
Qed.
Lemma has_type_fall m s Γ a :
[ Γ, a + m, a + m ⊢ s :- Void ] ->
[ Γ, a, a ⊢ fall m s :- Void ].
Proof.
elim: m a=> [|? ih] ? /= h.
- by rewrite addn0 in h.
- apply ty_tall, ih=>//.
by rewrite addSnnS.
Qed.