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.