Library Lambda.Russell.Coercion


Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.Conv.

Require
 Import
 Lambda.LiftSubst.

Require
 Import
 Lambda.Env.

Require
 Import
 Lambda.Russell.Types.

Require
 Import
 Lambda.Russell.Thinning.

Require
 Import
 Lambda.Russell.Substitution.







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.




Inductive
 coerce_in_env : env → env → Prop
 :=

  | coerce_env_hd : ∀ e
 t
 u
 s
, e
 |-- t
 >> u
 : s
 → 

        coerce_in_env (u
 :: e
) (t
 :: e
)

  | coerce_env_tl :

        ∀ e
 f
 t
, wf
 (t
 :: f
) → coerce_in_env e
 f
 → coerce_in_env (t
 :: e
) (t
 :: f
).




Hint
 Resolve
 coerce_env_hd coerce_env_tl: coc
.




Lemma
 conv_item :

   ∀ n
 t
 e
,

   item_lift t
 e
 n
 →

   ∀ f
, coerce_in_env e
 f
 →

   item_lift t
 f
 n
 ∨

   ((∀ g
, trunc _
 (S n
) e
 g
 → trunc _
 (S n
) f
 g
) ∧

   ∃ u
, item_lift u
 f
 n
 ∧ (∃ s
, f
 |-- u
 >> t
 : s
)).




Lemma
 double_conv_env :

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

  ∀ f
, coerce_in_env e
 f
 → 

  wf
 f
 → f
 |-- t
 : T
) ∧

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

  ∀ f
, coerce_in_env e
 f
 → 

  wf
 f
 → f
 |-- T
 >> U
 : s
).




Lemma
 typ_conv_env : ∀ e
 t
 T
, e
 |-- t
 : T
 → ∀ f
, coerce_in_env e
 f
 → 

  wf
 f
 → f
 |-- t
 : T
.




Lemma
 coerce_conv_env : ∀ e
 T
 U
 s
, e
 |-- T
 >> U
 : s
 → 

  ∀ f
, coerce_in_env e
 f
 → 

  wf
 f
 → f
 |-- T
 >> U
 : s
.




Lemma
 coerce_sym : ∀ e
 T
 U
 s
, e
 |-- T
 >> U
 : s
 → e
 |-- U
 >> T
 : s
.




Hint
 Resolve
 coerce_sym : coc
.