Library Lambda.JRussell.Thinning


Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.LiftSubst.

Require
 Import
 Lambda.Env.

Require
 Import
 Lambda.Conv.

Require
 Import
 Lambda.JRussell.Types.







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.




Lemma
 type_weak_lift_rec : ∀ e
 t
 T
, e
 |-= t
 : T
 → ∀ A
 s
, e
 |-= A
 : Srt s
 →

  (A
 :: e
) |-= lift_rec 1 t
 0 : lift_rec 1 T
 0.




Lemma
 coerce_weak_lift_rec : ∀ e
 T
 U
 s
, e
 |-= T
 >> U
 : s
 → ∀ A
 s'
, e
 |-= A
 : Srt s'
 →

  (A
 :: e
) |-= lift_rec 1 T
 0 >> lift_rec 1 U
 0 : s
.




Lemma
 jeq_weak_lift_rec : ∀ e
 t
 u
 T
, e
 |-= t
 = u
 : T
 → ∀ A
 s
, e
 |-= A
 : Srt s
 →

  (A
 :: e
) |-= lift_rec 1 t
 0 = lift_rec 1 u
 0 : lift_rec 1 T
 0.




Hint
 Resolve
 type_weak_lift_rec : coc
.




Lemma
 ind_weak_weak : ∀ g
 A
 s
, g
 |-= A
 : Srt s
 →

  (∀ e
 t
 T
, e
 |-= t
 : T
 →

   ∀ n
 f
, ins_in_env A
 n
 e
 f
 →

   trunc _
 n
 e
 g
 →

   f
 |-= (lift_rec 1 t
 n
) : (lift_rec 1 T
 n
)) ∧

 (∀ e
 T
 U
 s
, e
 |-= T
 >> U
 : s
 →

  ∀ n
 f
, ins_in_env A
 n
 e
 f
 →

  trunc _
 n
 e
 g
 →

  f
 |-= (lift_rec 1 T
 n
) >> (lift_rec 1 U
 n
) : s
) ∧

 (∀ e
 U
 V
 T
, e
 |-= U
 = V
 : T
 →

  ∀ n
 f
, ins_in_env A
 n
 e
 f
 →

  trunc _
 n
 e
 g
 →

  f
 |-= (lift_rec 1 U
 n
) = (lift_rec 1 V
 n
) : (lift_rec 1 T
 n
)).

coercion

Judgemental equality





Lemma
 type_weak_weak : ∀ g
 A
 s
, g
 |-= A
 : Srt s
 →

  ∀ e
 t
 T
, e
 |-= t
 : T
 →

   ∀ n
 f
, ins_in_env A
 n
 e
 f
 →

   trunc _
 n
 e
 g
 →

   f
 |-= (lift_rec 1 t
 n
) : (lift_rec 1 T
 n
).




Lemma
 coerce_weak_weak : ∀ g
 A
 s
, g
 |-= A
 : Srt s
 →

  ∀ e
 T
 U
 s
, e
 |-= T
 >> U
 : s
 →

  ∀ n
 f
, ins_in_env A
 n
 e
 f
 →

  trunc _
 n
 e
 g
 →

  f
 |-= (lift_rec 1 T
 n
) >> (lift_rec 1 U
 n
) : s
.




Lemma
 jeq_weak_weak : ∀ g
 A
 s
, g
 |-= A
 : Srt s
 →

  ∀ e
 U
 V
 T
, e
 |-= U
 = V
 : T
 →

  ∀ n
 f
, ins_in_env A
 n
 e
 f
 →

  trunc _
 n
 e
 g
 →

  f
 |-= (lift_rec 1 U
 n
) = (lift_rec 1 V
 n
) : (lift_rec 1 T
 n
).




Lemma
 thinning_n :

   ∀ n
 e
 f
,

   trunc _
 n
 e
 f
 →

   consistent e
 →

   ∀ t
 T
, typ f
 t
 T
 → typ e
 (lift n
 t
) (lift n
 T
).




Lemma
 thinning_n_coerce : ∀ n
 e
 f
, trunc _
 n
 e
 f
 → 

  ∀ T
 U
 s
, f
 |-= T
 >> U
 : s
 → consistent e
 → e
 |-= (lift n
 T
) >> (lift n
 U
) : s
.




Hint
 Resolve
 thinning_n thinning_n_coerce : coc
.




Lemma
 item_ref_lift :

 ∀ n
 e
 t
, item _
 t
 e
 n
 → consistent e
 → e
 |-= Ref n
 : lift (S n
) t
.