Library TermECC


Require Export Arith.
Require Export Compare_dec.
Require Export Relations.

Hint Resolve t_step rt_step rt_refl: core.
Hint Unfold transp: core.

Section Termes.

  Inductive sort : Set :=
    | kind : nat -> sort
    | prop : sort.

  Inductive term : Set :=
    | Srt : sort -> term
    | Ref : nat -> term
    | Abs : term -> term -> term
    | App : term -> term -> term
    | Prod : term -> term -> term.

  Fixpoint lift_rec (n : nat) (t : term) (k : nat) {struct t} : term :=
    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)
    | Prod A B => Prod (lift_rec n A k) (lift_rec n B (S k))
    end.

  Definition lift n t := lift_rec n t 0.

  Fixpoint subst_rec (N M : term) (k : nat) {struct M} : term :=
    match M with
    | Srt s => Srt s
    | Ref i =>
        match lt_eq_lt_dec k i with
        | inleft (left _) => Ref (pred i)
        | inleft (right _) => lift k N
        | 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)
    | Prod T U => Prod (subst_rec N T k) (subst_rec N U (S k))
    end.

  Definition subst N M := subst_rec N M 0.

  Inductive subterm : term -> term -> Prop :=
    | sbtrm_abs_l : forall A B, subterm A (Abs A B)
    | sbtrm_abs_r : forall A B, subterm B (Abs A B)
    | sbtrm_app_l : forall A B, subterm A (App A B)
    | sbtrm_app_r : forall A B, subterm B (App A B)
    | sbtrm_prod_l : forall A B, subterm A (Prod A B)
    | sbtrm_prod_r : forall A B, subterm B (Prod A B).

  Inductive mem_sort (s : sort) : term -> Prop :=
    | mem_eq : mem_sort s (Srt s)
    | mem_prod_l : forall u v, mem_sort s u -> mem_sort s (Prod u v)
    | mem_prod_r : forall u v, mem_sort s v -> mem_sort s (Prod u v)
    | mem_abs_l : forall u v, mem_sort s u -> mem_sort s (Abs u v)
    | mem_abs_r : forall u v, mem_sort s v -> mem_sort s (Abs u v)
    | mem_app_l : forall u v, mem_sort s u -> mem_sort s (App u v)
    | mem_app_r : forall u v, mem_sort s v -> mem_sort s (App u v).

End Termes.

  Hint Constructors subterm: coc.
  Hint Constructors mem_sort: coc.

Section Beta_Reduction.

  Inductive red1 : term -> term -> Prop :=
    | beta : forall M N T, red1 (App (Abs T M) N) (subst N M)
    | abs_red_l :
        forall M M', red1 M M' -> forall N, red1 (Abs M N) (Abs M' N)
    | abs_red_r :
        forall M M', red1 M M' -> forall N, red1 (Abs N M) (Abs N M')
    | app_red_l :
        forall M1 N1, red1 M1 N1 -> forall M2, red1 (App M1 M2) (App N1 M2)
    | app_red_r :
        forall M2 N2, red1 M2 N2 -> forall M1, red1 (App M1 M2) (App M1 N2)
    | prod_red_l :
        forall M1 N1, red1 M1 N1 -> forall M2, red1 (Prod M1 M2) (Prod N1 M2)
    | prod_red_r :
        forall M2 N2, red1 M2 N2 -> forall M1, red1 (Prod M1 M2) (Prod M1 N2).

  Inductive red (M : term) : term -> Prop :=
    | refl_red : red M M
    | trans_red : forall P N, red M P -> red1 P N -> red M N.

  Inductive conv (M : term) : term -> Prop :=
    | refl_conv : conv M M
    | trans_conv_red : forall P N, conv M P -> red1 P N -> conv M N
    | trans_conv_exp : forall P N, conv M P -> red1 N P -> conv M N.

  Inductive par_red1 : term -> term -> Prop :=
    | par_beta :
        forall M M' N N' T,
        par_red1 M M' ->
        par_red1 N N' -> par_red1 (App (Abs T M) N) (subst N' M')
    | sort_par_red : forall s, par_red1 (Srt s) (Srt s)
    | ref_par_red : forall n, par_red1 (Ref n) (Ref n)
    | abs_par_red :
        forall M M' T T',
        par_red1 M M' -> par_red1 T T' -> par_red1 (Abs T M) (Abs T' M')
    | app_par_red :
        forall M M' N N',
        par_red1 M M' -> par_red1 N N' -> par_red1 (App M N) (App M' N')
    | prod_par_red :
        forall M M' N N',
        par_red1 M M' -> par_red1 N N' -> par_red1 (Prod M N) (Prod M' N').

  Definition par_red := clos_trans term par_red1.

End Beta_Reduction.

  Hint Constructors red1: coc.
  Hint Constructors par_red1: coc.
  Hint Resolve refl_red refl_conv: coc.
  Hint Unfold par_red: coc.

Section Normalisation_Forte.

  Definition normal t := forall u, ~ red1 t u.

  Definition sn := Acc (transp _ red1).

End Normalisation_Forte.

  Hint Unfold sn: coc.

  Lemma inv_lift_sort : forall s n t k, lift_rec n t k = Srt s -> t = Srt s.

  Lemma inv_subst_sort :
    forall s x t k, subst_rec x t k = Srt s -> t = Srt s \/ x = Srt s.

  Lemma lift_ref_ge :
   forall k n p, p <= n -> lift_rec k (Ref n) p = Ref (k + n).

  Lemma lift_ref_lt : forall k n p, p > n -> lift_rec k (Ref n) p = Ref n.

  Lemma subst_ref_lt : forall u n k, k > n -> subst_rec u (Ref n) k = Ref n.

  Lemma subst_ref_gt :
   forall u n k, n > k -> subst_rec u (Ref n) k = Ref (pred n).

  Lemma subst_ref_eq : forall u n, subst_rec u (Ref n) n = lift n u.

  Lemma lift_rec0 : forall M k, lift_rec 0 M k = M.

  Lemma lift0 : forall M, lift 0 M = M.

  Lemma simpl_lift_rec :
   forall M n k p i,
   i <= k + n ->
   k <= i -> lift_rec p (lift_rec n M k) i = lift_rec (p + n) M k.

  Lemma simpl_lift : forall M n, lift (S n) M = lift 1 (lift n M).

  Lemma permute_lift_rec :
   forall M n k p i,
   i <= k ->
   lift_rec p (lift_rec n M k) i = lift_rec n (lift_rec p M i) (p + k).

  Lemma permute_lift :
   forall M k, lift 1 (lift_rec 1 M k) = lift_rec 1 (lift 1 M) (S k).

  Lemma simpl_subst_rec :
   forall N M n p k,
   p <= n + k ->
   k <= p -> subst_rec N (lift_rec (S n) M k) p = lift_rec n M k.

  Lemma simpl_subst :
   forall N M n p, p <= n -> subst_rec N (lift (S n) M) p = lift n M.

  Lemma commut_lift_subst_rec :
   forall M N n p k,
   k <= p ->
   lift_rec n (subst_rec N M p) k = subst_rec N (lift_rec n M k) (n + p).

  Lemma commut_lift_subst :
   forall M N k, subst_rec N (lift 1 M) (S k) = lift 1 (subst_rec N M k).

  Lemma distr_lift_subst_rec :
   forall M N n p k,
   lift_rec n (subst_rec N M p) (p + k) =
   subst_rec (lift_rec n N k) (lift_rec n M (S (p + k))) p.

  Lemma distr_lift_subst :
   forall M N n k,
   lift_rec n (subst N M) k = subst (lift_rec n N k) (lift_rec n M (S k)).

  Lemma distr_subst_rec :
   forall M N P n p,
   subst_rec P (subst_rec N M p) (p + n) =
   subst_rec (subst_rec P N n) (subst_rec P M (S (p + n))) p.

  Lemma distr_subst :
   forall P N M k,
   subst_rec P (subst N M) k = subst (subst_rec P N k) (subst_rec P M (S k)).

  Lemma one_step_red : forall M N, red1 M N -> red M N.

  Hint Resolve one_step_red: coc.

  Lemma red1_red_ind :
   forall N P,
   (P:term -> Prop) N ->
   (forall M R, red1 M R -> red R N -> P R -> P M) ->
   forall M, red M N -> P M.

  Lemma trans_red_red : forall M N P, red M N -> red N P -> red M P.

  Lemma red_red_app :
   forall u u0 v v0, red u u0 -> red v v0 -> red (App u v) (App u0 v0).

  Lemma red_red_abs :
   forall u u0 v v0, red u u0 -> red v v0 -> red (Abs u v) (Abs u0 v0).

  Lemma red_red_prod :
   forall u u0 v v0, red u u0 -> red v v0 -> red (Prod u v) (Prod u0 v0).

  Hint Resolve red_red_app red_red_abs red_red_prod: coc.

  Lemma red1_lift :
   forall n u v, red1 u v -> forall k, red1 (lift_rec n u k) (lift_rec n v k).

  Hint Resolve red1_lift: coc.

  Lemma red1_subst_r :
   forall a t u,
   red1 t u -> forall k, red1 (subst_rec a t k) (subst_rec a u k).

  Lemma red1_subst_l :
   forall t u,
   red1 t u -> forall a k, red (subst_rec t a k) (subst_rec u a k).

  Hint Resolve red1_subst_l red1_subst_r: coc.

  Lemma red_prod_prod :
   forall u v t,
   red (Prod u v) t ->
   forall P : Prop,
   (forall a b, t = Prod a b -> red u a -> red v b -> P) -> P.

  Lemma red_sort_sort : forall s t, red (Srt s) t -> t <> Srt s -> False.

  Lemma one_step_conv_exp : forall M N, red1 M N -> conv N M.

  Lemma red_conv : forall M N, red M N -> conv M N.

  Hint Resolve one_step_conv_exp red_conv: coc.

  Lemma sym_conv : forall M N, conv M N -> conv N M.

  Hint Immediate sym_conv: coc.

  Lemma trans_conv_conv : forall M N P, conv M N -> conv N P -> conv M P.

  Lemma conv_conv_prod :
   forall a b c d, conv a b -> conv c d -> conv (Prod a c) (Prod b d).

  Lemma conv_conv_lift :
   forall a b n k, conv a b -> conv (lift_rec n a k) (lift_rec n b k).

  Lemma conv_conv_subst :
   forall a b c d k,
   conv a b -> conv c d -> conv (subst_rec a c k) (subst_rec b d k).

  Hint Resolve conv_conv_prod conv_conv_lift conv_conv_subst: coc.

  Lemma refl_par_red1 : forall M, par_red1 M M.

  Hint Resolve refl_par_red1: coc.

  Lemma red1_par_red1 : forall M N, red1 M N -> par_red1 M N.

  Hint Resolve red1_par_red1: coc.

  Lemma red_par_red : forall M N, red M N -> par_red M N.

  Lemma par_red_red : forall M N, par_red M N -> red M N.

  Hint Resolve red_par_red par_red_red: coc.

  Lemma par_red1_lift :
   forall n a b,
   par_red1 a b -> forall k, par_red1 (lift_rec n a k) (lift_rec n b k).

  Lemma par_red1_subst :
   forall a b c d,
   par_red1 a b ->
   par_red1 c d -> forall k, par_red1 (subst_rec a c k) (subst_rec b d k).

  Lemma inv_par_red_abs :
   forall (P : Prop) T U x,
   par_red1 (Abs T U) x ->
   (forall T' U', x = Abs T' U' -> par_red1 U U' -> P) -> P.

  Hint Resolve par_red1_lift par_red1_subst: coc.

  Lemma mem_sort_lift :
   forall t n k s, mem_sort s (lift_rec n t k) -> mem_sort s t.

  Lemma mem_sort_subst :
   forall b a n s,
   mem_sort s (subst_rec a b n) -> mem_sort s a \/ mem_sort s b.

  Lemma red_sort_mem : forall t s, red t (Srt s) -> mem_sort s t.

  Lemma red_normal : forall u v, red u v -> normal u -> u = v.

  Lemma sn_red_sn : forall a b, sn a -> red a b -> sn b.

  Lemma commut_red1_subterm : commut _ subterm (transp _ red1).

  Lemma subterm_sn : forall a, sn a -> forall b, subterm b a -> sn b.

  Lemma sn_prod : forall A, sn A -> forall B, sn B -> sn (Prod A B).

  Lemma sn_subst : forall T M, sn (subst T M) -> sn M.