Library Lambda.TPOSR.Types


Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.Conv.

Require
 Import
 Lambda.LiftSubst.

Require
 Import
 Lambda.Env.

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.




Implicit
 Types
 s
 : sort.










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




Definition
 sum_sort s1
 s2
 s3
 :=

  (s1
 = set ∧ s2
 = set ∧ s3
 = set) ∨

  (s1
 = prop ∧ s2
 = prop ∧ s3
 = prop).




Coercion
 Srt_l : sort
 >-> lterm
.







Reserved Notation
 "G |-- T ~= U : s" (at
 level
 70, T
, U
, s
 at
 next
 level
).

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




Inductive
 tposr_wf : lenv -> Prop
 :=

  | wf_nil : tposr_wf nil

  | wf_cons : ∀ G
 A
 s
, G
 |-- A
 -> A
 : s
 -> tposr_wf (A
 :: G
)





with
 tposr : lenv -> lterm -> lterm -> lterm -> Prop
 :=



  | tposr_var : ∀ e
, tposr_wf e
 -> 

  ∀ n
 T
, item_llift T
 e
 n
 -> e
 |-- (Ref_l n
) -> (Ref_l n
) : T




  | tposr_set : ∀ e
, tposr_wf e
 -> e
 |-- set -> set : kind



  | tposr_prop : ∀ e
, tposr_wf e
 -> e
 |-- prop -> prop : kind



  | tposr_prod : ∀ e
 A
 A'
 s1
, e
 |-- A
 -> A'
 : s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 -> B'
 : s2
 ->

  e
 |-- Prod_l A
 B
 -> Prod_l A'
 B'
 : s2


  

  | tposr_abs : ∀ e
 A
 A'
 s1
, e
 |-- A
 -> A'
 : s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 -> B'
 : s2
 ->

  ∀ M
 M'
, (A
 :: e
) |-- M
 -> M'
 : B
 -> 

  e
 |-- Abs_l A
 M
 -> Abs_l A'
 M'
 : (Prod_l A
 B
)

  

  | tposr_app : ∀ e
 A
 A'
 s1
, e
 |-- A
 -> A'
 : s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 >-> B'
 : s2
 ->

  ∀ M
 M'
, e
 |-- M
 -> M'
 : (Prod_l A
 B
) -> 

  ∀ N
 N'
, e
 |-- N
 -> N'
 : A
 ->

  e
 |-- App_l B
 M
 N
 -> App_l B'
 M'
 N'
 : lsubst N
 B




  | tposr_beta : ∀ e
 A
 A'
 s1
, e
 |-- A
 -> A'
 : s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 -> B'
 : s2
 ->

  ∀ M
 M'
, (A
 :: e
) |-- M
 -> M'
 : B
 -> 

  ∀ N
 N'
, e
 |-- N
 -> N'
 : A
 ->

  e
 |-- App_l B
 (Abs_l A
 M
) N
 -> lsubst N'
 M'
 : lsubst N
 B




  | tposr_conv : ∀ e
 M
 N
 A
, e
 |-- M
 -> N
 : A
 -> 

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

  e
 |-- M
 -> N
 : B


  

  | tposr_subset : ∀ e
 A
 A'
, e
 |-- A
 -> A'
 : set ->

  ∀ B
 B'
, (A
 :: e
) |-- B
 -> B'
 : prop ->

  e
 |-- Subset_l A
 B
 -> Subset_l A'
 B'
 : set



  | tposr_sum : ∀ e
 A
 A'
 s1
, e
 |-- A
 -> A'
 : s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 -> B'
 : s2
 ->

  ∀ s3
, sum_sort s1
 s2
 s3
 ->

  e
 |-- Sum_l A
 B
 -> Sum_l A'
 B'
 : s3


  

  | tposr_pair : ∀ e
 A
 A'
 s1
, e
 |-- A
 -> A'
 : s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 -> B'
 : s2
 ->

  ∀ s3
, sum_sort s1
 s2
 s3
 ->

  ∀ u
 u'
, e
 |-- u
 -> u'
 : A
 ->

  ∀ v
 v'
, e
 |-- v
 -> v'
 : lsubst u
 B
 ->

  e
 |-- Pair_l (Sum_l A
 B
) u
 v
 -> Pair_l (Sum_l A'
 B'
) u'
 v'
 : Sum_l A
 B




  | tposr_pi1 : ∀ e
 A
 A'
 s1
, e
 |-- A
 -> A
 : s1
 -> e
 |-- A
 >-> A'
 : s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 >-> B'
 : s2
 ->

  ∀ s3
, sum_sort s1
 s2
 s3
 ->

  ∀ t
 t'
, e
 |-- t
 -> t'
 : Sum_l A
 B
 ->

  e
 |-- Pi1_l (Sum_l A
 B
) t
 -> Pi1_l (Sum_l A'
 B'
) t'
 : A




  | tposr_pi1_red : ∀ e
 A
 A'
 s1
, e
 |-- A
 -> A'
 : s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 -> B'
 : s2
 ->

  ∀ s3
, sum_sort s1
 s2
 s3
 ->

  ∀ u
 u'
 v
 v'
, e
 |-- Pair_l (Sum_l A
 B
) u
 v
 -> Pair_l (Sum_l A'
 B'
) u'
 v'
 : Sum_l A
 B
 ->

  ∀ A''
, e
 |-- A''
 -> A''
 : s1
 -> e
 |-- A''
 >-> A
 : s1
 ->

  ∀ B''
, A''
 :: e
 |-- B''
 >-> B
 : s2
 ->

  e
 |-- Sum_l A''
 B''
 >-> Sum_l A
 B
 : s3
 ->

  e
 |-- Pi1_l (Sum_l A''
 B''
) (Pair_l (Sum_l A
 B
) u
 v
) -> u'
 : A''




  | tposr_pi2 : ∀ e
 A
 A'
 s1
, e
 |-- A
 -> A
 : s1
 -> e
 |-- A
 >-> A'
 : s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 >-> B'
 : s2
 ->

  ∀ s3
, sum_sort s1
 s2
 s3
 ->

  ∀ t
 t'
, e
 |-- t
 -> t'
 : Sum_l A
 B
 ->

  e
 |-- Pi2_l (Sum_l A
 B
) t
 -> Pi2_l (Sum_l A'
 B'
) t'
 : lsubst (Pi1_l (Sum_l A
 B
) t
) B




 | tposr_pi2_red : ∀ e
 A
 A'
 s1
, e
 |-- A
 -> A'
 : s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 -> B'
 : s2
 ->

  ∀ s3
, sum_sort s1
 s2
 s3
 ->

  ∀ u
 u'
 v
 v'
, 

  e
 |-- Pair_l (Sum_l A
 B
) u
 v
 -> Pair_l (Sum_l A'
 B'
) u'
 v'
 : Sum_l A
 B
 ->

  ∀ A''
, e
 |-- A''
 -> A''
 : s1
 -> e
 |-- A''
 >-> A
 : s1
 ->

  ∀ B''
, A''
 :: e
 |-- B''
 >-> B
 : s2
 ->

  e
 |-- Sum_l A''
 B''
 >-> Sum_l A
 B
 : s3
 ->

  e
 |-- Pi2_l (Sum_l A''
 B''
) (Pair_l (Sum_l A
 B
) u
 v
) -> v'
 : lsubst (Pi1_l (Sum_l A''
 B''
) (Pair_l (Sum_l A
 B
) u
 v
)) B''




where
 "G |-- T -> U : s" := (tposr G
 T
 U
 s
)



with
 tposr_eq : lenv -> lterm -> lterm -> sort -> Prop
 :=

  | tposr_eq_tposr : ∀ e
 X
 Y
 s
, e
 |-- X
 -> Y
 : s
 -> e
 |-- X
 ~= Y
 : s


  | tposr_eq_sym : ∀ e
 X
 Y
 s
, e
 |-- X
 ~= Y
 : s
 -> e
 |-- Y
 ~= X
 : s


  | tposr_eq_trans : ∀ e
 W
 X
 Y
 s
, e
 |-- W
 ~= X
 : s
 -> e
 |-- X
 ~= Y
 : s
 -> e
 |-- W
 ~= Y
 : s




where
 "G |-- T ~= U : s" := (tposr_eq G
 T
 U
 s
)



with
 tposr_coerce : lenv -> lterm -> lterm -> sort -> Prop
 :=

  | tposr_coerce_conv : ∀ e
 A
 B
 s
,  e
 |-- A
 ~= B
 : s
 -> e
 |-- A
 >-> B
 : s


  

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

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

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

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

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

  e
 |-- (Prod_l A
 B
) >-> (Prod_l A'
 B'
) : s'


  

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

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

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

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

   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''




  | tposr_coerce_sub_l : ∀ e
 U
 P
 U'
, 	

  e
 |-- U
 >-> U'
 : set ->

   e
 |-- U
 -> U
 :  set -> e
 |-- U'
 -> U'
 :  set -> 

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

  e
 |-- Subset_l U
 P
 >-> U'
 : set



  | tposr_coerce_sub_r : ∀ e
 U
 U'
 P
,

  e
 |-- U
 >-> U'
 : set -> 

   e
 |-- U
 -> U
 :  set -> e
 |-- U'
 -> U'
 :  set ->

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

  e
 |-- U
 >-> (Subset_l U'
 P
) : set



  | tposr_coerce_sym : ∀ e
 U
 V
 s
, e
 |-- U
 >-> V
 : s
 -> e
 |-- V
 >-> U
 : s




  | tposr_coerce_trans : ∀ e
 A
 B
 C
 s
,  

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




where
 "G |-- T >-> U : s" := (tposr_coerce G
 T
 U
 s
).







Scheme
 ind_tposr
 := Induction
 for
 tposr
 Sort
 Prop
.




Scheme
 tposr_wf_mutind
 := Induction
 for
 tposr
 Sort
 Prop


with
 wf_tposr_mutind
 :=  Induction
 for
 tposr_wf
 Sort
 Prop
.







Scheme
 tposr_mutind
 := Induction
 for
 tposr
 Sort
 Prop


with
 wf_mutind
 :=  Induction
 for
 tposr_wf
 Sort
 Prop


with
 eq_mutind
 :=  Induction
 for
 tposr_eq
 Sort
 Prop


with
 coerce_mutind
 :=  Induction
 for
 tposr_coerce
 Sort
 Prop
.







Lemma
 wf_tposr : ∀ e
 M
 N
 T
, e
 |-- M
 -> N
 : T
 -> tposr_wf e
.




Hint
 Resolve
 wf_tposr : ecoc
.




Reserved Notation
 "G |-- M -+> N : B" (at
 level
 70, M
, N
, B
 at
 next
 level
).




Inductive
 tposrp : lenv -> lterm -> lterm -> lterm -> Prop
 :=

  | tposrp_tposr : ∀ e
 X
 Y
 Z
, e
 |-- X
 -> Y
 : Z
 -> e
 |-- X
 -+> Y
 : Z


  | tposrp_trans : ∀ e
 W
 X
 Y
 Z
, e
 |-- W
 -+> X
 : Z
 -> e
 |-- X
 -+> Y
 : Z
 -> e
 |-- W
 -+> Y
 : Z


where
 "G |-- M -+> N : B" := (tposrp G
 M
 N
 B
).




Hint
 Resolve
 tposrp_tposr : coc
.

Hint
 Resolve
 tposrp_trans : ecoc
.




Definition
 tposr_term G
 M
 A
 := ∃ M'
, G
 |-- M
 -> M'
 : A
.




Lemma
 tposr_tposr_term : ∀ G
 M
 M'
 A
, tposr G
 M
 M'
 A
 -> tposr_term G
 M
 A
.




Hint
 Resolve
 tposr_tposr_term : ecoc
.