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.