Library Lambda.Russell.Transitivity


Require
 Import
 Lambda.Utils.

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.

Require
 Import
 Lambda.Russell.Generation.

Require
 Import
 Lambda.Russell.UnicityOfSorting.

Require
 Import
 Lambda.Russell.Narrowing.

Require
 Import
 Lambda.Russell.Injectivity.







Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

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




Require
 Import
 Omega.

Require
 Import
 Coq.Arith.Max.




Lemma
 depth_prod_prod_l :  ∀ n0
 n1
 n2
 n3
, 

 n3
 + n2
 < S (max n2
 n1
 + S (max n3
 n0
)).




Lemma
 depth_prod_prod_r : ∀ n0
 n1
 n2
 n3
, n3
 + n1
 < S (max n0
 n3
 + S (max n2
 n1
)).




Lemma
 depth_prod_conv_prod : 

  ∀ n0
 n1
 n2
 n3
, n3
 + S n2
 < S (max n2
 n1
 + S (S (max n3
 n0
))).




Lemma
 depth_prod_conv_prod2 : ∀ n0
 n1
 n2
 n3
, n1
 + S n0
 < S (max n2
 n1
 + S (S (max n3
 n0
))).




Lemma
 depth_sum_conv_sum : ∀ n0
 n1
 n2
 n3
, S (n3
 + n2
) < S (max n2
 n1
 + S (S (max n3
 n0
))).




Lemma
 depth_sum_conv_sum2 : ∀ n0
 n1
 n2
 n3
, n3
 + S n2
 < S (max n3
 n1
 + S (S (max n2
 n0
))).




Lemma
 depth_conv_prod : ∀ n0
 n1
 n2
 n3
, S (n3
 + n2
) < S (S (max n2
 n1
 + (S (max n3
 n0
)))).




Lemma
 depth_conv_prod2 : ∀ n0
 n1
 n2
 n3
, S (n1
 + n3
) < S (S (max n2
 n1
 + S (max n0
 n3
))).

Lemma
 depth_conv_sum : ∀ n0
 n1
 n2
 n3
, S (n3
 + n2
) < S (S (max n3
 n0
 + S (max n2
 n1
))).




Lemma
 depth_conv_sum2 : ∀ n0
 n1
 n2
 n3
, n3
 + S n2
 < S (S (max n1
 n3
 + S (max n0
 n2
))).




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




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




Theorem
 coerce_trans_aux : ∀ n
 : nat,

(∀ e
 A
 B
 s
, ∀ d1
 : e
 |-- A
 >>> B
 : s
, 

∀ C
, ∀ d2
 : e
 |-- B
 >>> C
 : s
,

  n
 = (depth d1
) + (depth d2
) →

  e
 |-- A
 >>> C
 : s
).








Theorem
 coerce_trans_db_set : ∀ e
 A
 B
 C
 s
, e
 |-- A
 >>> B
 : s
 → e
 |-- B
 >>> C
 : s
 →

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




Require
 Import
 Lambda.Russell.Depth.




Theorem
 coerce_trans_d : ∀ e
 A
 B
 C
 s
 n1
 n2
, e
 |-- A
 >>> B
 : s
 [n1
] → e
 |-- B
 >>> C
 : s
 [n2
]→

  ∃ m
, e
 |-- A
 >>> C
 : s
 [m
].




Theorem
 coerce_trans : ∀ e
 A
 B
 C
 s
, e
 |-- A
 >> B
 : s
 → e
 |-- B
 >> C
 : s
 → e
 |-- A
 >> C
 : s
.