Library Lambda.TPOSR.Reduction


Require
 Import
 Lambda.TPOSR.Terms.

Require
 Import
 Lambda.TPOSR.LiftSubst.




Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

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




Inductive
 lred1 : lterm → lterm → Prop
 :=

| beta : ∀ T1
 M
 N
 T
, lred1 (App_l T1
 (Abs_l T
 M
) N
) (lsubst N
 M
)

| pi1 : ∀ T1
 T
 M
 N
, lred1 (Pi1_l T1
 (Pair_l T
 M
 N
)) M


| pi2 : ∀ T1
 T
 M
 N
, lred1 (Pi2_l T1
 (Pair_l T
 M
 N
)) N


| abs_lred_l : ∀ M
 M'
, lred1 M
 M'
 → ∀ N
, lred1 (Abs_l M
 N
) (Abs_l M'
 N
)

| abs_lred_r : ∀ M
 M'
, lred1 M
 M'
 → ∀ N
, lred1 (Abs_l N
 M
) (Abs_l N
 M'
)

| app_lred_T :

∀ T
 S
, lred1 T
 S
 → ∀ M1
 M2
, lred1 (App_l T
 M1
 M2
) (App_l S
 M1
 M2
)

| app_lred_l : ∀ M1
 N1
, lred1 M1
 N1
 → ∀ T1
 M2
, lred1 (App_l T1
 M1
 M2
) (App_l T1
 N1
 M2
)

| app_lred_r :

∀ M2
 N2
, lred1 M2
 N2
 → ∀ T1
 M1
, lred1 (App_l T1
 M1
 M2
) (App_l T1
 M1
 N2
)

| pair_lred_T :

∀ T
 S
, lred1 T
 S
 → ∀ M1
 M2
, lred1 (Pair_l T
 M1
 M2
) (Pair_l S
 M1
 M2
)

| pair_lred_l :

∀ M1
 N1
, lred1 M1
 N1
 → ∀ T
 M2
, lred1 (Pair_l T
 M1
 M2
) (Pair_l T
 N1
 M2
)

| pair_lred_r :

∀ M2
 N2
, lred1 M2
 N2
 → ∀ T
 M1
, lred1 (Pair_l T
 M1
 M2
) (Pair_l T
 M1
 N2
)

| prod_lred_l :

∀ M1
 N1
, lred1 M1
 N1
 → ∀ M2
, lred1 (Prod_l M1
 M2
) (Prod_l N1
 M2
)

| prod_lred_r :

∀ M2
 N2
, lred1 M2
 N2
 → ∀ M1
, lred1 (Prod_l M1
 M2
) (Prod_l M1
 N2
)

| sum_lred_l :

∀ M1
 N1
, lred1 M1
 N1
 → ∀ M2
, lred1 (Sum_l M1
 M2
) (Sum_l N1
 M2
)

    | sum_lred_r :

        ∀ M2
 N2
, lred1 M2
 N2
 → ∀ M1
, lred1 (Sum_l M1
 M2
) (Sum_l M1
 N2
)

    | subset_lred_l :

        ∀ M1
 N1
, lred1 M1
 N1
 → ∀ M2
, lred1 (Subset_l M1
 M2
) (Subset_l N1
 M2
)

    | subset_lred_r :

        ∀ M2
 N2
, lred1 M2
 N2
 → ∀ M1
, lred1 (Subset_l M1
 M2
) (Subset_l M1
 N2
)

    | pi1_lred_T :

        ∀ M
 N
, lred1 M
 N
 → ∀ M2
, lred1 (Pi1_l M
 M2
) (Pi1_l N
 M2
)

    | pi1_lred :

        ∀ M
 N
, lred1 M
 N
 → ∀ M2
, lred1 (Pi1_l M2
 M
) (Pi1_l M2
 N
)

    | pi2_lred_T :

        ∀ M
 N
, lred1 M
 N
 → ∀ M2
, lred1 (Pi2_l M
 M2
) (Pi2_l N
 M2
)

    | pi2_lred :

        ∀ M
 N
, lred1 M
 N
 → ∀ M2
, lred1 (Pi2_l M2
 M
) (Pi2_l M2
 N
).




  Inductive
 lred M
 : lterm → Prop
 :=

    | refl_lred : lred M
 M


    | trans_lred : ∀ (P
 : lterm) N
, lred M
 P
 → lred1 P
 N
 → lred M
 N
.




  Inductive
 conv M
 : lterm → Prop
 :=

    | refl_conv : conv M
 M


    | trans_conv_lred : ∀ (P
 : lterm) N
, conv M
 P
 → lred1 P
 N
 → conv M
 N


    | trans_conv_exp : ∀ (P
 : lterm) N
, conv M
 P
 → lred1 N
 P
 → conv M
 N
.




  Inductive
 par_lred1 : lterm → lterm → Prop
 :=

    | par_beta :

        ∀ Typ
, 

        ∀ M
 M'
,

        par_lred1 M
 M'
 →

        ∀ N
 N'
,

        par_lred1 N
 N'
 → ∀ T
, par_lred1 (App_l Typ
 (Abs_l T
 M
) N
) (lsubst N'
 M'
)

    | par_pi1 : ∀ Typ
, ∀ M
 M'
, par_lred1 M
 M'
 → 

      ∀ T
 N
, par_lred1 (Pi1_l Typ
 (Pair_l T
 M
 N
)) M'


    | par_pi2 : ∀ Typ
 N
 N'
, par_lred1 N
 N'
 → ∀ T
 M
,

      par_lred1 (Pi2_l Typ
 (Pair_l T
 M
 N
)) N'


    | sort_par_lred : ∀ s
, par_lred1 (Srt_l s
) (Srt_l s
)

    | ref_par_lred : ∀ n
, par_lred1 (Ref_l n
) (Ref_l n
)

    | abs_par_lred :

        ∀ M
 M'
,

        par_lred1 M
 M'
 →

        ∀ T
 T'
, par_lred1 T
 T'
 → par_lred1 (Abs_l T
 M
) (Abs_l T'
 M'
)

    | app_par_lred :forall T
 T'
, par_lred1 T
 T'
 →

        ∀ M
 M'
,

        par_lred1 M
 M'
 →

        ∀ N
 N'
, par_lred1 N
 N'
 → par_lred1 (App_l T
 M
 N
) (App_l T'
 M'
 N'
)

    | pair_par_lred : ∀ T
 T'
, par_lred1 T
 T'
 →

        ∀ M
 M'
,

        par_lred1 M
 M'
 →

        ∀ N
 N'
, par_lred1 N
 N'
 → par_lred1 (Pair_l T
 M
 N
) (Pair_l T'
 M'
 N'
)

    | prod_par_lred :

        ∀ M
 M'
,

        par_lred1 M
 M'
 →

        ∀ N
 N'
, par_lred1 N
 N'
 → par_lred1 (Prod_l M
 N
) (Prod_l M'
 N'
)

    | sum_par_lred :

        ∀ M
 M'
,

        par_lred1 M
 M'
 →

        ∀ N
 N'
, par_lred1 N
 N'
 → par_lred1 (Sum_l M
 N
) (Sum_l M'
 N'
)

    | subset_par_lred :

        ∀ M
 M'
,

        par_lred1 M
 M'
 →

        ∀ N
 N'
, par_lred1 N
 N'
 → par_lred1 (Subset_l M
 N
) (Subset_l M'
 N'
)

    | pi1_par_lred :forall T
 T'
, par_lred1 T
 T'
 →

        ∀ M
 M'
, par_lred1 M
 M'
 → par_lred1 (Pi1_l T
 M
) (Pi1_l T'
 M'
)

    | pi2_par_lred :forall T
 T'
, par_lred1 T
 T'
 →

        ∀ M
 M'
, par_lred1 M
 M'
 → par_lred1 (Pi2_l T
 M
) (Pi2_l T'
 M'
).




  Definition
 par_lred := clos_trans lterm par_lred1.




  Hint
 Resolve
 beta pi1 pi2 abs_lred_l abs_lred_r app_lred_T app_lred_l app_lred_r pair_lred_T pair_lred_l pair_lred_r : coc
.

  Hint
 Resolve
 prod_lred_l prod_lred_r sum_lred_l sum_lred_r subset_lred_l subset_lred_r pi1_lred_T pi1_lred  pi2_lred_T pi2_lred : coc
.

  Hint
 Resolve
 refl_lred refl_conv: coc
.

  Hint
 Resolve
 par_beta par_pi1 par_pi2 sort_par_lred ref_par_lred abs_par_lred app_par_lred pair_par_lred

    prod_par_lred sum_par_lred subset_par_lred pi1_par_lred pi2_par_lred : coc
.




  Hint
 Unfold
 par_lred: coc
.




Section
 Normalisation_Forte.




  Definition
 normal t
 : Prop
 := ∀ u
, ¬ lred1 t
 u
.




  Definition
 sn : lterm → Prop
 := Acc (transp _
 lred1).




End
 Normalisation_Forte.




  Hint
 Unfold
 sn: coc
.




  Lemma
 one_step_lred : ∀ M
 N
, lred1 M
 N
 → lred M
 N
.




  Hint
 Resolve
 one_step_lred: coc
.




  Lemma
 lred1_lred_ind :

   ∀ N
 (P
 : lterm → Prop
),

   P
 N
 →

   (∀ M
 (R
 : lterm), lred1 M
 R
 → lred R
 N
 → P
 R
 → P
 M
) →

   ∀ M
, lred M
 N
 → P
 M
.




  Lemma
 trans_lred_lred : ∀ M
 N
 (P
 : lterm), lred M
 N
 → lred N
 P
 → lred M
 P
.




  Lemma
 lred_lred_app :

   ∀ T
 T0
 u
 u0
 v
 v0
, lred T
 T0
 → lred u
 u0
 → lred v
 v0
 → lred (App_l T
 u
 v
) (App_l T0
 u0
 v0
).




Lemma
 lred_lred_pair :

   ∀ T
 T0
 u
 u0
 v
 v0
, lred T
 T0
 → lred u
 u0
 → lred v
 v0
 → lred (Pair_l T
 u
 v
) (Pair_l T0
 u0
 v0
).




Ltac
 lred_lred_tac
 t
 :=

  intros
 u
 ; elim
 u
 ; 

  [ (intros
 u0
 ; elim
 u0
; intros
 v
 v0
 P
; auto
 with
 coc
 core
 arith
 sets
 ;

     apply
 trans_lred with
 (t
 u
 P
); auto
 with
 coc
 core
 arith
 sets
) 

  | intros
 v
 v0
 P
 ; apply
 trans_lred with
 (t
 P
 v0
); auto
 with
 coc
 core
 arith
 sets
 ].




Lemma
 lred_lred_abs :

   ∀ u
 u0
 v
 v0
, lred u
 u0
 → lred v
 v0
 → lred (Abs_l u
 v
) (Abs_l u0
 v0
).




  Lemma
 lred_lred_prod :

   ∀ u
 u0
 v
 v0
, lred u
 u0
 → lred v
 v0
 → lred (Prod_l u
 v
) (Prod_l u0
 v0
).




  Lemma
 lred_lred_sum :

   ∀ u
 u0
 v
 v0
, lred u
 u0
 → lred v
 v0
 → lred (Sum_l u
 v
) (Sum_l u0
 v0
).




  Lemma
 lred_lred_subset :

   ∀ u
 u0
 v
 v0
, lred u
 u0
 → lred v
 v0
 → lred (Subset_l u
 v
) (Subset_l u0
 v0
).




  Lemma
 lred_lred_pi1 : ∀ u
 u0
 v
 v0
, lred u
 u0
 → lred v
 v0
 → lred (Pi1_l u
 v
) (Pi1_l u0
 v0
).




  Lemma
 lred_lred_pi2 : ∀ u
 u0
 v
 v0
, lred u
 u0
 → lred v
 v0
 → lred (Pi2_l u
 v
) (Pi2_l u0
 v0
).




  Hint
 Resolve
 lred_lred_app lred_lred_abs lred_lred_prod: coc
.

  Hint
 Resolve
 lred_lred_pair lred_lred_sum lred_lred_subset lred_lred_pi1 lred_lred_pi2 : coc
.




  Lemma
 lred1_llift :

   ∀ u
 v
, lred1 u
 v
 → ∀ n
 k
, lred1 (llift_rec n
 u
 k
) (llift_rec n
 v
 k
).




  Hint
 Resolve
 lred1_llift: coc
.




  Lemma
 lred1_lsubst_r :

   ∀ t
 u
,

   lred1 t
 u
 → ∀ (a
 : lterm) k
, lred1 (lsubst_rec a
 t
 k
) (lsubst_rec a
 u
 k
).




  Lemma
 lred1_lsubst_l :

   ∀ (a
 : lterm) t
 u
 k
,

   lred1 t
 u
 → lred (lsubst_rec t
 a
 k
) (lsubst_rec u
 a
 k
).




  Hint
 Resolve
 lred1_lsubst_l lred1_lsubst_r: coc
.




  Lemma
 lred_prod_prod :

   ∀ u
 v
 t
,

   lred (Prod_l u
 v
) t
 →

   ∀ P
 : Prop
,

   (∀ a
 b
 : lterm, t
 = Prod_l a
 b
 → lred u
 a
 → lred v
 b
 → P
) → P
.




  Lemma
 lred_sum_sum :

   ∀ u
 v
 t
,

   lred (Sum_l u
 v
) t
 →

   ∀ P
 : Prop
,

   (∀ a
 b
 : lterm, t
 = Sum_l a
 b
 → lred u
 a
 → lred v
 b
 → P
) → P
.




  Lemma
 lred_subset_subset :

   ∀ u
 v
 t
,

   lred (Subset_l u
 v
) t
 →

   ∀ P
 : Prop
,

   (∀ a
 b
 : lterm, t
 = Subset_l a
 b
 → lred u
 a
 → lred v
 b
 → P
) → P
.




  Lemma
 lred_sort_sort : ∀ s
 t
, lred (Srt_l s
) t
 → t
 ≠ Srt_l s
 → False.




  Lemma
 lred_ref_ref : ∀ n
 t
, lred (Ref_l n
) t
 → t
 ≠ Ref_l n
 → False.




  Lemma
 one_step_conv_exp : ∀ M
 N
, lred1 M
 N
 → conv N
 M
.




  Lemma
 lred_conv : ∀ M
 N
, lred M
 N
 → conv M
 N
.




  Hint
 Resolve
 one_step_conv_exp lred_conv: coc
.




  Lemma
 sym_conv : ∀ M
 N
, conv M
 N
 → conv N
 M
.




  Hint
 Immediate
 sym_conv: coc
.




  Lemma
 trans_conv_conv :

   ∀ M
 N
 (P
 : lterm), conv M
 N
 → conv N
 P
 → conv M
 P
.




  Lemma
 conv_conv_prod :

   ∀ a
 b
 c
 d
 : lterm, conv a
 b
 → conv c
 d
 → conv (Prod_l a
 c
) (Prod_l b
 d
).




Lemma
 conv_conv_sum : ∀ a
 b
 c
 d
 : lterm, conv a
 b
 → conv c
 d
 → conv (Sum_l a
 c
) (Sum_l b
 d
).




Lemma
 conv_conv_subset : 

  ∀ a
 b
 c
 d
 : lterm, conv a
 b
 → conv c
 d
 → conv (Subset_l a
 c
) (Subset_l b
 d
).




Lemma
 conv_conv_pair : ∀ T
 S
 a
 b
 c
 d
 : lterm, conv T
 S
 → conv a
 b
 → conv c
 d
 → conv (Pair_l T
 a
 c
) (Pair_l S
 b
 d
).




  Lemma
 conv_conv_llift :

   ∀ (a
 b
 : lterm) n
 k
,

   conv a
 b
 → conv (llift_rec n
 a
 k
) (llift_rec n
 b
 k
).




  Lemma
 conv_conv_lsubst :

   ∀ (a
 b
 c
 d
 : lterm) k
,

   conv a
 b
 → conv c
 d
 → conv (lsubst_rec a
 c
 k
) (lsubst_rec b
 d
 k
).




  Hint
 Resolve
 conv_conv_prod conv_conv_llift conv_conv_lsubst: coc
.




  Lemma
 refl_par_lred1 : ∀ M
, par_lred1 M
 M
.




  Hint
 Resolve
 refl_par_lred1: coc
.




  Lemma
 lred1_par_lred1 : ∀ M
 N
, lred1 M
 N
 → par_lred1 M
 N
.




  Hint
 Resolve
 lred1_par_lred1: coc
.




  Lemma
 lred_par_lred : ∀ M
 N
, lred M
 N
 → par_lred M
 N
.




  Lemma
 par_lred_lred : ∀ M
 N
, par_lred M
 N
 → lred M
 N
.




  Hint
 Resolve
 lred_par_lred par_lred_lred: coc
.




  Lemma
 par_lred1_llift :

   ∀ n
 (a
 b
 : lterm),

   par_lred1 a
 b
 → ∀ k
, par_lred1 (llift_rec n
 a
 k
) (llift_rec n
 b
 k
).




  Lemma
 par_lred1_lsubst :

   ∀ c
 d
 : lterm,

   par_lred1 c
 d
 →

   ∀ a
 b
 : lterm,

   par_lred1 a
 b
 → ∀ k
, par_lred1 (lsubst_rec a
 c
 k
) (lsubst_rec b
 d
 k
).




  Lemma
 inv_par_lred_abs :

   ∀ (P
 : Prop
) T
 (U
 x
 : lterm),

   par_lred1 (Abs_l T
 U
) x
 →

   (∀ T'
 (U'
 : lterm), x
 = Abs_l T'
 U'
 → par_lred1 U
 U'
 → P
) → P
.




  Lemma
 inv_par_lred_pair :

   ∀ (P
 : Prop
) T
 (U
 V
 x
 : lterm),

   par_lred1 (Pair_l T
 U
 V
) x
 →

   (∀ T'
 (U'
 V'
 : lterm), x
 = Pair_l T'
 U'
 V'
 → par_lred1 U
 U'
 → par_lred1 V
 V'
 → P
) → P
.




  Hint
 Resolve
 par_lred1_llift par_lred1_lsubst: coc
.




  Lemma
 sublterm_abs : ∀ t
 (m
 : lterm), sublterm m
 (Abs_l t
 m
).




  Lemma
 sublterm_prod : ∀ t
 (m
 : lterm), sublterm m
 (Prod_l t
 m
).




  Lemma
 sublterm_sum : ∀ t
 (m
 : lterm), sublterm m
 (Sum_l t
 m
).




  Lemma
 sublterm_subset : ∀ t
 (m
 : lterm), sublterm m
 (Subset_l t
 m
).




Hint
 Resolve
 sublterm_abs sublterm_prod sublterm_sum sublterm_subset : coc
.




  Lemma
 mem_sort_llift :

   ∀ t
 n
 k
 s
, mem_sort s
 (llift_rec n
 t
 k
) → mem_sort s
 t
.




  Lemma
 mem_sort_lsubst :

   ∀ (b
 a
 : lterm) n
 s
,

   mem_sort s
 (lsubst_rec a
 b
 n
) → mem_sort s
 a
 ∨ mem_sort s
 b
.




  Lemma
 lred_sort_mem : ∀ t
 s
, lred t
 (Srt_l s
) → mem_sort s
 t
.




  Lemma
 lred_normal : ∀ u
 v
, lred u
 v
 → normal u
 → u
 = v
.




  Lemma
 sn_lred_sn : ∀ a
 b
 : lterm, sn a
 → lred a
 b
 → sn b
.




  Lemma
 commut_lred1_sublterm : commut _
 sublterm (transp _
 lred1).




 Lemma
 sublterm_sn :

   ∀ a
 : lterm, sn a
 → ∀ b
 : lterm, sublterm b
 a
 → sn b
.




  Lemma
 sn_prod : ∀ A
, sn A
 → ∀ B
, sn B
 → sn (Prod_l A
 B
).




  Lemma
 sn_sum : ∀ A
, sn A
 → ∀ B
, sn B
 → sn (Sum_l A
 B
).




  Lemma
 sn_pair : ∀ T
, sn T
 → ∀ A
, sn A
 → ∀ B
, sn B
 → sn (Pair_l T
 A
 B
).




  Lemma
 sn_subset : ∀ A
, sn A
 → ∀ B
, sn B
 → sn (Subset_l A
 B
).




  Lemma
 sn_lsubst : ∀ T
 M
, sn (lsubst T
 M
) → sn M
.