Library SK_neutral
Weak Normalization of SK combinators with natural number terms.
Proof is by Tait Computability.
Set Implicit Arguments.
object-level propositions (types).
Inductive prop : Set :=
| atom: nat -> prop
| arrow: prop -> prop -> prop .
Implicit Types p q r : prop.
Notation "p ~> q" := (arrow p q) (at level 80, right associativity).
| atom: nat -> prop
| arrow: prop -> prop -> prop .
Implicit Types p q r : prop.
Notation "p ~> q" := (arrow p q) (at level 80, right associativity).
object-level terms: note typed variables (v n p).
Inductive term : Set :=
| k: term
| s: term
| v: nat -> prop -> term
| app: term -> term -> term.
Implicit Types a b c M N : term.
Notation "a & b" := (app a b) (at level 81, left associativity).
| k: term
| s: term
| v: nat -> prop -> term
| app: term -> term -> term.
Implicit Types a b c M N : term.
Notation "a & b" := (app a b) (at level 81, left associativity).
reduction relation (untyped) on object-level terms
Inductive red : term -> term -> Prop :=
| kred: forall a b, red (k & a & b) a
| sred: forall a b c, red (s & a & b & c) (a & c & (b & c))
| app_lcong: forall a a' b, (red a a') -> red (a & b) (a' & b)
| app_rcong: forall a a' b, (red a a') -> red (b & a) (b & a').
Notation "a --> b" := (red a b) (at level 79).
Hint Constructors red.
| kred: forall a b, red (k & a & b) a
| sred: forall a b c, red (s & a & b & c) (a & c & (b & c))
| app_lcong: forall a a' b, (red a a') -> red (a & b) (a' & b)
| app_rcong: forall a a' b, (red a a') -> red (b & a) (b & a').
Notation "a --> b" := (red a b) (at level 79).
Hint Constructors red.
definition of weakly normalizing simultaneous with Neutral
Inductive WNorm : term -> Prop :=
| ntk: WNorm k
| nts: WNorm s
| ntkM: forall M, WNorm M -> WNorm (k & M)
| ntsM: forall M, WNorm M -> WNorm (s & M)
| ntsMN: forall M N, WNorm M -> WNorm N -> WNorm (s & M & N)
| ntNu: forall M, Neutral M -> WNorm M
| ntStep: forall M N, (M --> N) -> WNorm N -> WNorm M
with
Neutral : term -> Prop :=
| nuvar: forall n p, Neutral (v n p)
| nuapp: forall N M, Neutral N -> WNorm M -> Neutral (N & M).
Hint Constructors WNorm Neutral.
Scheme WN_ind' := Induction for WNorm Sort Prop
with Neutral_ind' := Induction for Neutral Sort Prop.
Combined Scheme WNorm_induc from WN_ind', Neutral_ind'.
Lemma NeutHead: forall a b, Neutral (a & b) -> Neutral a.
intros. inversion H. assumption.
Qed.
| ntk: WNorm k
| nts: WNorm s
| ntkM: forall M, WNorm M -> WNorm (k & M)
| ntsM: forall M, WNorm M -> WNorm (s & M)
| ntsMN: forall M N, WNorm M -> WNorm N -> WNorm (s & M & N)
| ntNu: forall M, Neutral M -> WNorm M
| ntStep: forall M N, (M --> N) -> WNorm N -> WNorm M
with
Neutral : term -> Prop :=
| nuvar: forall n p, Neutral (v n p)
| nuapp: forall N M, Neutral N -> WNorm M -> Neutral (N & M).
Hint Constructors WNorm Neutral.
Scheme WN_ind' := Induction for WNorm Sort Prop
with Neutral_ind' := Induction for Neutral Sort Prop.
Combined Scheme WNorm_induc from WN_ind', Neutral_ind'.
Lemma NeutHead: forall a b, Neutral (a & b) -> Neutral a.
intros. inversion H. assumption.
Qed.
object-level provability judgement
Inductive thm : term -> prop -> Prop :=
| K: forall p q, thm k (p ~> q ~> p)
| S: forall p q r,
thm s ((p ~> q ~> r) ~> (p ~> q) ~> (p ~> r))
| V: forall n p, thm (v n p) p
| MP: forall a b p q (lp: thm a (p ~> q)) (rp: thm b p),
(thm (a & b) q).
Hint Constructors thm.
| K: forall p q, thm k (p ~> q ~> p)
| S: forall p q r,
thm s ((p ~> q ~> r) ~> (p ~> q) ~> (p ~> r))
| V: forall n p, thm (v n p) p
| MP: forall a b p q (lp: thm a (p ~> q)) (rp: thm b p),
(thm (a & b) q).
Hint Constructors thm.
Now we can state the main theorem: all well-typed terms are normalizing
forall p M, (thm M p) -> WNorm M.
The proof follows. Everything above, you must understand; everything below is "purely technical", and you can trust Coq's proofchecking.
forall p M, (thm M p) -> WNorm M.
The proof follows. Everything above, you must understand; everything below is "purely technical", and you can trust Coq's proofchecking.
Main idea due to Tait:
Define computability at a prop by recursion on prop:
Fixpoint Comp p M {struct p} : Prop :=
match p with
| atom n => thm M (atom n) /\ WNorm M
| q ~> r => thm M (q ~> r) /\ WNorm M
/\ (forall N, Comp q N -> Comp r (M & N))
end.
match p with
| atom n => thm M (atom n) /\ WNorm M
| q ~> r => thm M (q ~> r) /\ WNorm M
/\ (forall N, Comp q N -> Comp r (M & N))
end.
This inductive definition is not accepted due to negative
occurrence of COMP q N.
Inductive COMP : prop -> term -> Prop :=
| cAtm : forall M n, thm M (atom n) -> WNorm M ->
COMP (atom n) M
| cArr : forall q r M, thm M (q ~> r) -> WNorm M ->
(forall N, COMP q N -> COMP r (M & N)) ->
COMP (q ~> r) M.
Inductive COMP : prop -> term -> Prop :=
| cAtm : forall M n, thm M (atom n) -> WNorm M ->
COMP (atom n) M
| cArr : forall q r M, thm M (q ~> r) -> WNorm M ->
(forall N, COMP q N -> COMP r (M & N)) ->
COMP (q ~> r) M.
some properties of computability
Lemma CompThm: forall p M, (Comp p M) -> thm M p.
intros p M; case p; simpl; intuition.
Qed.
Lemma CompWNorm: forall p M, (Comp p M) -> WNorm M.
destruct p; intros; simpl in H; intuition.
Qed.
Lemma appPreserveComp: forall p q M N,
(Comp (p ~> q) M) -> (Comp p N) -> Comp q (M & N).
intros. simpl in H. intuition.
Qed.
Lemma ExpandPreserveComp:
forall p M N, thm M p -> (M --> N) -> Comp p N -> Comp p M.
induction p; intros.
destruct H1. split. assumption. apply (ntStep H0 H2).
simpl. split. assumption.
split. apply (ntStep H0). apply (CompWNorm _ _ H1).
intros O X. eapply (IHp2 _ (N & O)). apply (MP H). apply (CompThm _ _ X).
apply (app_lcong _ H0).
apply (appPreserveComp _ H1 X).
Qed.
intros p M; case p; simpl; intuition.
Qed.
Lemma CompWNorm: forall p M, (Comp p M) -> WNorm M.
destruct p; intros; simpl in H; intuition.
Qed.
Lemma appPreserveComp: forall p q M N,
(Comp (p ~> q) M) -> (Comp p N) -> Comp q (M & N).
intros. simpl in H. intuition.
Qed.
Lemma ExpandPreserveComp:
forall p M N, thm M p -> (M --> N) -> Comp p N -> Comp p M.
induction p; intros.
destruct H1. split. assumption. apply (ntStep H0 H2).
simpl. split. assumption.
split. apply (ntStep H0). apply (CompWNorm _ _ H1).
intros O X. eapply (IHp2 _ (N & O)). apply (MP H). apply (CompThm _ _ X).
apply (app_lcong _ H0).
apply (appPreserveComp _ H1 X).
Qed.
term constructors s, k, v, are computable
Lemma kComp: forall p q, Comp (p ~> q ~> p) k.
intros. split. apply K. split. apply ntk.
intros N h. split. eapply MP. eapply K. eapply CompThm. assumption.
split. apply ntkM. apply (CompWNorm _ _ h).
intros M j. eapply (ExpandPreserveComp). eapply MP. eapply MP. eapply K.
apply CompThm. assumption. apply CompThm. eassumption.
apply kred. assumption.
Qed.
Lemma sComp: forall p q r,
Comp ((p ~> q ~> r) ~> (p ~> q) ~> (p ~> r)) s.
intros. split. apply S. split. apply nts.
intros N h. split. eapply MP. eapply S. eapply CompThm. assumption.
split. apply ntsM. apply (CompWNorm _ _ h).
intros M j. simpl. split.
eapply MP. eapply MP. eapply S. eapply CompThm. eassumption.
eapply CompThm. eassumption.
split. apply ntsMN. eapply CompWNorm. eassumption.
eapply CompWNorm. eassumption.
intros O j1. eapply (ExpandPreserveComp).
eapply MP. eapply MP. eapply MP. eapply S.
apply CompThm. eassumption. apply CompThm. assumption.
apply CompThm. assumption.
apply (sred N M O).
apply appPreserveComp with q.
apply appPreserveComp with p; assumption.
apply appPreserveComp with p; assumption.
Qed.
Lemma NeutComp: forall p N, thm N p -> Neutral N -> Comp p N.
induction p; intros N h j.
split. assumption. apply ntNu. assumption.
split. assumption. split. apply ntNu. assumption.
intros N0 l. apply IHp2. eapply MP. eassumption. apply CompThm. assumption.
eapply (nuapp j). eapply CompWNorm. eassumption.
Qed.
intros. split. apply K. split. apply ntk.
intros N h. split. eapply MP. eapply K. eapply CompThm. assumption.
split. apply ntkM. apply (CompWNorm _ _ h).
intros M j. eapply (ExpandPreserveComp). eapply MP. eapply MP. eapply K.
apply CompThm. assumption. apply CompThm. eassumption.
apply kred. assumption.
Qed.
Lemma sComp: forall p q r,
Comp ((p ~> q ~> r) ~> (p ~> q) ~> (p ~> r)) s.
intros. split. apply S. split. apply nts.
intros N h. split. eapply MP. eapply S. eapply CompThm. assumption.
split. apply ntsM. apply (CompWNorm _ _ h).
intros M j. simpl. split.
eapply MP. eapply MP. eapply S. eapply CompThm. eassumption.
eapply CompThm. eassumption.
split. apply ntsMN. eapply CompWNorm. eassumption.
eapply CompWNorm. eassumption.
intros O j1. eapply (ExpandPreserveComp).
eapply MP. eapply MP. eapply MP. eapply S.
apply CompThm. eassumption. apply CompThm. assumption.
apply CompThm. assumption.
apply (sred N M O).
apply appPreserveComp with q.
apply appPreserveComp with p; assumption.
apply appPreserveComp with p; assumption.
Qed.
Lemma NeutComp: forall p N, thm N p -> Neutral N -> Comp p N.
induction p; intros N h j.
split. assumption. apply ntNu. assumption.
split. assumption. split. apply ntNu. assumption.
intros N0 l. apply IHp2. eapply MP. eassumption. apply CompThm. assumption.
eapply (nuapp j). eapply CompWNorm. eassumption.
Qed.
Key lemma: a well-typed term is computable at its type
Lemma AllComp: forall M p, (thm M p) -> Comp p M.
induction 1.
apply kComp.
apply sComp.
apply NeutComp. auto. auto.
intros. apply (@appPreserveComp p); assumption.
Qed.
induction 1.
apply kComp.
apply sComp.
apply NeutComp. auto. auto.
intros. apply (@appPreserveComp p); assumption.
Qed.
Main theorem: all well-typed terms are normalizing
Theorem AllWNorm: forall p M, (thm M p) -> WNorm M.
intros; eapply CompWNorm; eapply AllComp; eauto.
Qed.
intros; eapply CompWNorm; eapply AllComp; eauto.
Qed.
Some auxiliary facts to give confidence in our defintions
subject reduction: reduction preserves types
Ltac rewritesThenAssumption :=
match goal with
| id:_ = _ |- _ => rewrite id; assumption
| id:_ = _ |- _ => rewrite <- id; assumption
| id:_ = _ |- _ => rewrite id; clear id; rewritesThenAssumption
| id:_ = _ |- _ => rewrite <- id; clear id; rewritesThenAssumption
end.
Lemma subjRed: forall M N, (M --> N) -> forall (r:prop), (thm M r) -> thm N r.
induction 1; intros.
inversion H.
inversion lp.
inversion lp0.
rewrite <- H9.
assumption.
inversion H.
inversion lp.
inversion lp0.
inversion lp1.
apply (@MP (a & c) (b & c) q2).
apply (@MP a c p2).
rewritesThenAssumption.
rewritesThenAssumption.
apply (@MP b c p2).
rewritesThenAssumption.
rewritesThenAssumption.
inversion H0. apply (@MP a' b p); auto.
inversion H0. apply (@MP b a' p); auto.
Qed.
match goal with
| id:_ = _ |- _ => rewrite id; assumption
| id:_ = _ |- _ => rewrite <- id; assumption
| id:_ = _ |- _ => rewrite id; clear id; rewritesThenAssumption
| id:_ = _ |- _ => rewrite <- id; clear id; rewritesThenAssumption
end.
Lemma subjRed: forall M N, (M --> N) -> forall (r:prop), (thm M r) -> thm N r.
induction 1; intros.
inversion H.
inversion lp.
inversion lp0.
rewrite <- H9.
assumption.
inversion H.
inversion lp.
inversion lp0.
inversion lp1.
apply (@MP (a & c) (b & c) q2).
apply (@MP a c p2).
rewritesThenAssumption.
rewritesThenAssumption.
apply (@MP b c p2).
rewritesThenAssumption.
rewritesThenAssumption.
inversion H0. apply (@MP a' b p); auto.
inversion H0. apply (@MP b a' p); auto.
Qed.
Normalizing terms reduce to a normal form
Definition of Normal Form
Inductive NF : term -> Prop :=
| nfk: NF k
| nfs: NF s
| nfkM: forall M, NF M -> NF (k & M)
| nfsM: forall M, NF M -> NF (s & M)
| nfsMN: forall M N, NF M -> NF N -> NF (s & M & N)
| nfNu: forall M, NF_Neutral M -> NF M
with
NF_Neutral : term -> Prop :=
| nfvar: forall n p, NF_Neutral (v n p)
| nfapp: forall M N, NF M -> NF_Neutral N -> NF_Neutral (N & M).
Hint Constructors NF NF_Neutral.
Scheme NF_ind' := Induction for NF Sort Prop
with NF_Neutral_ind' := Induction for NF_Neutral Sort Prop.
Combined Scheme NF_induc from NF_ind', NF_Neutral_ind'.
| nfk: NF k
| nfs: NF s
| nfkM: forall M, NF M -> NF (k & M)
| nfsM: forall M, NF M -> NF (s & M)
| nfsMN: forall M N, NF M -> NF N -> NF (s & M & N)
| nfNu: forall M, NF_Neutral M -> NF M
with
NF_Neutral : term -> Prop :=
| nfvar: forall n p, NF_Neutral (v n p)
| nfapp: forall M N, NF M -> NF_Neutral N -> NF_Neutral (N & M).
Hint Constructors NF NF_Neutral.
Scheme NF_ind' := Induction for NF Sort Prop
with NF_Neutral_ind' := Induction for NF_Neutral Sort Prop.
Combined Scheme NF_induc from NF_ind', NF_Neutral_ind'.
there is no reduction from a normal form
Lemma NF_nored: (forall N, NF N -> forall M, ~(N --> M)) /\
(forall N, NF_Neutral N -> forall M, ~(N --> M)).
apply NF_induc; intros P h.
inversion h. inversion h.
intros j Q l. inversion l. inversion H2. assert (j1 := j a'). contradiction.
intros j Q l. inversion l. inversion H2. assert (j1 := j a'). contradiction.
intros j1 j2 j3 j4 Q l.
inversion l. inversion H2. inversion H6.
assert (j2' := j2 a'0). contradiction.
assert (j4' := j4 a'). contradiction.
intros j Q l. assert (j' := j Q). contradiction.
intros M j. inversion j.
intros j1 j2 j3 j4 M l. inversion l.
rewrite <- H0 in j3. inversion j3. inversion H5.
rewrite <- H0 in j3. inversion j3. inversion H5. inversion H9.
assert (j5 := j4 a'). contradiction.
assert (j5 := j2 a'). contradiction.
Qed.
(forall N, NF_Neutral N -> forall M, ~(N --> M)).
apply NF_induc; intros P h.
inversion h. inversion h.
intros j Q l. inversion l. inversion H2. assert (j1 := j a'). contradiction.
intros j Q l. inversion l. inversion H2. assert (j1 := j a'). contradiction.
intros j1 j2 j3 j4 Q l.
inversion l. inversion H2. inversion H6.
assert (j2' := j2 a'0). contradiction.
assert (j4' := j4 a'). contradiction.
intros j Q l. assert (j' := j Q). contradiction.
intros M j. inversion j.
intros j1 j2 j3 j4 M l. inversion l.
rewrite <- H0 in j3. inversion j3. inversion H5.
rewrite <- H0 in j3. inversion j3. inversion H5. inversion H9.
assert (j5 := j4 a'). contradiction.
assert (j5 := j2 a'). contradiction.
Qed.
Transitive reflexive closure of reduction, -->>
Require Import Relation_Operators.
Definition redd : term -> term -> Prop := clos_refl_trans _ red.
Notation "a -->> b" := (redd a b) (at level 79).
Definition redd : term -> term -> Prop := clos_refl_trans _ red.
Notation "a -->> b" := (redd a b) (at level 79).
Congruence properties of -->>
Lemma redd_app_lcong:
forall a a' b, (a -->> a') -> (a & b) -->> (a' & b).
induction 1; intros.
apply rt_step. apply app_lcong. assumption.
apply rt_refl.
apply (rt_trans _ _ _ (y & b)); assumption.
Qed.
Lemma redd_app_rcong:
forall a b b', (b -->> b') -> (a & b) -->> (a & b').
induction 1; intros.
apply rt_step. apply app_rcong. assumption.
apply rt_refl.
apply (rt_trans _ _ _ (a & y)); assumption.
Qed.
Lemma redd_app_cong:
forall a a' b b', (a -->> a') -> (b -->> b') -> (a & b) -->> (a' & b').
intros. apply (rt_trans _ _ _ (a' & b)).
apply (redd_app_lcong _ H). apply (redd_app_rcong _ H0).
Qed.
forall a a' b, (a -->> a') -> (a & b) -->> (a' & b).
induction 1; intros.
apply rt_step. apply app_lcong. assumption.
apply rt_refl.
apply (rt_trans _ _ _ (y & b)); assumption.
Qed.
Lemma redd_app_rcong:
forall a b b', (b -->> b') -> (a & b) -->> (a & b').
induction 1; intros.
apply rt_step. apply app_rcong. assumption.
apply rt_refl.
apply (rt_trans _ _ _ (a & y)); assumption.
Qed.
Lemma redd_app_cong:
forall a a' b b', (a -->> a') -> (b -->> b') -> (a & b) -->> (a' & b').
intros. apply (rt_trans _ _ _ (a' & b)).
apply (redd_app_lcong _ H). apply (redd_app_rcong _ H0).
Qed.
Normalizing terms reduce to a normal form
Lemma WNorm_NF: (forall M, WNorm M -> exists nM, NF nM /\ M -->> nM) /\
(forall M, Neutral M -> exists nM, NF_Neutral nM /\ M -->> nM).
apply WNorm_induc; intros.
exists k; split; eauto. apply rt_refl.
exists s; split; eauto. apply rt_refl.
destruct H. destruct H.
exists (k & x); split; auto.
apply redd_app_rcong. assumption.
destruct H. destruct H.
exists (s & x); split; auto.
apply redd_app_rcong. assumption.
destruct H. destruct H. destruct H0. destruct H0.
exists (s & x & x0). split; auto.
apply redd_app_cong. apply redd_app_rcong. assumption. assumption.
destruct H. destruct H. exists x. split.
apply nfNu. assumption. assumption.
destruct H. destruct H. exists x.
split. assumption. apply (rt_trans _ _ _ N). apply rt_step. assumption.
assumption.
exists (v n p). split. auto. apply rt_refl.
destruct H. destruct H. destruct H0. destruct H0.
exists (x & x0). split. apply nfapp; assumption.
apply redd_app_cong; assumption.
Qed.
(forall M, Neutral M -> exists nM, NF_Neutral nM /\ M -->> nM).
apply WNorm_induc; intros.
exists k; split; eauto. apply rt_refl.
exists s; split; eauto. apply rt_refl.
destruct H. destruct H.
exists (k & x); split; auto.
apply redd_app_rcong. assumption.
destruct H. destruct H.
exists (s & x); split; auto.
apply redd_app_rcong. assumption.
destruct H. destruct H. destruct H0. destruct H0.
exists (s & x & x0). split; auto.
apply redd_app_cong. apply redd_app_rcong. assumption. assumption.
destruct H. destruct H. exists x. split.
apply nfNu. assumption. assumption.
destruct H. destruct H. exists x.
split. assumption. apply (rt_trans _ _ _ N). apply rt_step. assumption.
assumption.
exists (v n p). split. auto. apply rt_refl.
destruct H. destruct H. destruct H0. destruct H0.
exists (x & x0). split. apply nfapp; assumption.
apply redd_app_cong; assumption.
Qed.
A different approach: the definition of NormTo keeps track of the
normal form as it goes
Inductive NormTo : term -> term ->Prop :=
| NTk: NormTo k k
| NTs: NormTo s s
| NTkM: forall M M', NormTo M M' -> NormTo (k & M) (k & M')
| NTsM: forall M M', NormTo M M' -> NormTo (s & M) (s & M')
| NTsMN: forall M M' N N' , NormTo M M' -> NormTo N N' ->
NormTo (s & M & N) (s & M' & N')
| NTNu: forall M M', NeutTo M M' -> NormTo M M'
| NTStep: forall M N N', (M --> N) -> NormTo N N' -> NormTo M N'
with
NeutTo : term -> term -> Prop :=
| NUvar: forall n p, NeutTo (v n p) (v n p)
| NUapp: forall N N' M M', NeutTo N N' -> NormTo M M' ->
NeutTo (N & M) (N' & M').
Hint Constructors NormTo NeutTo.
Scheme NT_ind' := Induction for NormTo Sort Prop
with NeutT_ind' := Induction for NeutTo Sort Prop.
Combined Scheme NT_induc from NT_ind', NeutT_ind'.
Lemma NT_app: forall a a', NeutTo a a' -> forall b b', NormTo b b' ->
NormTo (a & b) (a' & b').
induction 1; intros b b' h. auto.
apply NTNu. apply NUapp; try assumption. apply NUapp; assumption.
Qed.
Lemma NormTo_NF: (forall M nM, NormTo M nM -> NF nM) /\
(forall M nM, NeutTo M nM -> NF_Neutral nM).
apply NT_induc; intros; eauto.
Qed.
Lemma NormTo_red: (forall M nM, NormTo M nM -> M -->> nM) /\
(forall M nM, NeutTo M nM -> M -->> nM).
apply NT_induc; intros; try apply rt_refl.
apply redd_app_rcong; assumption.
apply redd_app_rcong; assumption.
apply redd_app_cong. apply redd_app_rcong. assumption. assumption.
assumption.
apply (rt_trans _ _ _ N). apply rt_step. assumption. assumption.
apply redd_app_cong; assumption.
Qed.
| NTk: NormTo k k
| NTs: NormTo s s
| NTkM: forall M M', NormTo M M' -> NormTo (k & M) (k & M')
| NTsM: forall M M', NormTo M M' -> NormTo (s & M) (s & M')
| NTsMN: forall M M' N N' , NormTo M M' -> NormTo N N' ->
NormTo (s & M & N) (s & M' & N')
| NTNu: forall M M', NeutTo M M' -> NormTo M M'
| NTStep: forall M N N', (M --> N) -> NormTo N N' -> NormTo M N'
with
NeutTo : term -> term -> Prop :=
| NUvar: forall n p, NeutTo (v n p) (v n p)
| NUapp: forall N N' M M', NeutTo N N' -> NormTo M M' ->
NeutTo (N & M) (N' & M').
Hint Constructors NormTo NeutTo.
Scheme NT_ind' := Induction for NormTo Sort Prop
with NeutT_ind' := Induction for NeutTo Sort Prop.
Combined Scheme NT_induc from NT_ind', NeutT_ind'.
Lemma NT_app: forall a a', NeutTo a a' -> forall b b', NormTo b b' ->
NormTo (a & b) (a' & b').
induction 1; intros b b' h. auto.
apply NTNu. apply NUapp; try assumption. apply NUapp; assumption.
Qed.
Lemma NormTo_NF: (forall M nM, NormTo M nM -> NF nM) /\
(forall M nM, NeutTo M nM -> NF_Neutral nM).
apply NT_induc; intros; eauto.
Qed.
Lemma NormTo_red: (forall M nM, NormTo M nM -> M -->> nM) /\
(forall M nM, NeutTo M nM -> M -->> nM).
apply NT_induc; intros; try apply rt_refl.
apply redd_app_rcong; assumption.
apply redd_app_rcong; assumption.
apply redd_app_cong. apply redd_app_rcong. assumption. assumption.
assumption.
apply (rt_trans _ _ _ N). apply rt_step. assumption. assumption.
apply redd_app_cong; assumption.
Qed.