(** * 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.


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

(** 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.
intros M; induction M; destruct N; intros;
simpl in *; try (discriminate || intuition); (try (destruct (le_gt_dec m v) ; discriminate)).
destruct (le_gt_dec m v); destruct (le_gt_dec m v0) ; injection H; intros; subst; intuition.
apply plus_reg_l in H0; rewrite H0; trivial. 
elim (lt_irrefl m). apply le_lt_trans with v. trivial. induction n; intuition.
elim (lt_irrefl v0). apply lt_le_trans with m. induction n; intuition. trivial.
injection H; intros; rewrite (IHM1 N1 n m H1); rewrite (IHM2 N2 n m H0); reflexivity.
injection H; intros; rewrite (IHM1 N1 n m H1); rewrite (IHM2 N2 n (S m) H0); reflexivity.
injection H; intros; rewrite (IHM1 N1 n m H1); rewrite (IHM2 N2 n (S m) H0); reflexivity.
Qed.

Lemma lift_rec0 : forall M n, M ↑ 0 # n = M.
induction M; intros; simpl.
destruct (le_gt_dec n v); reflexivity.
reflexivity.
rewrite IHM1; rewrite IHM2; reflexivity.
rewrite IHM1; rewrite IHM2; reflexivity.
rewrite IHM1; rewrite IHM2; reflexivity. 
Qed.

Lemma lift0 : forall M, M ↑ 0 = M .
intros; apply lift_rec0.
Qed.

Lemma liftP1 : forall M i j  k, (M ↑ j # i) ↑ k # (j+i) = M ↑ (j+k) # i.
intros M; induction M; intros;simpl.
destruct (le_gt_dec i v); simpl.
destruct (le_gt_dec (j+i) (j+v)); simpl. 
rewrite plus_assoc. replace (k+j) with (j+k) by (apply plus_comm).  trivial. 
apply plus_gt_reg_l in g. elim (lt_irrefl v).
apply lt_le_trans with i; intuition.
simpl; destruct (le_gt_dec (j+i)); intuition.
elim (lt_irrefl v).
apply lt_le_trans with i; intuition. induction j; intuition.
reflexivity.
rewrite IHM1;rewrite IHM2;reflexivity.
rewrite IHM1; rewrite <-IHM2 ;replace (j+S i) with (S(j+i)) by intuition; reflexivity.
rewrite IHM1; rewrite <- IHM2 ;replace (j+S i) with (S(j+i)) by intuition; reflexivity.
Qed.

Lemma liftP2: forall M i j k n, i <= n ->
  (M ↑ j # i) ↑ k # (j+n) = (M ↑ k # n) ↑ j # i.
intro M; induction M; intros; simpl.
destruct (le_gt_dec i v); destruct (le_gt_dec n v).
simpl.
destruct le_gt_dec. destruct le_gt_dec.
rewrite 2! plus_assoc. replace (k+j) with (j+k) by (apply plus_comm).  trivial. 
elim (lt_irrefl v). apply lt_le_trans with i. induction k; intuition. trivial.
apply plus_gt_reg_l in g. elim (lt_irrefl v).
apply lt_le_trans with n; intuition.
simpl.
destruct le_gt_dec. apply plus_le_reg_l in l0. elim (lt_irrefl v).
apply lt_le_trans with n; intuition. destruct le_gt_dec. trivial.
elim (lt_irrefl v). apply lt_le_trans with i; intuition.
simpl. destruct le_gt_dec. elim (lt_irrefl n). apply lt_le_trans with i.
apply le_lt_trans with v; intuition. trivial. elim (lt_irrefl v).
apply lt_le_trans with n. apply lt_le_trans with i; intuition. trivial.
simpl. destruct le_gt_dec. elim (lt_irrefl v). apply lt_le_trans with n.
intuition. induction j; intuition. destruct le_gt_dec. elim (lt_irrefl i).
apply le_lt_trans with v; intuition. trivial.
trivial.

rewrite IHM1; intuition;  rewrite IHM2; intuition;  reflexivity.
rewrite IHM1; intuition.
replace (S(j+n)) with (j+S n) by intuition.
rewrite (IHM2 (S i) j k (S n)); intuition.
rewrite IHM1; intuition.
replace (S(j+n)) with (j+S n) by intuition.
rewrite (IHM2 (S i) j k (S n) ); intuition.
Qed.

Lemma liftP3 : forall M i k j n , i <= k -> k <= (i+n) ->
  (M ↑ n # i) ↑ j # k = M ↑ (j+n) # i.
intro M; induction M; intros; simpl.
destruct (le_gt_dec i v); simpl.
destruct (le_gt_dec k (n+v)); intuition.
elim (lt_irrefl (i+n)). apply lt_le_trans with k.
apply le_lt_trans with (n+v). rewrite plus_comm. intuition. intuition. trivial.
destruct (le_gt_dec k v); intuition. elim (lt_irrefl k).
apply lt_le_trans with i.  apply le_lt_trans with v. trivial. intuition. trivial.
reflexivity.
rewrite IHM1; intuition;rewrite IHM2; intuition.
rewrite IHM1; intuition;rewrite IHM2; intuition. change (S i + n) with (S (i+n)). intuition.
rewrite IHM1; intuition; rewrite IHM2; intuition. change (S i + n) with (S (i+n)). intuition.
Qed.


Lemma lift_lift : forall M n m, (M ↑ m) ↑ n  = M↑ (n+m).
intros.
apply liftP3; intuition.
Qed.


(** 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 (* v < n *)
      | inleft (right _) => U ↑ n  (* v = n *)
      | inright _ => # (x - 1) (* v > n *)
      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 ) ].
intros M; induction M; intros.
simpl (#v [j ← N] ↑ k # (j+i)).
change (#v ↑ k # (S (j+i))) with  (if le_gt_dec (S (j+i)) v then #(k+v) else #v).
destruct (lt_eq_lt_dec v j) as [[] | ].
destruct (le_gt_dec (S (j+i)) v).
elim (lt_irrefl v). apply lt_le_trans with j; intuition.
apply le_trans with (S (j+i)); intuition.
simpl.
destruct (le_gt_dec (j+i) v).
elim (lt_irrefl v). apply lt_le_trans with j; intuition. apply le_trans with (j+i); intuition.
destruct (lt_eq_lt_dec v j) as [[] | ]. trivial.
subst. elim (lt_irrefl j);trivial.
elim (lt_irrefl j); apply lt_trans with v; trivial.
destruct (le_gt_dec (S(j+i)) v). subst.
elim (lt_irrefl j). apply lt_le_trans with (S (j+i)). intuition. trivial.
simpl. destruct (lt_eq_lt_dec v j) as [[] | ].
subst. elim (lt_irrefl j); trivial.
apply liftP2; intuition.
subst. elim (lt_irrefl j); trivial.
destruct (le_gt_dec (S (j+i)) v).
simpl.
destruct (le_gt_dec (j+i) (v-1)). destruct (lt_eq_lt_dec (k+v) j) as [[] | ].
elim (lt_irrefl j). apply lt_le_trans with v. trivial. induction k; intuition.
subst. elim (lt_irrefl v). apply lt_le_trans with (S(k+v+i)). intuition. trivial.
destruct v. apply lt_n_O in l; elim l. rewrite <- 2! pred_of_minus. replace (k+ S v) with (S (k+v)) by intuition.
simpl. trivial.
elim (lt_irrefl v). apply lt_le_trans with (S (j+i)). destruct v. apply lt_n_O in l; elim l. 
rewrite <- pred_of_minus in g. simpl in g. intuition. trivial.
simpl.
destruct (le_gt_dec (j+i) (v-1)). destruct (lt_eq_lt_dec v j) as [[] | ].
elim (lt_irrefl j); apply lt_trans with v; trivial.
subst. elim (lt_irrefl j); trivial.
elim (lt_irrefl v). apply lt_le_trans with (S (j+i)). intuition. 
destruct v. apply lt_n_O in l; elim l. rewrite <- pred_of_minus in l0. simpl in l0. intuition.
destruct (lt_eq_lt_dec) as [[] | ]. elim (lt_irrefl j); apply lt_trans with v; trivial.
subst. elim (lt_irrefl j); trivial. trivial.
simpl; trivial.
simpl; rewrite IHM1; intuition; rewrite IHM2; intuition.
simpl; rewrite IHM1; intuition.
replace (S(S(j+i))) with (S((S j)+i)) by intuition.
rewrite <- (IHM2 N i (S j)  k ); intuition.
simpl; rewrite IHM1; intuition.
replace (S(S(j+i))) with ((S ((S j)+i))) by intuition.
rewrite <- (IHM2 N i (S j)  k ); intuition.
Qed.

Lemma substP2: forall M N i j n, i <= n ->
  (M ↑ j # i ) [ j+n ← N ] = ( M [ n ← N]) ↑ j # i .
intro M; induction M; intros; simpl.
destruct (le_gt_dec i v); destruct (lt_eq_lt_dec v n) as [[] | ].
simpl.
destruct (le_gt_dec i v).  destruct (lt_eq_lt_dec (j+v) (j+n)) as [[] | ].
reflexivity.
apply plus_reg_l in e. subst. elim (lt_irrefl n); trivial.
apply plus_lt_reg_l in l2. elim (lt_asym v n); trivial.
elim (lt_irrefl i). apply le_lt_trans with v; intuition. subst.
simpl.
destruct (lt_eq_lt_dec (j+n) (j+n)) as [[] | ].
apply lt_irrefl in l0; elim l0.
symmetry.
apply liftP3; intuition.
apply lt_irrefl in l0; elim l0.
simpl.
destruct (le_gt_dec i (v-1)). destruct (lt_eq_lt_dec (j+v) (j+n))as [[] | ].
apply plus_lt_reg_l in l2. elim (lt_asym  v n ); trivial.
apply plus_reg_l in e; subst. elim (lt_irrefl n); trivial.
destruct v. apply lt_n_O in l0; elim l0. rewrite <- 2! pred_of_minus. replace (j+ S v) with (S (j+v)) by intuition.
simpl. trivial.
unfold gt in g. unfold lt in g. rewrite <- pred_of_minus in g. 
rewrite <- (S_pred  v n l0) in g.
elim (lt_irrefl n). apply lt_le_trans with v; trivial. apply le_trans with i; trivial.
simpl. 
destruct (le_gt_dec i v).  elim (lt_irrefl i). apply le_lt_trans with v; trivial.
destruct (lt_eq_lt_dec v (j+n)) as [[] | ]. reflexivity.
subst. elim (lt_irrefl n). apply le_lt_trans with (j+n); intuition. 
elim (lt_irrefl n). apply lt_trans with v.  apply le_lt_trans with (j+n); intuition. trivial.
simpl. subst. 
elim (lt_irrefl n). apply lt_le_trans with i; intuition.
simpl. elim (lt_irrefl n). apply lt_le_trans with v; intuition.
apply le_trans with i; intuition.
trivial.

rewrite IHM1; intuition;rewrite IHM2; intuition.
rewrite IHM1; intuition;
rewrite <- (IHM2 N (S i) j (S n)); intuition.
replace (S(j+n)) with (j+(S n)) by intuition.
reflexivity.
rewrite IHM1; intuition;
rewrite <- (IHM2 N (S i) j (S n)); intuition.
replace (S(j+n)) with (j+(S n)) by intuition.
reflexivity.
Qed.


Lemma substP3: forall M N i  k n, i <= k -> k <= i+n ->
  (M↑ (S n) # i) [ k← N] = M ↑ n # i.
intro M; induction M; intros; simpl.
destruct (le_gt_dec i v).
unfold subst_rec.
destruct (lt_eq_lt_dec (S(n+v)) k) as [[] | ].
elim (lt_irrefl (i+n)). apply lt_le_trans with k; intuition.
apply le_lt_trans with (v+n). intuition. rewrite plus_comm; intuition.
subst. replace (i+n) with (n+i) in H0 by (apply plus_comm) . replace (S (n+v)) with (n + S v) in H0 by intuition. 
apply plus_le_reg_l in H0. elim (lt_irrefl i). apply le_lt_trans with v; intuition.
simpl. rewrite <- minus_n_O. trivial.
simpl. destruct (lt_eq_lt_dec v k) as [[] | ].
reflexivity. subst. elim (lt_irrefl i). apply le_lt_trans with k; intuition.
elim (lt_irrefl k). apply lt_trans with v; trivial. apply lt_le_trans with i; intuition.

reflexivity.
rewrite IHM1; intuition;rewrite IHM2; intuition.
rewrite IHM1; intuition; rewrite <- (IHM2 N (S i) (S k) n); intuition.
change (S i + n) with (S (i+n)). intuition.
rewrite IHM1; intuition; rewrite <- (IHM2 N (S i) (S k) n); intuition.
change (S i + n) with (S (i+n)). intuition.
Qed.

Lemma substP4: forall M N P i j, 
   (M [ i← N]) [i+j ← P] = (M [S(i+j) ← P]) [i← N[j← P]].
intro M; induction M; intros; simpl.
destruct (lt_eq_lt_dec v i) as [[] | ] ; destruct (lt_eq_lt_dec v (S(i+j))) as [[] | ].
simpl.
destruct (lt_eq_lt_dec v (i+j)) as [[] | ]. destruct (lt_eq_lt_dec v i) as [[] | ].
trivial.
subst. apply lt_irrefl in l; elim l. elim ( lt_asym v i); trivial.
subst. rewrite plus_comm in l. elim (lt_irrefl i). induction j; simpl in *; intuition.
elim (lt_irrefl i). apply le_lt_trans with v;intuition. rewrite plus_comm in l1; intuition.  induction j; simpl in *; intuition.
subst. elim (lt_irrefl i). apply lt_trans with (S (i+j)); intuition.
elim (lt_irrefl i). apply lt_trans with (S (i+j)); intuition. apply lt_trans with v; trivial.
simpl. subst. destruct (lt_eq_lt_dec i i) as [[] | ].
elim (lt_irrefl i); trivial. apply substP2; intuition.
elim (lt_irrefl i); trivial.
subst. rewrite plus_comm in e0. apply succ_plus_discr in e0. elim e0.
subst. elim (lt_irrefl i). apply le_lt_trans with (i+j); intuition.
simpl.
destruct (lt_eq_lt_dec (v-1) (i+j)) as  [[] | ]. destruct (lt_eq_lt_dec v i) as [[] | ].
elim (lt_asym v i); trivial. subst. elim (lt_irrefl i); trivial.
trivial. rewrite <- e in l0. rewrite <- pred_of_minus in l0.
rewrite <- (S_pred  v i l) in l0. elim (lt_irrefl v); trivial.
apply lt_n_S in l1. elim (lt_irrefl v).
apply lt_trans with (S(i+j)); trivial.
rewrite <- pred_of_minus in l1. rewrite <- (S_pred  v i l) in l1. trivial. 
subst. simpl. rewrite <- minus_n_O.
destruct (lt_eq_lt_dec (i+j) (i+j)) as [[] | ].
elim (lt_irrefl (i+j)) ; trivial.
symmetry. apply substP3; intuition.
elim (lt_irrefl (i+j)) ; trivial.
simpl.
destruct (lt_eq_lt_dec (v-1) (i+j)) as  [[] | ].
elim (lt_irrefl v). apply lt_trans with (S (i+j)) ;trivial.
apply lt_n_S in l1. rewrite <- pred_of_minus in l1. rewrite <- (S_pred v i l) in l1. trivial.
apply eq_S in e. rewrite <- pred_of_minus in e. rewrite <- (S_pred v i l) in e.
subst. elim (lt_irrefl (S(i+j))); trivial.
destruct (lt_eq_lt_dec (v-1) i) as [[] | ].
elim (lt_irrefl v). apply le_lt_trans with i; trivial. destruct v. apply lt_n_O in l; elim l.
rewrite <- pred_of_minus in l2. simpl in l2. trivial.
destruct v. elim (lt_n_O i); trivial. rewrite <- pred_of_minus in e. simpl in e. subst.
rewrite <- pred_of_minus in l1. simpl in l1. elim (lt_irrefl i).
apply le_lt_trans with (i+j); intuition.
trivial.
trivial.
rewrite IHM1; rewrite IHM2; intuition.
rewrite IHM1; replace (S(S(i+j))) with (S((S i)+ j)) by intuition;
  rewrite <- (IHM2 N P (S i)); replace (S(i+j)) with ((S i)+ j) by intuition; intuition.
rewrite IHM1; replace (S(S(i+j))) with (S((S i)+j)) by intuition;
  rewrite <- (IHM2 N P (S i)); replace (S(i+j)) with ((S i)+ j) by intuition; intuition.
Qed.

Lemma subst_travers : 
 forall  M N P n, (M [← N]) [n ← P] = (M [n+1 ← P])[← N[n← P]].
intros.
rewrite plus_comm. change n with (O+n). apply substP4.
Qed.

(** 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.
induction M; intros.
unfold lift_rec.
destruct (le_gt_dec (S n) v). unfold subst_rec.
destruct (lt_eq_lt_dec (1+v) n) as [[] | ].
apply le_not_lt in l. elim l. intuition.
elim (lt_irrefl v). apply lt_le_trans with (S (S v)). intuition. subst; trivial.
change (1+v) with (S v). destruct v; simpl; trivial.
simpl.
destruct (lt_eq_lt_dec v n) as [[] | ].
trivial.
simpl; subst; trivial.
rewrite <- plus_n_O. trivial.
elim (lt_irrefl n). apply lt_le_trans with v; intuition.
simpl; trivial.
simpl. rewrite IHM1. rewrite IHM2. reflexivity.
simpl. rewrite IHM1. rewrite IHM2. reflexivity.
simpl. rewrite IHM1. rewrite IHM2. reflexivity.
Qed.

End ut_term_mod.