Library ut_term
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.
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.
| 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.
M ↑ n # m recursivly add n to all variables that are above m in M.
M ↑ n # 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.
| # 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 [ n ← N ] 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.
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.