(** 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     (* countably many atomic props *)
 | 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.

(* some uncompleted ideas.  Are they correct?
Lemma WNormHead: forall a b, WNorm (a & b) -> WNorm a.
intros a b h; inversion h.
apply ntk. apply nts. apply ntsM. assumption.
apply ntNu. eapply NeutHead. eassumption.
induction N. inversion h. apply ntk. apply nts. apply ntsM. assumption.
  apply ntNu. eapply NeutHead. eassumption.


inversion H. apply ntkM. assumption.
apply ntsMN. rewrite <- H3 in H. rewrite <- H2 in H.
  inversion H.


Lemma WNormHead: forall c, WNorm c -> forall a b, c = (a & b) -> WNorm a.
induction 1; intros a b h. discriminate h. discriminate h.
injection h; intros. rewrite <- H1. apply ntk.
injection h; intros. rewrite <- H1. apply nts.
injection h; intros. rewrite <- H2. apply ntsM. assumption.
rewrite h in H. inversion H. apply ntNu. assumption.
assert (j := ntStep H H0). rewrite h in j. inversion j.
   apply ntk. apply nts. apply ntsM. assumption.
   apply ntNu. eapply NeutHead. eassumption.


rewrite h in H. inversion H.
  apply ntkM. assumption.
  apply ntsMN. rewrite <-
**)

(*
Lemma WNormHead: forall a b, WNorm (a & b) -> WNorm a.
induction a; intros b h; auto.

intros. inversion H; auto; try assumption.
apply ntNu. eapply NeutHead. eassumption.

Lemma redPresWN: forall M N, (N --> M) -> WNorm N -> WNorm M.
induction N; intros h1 h2. inversion h1. inversion h1. inversion h1.
inversion h1.

Lemma redPresNeut: forall a, Neutral a -> forall b, (a --> b) -> Neutral b.
induction a; intros h1 b h2.
inversion h2.
inversion h2.
inversion h2.
inversion h1. inversion h2.
Check (IHa1 (NeutHead h1)).
***)

(*
Lemma redPresNeut: forall a, Neutral a -> forall b, (a --> b) -> Neutral b.
induction 1; intros b h. inversion h.
inversion h. rewrite <- H2 in H. inversion H. inversion H6.
  rewrite <- H2 in H. inversion H. inversion H6. inversion H10.
apply nuapp. apply IHNeutral. assumption.
assumption.
apply nuapp. assumption. apply (ntStep H4).

Lemma redPresNeut: forall a b, (a --> b) -> Neutral a -> Neutral b.
induction 1; intros h.
inversion h. inversion H1. inversion H5.
inversion h. inversion H1. inversion H5. inversion H9.
admit.
admit.
Admitted.

Lemma redPresNeut: 
   (forall a, WNorm a -> forall b, (a --> b) -> WNorm b) /\
   (forall a, Neutral a -> forall b, (a --> b) -> Neutral b).
apply WNorm_induc.
*)

(** 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.
(* atom *) destruct H1. split. assumption. apply (ntStep H0 H2).
(* arr *)
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.
(* k *)
apply kComp.
(* s *)
apply sComp.
(* v *)
apply NeutComp. auto. auto.
(* app *)
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.
(* kred *)
inversion H.
inversion lp.
inversion lp0.
rewrite <- H9.
assumption.
(* sred *)
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.
(* app_lcong *)
inversion H0. apply (@MP a' b p); auto.
(* app_rcong *)
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.
(* rt_step *) apply rt_step. apply app_lcong. assumption.
(* rt_refl *) apply rt_refl.
(* rt_trans *) apply (rt_trans _ _ _ (y & b)); assumption.
Qed.

Lemma redd_app_rcong:
   forall a b b', (b -->> b') -> (a & b) -->> (a & b').
induction 1; intros.
(* rt_step *) apply rt_step. apply app_rcong. assumption.
(* rt_refl *) apply rt_refl.
(* rt_trans *) 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.
(* ntk *) exists k; split; eauto. apply rt_refl.
(* nts *) exists s; split; eauto. apply rt_refl.
(* ntkM *) destruct H. destruct H.
  exists (k & x); split; auto.
  apply redd_app_rcong. assumption.
(* ntsM *) destruct H. destruct H.
  exists (s & x); split; auto.
  apply redd_app_rcong. assumption.
(* ntsMN *) destruct H. destruct H. destruct H0. destruct H0.
  exists (s & x & x0). split; auto.
  apply redd_app_cong. apply redd_app_rcong. assumption. assumption.
(* ntNu *) destruct H. destruct H. exists x. split.
   apply nfNu. assumption. assumption.
(* ntStep *) destruct H. destruct H. exists x.
split. assumption. apply (rt_trans _ _ _ N). apply rt_step. assumption.
   assumption. 
(* nuvar *) exists (v n p). split. auto. apply rt_refl.
(* nuapp *) 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.