Library Lambda.JRussell.Substitution


Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.LiftSubst.

Require
 Import
 Lambda.Env.

Require
 Import
 Lambda.JRussell.Types.

Require
 Import
 Lambda.JRussell.Coercion.







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
 ind_sub_weak : ∀ g
 (d
 : term) t
, g
 |-= d
 : t
 →

   (∀ e
 u
 (U
 : term), e
 |-= u
 : U
 →

   ∀ f
 n
, sub_in_env d
 t
 n
 e
 f
 → trunc _
 n
 f
 g
 → 

   f
 |-= (subst_rec d
 u
 n
) : (subst_rec d
 U
 n
)) ∧

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

   ∀ f
 n
, sub_in_env d
 t
 n
 e
 f
 → trunc _
 n
 f
 g
 → 

   f
 |-= (subst_rec d
 T
 n
) >> (subst_rec d
 U
 n
) : s
) ∧

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

   ∀ f
 n
, sub_in_env d
 t
 n
 e
 f
 → trunc _
 n
 f
 g
 → 

   f
 |-= (subst_rec d
 U
 n
) = (subst_rec d
 V
 n
) : (subst_rec d
 T
 n
)).




Lemma
 typ_sub_weak : ∀ g
 (d
 : term) t
, g
 |-= d
 : t
 →

   ∀ e
 u
 (U
 : term), e
 |-= u
 : U
 →

   ∀ f
 n
, sub_in_env d
 t
 n
 e
 f
 → trunc _
 n
 f
 g
 → 

   f
 |-= (subst_rec d
 u
 n
) : (subst_rec d
 U
 n
).




Lemma
 coerce_sub_weak : ∀ g
 (d
 : term) t
, g
 |-= d
 : t
 →

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

   ∀ f
 n
, sub_in_env d
 t
 n
 e
 f
 → trunc _
 n
 f
 g
 → 

   f
 |-= (subst_rec d
 T
 n
) >> (subst_rec d
 U
 n
) : s
.




Lemma
 jeq_sub_weak : ∀ g
 (d
 : term) t
, g
 |-= d
 : t
 →

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

   ∀ f
 n
, sub_in_env d
 t
 n
 e
 f
 → trunc _
 n
 f
 g
 → 

   f
 |-= (subst_rec d
 U
 n
) = (subst_rec d
 V
 n
) : (subst_rec d
 T
 n
).




Theorem
 substitution : ∀ e
 t
 u
 U
, (t
 :: e
) |-= u
 : U
 →

  ∀ d
, e
 |-= d
 : t
 → e
 |-= (subst d
 u
) : (subst d
 U
).




Theorem
 substitution_coerce : ∀ e
 t
 T
 (U
 : term) s
,

  (t
 :: e
) |-= T
 >> U
 : s
 →

  ∀ d
, e
 |-= d
 : t
 → e
 |-= (subst d
 T
) >> (subst d
 U
) : s
.




Theorem
 substitution_jeq : ∀ e
 t
 U
 V
 T
,

  (t
 :: e
) |-= U
 = V
 : T
 →

  ∀ d
, e
 |-= d
 : t
 → e
 |-= (subst d
 U
) = (subst d
 V
) : subst d
 T
.




Hint
 Resolve
 substitution substitution_coerce substitution_jeq : coc
.