Library term

Annotated Terms syntax

In this file, we describe a slightly different syntax for terms: we add two annotations to applications. If the head of an application if a function from A to B, we had both informations in the application, in order to keep track of the conversion during the typing that would be impossible to rebuild after.

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.

Term syntax. Notice the two additional Term in the application.

this notation means that the product x y is annotated by the function space A -> B.

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

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

Delimit Scope Typ_scope with Typ.

Same as for usual terms, we need lift and subst functions, with the very same properties. They are just extended to deal with the two annotations.

Open Scope Typ_scope.

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 ·(A, B) N=> App (M ↑ n # k) (A↑ n # k) (B ↑ n # (S 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) : Typ_scope.

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

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).

Reserved Notation "M [ n ← N ]" (at level 5, n 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 ·(A,B) N => (M [ n ← U ]) ·(A[n← U], B [ S 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) : Typ_scope.

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

Lemma expand_term_with_subst : forall M n, (M ↑ 1 # (S n)) [ n ← #0 ] = M.

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]].

End term_mod.