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