Library Types


Require
 Export
 Conv.

Require
 Export
 Env
.




Section
 Typage.




  Inductive
 wf
 : env
 -> Prop
 :=

    | wf_nil : wf
 nil

    | wf_var : forall
 e
 T
 s
, typ e
 T
 (Srt s
) -> wf
 (T
 :: e
)

  with
 typ : env
 -> term -> term -> Prop
 :=

    | type_prop :

        forall
 e
,

        wf
 e
 ->

        typ e
 (Srt prop) (Srt kind)

    | type_var :

        forall
 e
 v
 t
,

        wf
 e
 ->

        item_lift
 t
 e
 v
 ->

        typ e
 (Ref v
) t


    | type_abs :

        forall
 e
 T
 M
 U
 s1
 s2
,

        typ e
 T
 (Srt s1
) ->

        typ (T
 :: e
) U
 (Srt s2
) ->

        typ (T
 :: e
) M
 U
 ->

        typ e
 (Abs T
 M
) (Prod T
 U
)

    | type_app :

        forall
 e
 u
 v
 V
 Ur
,

        typ e
 v
 V
 ->

        typ e
 u
 (Prod V
 Ur
) ->

        typ e
 (App u
 v
) (subst v
 Ur
)

    | type_prod :

        forall
 e
 T
 U
 s1
 s2
,

        typ e
 T
 (Srt s1
) ->

        typ (T
 :: e
) U
 (Srt s2
) ->

        typ e
 (Prod T
 U
) (Srt s2
)

    | type_conv :

        forall
 e
 t
 U
 V
 s
,

        typ e
 t
 U
 ->

        conv U
 V
 ->

        typ e
 V
 (Srt s
) ->

        typ e
 t
 V
.




  Hint
 Resolve
 wf_nil type_prop type_var: coc
.




Scheme
 typ_mind
 := Minimality
 for
 typ
 Sort
 Prop


  with
 wf_mind
 := Minimality
 for
 wf
 Sort
 Prop
.




  Lemma
 typ_wf : forall
 e
 t
 T
, typ e
 t
 T
 -> wf
 e
.

simple
 induction
 1; auto
 with
 coc
.

Qed
.




  Hint
 Resolve
 typ_wf: coc
.




  Lemma
 wf_sort :

   forall
 n
 e
 f
 t
,

   trunc (S n
) e
 f
 -> wf
 e
 -> item t
 e
 n
 -> exists
 s
, typ f
 t
 (Srt s
).

simple
 induction
 n
.

do
 4 intro
.

inversion_clear
 H
.

inversion_clear
 H0
.

intros
.

inversion_clear
 H0
.

inversion_clear
 H
.

eauto
 with
 coc
.




do
 6 intro
.

inversion_clear
 H0
.

intros
.

inversion_clear
 H2
.

inversion_clear
 H0
.

elim
 H
 with
 e0
 f
 t
; intros
; eauto
 with
 coc
.

Qed
.




  Definition
 inv_type (P
 : Prop
) e
 t
 T
 :=

    match
 t
 with


    | Srt prop => conv T
 (Srt kind) -> P


    | Srt kind => True

    | Ref n
 => forall
 x
, item x
 e
 n
 -> conv T
 (lift (S n
) x
) -> P


    | Abs A
 M
 =>

        forall
 s1
 s2
 U
,

        typ e
 A
 (Srt s1
) ->

        typ (A
 :: e
) M
 U
 -> typ (A
 :: e
) U
 (Srt s2
) -> conv T
 (Prod A
 U
) -> P


    | App u
 v
 =>

        forall
 Ur
 V
,

        typ e
 v
 V
 -> typ e
 u
 (Prod V
 Ur
) -> conv T
 (subst v
 Ur
) -> P


    | Prod A
 B
 =>

        forall
 s1
 s2
,

        typ e
 A
 (Srt s1
) -> typ (A
 :: e
) B
 (Srt s2
) -> conv T
 (Srt s2
) -> P


    end
.




  Lemma
 inv_type_conv :

   forall
 P
 e
 t
 U
 V
, conv U
 V
 -> inv_type P
 e
 t
 U
 -> inv_type P
 e
 t
 V
.

do
 6 intro
.

cut
 (forall
 x
 : term, conv V
 x
 -> conv U
 x
).

intro
.

case
 t
; simpl
 in
 |- *; intros
.

generalize
 H1
.

elim
 s
; auto
 with
 coc
; intros
.




apply
 H1
 with
 x
; auto
 with
 coc
.




apply
 H1
 with
 s1
 s2
 U0
; auto
 with
 coc
.




apply
 H1
 with
 Ur
 V0
; auto
 with
 coc
.




apply
 H1
 with
 s1
 s2
; auto
 with
 coc
.




intros
.

apply
 trans_conv_conv with
 V
; auto
 with
 coc
.

Qed
.




  Theorem
 typ_inversion : forall
 P
 e
 t
 T
, typ e
 t
 T
 -> inv_type P
 e
 t
 T
 -> P
.

simple
 induction
 1; simpl
 in
 |- *; intros
.

auto
 with
 coc
.




elim
 H1
; intros
.

apply
 H2
 with
 x
; auto
 with
 coc
.

rewrite
 H3
; auto
 with
 coc
.




apply
 H6
 with
 s1
 s2
 U
; auto
 with
 coc
.




apply
 H4
 with
 Ur
 V
; auto
 with
 coc
.




apply
 H4
 with
 s1
 s2
; auto
 with
 coc
.




apply
 H1
.

apply
 inv_type_conv with
 V
; auto
 with
 coc
.

Qed
.




  Lemma
 inv_typ_kind : forall
 e
 t
, ~ typ e
 (Srt kind) t
.

red
 in
 |- *; intros
.

apply
 typ_inversion with
 e
 (Srt kind) t
; simpl
 in
 |- *; auto
 with
 coc
.

Qed
.




  Lemma
 inv_typ_prop : forall
 e
 T
, typ e
 (Srt prop) T
 -> conv T
 (Srt kind).

intros
.

apply
 typ_inversion with
 e
 (Srt prop) T
; simpl
 in
 |- *; auto
 with
 coc
.

Qed
.




  Lemma
 inv_typ_ref :

   forall
 (P
 : Prop
) e
 T
 n
,

   typ e
 (Ref n
) T
 ->

   (forall
 U
 : term, item U
 e
 n
 -> conv T
 (lift (S n
) U
) -> P
) -> P
.

intros
.

apply
 typ_inversion with
 e
 (Ref n
) T
; simpl
 in
 |- *; intros
; auto
 with
 coc
.

apply
 H0
 with
 x
; auto
 with
 coc
.

Qed
.




  Lemma
 inv_typ_abs :

   forall
 (P
 : Prop
) e
 A
 M
 U
,

   typ e
 (Abs A
 M
) U
 ->

   (forall
 s1
 s2
 T
,

    typ e
 A
 (Srt s1
) ->

    typ (A
 :: e
) M
 T
 -> typ (A
 :: e
) T
 (Srt s2
) -> conv (Prod A
 T
) U
 -> P
) ->

   P
.

intros
.

apply
 typ_inversion with
 e
 (Abs A
 M
) U
; simpl
 in
 |- *; auto
 with
 coc
; intros
.

apply
 H0
 with
 s1
 s2
 U0
; auto
 with
 coc
.

Qed
.




  Lemma
 inv_typ_app :

   forall
 (P
 : Prop
) e
 u
 v
 T
,

   typ e
 (App u
 v
) T
 ->

   (forall
 V
 Ur
, typ e
 u
 (Prod V
 Ur
) -> typ e
 v
 V
 -> conv T
 (subst v
 Ur
) -> P
) ->

   P
.

intros
.

apply
 typ_inversion with
 e
 (App u
 v
) T
; simpl
 in
 |- *; auto
 with
 coc
; intros
.

apply
 H0
 with
 V
 Ur
; auto
 with
 coc
.

Qed
.




  Lemma
 inv_typ_prod :

   forall
 (P
 : Prop
) e
 T
 U
 s
,

   typ e
 (Prod T
 U
) s
 ->

   (forall
 s1
 s2
,

    typ e
 T
 (Srt s1
) -> typ (T
 :: e
) U
 (Srt s2
) -> conv (Srt s2
) s
 -> P
) -> P
.

intros
.

apply
 typ_inversion with
 e
 (Prod T
 U
) s
; simpl
 in
 |- *; auto
 with
 coc
; intros
.

apply
 H0
 with
 s1
 s2
; auto
 with
 coc
.

Qed
.




  Lemma
 typ_mem_kind : forall
 e
 t
 T
, mem_sort kind t
 -> ~ typ e
 t
 T
.

red
 in
 |- *; intros
.

apply
 typ_inversion with
 e
 t
 T
; auto
 with
 coc
.

generalize
 e
 T
.

clear
 H0
.

elim
 H
; simpl
 in
 |- *; auto
 with
 coc
; intros
.

apply
 typ_inversion with
 e0
 u
 (Srt s1
); auto
 with
 coc
.




apply
 typ_inversion with
 (u
 :: e0
) v
 (Srt s2
); auto
 with
 coc
.




apply
 typ_inversion with
 e0
 u
 (Srt s1
); auto
 with
 coc
.




apply
 typ_inversion with
 (u
 :: e0
) v
 U
; auto
 with
 coc
.




apply
 typ_inversion with
 e0
 u
 (Prod V
 Ur
); auto
 with
 coc
.




apply
 typ_inversion with
 e0
 v
 V
; auto
 with
 coc
.

Qed
.




  Lemma
 inv_typ_conv_kind : forall
 e
 t
 T
, conv t
 (Srt kind) -> ~ typ e
 t
 T
.

intros
.

apply
 typ_mem_kind.

apply
 red_sort_mem.

elim
 church_rosser with
 t
 (Srt kind); intros
; auto
 with
 coc
.

rewrite
 (red_normal (Srt kind) x
); auto
 with
 coc
.

red
 in
 |- *; red
 in
 |- *; intros
.

inversion_clear
 H2
.

Qed
.




  Lemma
 typ_weak_weak :

   forall
 A
 e
 t
 T
,

   typ e
 t
 T
 ->

   forall
 n
 f
,

   ins_in_env
 A
 n
 e
 f
 -> wf
 f
 -> typ f
 (lift_rec 1 t
 n
) (lift_rec 1 T
 n
).

simple
 induction
 1; simpl
 in
 |- *; intros
; auto
 with
 coc
.

elim
 (le_gt_dec n
 v
); intros
; apply
 type_var; auto
 with
 coc
.

apply
 ins_item_lift_ge
 with
 A
 e0
; auto
 with
 coc
.




apply
 ins_item_lift_lt
 with
 A
 e0
; auto
 with
 coc
.




cut
 (wf
 (lift_rec 1 T0
 n
 :: f
)).

intro
.

apply
 type_abs with
 s1
 s2
; auto
 with
 coc
.




apply
 wf_var with
 s1
; auto
 with
 coc
.




rewrite
 distr_lift_subst.

apply
 type_app with
 (lift_rec 1 V
 n
); auto
 with
 coc
.




cut
 (wf
 (lift_rec 1 T0
 n
 :: f
)).

intro
.

apply
 type_prod with
 s1
; auto
 with
 coc
.




apply
 wf_var with
 s1
; auto
 with
 coc
.




apply
 type_conv with
 (lift_rec 1 U
 n
) s
; auto
 with
 coc
.

Qed
.




  Theorem
 thinning :

   forall
 e
 t
 T
 A
,

   typ e
 t
 T
 -> wf
 (A
 :: e
) -> typ (A
 :: e
) (lift 1 t
) (lift 1 T
).

unfold
 lift
 in
 |- *.

intros
.

inversion_clear
 H0
.

apply
 typ_weak_weak with
 A
 e
; auto
 with
 coc
.

apply
 wf_var with
 s
; auto
 with
 coc
.

Qed
.




  Lemma
 thinning_n :

   forall
 n
 e
 f
 t
 T
,

   trunc n
 (e
:env) (f
:env) ->

   typ f
 t
 T
 -> wf
 e
 -> typ e
 (lift n
 t
) (lift n
 T
).

simple
 induction
 1.

intros
.

rewrite
 lift0.

rewrite
 lift0.

trivial
.




intros
.

rewrite
 simpl_lift; auto
 with
 coc
.

pattern
 (lift (S k
) T
) in
 |- *.

rewrite
 simpl_lift; auto
 with
 coc
.

apply
 thinning; auto
 with
 coc
.

apply
 H1
; trivial
.

inversion_clear
 H3
.

eauto
 with
 coc
.

Qed
.




  Lemma
 wf_sort_lift :

   forall
 n
 e
 t
, wf
 e
 -> item_lift
 t
 e
 n
 -> exists
 s
, typ e
 t
 (Srt s
).

simple
 induction
 n
.

simple
 destruct
 e
; intros
.

elim
 H0
; intros
.

inversion_clear
 H2
.




elim
 H0
; intros
.

rewrite
 H1
.

inversion_clear
 H2
.

inversion_clear
 H
.

exists
 s
.

replace
 (Srt s
) with
 (lift 1 (Srt s
)); auto
 with
 coc
.

apply
 thinning; auto
 with
 coc
.

apply
 wf_var with
 s
; auto
 with
 coc
.




intros
.

elim
 H1
; intros
.

rewrite
 H2
.

generalize
 H0
.

inversion_clear
 H3
; intros
.

rewrite
 simpl_lift; auto
 with
 coc
.

cut
 (wf
 l
); intros
.

elim
 H
 with
 l
 (lift (S n0
) x
); intros
; auto
 with
 coc
.

inversion_clear
 H3
.

exists
 x0
.

change
 (typ (y
 :: l
) (lift 1 (lift (S n0
) x
)) (lift 1 (Srt x0
))) in
 |- *.

apply
 thinning; auto
 with
 coc
.

apply
 wf_var with
 s
; auto
 with
 coc
.




exists
 x
; auto
 with
 coc
.




inversion_clear
 H3
.

eauto
 with
 coc
.

Qed
.




  Lemma
 typ_sub_weak :

   forall
 g
 d
 t
 e
 u
 U
,

   typ g
 d
 t
 ->

   typ e
 u
 U
 ->

   forall
 f
 n
,

   sub_in_env
 d
 t
 n
 e
 f
 ->

   wf
 f
 -> trunc n
 f
 g
 -> typ f
 (subst_rec d
 u
 n
) (subst_rec d
 U
 n
).

Proof
.

simple
 induction
 2; simpl
 in
 |- *; intros
; auto
 with
 coc
.

destruct
 (lt_eq_lt_dec n
 v
) as
 [[fvar
|eq_var]|bvar].

constructor
; trivial
.

apply
 sub_item_lift_sup
 with
 (1 := H3
) (2 := fvar
) (3 := H2
).




subst
 v
; rewrite
 sub_item_lift_eq
 with
 (1 := H3
) (2 := H2
).

apply
 thinning_n with
 g
; auto
 with
 coc
.




constructor
; trivial
.

apply
 nth_sub_inf
 with
 (1 := H3
); trivial
.




cut
 (wf
 (subst_rec d
 T
 n
 :: f
)); intros
.

apply
 type_abs with
 s1
 s2
; auto
 with
 coc
.




apply
 wf_var with
 s1
; auto
 with
 coc
.




rewrite
 distr_subst.

apply
 type_app with
 (subst_rec d
 V
 n
); auto
 with
 coc
.




cut
 (wf
 (subst_rec d
 T
 n
 :: f
)); intros
.

apply
 type_prod with
 s1
; auto
 with
 coc
.




apply
 wf_var with
 s1
; auto
 with
 coc
.




apply
 type_conv with
 (subst_rec d
 U0
 n
) s
; auto
 with
 coc
.

Qed
.




  Theorem
 substitution :

   forall
 e
 t
 u
 U
 d
,

   typ (t
 :: (e
:env)) u
 U
 -> typ e
 d
 t
 -> typ e
 (subst d
 u
) (subst d
 U
).

intros
.

unfold
 subst
 in
 |- *.

apply
 typ_sub_weak with
 e
 t
 (t
 :: e
); auto
 with
 coc
.

apply
 typ_wf with
 d
 t
; auto
 with
 coc
.

Qed
.




  Theorem
 typ_unique :

   forall
 e
 t
 T
, typ e
 t
 T
 -> forall
 U
, typ e
 t
 U
 -> conv T
 U
.

simple
 induction
 1; intros
.

apply
 sym_conv.

apply
 inv_typ_prop with
 e0
; auto
 with
 coc
.




apply
 inv_typ_ref with
 e0
 U
 v
; auto
 with
 coc
; intros
.

elim
 H1
; intros
.

rewrite
 H5
.

elim
 fun_item with
 (1 := H3
) (2 := H6
); auto
 with
 coc
.




apply
 inv_typ_abs with
 (1 := H6
); intros
.

apply
 trans_conv_conv with
 (Prod T0
 T1
); auto
 with
 coc
.




apply
 inv_typ_app with
 (1 := H4
); intros
.

apply
 trans_conv_conv with
 (subst v
 Ur0
); auto
 with
 coc
.

unfold
 subst
 in
 |- *; apply
 conv_conv_subst; auto
 with
 coc
.

apply
 inv_conv_prod_r with
 (1 := H3
 _
 H5
).




apply
 inv_typ_prod with
 (1 := H4
); intros
.

apply
 trans_conv_conv with
 (Srt s3
); auto
 with
 coc
.




apply
 trans_conv_conv with
 U
; auto
 with
 coc
.

Qed
.




  Theorem
 type_case :

   forall
 e
 t
 T
, typ e
 t
 T
 -> (exists
 s
, typ e
 T
 (Srt s
)) \/ T
 = Srt kind.

simple
 induction
 1; intros
; auto
 with
 coc
.

left
.

elim
 wf_sort_lift with
 (2 := H1
); trivial
; intros
.

exists
 x
; auto
 with
 coc
.




left
.

exists
 s2
.

apply
 type_prod with
 s1
; auto
 with
 coc
.




left
.

elim
 H3
; intros
.

elim
 H4
; intros
.

apply
 inv_typ_prod with
 (1 := H5
); intros
.

exists
 s2
.

replace
 (Srt s2
) with
 (subst v
 (Srt s2
)); auto
 with
 coc
.

apply
 substitution with
 V
; auto
 with
 coc
.




discriminate
 H4
.




case
 s2
; auto
 with
 coc
.

left
.

exists
 kind.

apply
 type_prop.

apply
 typ_wf with
 (1 := H0
).




left
.

exists
 s
; auto
 with
 coc
.

Qed
.




  Lemma
 type_kind_not_conv :

   forall
 e
 t
 T
, typ e
 t
 T
 -> typ e
 t
 (Srt kind) -> T
 = Srt kind.

intros
.

elim
 type_case with
 e
 t
 T
; intros
; auto
 with
 coc
.

elim
 H1
; intros
.

elim
 inv_typ_conv_kind with
 e
 T
 (Srt x
); auto
 with
 coc
.

apply
 typ_unique with
 e
 t
; trivial
.

Qed
.




  Lemma
 typ_red_env :

   forall
 e
 t
 T
, typ e
 t
 T
 ->

   forall
 f
, red1_in_env
 red1 e
 f
 -> wf
 f
 -> typ f
 t
 T
.

simple
 induction
 1; intros
.

auto
 with
 coc
.




elim
 red_item
 with
 (2 := H1
) (3 := H2
); auto
 with
 coc
; intros
.

inversion_clear
 H4
.

inversion_clear
 H6
.

elim
 H1
; intros
.

elim
 item_trunc with
 (1 := H8
); intros
.

elim
 wf_sort with
 (1 := H9
) (3 := H8
); eauto
; intros
.

apply
 type_conv with
 x
 x2
; auto
 with
 coc
.

rewrite
 H6
.

replace
 (Srt x2
) with
 (lift (S v
) (Srt x2
)); auto
 with
 coc
.

apply
 thinning_n with
 x1
; auto
 with
 coc
.




cut
 (wf
 (T0
 :: f
)); intros
.

apply
 type_abs with
 s1
 s2
; auto
 with
 coc
.




apply
 wf_var with
 s1
; auto
 with
 coc
.




apply
 type_app with
 V
; auto
 with
 coc
.




cut
 (wf
 (T0
 :: f
)); intros
.

apply
 type_prod with
 s1
; auto
 with
 coc
.




apply
 wf_var with
 s1
; auto
 with
 coc
.




apply
 type_conv with
 U
 s
; auto
 with
 coc
.

Qed
.




  Lemma
 subj_red : forall
 e
 t
 T
, typ e
 t
 T
 -> forall
 u
, red1 t
 u
 -> typ e
 u
 T
.

simple
 induction
 1; intros
.

inversion_clear
 H1
.




inversion_clear
 H2
.




inversion_clear
 H6
.

cut
 (wf
 (M'
 :: e0
)); intros
.

apply
 type_conv with
 (Prod M'
 U
) s2
; auto
 with
 coc
.

apply
 type_abs with
 s1
 s2
; auto
 with
 coc
.

apply
 typ_red_env with
 (T0
 :: e0
); auto
 with
 coc
.




apply
 typ_red_env with
 (T0
 :: e0
); auto
 with
 coc
.




apply
 type_prod with
 s1
; auto
 with
 coc
.




apply
 wf_var with
 s1
; auto
 with
 coc
.




apply
 type_abs with
 s1
 s2
; auto
 with
 coc
.




elim
 type_case with
 (1 := H2
); intros
.

inversion_clear
 H5
.

apply
 inv_typ_prod with
 (1 := H6
); intros
.

generalize
 H2
 H3
; clear
 H2
 H3
.

inversion_clear
 H4
; intros
.

apply
 inv_typ_abs with
 (1 := H2
); intros
.

apply
 type_conv with
 (subst v
 T1
) s2
; auto
 with
 coc
.

apply
 substitution with
 T0
; auto
 with
 coc
.

apply
 type_conv with
 V
 s0
; auto
 with
 coc
.

apply
 sym_conv.

apply
 inv_conv_prod_l with
 (1 := H11
).




unfold
 subst
 in
 |- *.

apply
 conv_conv_subst; auto
 with
 coc
.

apply
 inv_conv_prod_r with
 (1 := H11
); auto
 with
 coc
.




replace
 (Srt s2
) with
 (subst v
 (Srt s2
)); auto
 with
 coc
.

apply
 substitution with
 V
; auto
 with
 coc
.




apply
 type_app with
 V
; auto
 with
 coc
.




apply
 type_conv with
 (subst N2
 Ur
) s2
; auto
 with
 coc
.

apply
 type_app with
 V
; auto
 with
 coc
.




unfold
 subst
 in
 |- *.

apply
 conv_conv_subst; auto
 with
 coc
.




replace
 (Srt s2
) with
 (subst v
 (Srt s2
)); auto
 with
 coc
.

apply
 substitution with
 V
; auto
 with
 coc
.




discriminate
 H5
.




inversion_clear
 H4
.

apply
 type_prod with
 s1
; auto
 with
 coc
.

apply
 typ_red_env with
 (T0
 :: e0
); auto
 with
 coc
.

apply
 wf_var with
 s1
; auto
 with
 coc
.




apply
 type_prod with
 s1
; auto
 with
 coc
.




apply
 type_conv with
 U
 s
; auto
 with
 coc
.

Qed
.




  Theorem
 subject_reduction :

   forall
 e
 t
 u
, red t
 u
 -> forall
 T
, typ e
 t
 T
 -> typ e
 u
 T
.

simple
 induction
 1; intros
; auto
 with
 coc
.

apply
 subj_red with
 P
; intros
; auto
 with
 coc
.

Qed
.




  Lemma
 type_reduction : forall
 e
 t
 T
 U
, red T
 U
 -> typ e
 t
 T
 -> typ e
 t
 U
.

intros
.

elim
 type_case with
 (1 := H0
); intros
.

inversion_clear
 H1
.

apply
 type_conv with
 T
 x
; auto
 with
 coc
.

apply
 subject_reduction with
 T
; trivial
.




elim
 red_normal with
 (1 := H
); trivial
.

rewrite
 H1
.

red
 in
 |- *; red
 in
 |- *; intros
.

inversion_clear
 H2
.

Qed
.




  Lemma
 typ_conv_conv :

   forall
 e
 u
 U
 v
 V
, typ e
 u
 U
 -> typ e
 v
 V
 -> conv u
 v
 -> conv U
 V
.

intros
.

elim
 church_rosser with
 (1 := H1
); auto
 with
 coc
; intros
.

apply
 typ_unique with
 e
 x
.

apply
 subject_reduction with
 u
; trivial
.




apply
 subject_reduction with
 v
; trivial
.

Qed
.




End
 Typage.