Library Lambda.JRussell.GenerationCoerce


Require
 Import
 Lambda.Tactics.




Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.Conv.

Require
 Import
 Lambda.Conv_Dec.

Require
 Import
 Lambda.LiftSubst.

Require
 Import
 Lambda.Env.

Require
 Import
 Lambda.JRussell.Types.

Require
 Import
 Lambda.JRussell.Thinning.

Require
 Import
 Lambda.JRussell.Substitution.

Require
 Import
 Lambda.JRussell.Coercion.

Require
 Import
 Lambda.JRussell.GenerationNotKind.

Require
 Import
 Lambda.JRussell.Validity.




Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

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

Implicit
 Types
 e
 f
 g
 : env.







Fixpoint
 type_range (t
 : term) : term :=

  match
 t
 with


  | Prod U
 V
 ⇒ type_range V


  | _
 ⇒ t


  end
.




Lemma
 subst_to_sort : ∀ t
 t'
 s
, subst t
 t'
 = Srt s
 → t
 ≠ Srt s
 →

  t'
 = Srt s
.




Fixpoint
 is_low t
 : Prop
 :=

  match
 t
 with
 

  | Prod T
 U
 ⇒ is_low U


  | Srt s
 ⇒ is_prop s


  | _
 ⇒ False

  end
.




Lemma
 red_sort_eq : ∀ s
 t
, red (Srt s
) t
 → t
 = Srt s
.




Lemma
 is_low_lift : ∀ t
, is_low t
 → ∀ n
 k
, is_low (lift_rec n
 t
 k
).




Lemma
 kind_is_prod_aux : ∀ G
 t
 T
, G
 |-= t
 : T
 → 

  T
 = Srt kind → is_low t
.




Lemma
 type_kind_range : ∀ G
 t
, G
 |-= t
 : Srt kind → is_low t
.




Lemma
 sort_conv_eq : ∀ G
 T
 s
, G
 |-= T
 : Srt kind → conv T
 (Srt s
) → T
 = Srt s
.




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




Lemma
 coerce_sort_l_in_kind : ∀ G
 A
 s
 s'
, G
 |-= Srt s
 >> A
 : s'
 → s'
 = kind.




Lemma
 coerce_sort_r_in_kind : ∀ G
 A
 s
 s'
, G
 |-= A
 >> Srt s
 : s'
 → s'
 = kind.




Lemma
 coerce_not_kind_l : ∀ G
 T
 s
, ¬ G
 |-= Srt kind >> T
 : s
.




Lemma
 coerce_not_kind_r : ∀ G
 T
 s
, ¬ G
 |-= T
 >> Srt kind : s
.




Lemma
 eq_conv : ∀ e
 t
 u
 T
, e
 |-= t
 = u
 : T
 → conv t
 u
.




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




Lemma
 coerce_propset_aux : ∀ G
 A
 B
 s'
, G
 |-= A
 >> B
 : s'
 →

  (∀ s
, A
 = Srt s
 →  s'
 = kind → B
 = Srt s
) ∧

  (∀ s
, B
 = Srt s
 →  s'
 = kind → A
 = Srt s
).




Lemma
 coerce_propset_l :  ∀ G
 s
 A
 s'
, G
 |-= Srt s
 >> A
 : s'
 →

  A
 = Srt s
.




Lemma
 coerce_propset_r :  ∀ G
 s
 A
 s'
, G
 |-= A
 >> Srt s
 : s'
 →

  A
 = Srt s
.




Fixpoint
 no_sort t
 : Prop
 :=

  match
 t
 with
 

  | Prod T
 U
 ⇒ no_sort U


  | Srt s
 ⇒ False

  | _
 ⇒ True

  end
.




Lemma
 no_sort_lift : ∀ t
, no_sort t
 → ∀ n
 k
, no_sort (lift_rec n
 t
 k
).




Fixpoint
 is_low_full t
 : Prop
 :=

  match
 t
 with
 

  | Prod T
 U
 ⇒ is_low_full U


  | Srt s
 ⇒ is_prop s


  | _
 ⇒ False

  end
.




Lemma
 is_low_full_lift : ∀ t
, is_low_full t
 → ∀ n
 k
, is_low_full (lift_rec n
 t
 k
).




Lemma
 sort_of_kinded_aux : ∀ G
 t
 T
, G
 |-= t
 : T
 → 

  ∀ s
, T
 = Srt s
 → 

  (s
 = kind → is_low_full t
) ∧ (is_prop s
 → no_sort t
).




Lemma
 sorts_of_sorted : ∀ G
 t
 s
, G
 |-= t
 : Srt s
 → 

  (s
 = kind → is_low_full t
) ∧ (is_prop s
 → no_sort t
).




Lemma
 sort_of_kinded : ∀ G
 t
, G
 |-= t
 : Srt kind → 

  is_low_full t
.




Lemma
 sort_of_propset : ∀ G
 t
 s
, G
 |-= t
 : Srt s
 → 

  is_prop s
 → no_sort t
.