Library Lambda

Require Export Setoid Morphisms.
Require Import Arith.
Require Export Compare_dec.
Require Export Relations.

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

Section Terms.

Inductive term : Set :=
| Ref (_:nat)
| Abs (body:term)
| App (f arg:term).

Fixpoint lift_rec (n : nat) (t : term) (k : nat) {struct t} : term :=
match t with
| Ref i =>
match le_gt_dec k i with
| left _ => Ref (n + i)
| right _ => Ref i
end
| Abs M => Abs (lift_rec n M (S k))
| App u v => App (lift_rec n u k) (lift_rec n v k)
end.

Definition lift n t := lift_rec n t 0.

Definition K := Abs (Abs (Ref 1)).
Definition App2 f x y := App (App f x) y.

Fixpoint subst_rec (N M : term) (k : nat) {struct M} : term :=
match M with
| 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 B => Abs (subst_rec N B (S k))
| App u v => App (subst_rec N u k) (subst_rec N v k)
end.

Definition subst N M := subst_rec N M 0.

Inductive subterm : term -> term -> Prop :=
| sbtrm_abs : forall B, subterm B (Abs B)
| sbtrm_app_l : forall A B, subterm A (App A B)
| sbtrm_app_r : forall A B, subterm B (App A B).

End Terms.

Hint Constructors subterm.

Section Beta_Reduction.

Inductive red1 : term -> term -> Prop :=
| beta : forall M N, red1 (App (Abs M) N) (subst N M)
| abs_red : forall M M', red1 M M' -> red1 (Abs M) (Abs 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).

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.

Definition redp := clos_trans _ red1.

End Beta_Reduction.

Hint Constructors red red1 conv : coc.

Section StrongNormalisation.

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

Definition sn := Acc (transp _ red1).

End StrongNormalisation.

Hint Unfold sn: coc.

Lemma eqterm : forall u v : term, {u = v} + {u <> v}.

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 red1_beta : forall M N T,
T = subst N M -> red1 (App (Abs M) N) T.

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

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

Instance red_refl : Reflexive red.
Qed.

Instance red_trans : Transitive red.
Qed.

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

Instance app_red_morph : Proper (red ==> red ==> red) App.

Qed.

Lemma red_red_app :
forall u u0, red u u0 ->
forall v v0, red v v0 ->
red (App u v) (App u0 v0).
Hint Resolve red_red_app : coc.
Instance abs_red_morph : Proper (red ==> red) Abs.
Qed.

Lemma red_red_abs :
forall u u0, red u u0 -> red (Abs u) (Abs u0).
Hint Resolve red_red_abs : coc.
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: coc.

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

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

Instance conv_refl : Equivalence conv.

Qed.

Lemma red_sym_conv : forall M N, red M N -> conv N M.
Hint Resolve red_sym_conv : coc.

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

Lemma redp_lift_rec : forall n M M',
redp M M' -> forall k, redp (lift_rec n M k) (lift_rec n M' k).

Lemma redp_abs : forall M M', redp M M' -> redp (Abs M) (Abs M').

Lemma redp_app_l :
forall M1 N1 M2, redp M1 N1 -> redp (App M1 M2) (App N1 M2).

Lemma redp_app_r :
forall M1 M2 N2, redp M2 N2 -> redp (App M1 M2) (App M1 N2).

Hint Resolve redp_abs redp_app_l redp_app_r : coc.

Lemma redp_K : forall M T, redp (App2 K M T) M.

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

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

Lemma sn_red_sn : forall x y, sn x -> red x y -> sn y.

Lemma sn_abs : forall M, sn M -> sn (Abs M).

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

Theorem church_rosser :
forall u v, conv u v -> exists2 t, red u t & red v t.

Theorem confluence :
forall m u v, red m u -> red m v -> exists2 t, red u t & red v t.