47 lines
805 B
Coq
47 lines
805 B
Coq
|
From Coq Require Import Lists.List.
|
||
|
|
Require Import Atom.
|
||
|
|
Require Import Environment.
|
||
|
|
Require Import Metatheory.
|
||
|
|
Require Import debruijn.
|
||
|
|
Require Import subtype.
|
||
|
|
Require Import env.
|
||
|
|
Require Import morph.
|
||
|
|
Require Import typing.
|
||
|
|
|
||
|
|
|
||
|
|
Lemma type_lc_sub : forall τ1 τ2,
|
||
|
|
type_lc τ1 ->
|
||
|
|
τ1 :<= τ2 ->
|
||
|
|
type_lc τ2
|
||
|
|
.
|
||
|
|
Proof.
|
||
|
|
intros.
|
||
|
|
Admitted.
|
||
|
|
|
||
|
|
Lemma type_morph_lc_inv : forall τ1 τ2,
|
||
|
|
type_lc (ty_morph τ1 τ2) ->
|
||
|
|
type_lc τ1 /\ type_lc τ2
|
||
|
|
.
|
||
|
|
Proof.
|
||
|
|
intros.
|
||
|
|
inversion H.
|
||
|
|
auto.
|
||
|
|
Qed.
|
||
|
|
|
||
|
|
Lemma typing_regular_expr_lc : forall Γ e τ,
|
||
|
|
(Γ |- e \is τ) ->
|
||
|
|
expr_lc e.
|
||
|
|
Proof.
|
||
|
|
intros Γ e τ H.
|
||
|
|
induction H; eauto.
|
||
|
|
- apply Elc_Var.
|
||
|
|
- apply Elc_Let with (L:=L).
|
||
|
|
apply IHtyping.
|
||
|
|
Admitted.
|
||
|
|
|
||
|
|
Lemma typing_regular_type_lc : forall Γ e τ,
|
||
|
|
(Γ |- e \is τ) ->
|
||
|
|
type_lc τ.
|
||
|
|
Proof.
|
||
|
|
Admitted.
|