Library Lambda.TPOSR.CoerceDepth


Require
 Import
 Lambda.Tactics.

Require
 Import
 Lambda.TPOSR.Terms.

Require
 Import
 Lambda.TPOSR.Reduction.

Require
 Import
 Lambda.TPOSR.Conv.

Require
 Import
 Lambda.TPOSR.LiftSubst.

Require
 Import
 Lambda.TPOSR.Env.




Require
 Import
 Lambda.TPOSR.Types.

Require
 Import
 Lambda.TPOSR.Thinning.

Require
 Import
 Lambda.TPOSR.Substitution.

Require
 Import
 Lambda.TPOSR.LeftReflexivity.

Require
 Import
 Lambda.TPOSR.RightReflexivity.







Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

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

Implicit
 Types
 e
 f
 g
 : lenv.




Require
 Export
 Coq.Arith.Max.




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




Inductive
 coerce_rc_depth : lenv -> lterm -> lterm -> sort -> nat -> Prop
 :=

  | coerce_rc_depth_refl : ∀ e
 A
 s
, e
 |-- A
 -> A
 : s
 -> e
 |-- A
 >-> A
 : s
 [0]



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

  ∀ s
 n
, e
 |-- A'
 >-> A
 : s
 [n
] ->

   e
 |-- A'
 -> A'
 : s
 -> e
 |-- A
 -> A
 : s
 ->

  ∀ s'
 m
, (A'
 :: e
) |-- B
 >-> B'
 : s'
 [m
] ->

   A
 :: e
 |-- B
 -> B
 : s'
 -> A'
 :: e
 |-- B'
 -> B'
 : s'
 ->

  e
 |-- (Prod_l A
 B
) >-> (Prod_l A'
 B'
) : s'
 [S (max n
 m
)]



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

  ∀ s
 n
, e
 |-- A
 >-> A'
 : s
 [n
] ->

   e
 |-- A'
 -> A'
 : s
 -> e
 |-- A
 -> A
 : s
 ->

  ∀ s'
 m
, (A
 :: e
) |-- B
 >-> B'
 : s'
 [m
] ->

   A
 :: e
 |-- B
 -> B
 : s'
 -> A'
 :: e
 |-- B'
 -> B'
 : s'
 ->

  ∀ s''
, sum_sort s
 s'
 s''
 ->

  e
 |-- (Sum_l A
 B
) >-> (Sum_l A'
 B'
) : s''
 [S (max n
 m
)]



  | coerce_rc_depth_sub_l : ∀ e
 U
 P
 U'
 n
,

  e
 |-- U
 >-> U'
 : set [n
] ->

   U
 :: e
 |-- P
 -> P
 : prop ->

  e
 |-- Subset_l U
 P
 >-> U'
 : set [S n
]



  | coerce_rc_depth_sub_r : ∀ e
 U
 U'
 P
 n
,

  e
 |-- U
 >-> U'
 : set [n
] ->

   U'
 :: e
 |-- P
 -> P
 : prop ->

  e
 |-- U
 >-> (Subset_l U'
 P
) : set [S n
]



  | coerce_rc_depth_conv_l : ∀ e
 A
 B
 C
 s
 n
,

  e
 |-- A
 -> A
 : s
 -> e
 |-- B
 -> B
 : s
 -> e
 |-- C
 -> C
 : s
 ->

  e
 |-- A
 ~= B
 : s
 -> e
 |-- B
 >-> C
 : s
 [n
] -> e
 |-- A
 >-> C
 : s
 [S n
]



 | coerce_rc_depth_conv_r : ∀ e
 A
 B
 C
 s
 n
,

  e
 |-- A
 -> A
 : s
 -> e
 |-- B
 -> B
 : s
 -> e
 |-- C
 -> C
 : s
 ->

  e
 |-- A
 >-> B
 : s
 [n
] -> e
 |-- B
 ~= C
 : s
 -> e
 |-- A
 >-> C
 : s
 [S n
]



where
 "G |-- T >-> U : s [ n ] " := (coerce_rc_depth G
 T
 U
 s
 n
).




Hint
 Resolve
 coerce_rc_depth_refl coerce_rc_depth_prod coerce_rc_depth_sum coerce_rc_depth_sub_l coerce_rc_depth_sub_r : coc
.

Hint
 Resolve
 coerce_rc_depth_conv_l coerce_rc_depth_conv_r : coc
.




Scheme
 coerce_rc_depth_dep
 := Induction
 for
 coerce_rc_depth
 Sort
 Prop
.




Lemma
 coerce_rc_depth_coerce : ∀ G
 T
 U
 s
 n
, G
 |-- T
 >-> U
 : s
 [n
] -> G
 |-- T
 >-> U
 : s
.