Library Lambda.Reduction


Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.LiftSubst.




Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

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




Inductive
 red1 : term → term → Prop
 :=

| beta : ∀ M
 N
 T
, red1 (App (Abs T
 M
) N
) (subst N
 M
)

| pi1 : ∀ T
 M
 N
, red1 (Pi1 (Pair T
 M
 N
)) M


| pi2 : ∀ T
 M
 N
, red1 (Pi2 (Pair T
 M
 N
)) N


| abs_red_l : ∀ M
 M'
, red1 M
 M'
 → ∀ N
, red1 (Abs M
 N
) (Abs M'
 N
)

| abs_red_r : ∀ M
 M'
, red1 M
 M'
 → ∀ N
, red1 (Abs N
 M
) (Abs N
 M'
)

| app_red_l : ∀ M1
 N1
, red1 M1
 N1
 → ∀ M2
, red1 (App M1
 M2
) (App N1
 M2
)

| app_red_r :

∀ M2
 N2
, red1 M2
 N2
 → ∀ M1
, red1 (App M1
 M2
) (App M1
 N2
)

| pair_red_T :

∀ T
 S
, red1 T
 S
 → ∀ M1
 M2
, red1 (Pair T
 M1
 M2
) (Pair S
 M1
 M2
)

| pair_red_l :

∀ M1
 N1
, red1 M1
 N1
 → ∀ T
 M2
, red1 (Pair T
 M1
 M2
) (Pair T
 N1
 M2
)

| pair_red_r :

∀ M2
 N2
, red1 M2
 N2
 → ∀ T
 M1
, red1 (Pair T
 M1
 M2
) (Pair T
 M1
 N2
)

| prod_red_l :

∀ M1
 N1
, red1 M1
 N1
 → ∀ M2
, red1 (Prod M1
 M2
) (Prod N1
 M2
)

| prod_red_r :

∀ M2
 N2
, red1 M2
 N2
 → ∀ M1
, red1 (Prod M1
 M2
) (Prod M1
 N2
)

| sum_red_l :

∀ M1
 N1
, red1 M1
 N1
 → ∀ M2
, red1 (Sum M1
 M2
) (Sum N1
 M2
)

    | sum_red_r :

        ∀ M2
 N2
, red1 M2
 N2
 → ∀ M1
, red1 (Sum M1
 M2
) (Sum M1
 N2
)

    | subset_red_l :

        ∀ M1
 N1
, red1 M1
 N1
 → ∀ M2
, red1 (Subset M1
 M2
) (Subset N1
 M2
)

    | subset_red_r :

        ∀ M2
 N2
, red1 M2
 N2
 → ∀ M1
, red1 (Subset M1
 M2
) (Subset M1
 N2
)

    | pi1_red :

        ∀ M
 N
, red1 M
 N
 → red1 (Pi1 M
) (Pi1 N
)

    | pi2_red :

        ∀ M
 N
, red1 M
 N
 → red1 (Pi2 M
) (Pi2 N
).




  Inductive
 red M
 : term → Prop
 :=

    | refl_red : red M
 M


    | trans_red : ∀ (P
 : term) N
, red M
 P
 → red1 P
 N
 → red M
 N
.




  Inductive
 conv M
 : term → Prop
 :=

    | refl_conv : conv M
 M


    | trans_conv_red : ∀ (P
 : term) N
, conv M
 P
 → red1 P
 N
 → conv M
 N


    | trans_conv_exp : ∀ (P
 : term) N
, conv M
 P
 → red1 N
 P
 → conv M
 N
.




  Inductive
 par_red1 : term → term → Prop
 :=

    | par_beta :

        ∀ M
 M'
,

        par_red1 M
 M'
 →

        ∀ N
 N'
,

        par_red1 N
 N'
 → ∀ T
, par_red1 (App (Abs T
 M
) N
) (subst N'
 M'
)

    | par_pi1 : ∀ M
 M'
, par_red1 M
 M'
 → 

      ∀ T
 N
, par_red1 (Pi1 (Pair T
 M
 N
)) M'


    | par_pi2 : ∀ N
 N'
, par_red1 N
 N'
 → ∀ T
 M
,

      par_red1 (Pi2 (Pair T
 M
 N
)) N'


    | sort_par_red : ∀ s
, par_red1 (Srt s
) (Srt s
)

    | ref_par_red : ∀ n
, par_red1 (Ref n
) (Ref n
)

    | abs_par_red :

        ∀ M
 M'
,

        par_red1 M
 M'
 →

        ∀ T
 T'
, par_red1 T
 T'
 → par_red1 (Abs T
 M
) (Abs T'
 M'
)

    | app_par_red :

        ∀ M
 M'
,

        par_red1 M
 M'
 →

        ∀ N
 N'
, par_red1 N
 N'
 → par_red1 (App M
 N
) (App M'
 N'
)

    | pair_par_red : ∀ T
 T'
, par_red1 T
 T'
 →

        ∀ M
 M'
,

        par_red1 M
 M'
 →

        ∀ N
 N'
, par_red1 N
 N'
 → par_red1 (Pair T
 M
 N
) (Pair T'
 M'
 N'
)

    | prod_par_red :

        ∀ M
 M'
,

        par_red1 M
 M'
 →

        ∀ N
 N'
, par_red1 N
 N'
 → par_red1 (Prod M
 N
) (Prod M'
 N'
)

    | sum_par_red :

        ∀ M
 M'
,

        par_red1 M
 M'
 →

        ∀ N
 N'
, par_red1 N
 N'
 → par_red1 (Sum M
 N
) (Sum M'
 N'
)

    | subset_par_red :

        ∀ M
 M'
,

        par_red1 M
 M'
 →

        ∀ N
 N'
, par_red1 N
 N'
 → par_red1 (Subset M
 N
) (Subset M'
 N'
)

    | pi1_par_red :

        ∀ M
 M'
, par_red1 M
 M'
 → par_red1 (Pi1 M
) (Pi1 M'
)

    | pi2_par_red :

        ∀ M
 M'
, par_red1 M
 M'
 → par_red1 (Pi2 M
) (Pi2 M'
).




  Definition
 par_red := clos_trans term par_red1.




  Hint
 Resolve
 beta pi1 pi2 abs_red_l abs_red_r app_red_l app_red_r pair_red_T pair_red_l pair_red_r : coc
.

  Hint
 Resolve
 prod_red_l prod_red_r sum_red_l sum_red_r subset_red_l subset_red_r pi1_red pi2_red  : coc
.

  Hint
 Resolve
 refl_red refl_conv: coc
.

  Hint
 Resolve
 par_beta par_pi1 par_pi2 sort_par_red ref_par_red abs_par_red app_par_red pair_par_red

    prod_par_red sum_par_red subset_par_red pi1_par_red pi2_par_red: coc
.




  Hint
 Unfold
 par_red: coc
.




Section
 Normalisation_Forte.




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




  Definition
 sn : term → Prop
 := Acc (transp _
 red1).




End
 Normalisation_Forte.




  Hint
 Unfold
 sn: coc
.




  Lemma
 one_step_red : ∀ M
 N
, red1 M
 N
 → red M
 N
.




  Hint
 Resolve
 one_step_red: coc
.




  Lemma
 red1_red_ind :

   ∀ N
 (P
 : term → Prop
),

   P
 N
 →

   (∀ M
 (R
 : term), red1 M
 R
 → red R
 N
 → P
 R
 → P
 M
) →

   ∀ M
, red M
 N
 → P
 M
.




  Lemma
 trans_red_red : ∀ M
 N
 (P
 : term), red M
 N
 → red N
 P
 → red M
 P
.




  Lemma
 red_red_app :

   ∀ u
 u0
 v
 v0
, red u
 u0
 → red v
 v0
 → red (App u
 v
) (App u0
 v0
).




Lemma
 red_red_pair :

   ∀ T
 T0
 u
 u0
 v
 v0
, red T
 T0
 → red u
 u0
 → red v
 v0
 → red (Pair T
 u
 v
) (Pair T0
 u0
 v0
).




Ltac
 red_red_tac
 t
 :=

  intros
 u
 ; elim
 u
 ; 

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

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

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




Lemma
 red_red_abs :

   ∀ u
 u0
 v
 v0
, red u
 u0
 → red v
 v0
 → red (Abs u
 v
) (Abs u0
 v0
).




  Lemma
 red_red_prod :

   ∀ u
 u0
 v
 v0
, red u
 u0
 → red v
 v0
 → red (Prod u
 v
) (Prod u0
 v0
).




  Lemma
 red_red_sum :

   ∀ u
 u0
 v
 v0
, red u
 u0
 → red v
 v0
 → red (Sum u
 v
) (Sum u0
 v0
).




  Lemma
 red_red_subset :

   ∀ u
 u0
 v
 v0
, red u
 u0
 → red v
 v0
 → red (Subset u
 v
) (Subset u0
 v0
).




  Lemma
 red_red_pi1 : ∀ u
 u0
, red u
 u0
 → red (Pi1 u
) (Pi1 u0
).




  Lemma
 red_red_pi2 : ∀ u
 u0
, red u
 u0
 → red (Pi2 u
) (Pi2 u0
).




  Hint
 Resolve
 red_red_app red_red_abs red_red_prod: coc
.

  Hint
 Resolve
 red_red_pair red_red_sum red_red_subset red_red_pi1 red_red_pi2 : coc
.




  Lemma
 red1_lift :

   ∀ u
 v
, red1 u
 v
 → ∀ n
 k
, red1 (lift_rec n
 u
 k
) (lift_rec n
 v
 k
).




  Hint
 Resolve
 red1_lift: coc
.




  Lemma
 red1_subst_r :

   ∀ t
 u
,

   red1 t
 u
 → ∀ (a
 : term) k
, red1 (subst_rec a
 t
 k
) (subst_rec a
 u
 k
).




  Lemma
 red1_subst_l :

   ∀ (a
 : term) t
 u
 k
,

   red1 t
 u
 → red (subst_rec t
 a
 k
) (subst_rec u
 a
 k
).




  Hint
 Resolve
 red1_subst_l red1_subst_r: coc
.




  Lemma
 red_prod_prod :

   ∀ u
 v
 t
,

   red (Prod u
 v
) t
 →

   ∀ P
 : Prop
,

   (∀ a
 b
 : term, t
 = Prod a
 b
 → red u
 a
 → red v
 b
 → P
) → P
.




  Lemma
 red_sum_sum :

   ∀ u
 v
 t
,

   red (Sum u
 v
) t
 →

   ∀ P
 : Prop
,

   (∀ a
 b
 : term, t
 = Sum a
 b
 → red u
 a
 → red v
 b
 → P
) → P
.




  Lemma
 red_subset_subset :

   ∀ u
 v
 t
,

   red (Subset u
 v
) t
 →

   ∀ P
 : Prop
,

   (∀ a
 b
 : term, t
 = Subset a
 b
 → red u
 a
 → red v
 b
 → P
) → P
.




  Lemma
 red_sort_sort : ∀ s
 t
, red (Srt s
) t
 → t
 ≠ Srt s
 → False.




  Lemma
 red_ref_ref : ∀ n
 t
, red (Ref n
) t
 → t
 ≠ Ref n
 → False.




  Lemma
 red_abs_abs :

   ∀ u
 v
 t
,

   red (Abs u
 v
) t
 →

   ∀ P
 : Prop
,

   (∀ a
 b
 : term, t
 = Abs a
 b
 → red u
 a
 → red v
 b
 → P
) → P
.




  Lemma
 red_pair_pair :

   ∀ u
 v
 w
 t
,

   red (Pair u
 v
 w
) t
 →

   ∀ P
 : Prop
,

   (∀ a
 b
 c
 : term, t
 = Pair a
 b
 c
 → red u
 a
 → red v
 b
 → red w
 c
 → P
) → P
.




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




  Lemma
 red_conv : ∀ M
 N
, red M
 N
 → conv M
 N
.




  Hint
 Resolve
 one_step_conv_exp red_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
 : term), conv M
 N
 → conv N
 P
 → conv M
 P
.




  Lemma
 conv_conv_prod :

   ∀ a
 b
 c
 d
 : term, conv a
 b
 → conv c
 d
 → conv (Prod a
 c
) (Prod b
 d
).




Lemma
 conv_conv_abs : ∀ a
 b
 c
 d
 : term, conv a
 b
 → conv c
 d
 → conv (Abs a
 c
) (Abs b
 d
).




Lemma
 conv_conv_sum : ∀ a
 b
 c
 d
 : term, conv a
 b
 → conv c
 d
 → conv (Sum a
 c
) (Sum b
 d
).




Lemma
 conv_conv_subset : 

  ∀ a
 b
 c
 d
 : term, conv a
 b
 → conv c
 d
 → conv (Subset a
 c
) (Subset b
 d
).




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




Lemma
 conv_conv_app : ∀ a
 b
 c
 d
 : term, conv a
 b
 → conv c
 d
 → conv (App a
 c
) (App b
 d
).




Lemma
 conv_conv_pi1 : ∀ a
 b
 : term, conv a
 b
 → conv (Pi1 a
) (Pi1 b
).




Lemma
 conv_conv_pi2 : ∀ a
 b
 : term, conv a
 b
 → conv (Pi2 a
) (Pi2 b
).




Hint
 Resolve
 conv_conv_pi1 conv_conv_pi2 : coc
.




  Lemma
 conv_conv_lift :

   ∀ (a
 b
 : term) n
 k
,

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




  Lemma
 conv_conv_subst :

   ∀ (a
 b
 c
 d
 : term) k
,

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




  Hint
 Resolve
 conv_conv_prod conv_conv_lift conv_conv_subst: coc
.




  Lemma
 refl_par_red1 : ∀ M
, par_red1 M
 M
.




  Hint
 Resolve
 refl_par_red1: coc
.




  Lemma
 red1_par_red1 : ∀ M
 N
, red1 M
 N
 → par_red1 M
 N
.




  Hint
 Resolve
 red1_par_red1: coc
.




  Lemma
 red_par_red : ∀ M
 N
, red M
 N
 → par_red M
 N
.




  Lemma
 par_red_red : ∀ M
 N
, par_red M
 N
 → red M
 N
.




  Hint
 Resolve
 red_par_red par_red_red: coc
.




  Lemma
 par_red1_lift :

   ∀ n
 (a
 b
 : term),

   par_red1 a
 b
 → ∀ k
, par_red1 (lift_rec n
 a
 k
) (lift_rec n
 b
 k
).




  Lemma
 par_red1_subst :

   ∀ c
 d
 : term,

   par_red1 c
 d
 →

   ∀ a
 b
 : term,

   par_red1 a
 b
 → ∀ k
, par_red1 (subst_rec a
 c
 k
) (subst_rec b
 d
 k
).




  Lemma
 inv_par_red_abs :

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

   par_red1 (Abs T
 U
) x
 →

   (∀ T'
 (U'
 : term), x
 = Abs T'
 U'
 → par_red1 U
 U'
 → P
) → P
.




  Lemma
 inv_par_red_pair :

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

   par_red1 (Pair T
 U
 V
) x
 →

   (∀ T'
 (U'
 V'
 : term), x
 = Pair T'
 U'
 V'
 → par_red1 U
 U'
 → par_red1 V
 V'
 → P
) → P
.




  Hint
 Resolve
 par_red1_lift par_red1_subst: coc
.




  Lemma
 subterm_abs : ∀ t
 (m
 : term), subterm m
 (Abs t
 m
).




  Lemma
 subterm_prod : ∀ t
 (m
 : term), subterm m
 (Prod t
 m
).




  Lemma
 subterm_sum : ∀ t
 (m
 : term), subterm m
 (Sum t
 m
).




  Lemma
 subterm_subset : ∀ t
 (m
 : term), subterm m
 (Subset t
 m
).




Hint
 Resolve
 subterm_abs subterm_prod subterm_sum subterm_subset

 : coc
.







  Lemma
 mem_sort_lift :

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




  Lemma
 mem_sort_subst :

   ∀ (b
 a
 : term) n
 s
,

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




  Lemma
 red_sort_mem : ∀ t
 s
, red t
 (Srt s
) → mem_sort s
 t
.




  Lemma
 red_normal : ∀ u
 v
, red u
 v
 → normal u
 → u
 = v
.




  Lemma
 sn_red_sn : ∀ a
 b
 : term, sn a
 → red a
 b
 → sn b
.




  Lemma
 commut_red1_subterm : commut _
 subterm (transp _
 red1).




 Lemma
 subterm_sn :

   ∀ a
 : term, sn a
 → ∀ b
 : term, subterm b
 a
 → sn b
.




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




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




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




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




  Lemma
 sn_subst : ∀ T
 M
, sn (subst T
 M
) → sn M
.