Library Lambda
Pure lambda terms
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 : ∀ B, subterm B (Abs B)
| sbtrm_app_l : ∀ A B, subterm A (App A B)
| sbtrm_app_r : ∀ A B, subterm B (App A B).
Inductive occur (n:nat) : term -> Prop :=
| occ_var : occur n (Ref n)
| occ_app_l : ∀ A B, occur n A -> occur n (App A B)
| occ_app_r : ∀ A B, occur n B -> occur n (App A B)
| occ_abs : ∀ M, occur (S n) M -> occur n (Abs M).
Fixpoint boccur (n:nat) (t:term) :=
match t with
| Ref i => if eq_nat_dec n i then true else false
| App u v => orb (boccur n u) (boccur n v)
| Abs m => boccur (S n) m
end.
End Terms.
Hint Constructors subterm occur.
Section Beta_Reduction.
Inductive red1 : term -> term -> Prop :=
| beta : ∀ M N, red1 (App (Abs M) N) (subst N M)
| abs_red : ∀ M M', red1 M M' -> red1 (Abs M) (Abs M')
| app_red_l :
∀ M1 N1, red1 M1 N1 -> ∀ M2, red1 (App M1 M2) (App N1 M2)
| app_red_r :
∀ M2 N2, red1 M2 N2 -> ∀ M1, red1 (App M1 M2) (App M1 N2).
Inductive red (M : term) : term -> Prop :=
| refl_red : red M M
| trans_red : ∀ 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 : ∀ P N, conv M P -> red1 P N -> conv M N
| trans_conv_exp : ∀ 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 := ∀ u, ~ red1 t u.
Definition sn := Acc (transp _ red1).
End StrongNormalisation.
Hint Unfold sn: coc.
Lemma eqterm : ∀ u v : term, {u = v} + {u <> v}.
Lemma lift_ref_ge :
∀ k n p, p <= n -> lift_rec k (Ref n) p = Ref (k + n).
Lemma lift_ref_lt : ∀ k n p, p > n -> lift_rec k (Ref n) p = Ref n.
Lemma subst_ref_lt : ∀ u n k, k > n -> subst_rec u (Ref n) k = Ref n.
Lemma subst_ref_gt :
∀ u n k, n > k -> subst_rec u (Ref n) k = Ref (pred n).
Lemma subst_ref_eq : ∀ u n, subst_rec u (Ref n) n = lift n u.
Lemma lift_rec0 : ∀ M k, lift_rec 0 M k = M.
Lemma lift0 : ∀ M, lift 0 M = M.
Lemma simpl_lift_rec :
∀ 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 : ∀ M n, lift (S n) M = lift 1 (lift n M).
Lemma permute_lift_rec :
∀ 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 :
∀ M k, lift 1 (lift_rec 1 M k) = lift_rec 1 (lift 1 M) (S k).
Lemma simpl_subst_rec :
∀ 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 :
∀ N M n p, p <= n -> subst_rec N (lift (S n) M) p = lift n M.
Lemma commut_lift_subst_rec :
∀ 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 :
∀ M N k, subst_rec N (lift 1 M) (S k) = lift 1 (subst_rec N M k).
Lemma distr_lift_subst_rec :
∀ 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 :
∀ 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 :
∀ 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 :
∀ P N M k,
subst_rec P (subst N M) k = subst (subst_rec P N k) (subst_rec P M (S k)).
Lemma occur_subst : ∀ k t,
occur k t <->
lift_rec 1 (subst_rec (Abs (Ref 0)) t k) k <> t.
Lemma red1_beta : ∀ M N T,
T = subst N M -> red1 (App (Abs M) N) T.
Lemma red1_lift :
∀ n u v, red1 u v -> ∀ k, red1 (lift_rec n u k) (lift_rec n v k).
Lemma red1_subst_r :
∀ a t u,
red1 t u -> ∀ 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 : ∀ 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 :
∀ u u0, red u u0 ->
∀ 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 :
∀ u u0, red u u0 -> red (Abs u) (Abs u0).
Hint Resolve red_red_abs : coc.
Lemma red1_subst_l :
∀ t u,
red1 t u -> ∀ a k, red (subst_rec t a k) (subst_rec u a k).
Hint Resolve red1_subst_l: coc.
Lemma red_conv : ∀ M N, red M N -> conv M N.
Hint Resolve red_conv: coc.
Lemma trans_conv_conv : ∀ M N P, conv M N -> conv N P -> conv M P.
Instance conv_refl : Equivalence conv.
Qed.
Lemma red_sym_conv : ∀ M N, red M N -> conv N M.
Hint Resolve red_sym_conv : coc.
Instance conv_conv_app : Proper (conv ==> conv ==> conv) App.
Qed.
Instance conv_conv_abs : Proper (conv ==> conv) Abs.
Qed.
Lemma conv_conv_lift :
∀ a b n k, conv a b -> conv (lift_rec n a k) (lift_rec n b k).
Lemma conv_conv_subst :
∀ a b c d k,
conv a b -> conv c d -> conv (subst_rec a c k) (subst_rec b d k).
Lemma sn_redp t : sn t -> Acc (transp _ redp) t.
Lemma redp_red_redp x y z :
redp x y -> red y z -> redp x z.
Lemma redp_lift_rec : ∀ n M M',
redp M M' -> ∀ k, redp (lift_rec n M k) (lift_rec n M' k).
Lemma redp_abs : ∀ M M', redp M M' -> redp (Abs M) (Abs M').
Lemma redp_app_l :
∀ M1 N1 M2, redp M1 N1 -> redp (App M1 M2) (App N1 M2).
Lemma redp_app_r :
∀ 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_app_l' :
∀ M1 N1 M2 N2, redp M1 N1 -> red M2 N2 -> redp (App M1 M2) (App N1 N2).
Lemma redp_app_r' :
∀ M1 N1 M2 N2, red M1 N1 -> redp M2 N2 -> redp (App M1 M2) (App N1 N2).
Lemma red1_subst_l_occur :
∀ t u,
red1 t u -> ∀ a k, boccur k a = true -> redp (subst_rec t a k) (subst_rec u a k).
Lemma redp_K : ∀ M T, redp (App2 K M T) M.
Lemma red_lift_inv : ∀ n t u,
red1 t u ->
∀ k t',
t = lift_rec n t' k ->
exists2 u',
red1 t' u' & u = lift_rec n u' k.
Lemma red1_subst_var n t k y :
red1 (subst_rec (Ref n) t k) y ->
exists2 t', red1 t t' & y = subst_rec (Ref n) t' k.
Lemma commut_red1_subterm : commut _ subterm (transp _ red1).
Lemma subterm_sn : ∀ a, sn a -> ∀ b, subterm b a -> sn b.
Lemma sn_red_sn : ∀ x y, sn x -> red x y -> sn y.
Lemma sn_var : ∀ n, sn (Ref n).
Lemma sn_abs : ∀ M, sn M -> sn (Abs M).
Lemma sn_abs_inv t:
sn t -> ∀ m, t = Abs m -> sn m.
Lemma sn_K : sn K.
Lemma sn_lift : ∀ n t k,
sn t -> sn (lift_rec n t k).
Lemma sn_lift_inv : ∀ M', sn M' -> ∀ n M k, M' = lift_rec n M k -> sn M.
Lemma sn_subst_inv_l u m k :
sn (subst_rec u m k) ->
boccur k m = true ->
sn u.
Lemma sn_subst_var n t k :
sn t -> sn (subst_rec (Ref n) t k).
Lemma sn_app_var u n :
sn u -> sn (App u (Ref n)).
Lemma sn_K2_reduced1 :
∀ A, sn A ->
∀ B, sn B ->
sn (App (Abs (lift 1 A)) B).
Lemma sn_K2 :
∀ A, sn A ->
∀ B, sn B ->
sn (App2 K A B).
Lemma sn_subst : ∀ T M, sn (subst T M) -> sn M.
Hint Resolve sn_abs sn_var sn_lift.
Definition neutral t :=
match t with
| Abs _ => False
| _ => True
end.
Inductive nf : term -> Prop :=
| Nf_var : ∀ n, nf (Ref n)
| Nf_app : ∀ u v, neutral u -> nf u -> nf v -> nf (App u v)
| Nf_abs : ∀ t, nf t -> nf (Abs t).
Hint Constructors nf.
Lemma nf_norm : ∀ t, nf t -> ∀ u, ~ red1 t u.
Lemma nf_sound : ∀ t, normal t -> nf t.
Lemma nf_neutral_open : ∀ t,
nf t ->
neutral t ->
exists k, occur k t.
Lemma lift_closed : ∀ m M n k,
k <= n ->
occur n (lift_rec m M k) ->
m+k <= n /\ occur (n-m) M.
Lemma subst_closed : ∀ N M n k,
k <= n ->
occur n (subst_rec N M k) ->
occur (n-k) N \/ occur (S n) M.
Lemma red_closed : ∀ t t',
red t t' ->
∀ k,
occur k t' ->
occur k t.
Lemma red1_dec : ∀ t, {u|red1 t u}+{nf t}.
Lemma norm : ∀ t, sn t -> { u | red t u /\ nf u}.
Section Confluence.
Inductive redpar : term->term->Prop :=
| Redpar_beta m m' n n':
redpar m m' -> redpar n n' -> redpar (App (Abs m) n) (subst n' m')
| Redpar_ref n : redpar (Ref n) (Ref n)
| Redpar_app m m' n n':
redpar m m' -> redpar n n' -> redpar (App m n) (App m' n')
| Redpar_abs m m':
redpar m m' -> redpar (Abs m) (Abs m').
Lemma rp_refl m : redpar m m.
Lemma rp1 m m' : red m m' -> clos_trans _ redpar m m'.
Lemma rp2 m m': clos_trans _ redpar m m' -> red m m'.
Lemma rp_lift n m m' :
redpar m m' ->
∀ k, redpar (lift_rec n m k) (lift_rec n m' k).
Lemma rp_subst m m' n n' k :
redpar m m' ->
redpar n n' ->
redpar (subst_rec n m k) (subst_rec n' m' k).
Lemma confl_rp t t1 :
redpar t t1 -> ∀ t2, redpar t t2 ->
exists2 t3, redpar t1 t3 & redpar t2 t3.
Lemma confl_rp' t t1 :
clos_trans _ redpar t t1 -> ∀ t2, redpar t t2 ->
exists2 t3, redpar t1 t3 & clos_trans _ redpar t2 t3.
Lemma confl_rp'' t t1 :
clos_trans _ redpar t t1 -> ∀ t2, clos_trans _ redpar t t2 ->
exists2 t3, clos_trans _ redpar t1 t3 & clos_trans _ redpar t2 t3.
Theorem confluence :
∀ m u v, red m u -> red m v -> exists2 t, red u t & red v t.
Theorem church_rosser :
∀ u v, conv u v -> exists2 t, red u t & red v t.
End Confluence.
Require VarMap.
Module LCeq.
Definition t := term.
Definition eq := @Logic.eq term.
Definition eq_equiv : Equivalence eq := eq_equivalence.
End LCeq.
Module I := VarMap.Make(LCeq).
Notation intt := I.map.
Notation eq_intt := I.eq_map.
Import I.
Definition ilift (j:intt) : intt :=
fun k => match k with
| 0 => Ref 0
| S n => lift 1 (j n)
end.
Instance ilift_morph : Proper (eq_intt ==> eq_intt) ilift.
Qed.
Lemma ilift_lams : ∀ k f j,
(∀ j j', (∀ a, lift 1 (j a) = j' a) ->
∀ a, lift 1 (f j a) = f j' a) ->
eq_intt (ilift (I.lams k f j)) (I.lams (S k) f (ilift j)).
Lemma ilift_binder : ∀ u j k,
eq_intt
(ilift (fun n => subst_rec u (j n) k))
(fun n => subst_rec u (ilift j n) (S k)).
Lemma ilift_binder_lift : ∀ j k,
eq_intt
(ilift (fun n => lift_rec 1 (j n) k))
(fun n => lift_rec 1 (ilift j n) (S k)).
Lemma cross_binder_cons k x y i :
lift 1 x = y ->
eq_intt (ilift (I.lams k (I.cons x) i)) (I.lams (S k) (I.cons y) (ilift i)).
Lemma cross_binder_shift n k i :
eq_intt (ilift (I.lams k (I.shift n) i)) (I.lams (S k) (I.shift n) (ilift i)).
Definition substitutive (t:intt->term) :=
∀ u j k,
t (fun n => subst_rec u (j n) k) = subst_rec u (t j) k.
Definition liftable (t:intt->term) :=
∀ j k,
t (fun n => lift_rec 1 (j n) k) = lift_rec 1 (t j) k.