Library Lambda.Terms


Require
 Export
 Arith.

Require
 Export
 Compare_dec.

Require
 Export
 Relations.




Implicit
 Types
 i
 k
 m
 n
 p
 : nat.




Inductive
 sort : Set
 :=

    | kind : sort

    | prop : sort

    | set : sort.




Implicit
 Type
 s
 : sort.




Definition
 is_prop s
 := s
 = prop ∨ s
 = set.




  Lemma
 sort_level_ind :

   ∀ P
 : sort → Prop
,

   P
 kind → (∀ s
, is_prop s
 → P
 s
) → ∀ s
, P
 s
.




  Inductive
 term : Set
 :=

    | Srt : sort → term

    | Ref : nat → term

    | Abs : term → term → term

    | App : term → term → term

    | Pair : term → term → term → term

    | Prod : term → term → term

    | Sum : term → term → term

    | Subset : term → term → term

    | Pi1 : term → term

    | Pi2 : term → term.




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




  Fixpoint
 lift_rec n
 t
 {struct
 t
} : nat → term :=

    fun
 k
 ⇒

      match
 t
 with


        | Srt s
 ⇒ Srt s


        | Ref i
 ⇒

          match
 le_gt_dec k
 i
 with


            | left _
 ⇒ Ref (n
 + i
)

            | right _
 ⇒ Ref i


          end


        | Abs T
 M
 ⇒ Abs (lift_rec n
 T
 k
) (lift_rec n
 M
 (S k
))

        | App u
 v
 ⇒ App (lift_rec n
 u
 k
) (lift_rec n
 v
 k
)

        | Pair T
 A
 B
 ⇒ Pair (lift_rec n
 T
 k
) (lift_rec n
 A
 k
) (lift_rec n
 B
 k
)

        | Prod A
 B
 ⇒ Prod (lift_rec n
 A
 k
) (lift_rec n
 B
 (S k
))

        | Sum A
 B
 ⇒ Sum (lift_rec n
 A
 k
) (lift_rec n
 B
 (S k
))

        | Subset A
 B
 ⇒ Subset (lift_rec n
 A
 k
) (lift_rec n
 B
 (S k
))

        | Pi1 A
 ⇒ Pi1 (lift_rec n
 A
 k
)

        | Pi2 A
 ⇒ Pi2 (lift_rec n
 A
 k
)

      end
.




  Definition
 lift n
 t
 := lift_rec n
 t
 0.




  Fixpoint
 subst_rec N
 M
 {struct
 M
} : nat → term :=

    fun
 k
 ⇒

      match
 M
 with


        | Srt s
 ⇒ Srt s


        | Ref i
 ⇒

          match
 lt_eq_lt_dec k
 i
 with


            | inleft C
 ⇒

              match
 C
 with


                | left _
 ⇒ Ref (pred i
)

                | right _
 ⇒ lift k
 N


              end


            | inright _
 ⇒ Ref i


          end


        | Abs A
 B
 ⇒ Abs (subst_rec N
 A
 k
) (subst_rec N
 B
 (S k
))

        | App u
 v
 ⇒ App (subst_rec N
 u
 k
) (subst_rec N
 v
 k
)

        | Pair T
 A
 B
 ⇒ Pair (subst_rec N
 T
 k
) (subst_rec N
 A
 k
) (subst_rec N
 B
 k
)

        | Prod T
 U
 ⇒ Prod (subst_rec N
 T
 k
) (subst_rec N
 U
 (S k
))

        | Sum T
 U
 ⇒ Sum (subst_rec N
 T
 k
) (subst_rec N
 U
 (S k
))

        | Subset T
 U
 ⇒ Subset (subst_rec N
 T
 k
) (subst_rec N
 U
 (S k
))

        | Pi1 T
 ⇒ Pi1 (subst_rec N
 T
 k
)

        | Pi2 T
 ⇒ Pi2 (subst_rec N
 T
 k
)

    end
.




  Definition
 subst N
 M
 := subst_rec N
 M
 0.




  Inductive
 free_db : nat → term → Prop
 :=

    | db_srt : ∀ n
 s
, free_db n
 (Srt s
)

    | db_ref : ∀ k
 n
, k
 > n
 → free_db k
 (Ref n
)

    | db_abs :

        ∀ k
 A
 M
, free_db k
 A
 → free_db (S k
) M
 → free_db k
 (Abs A
 M
)

    | db_app :

        ∀ k
 u
 v
, free_db k
 u
 → free_db k
 v
 → free_db k
 (App u
 v
)

    | db_pair :

        ∀ k
 T
 u
 v
, free_db k
 T
 → free_db k
 u
 → free_db k
 v
 → free_db k
 (Pair T
 u
 v
)

    | db_prod :

        ∀ k
 A
 B
, free_db k
 A
 → free_db (S k
) B
 → free_db k
 (Prod A
 B
) 

    | db_sum :

        ∀ k
 A
 B
, free_db k
 A
 → free_db (S k
) B
 → free_db k
 (Sum A
 B
)

    | db_subset :

        ∀ k
 A
 B
, free_db k
 A
 → free_db (S k
) B
 → free_db k
 (Subset A
 B
)

    | db_pi1 : ∀ k
 A
, free_db k
 A
 → free_db k
 (Pi1 A
)

    | db_pi2 : ∀ k
 A
, free_db k
 A
 → free_db k
 (Pi2 A
).




  Inductive
 subt_bind T
 M
 : term → Prop
 :=

    | Bsbt_abs : subt_bind T
 M
 (Abs T
 M
)

    | Bsbt_prod : subt_bind T
 M
 (Prod T
 M
)

    | Bsbt_sum : subt_bind T
 M
 (Sum T
 M
)

    | Bsbt_subset : subt_bind T
 M
 (Subset T
 M
).




  Inductive
 subt_nobind (m
 : term) : term → Prop
 :=

    | Nbsbt_abs : ∀ n
 : term, subt_nobind m
 (Abs m
 n
)

    | Nbsbt_app_l : ∀ v
, subt_nobind m
 (App m
 v
)

    | Nbsbt_app_r : ∀ u
, subt_nobind m
 (App u
 m
)

    | Nbsbt_pair_T : ∀ u
 v
, subt_nobind m
 (Pair m
 u
 v
)

    | Nbsbt_pair_l : ∀ T
 v
, subt_nobind m
 (Pair T
 m
 v
)

    | Nbsbt_pair_r : ∀ T
 u
, subt_nobind m
 (Pair T
 u
 m
)

    | Nbsbt_prod : ∀ n
 : term, subt_nobind m
 (Prod m
 n
)

    | Nbsbt_sum : ∀ n
 : term, subt_nobind m
 (Sum m
 n
)

    | Nbsbt_subset : ∀ n
 : term, subt_nobind m
 (Subset m
 n
)

    | Nbsbt_pi1 : subt_nobind m
 (Pi1 m
)

    | Nbsbt_pi2 : subt_nobind m
 (Pi2 m
).




  Inductive
 subterm (m
 n
 : term) : Prop
 :=

    | Sbtrm_bind : ∀ t
, subt_bind t
 m
 n
 → subterm m
 n


    | Sbtrm_nobind : subt_nobind m
 n
 → subterm m
 n
.




  Inductive
 mem_sort s
 : term → Prop
 :=

    | mem_eq : mem_sort s
 (Srt s
)

    | mem_prod_l : ∀ u
 v
, mem_sort s
 u
 → mem_sort s
 (Prod u
 v
)

    | mem_prod_r : ∀ u
 v
, mem_sort s
 v
 → mem_sort s
 (Prod u
 v
)

    | mem_abs_l : ∀ u
 v
, mem_sort s
 u
 → mem_sort s
 (Abs u
 v
)

    | mem_abs_r : ∀ u
 v
, mem_sort s
 v
 → mem_sort s
 (Abs u
 v
)

    | mem_app_l : ∀ u
 v
, mem_sort s
 u
 → mem_sort s
 (App u
 v
)

    | mem_app_r : ∀ u
 v
, mem_sort s
 v
 → mem_sort s
 (App u
 v
)

    | mem_pair_T : ∀ T
 u
 v
, mem_sort s
 T
 → mem_sort s
 (Pair T
 u
 v
)

    | mem_pair_l : ∀ T
 u
 v
, mem_sort s
 u
 → mem_sort s
 (Pair T
 u
 v
)

    | mem_pair_r : ∀ T
 u
 v
, mem_sort s
 v
 → mem_sort s
 (Pair T
 u
 v
)

    | mem_sum_l : ∀ u
 v
, mem_sort s
 u
 → mem_sort s
 (Sum u
 v
)

    | mem_sum_r : ∀ u
 v
, mem_sort s
 v
 → mem_sort s
 (Sum u
 v
)

    | mem_subset_l : ∀ u
 v
, mem_sort s
 u
 → mem_sort s
 (Subset u
 v
)

    | mem_subset_r : ∀ u
 v
, mem_sort s
 v
 → mem_sort s
 (Subset u
 v
)

    | mem_pi1 : ∀ u
, mem_sort s
 u
 → mem_sort s
 (Pi1 u
)

    | mem_pi2 : ∀ u
, mem_sort s
 u
 → mem_sort s
 (Pi2 u
).




Hint
 Resolve
 db_srt db_ref db_abs db_app db_pair db_prod db_sum db_subset db_pi1 db_pi2 : coc
.

Hint
 Resolve
 Bsbt_abs Bsbt_prod Bsbt_sum Bsbt_subset : coc
.

Hint
 Resolve
 Nbsbt_abs Nbsbt_app_l Nbsbt_app_r Nbsbt_pair_T Nbsbt_pair_l

    Nbsbt_pair_r Nbsbt_pi1 Nbsbt_pi2 Nbsbt_prod Nbsbt_sum Nbsbt_subset : coc
.

Hint
 Resolve
 Sbtrm_nobind: coc
.




Hint
 Resolve
 mem_eq mem_prod_l mem_prod_r mem_abs_l mem_abs_r mem_app_l

  mem_app_r mem_pair_T mem_pair_l mem_pair_r : coc
.

Hint
 Resolve
 mem_sum_l mem_sum_r mem_subset_l mem_subset_r mem_pi1 mem_pi2 : coc
.