Library ut_term

Term definition for PTS and de Bruijn manipulation .

Usual Term syntax .

Require Import Peano_dec.
Require Import Compare_dec.
Require Import Lt.
Require Import Le.
Require Import Gt.
Require Import Plus.
Require Import Minus.
Require Import Bool.
Require Import base.

Module Type ut_term_mod (X: term_sig).
  Import X.
Term syntax:
Inductive Term : Set:=
 | Var : Vars -> Term
 | Sort : Sorts -> Term
 | App : Term -> Term -> Term
 | Pi : Term -> Term -> Term
 | La :Term -> Term -> Term
.

Notation "x · y" := (App x y) (at level 15, left associativity) : UT_scope.
Notation "! s" := (Sort s) (at level 1) : UT_scope.
Notation "# v" := (Var v) (at level 1) : UT_scope.
Notation "'Π' ( U ) , V " := (Pi U V) (at level 20, U, V at level 30) : UT_scope.
Notation "'λ' [ U ] , v " := (La U v) (at level 20, U , v at level 30) : UT_scope.

Reserved Notation " t ↑ x # n " (at level 5, x at level 0, left associativity).

Delimit Scope UT_scope with UT.

Open Scope UT_scope.

In order to deal with variable bindings and captures, we need a lift function to deal with free and bounded variables.

Mn # m recursivly add n to all variables that are above m in M.
Fixpoint lift_rec (n:nat) (k:nat) (T:Term) {struct T} := match T with
   | # x => if le_gt_dec k x then Var (n+x) else Var x
   | ! s => Sort s
   | M · N => App (M n # k) (N n # k)
   | Π ( A ), B => Π (A n # k), (B n # (S k))
   | λ [ A ], M => λ [A n # k], (M n # (S k))
 end
   where "t ↑ n # k" := (lift_rec n k t) : UT_scope.

Notation " t ↑ n " := (lift_rec n 0 t) (at level 5, n at level 0, left associativity) : UT_scope.

Some basic properties of the lift function. That is everything we will ever need to handle de Bruijn indexes

Lemma inv_lift : forall M N n m , M n # m = N n # m -> M = N.

Lemma lift_rec0 : forall M n, M 0 # n = M.

Lemma lift0 : forall M, M 0 = M .

Lemma liftP1 : forall M i j k, (M j # i) k # (j+i) = M (j+k) # i.

Lemma liftP2: forall M i j k n, i <= n ->
  (M j # i) k # (j+n) = (M k # n) j # i.

Lemma liftP3 : forall M i k j n , i <= k -> k <= (i+n) ->
  (M n # i) j # k = M (j+n) # i.

Lemma lift_lift : forall M n m, (M m) n = M (n+m).

We will consider the usual implicit substitution without variable capture (this is where the lift operator comes in handy). M [ nN ] replace the variable n in M by the term N.
Reserved Notation "t [ x ← u ]" (at level 5, x at level 0, left associativity).

Fixpoint subst_rec U T n {struct T} :=
 match T with
  | # x => match (lt_eq_lt_dec x n) with
      | inleft (left _) => # x
      | inleft (right _) => U n
      | inright _ => # (x - 1)
      end
  | ! s => ! s
  | M · N => (M [ n U ]) · ( N [ n U ])
  | Π ( A ), B => Π ( A [ n U ] ), (B [ S n U ])
  | λ [ A ], M => λ [ A [ n U ] ], (M [ S n U ])
end
    where " t [ n ← w ] " := (subst_rec w t n) : UT_scope.

Notation " t [ ← w ] " := (subst_rec w t 0) (at level 5) : UT_scope.

Some basic properties of the substitution function. Again, we will only need a few functions to deal with indexes.

Lemma substP1: forall M N i j k ,
  ( M [ j N] ) k # (j+i) = (M k # (S (j+i))) [ j (N k # i ) ].

Lemma substP2: forall M N i j n, i <= n ->
  (M j # i ) [ j+n N ] = ( M [ n N]) j # i .

Lemma substP3: forall M N i k n, i <= k -> k <= i+n ->
  (M (S n) # i) [ k N] = M n # i.

Lemma substP4: forall M N P i j,
   (M [ i N]) [i+j P] = (M [S(i+j) P]) [i N[j P]].

Lemma subst_travers :
 forall M N P n, (M [← N]) [n P] = (M [n+1 P])[← N[n P]].

Tool function usefull when eta-conversion is used, but this is not the case here.
Lemma expand_term_with_subst : forall M n, (M 1 # (S n)) [ n #0 ] = M.

End ut_term_mod.