Library Lambda.Russell.Types


Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.LiftSubst.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.Conv.

Require
 Import
 Lambda.Env.







Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

Implicit
 Types
 A
 B
 M
 N
 T
 t
 u
 v
 : term.




Reserved Notation
 "G |-- T = U : s" (at
 level
 70, T
, U
, s
 at
 next
 level
).

Reserved Notation
 "G |-- T >> U : s" (at
 level
 70, T
, U
, s
 at
 next
 level
).

Reserved Notation
 "G |-- T : U" (at
 level
 70, T
, U
 at
 next
 level
).




Definition
 sum_sort s1
 s2
 s3
 :=

  (s1
 = set ∧ s2
 = set ∧ s3
 = set) ∨

  (s1
 = prop ∧ s2
 = prop ∧ s3
 = prop).




Inductive
 coerce : env → term → term → sort → Prop
 :=

  | coerce_refl : ∀ e
 A
 s
, e
 |-- A
 : Srt s
 → e
 |-- A
 >> A
 : s




  | coerce_prod : ∀ e
 A
 B
 A'
 B'
,

  ∀ s
, e
 |-- A'
 >> A
 : s
 →

   e
 |-- A'
 : Srt s
 → e
 |-- A
 : Srt s
 →

  ∀ s'
, (A'
 :: e
) |-- B
 >> B'
 : s'
 → 

   A
 :: e
 |-- B
 : Srt s'
 → A'
 :: e
 |-- B'
 : Srt s'
 →

  e
 |-- (Prod A
 B
) >> (Prod A'
 B'
) : s'


  

  | coerce_sum : ∀ e
 A
 B
 A'
 B'
,

  ∀ s
, e
 |-- A
 >> A'
 : s
 → 

   e
 |-- A'
 : Srt s
 → e
 |-- A
 : Srt s
 →

  ∀ s'
, (A
 :: e
) |-- B
 >> B'
 : s'
 →

   A
 :: e
 |-- B
 : Srt s'
 → A'
 :: e
 |-- B'
 : Srt s'
 →

  ∀ s''
, sum_sort s
 s'
 s''
 → sum_sort s
 s'
 s''
 →

  e
 |-- (Sum A
 B
) >> (Sum A'
 B'
) : s''




  | coerce_sub_l : ∀ e
 U
 P
 U'
, 

  e
 |-- U
 >> U'
 : set →

   U
 :: e
 |-- P
 : Srt prop →

  e
 |-- Subset U
 P
 >> U'
 : set



  | coerce_sub_r : ∀ e
 U
 U'
 P
,

  e
 |-- U
 >> U'
 : set → 

   U'
 :: e
 |-- P
 : Srt prop →

  e
 |-- U
 >> (Subset U'
 P
) : set



  | coerce_conv : ∀ e
 A
 B
 C
 D
 s
,

  e
 |-- A
 : Srt s
 → e
 |-- B
 : Srt s
 → e
 |-- C
 : Srt s
 → e
 |-- D
 : Srt s
 →

  conv A
 B
 → e
 |-- B
 >> C
 : s
 → conv C
 D
 → e
 |-- A
 >> D
 : s




where
 "G |-- T >> U : s" := (coerce G
 T
 U
 s
)



with
 wf
 : env → Prop
 :=

  | wf_nil : wf
 nil

  | wf_var : ∀ e
 T
 s
, e
 |-- T
 : (Srt s
) → wf
 (T
 :: e
)



with
 typ : env → term → term → Prop
 :=

  | type_prop : ∀ e
, wf
 e
 → e
 |-- (Srt prop) : (Srt kind)

  | type_set : ∀ e
, wf
 e
 → e
 |-- (Srt set) : (Srt kind)	

  | type_var : 

      ∀ e
, wf
 e
 → ∀ n
 T
, item_lift T
 e
 n
 → e
 |-- (Ref n
) : T


  | type_abs :

      ∀ e
 T
 s1
,

      e
 |-- T
 : (Srt s1
) →

      ∀ M
 (U
 : term) s2
,

      (T
 :: e
) |-- U
 : (Srt s2
) →

      (T
 :: e
) |-- M
 : U
 → 

      e
 |-- (Abs T
 M
) : (Prod T
 U
)

  | type_app :

      ∀ e
 v
 (V
 : term), e
 |-- v
 : V
 →

      ∀ u
 (Ur
 : term), e
 |-- u
 : (Prod V
 Ur
) → 

      e
 |-- (App u
 v
) : (subst v
 Ur
)	



  | type_pair :

    ∀ e
 (U
 : term) s1
, e
 |-- U
 : (Srt s1
) →

    ∀ u
, e
 |-- u
 : U
 →

    ∀ V
 s2
, (U
 :: e
) |-- V
 : (Srt s2
) →

    ∀ v
, e
 |-- v
 : (subst u
 V
) → 

    ∀ s3
, sum_sort s1
 s2
 s3
 →

    e
 |-- (Pair (Sum U
 V
) u
 v
) : (Sum U
 V
)



  | type_prod :

      ∀ e
 T
 s1
,

      e
 |-- T
 : (Srt s1
) →

      ∀ (U
 : term) s2
,

      (T
 :: e
) |-- U
 : (Srt s2
) → 

      e
 |-- (Prod T
 U
) : (Srt s2
)



  | type_sum :

      ∀ e
 T
 s1
,

      e
 |-- T
 : (Srt s1
) →

      ∀ (U
 : term) s2
,

      (T
 :: e
) |-- U
 : (Srt s2
) → 

      ∀ s3
, sum_sort s1
 s2
 s3
 →

      e
 |-- (Sum T
 U
) : Srt s3




  | type_subset : 

      ∀ e
 T
, e
 |-- T
 : (Srt set) →

      ∀ (U
 : term), (T
 :: e
) |-- U
 : (Srt prop) → 

      e
 |-- (Subset T
 U
) : (Srt set)



  | type_pi1 :

      ∀ e
 t
 U
 V
, e
 |-- t
 : (Sum U
 V
) → 

      e
 |-- (Pi1 t
) : U




  | type_pi2 :

      ∀ e
 t
 U
 V
, e
 |-- t
 : (Sum U
 V
) → 

      e
 |-- (Pi2 t
) : (subst (Pi1 t
) V
)



  | type_conv :

      ∀ e
 t
 (U
 V
 : term),

      e
 |-- t
 : U
 → 

      ∀ s
, e
 |-- V
 : (Srt s
) → e
 |-- U
 : (Srt s
) → 

      e
 |-- U
 >> V
 : s
 → 

      e
 |-- t
 : V




where
 "G |-- T : U" :=  (typ G
 T
 U
).




Hint
 Resolve
 coerce_refl coerce_conv coerce_prod coerce_sum coerce_sub_l coerce_sub_r : coc
.

Hint
 Resolve
 type_pi1 type_pi2 type_pair type_prop type_set type_var: coc
.

Hint
 Resolve
 wf_nil : coc
.




Scheme
 typ_dep
 := Induction
 for
 typ
 Sort
 Prop
.




Scheme
 typ_wf_mut
 := Induction
 for
 typ
 Sort
 Prop


with
 wf_typ_mut
 := Induction
 for
 wf
 Sort
 Prop
.




Scheme
 typ_coerce_mut
 := Induction
 for
 typ
 Sort
 Prop


with
 coerce_typ_mut
 := Induction
 for
 coerce
 Sort
 Prop
.




Scheme
 typ_coerce_wf_mut
 := Induction
 for
 typ
 Sort
 Prop


with
 coerce_typ_wf_mut
 := Induction
 for
 coerce
 Sort
 Prop


with
 wf_typ_coerce_mut
 := Induction
 for
 wf
 Sort
 Prop
.










  Lemma
 type_prop_set :

   ∀ s
, is_prop s
 → ∀ e
, wf
 e
 → typ e
 (Srt s
) (Srt kind).




Lemma
 typ_free_db : ∀ e
 t
 T
, typ e
 t
 T
 → free_db (length e
) t
.




Lemma
 typ_wf : ∀ e
 t
 T
, e
 |-- t
 : T
 → wf
 e
.




  Lemma
 wf_sort :

   ∀ n
 e
 f
,

   trunc _
 (S n
) e
 f
 →

   wf
 e
 → ∀ t
, item _
 t
 e
 n
 → ∃ s
 : sort, f
 |-- t
 : (Srt s
).




Lemma
 typ_sort_aux : ∀ G
 t
 T
, G
 |-- t
 : T
 → 

  ∀ s
, t
 = (Srt s
) → is_prop s
 ∧ T
 = (Srt kind).




Lemma
 typ_sort : ∀ G
 s
 T
, G
 |-- (Srt s
) : T
 → is_prop s
 ∧ T
 = (Srt kind).




Lemma
 typ_not_kind : ∀ G
 t
 T
, G
 |-- t
 : T
 → t
 ≠ Srt kind.




Hint
 Resolve
 typ_not_kind typ_wf : coc
.




Lemma
 coerce_sort : ∀ G
 T
 U
 s
, 

  G
 |-- T
 >> U
 : s
 → (G
 |-- T
 : Srt s
 ∧ G
 |-- U
 : Srt s
).




Lemma
 coerce_sort_l : ∀ G
 T
 U
 s
, 

  G
 |-- T
 >> U
 : s
 → G
 |-- T
 : Srt s
.




Lemma
 coerce_sort_r : ∀ G
 T
 U
 s
, 

  G
 |-- T
 >> U
 : s
 → G
 |-- U
 : Srt s
.




Lemma
 coerce_prop_prop : ∀ e
, wf
 e
 → e
 |-- Srt prop >> Srt prop : kind.




Lemma
 coerce_set_set : ∀ e
, wf
 e
 → e
 |-- Srt set >> Srt set : kind.




Lemma
 coerce_is_prop : ∀ e
, wf
 e
 → ∀ s
, is_prop s
 → e
 |-- Srt s
 >> Srt s
 : kind.




Lemma
 conv_coerce : ∀ e
 T
 T'
 s
, e
 |-- T
 : Srt s
 → e
 |-- T'
 : Srt s
 → conv T
 T'
 →

  e
 |-- T
 >> T'
 : s
.




Hint
 Resolve
 coerce_sort_l coerce_sort_r coerce_prop_prop coerce_set_set coerce_is_prop conv_coerce : coc
.