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

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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.

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

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.

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.

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.