(* weak normalization for typable combinator terms (expression style) *)
(*** Uses a pattern-matching definition of Computability ***)
Init XCC;
Logic;
[TYPE = Type(0)];   (* inductive elimination universe *)
[Set = Type(0)];    (* type of sets *)

(*  Object level  *)
[AP:Set];     (* a type of atomic propositions (types) *)

(* object-level propositions (types). *)
Inductive [prop:Set]
Constructors [atom:{a:AP}prop]
             [arrow:prop->prop->prop];

(* a right associative infix operator for "arrow" *)
Configure Infix >> right 5; 
[op>> = arrow]; 

(* object-level terms. *)
Inductive [term:Set]
Constructors [k:term]
             [s:term]
             [app:term->term->term];

(* a left associative infix operator for "app" *)
Configure Infix * left 5;
[op* = app];

(* object-level provability judgement. *)
Inductive [thm:term->prop->Prop] Relation
Constructors
   [K:{p,q:prop}thm k (p>>q>>p)]
   [S:{p,q,r:prop}thm s ((p>>q>>r) >> (p>>q) >> (p>>r))]
   [MP:{a,b|term}{p,q|prop}
        {lp:thm a (p>>q)}   {rp:thm b p}
     (************************************)
              thm (a*b) q];

(* Define the reduction relation on object-level terms. *)
Inductive [red:term->term->Prop] Relation
Constructors
   [kred:{a,b:term}red (k*a*b) a]
   [sred:{a,b,c:term}red (s*a*b*c) (a*c*(b*c))]
   [l_cong:{a,a'|term}{b:term}
            (red a a')->
        (**************************)
            red (a*b) (a'*b)]
   [r_cong:{a,a'|term}{b:term}
            (red a a')->
        (**************************)
            red (b*a) (b*a')];


(* Normalizing *)
Inductive [WNorm:term->Prop] Relation
Constructors
   [ntk:WNorm k]
   [nts:WNorm s]
   [ntkM:{M|term}
           {Mn:WNorm M}
        (**************************)
           WNorm (k*M)]
   [ntsM:{M|term}
           {Mn:WNorm M}
        (**************************)
           WNorm (s*M)]
   [ntsMN:{M,N|term}
           {Mn:WNorm M}
           {Nn:WNorm N}
        (**************************)
           WNorm (s*M*N)]
   [ntStep:{M,N|term}{p:red M N}
           {Nn:WNorm N}
        (**************************)
           WNorm M];


(* Define computability by induction on prop:
 * No term of atomic type is computable (without object level 
 *   assumptions there is no well-typed term of atomic type)
 * A term of type x1>>x2 is computable if it is Normalizing, and if
 *   for all terms N of type x1, if N is computable then (M*N) is
 *   computable.
 *)
[Cmptbl : {a:prop}{M:term}Prop];
[[ap:AP][M:term][p,q:prop]
   Cmptbl (atom ap) M ==> absurd
|| Cmptbl (arrow p q) M ==>
            and (WNorm M) ({N|term}(Cmptbl p N)->Cmptbl q (M*N))];
(* The definiton expands too eagerly, so block it with a definition *)
[Comp = Cmptbl];

(* some properties of computability *)
Goal {a|prop}{M|term}(Comp a M)->WNorm M;
Refine prop_elim [a:prop]
             {M|term}(Comp a M)->WNorm M;
intros; Refine H;
intros; Refine fst H;
Save CompWNorm;

Goal {a,b|prop}{M,N|term}(Comp (a>>b) M)->(Comp a N)->Comp b (M*N);
intros; Refine snd H H1;
Save appPreserveComp;

Goal {a|prop}{M,N|term}
     (red M N)->(Comp a N)->Comp a M;
Refine prop_elim [a|prop]{M,N|term}
     (red M N)->(Comp a N)->Comp a M;
intros; Refine H1;
intros; Refine pair;
  Refine ntStep H (CompWNorm H1);
  intros O _; Refine x2_ih (l_cong O H);
  Refine appPreserveComp; Immed;
Save ExpandPreserveComp;

Goal kComp: {p,q:prop}Comp (p>>q>>p) k;
intros; Refine pair; Refine ntk;
intros; Refine pair; Refine ntkM; Refine CompWNorm H;
intros M HM; Refine ExpandPreserveComp (kred ??); Immed;
Save kComp;

Goal sComp: {p,q,r:prop}Comp ((p>>q>>r)>>(p>>q)>>p>>r) s;
intros; Refine pair; Refine nts;
Equiv {N:term}(Comp (p>>q>>r) N)->(Comp ((p>>q)>>p>>r) (s*N));
intros; Refine pair; Refine ntsM; Refine CompWNorm H;
Equiv {O:term}(Comp (p>>q) O)->(Comp (p>>r) (s*N*O));
intros; Refine pair; Refine ntsMN; Refine CompWNorm H; Refine CompWNorm H1;
Equiv {P:term}(Comp p P)->(Comp r (s*N*O*P));
intros; 
Refine ExpandPreserveComp (sred N O P); 
Refine appPreserveComp|q|r;
Refine appPreserveComp H H2;
Refine appPreserveComp H1 H2;
Save sComp;


(** main theorem **)
Goal AllComp:
   {M|term}{a|prop}{thmM:thm M a}Comp a M; 
Refine thm_elim [M:term][a:prop]Comp a M;
(* k *)
Refine kComp;
(* s *)
Refine sComp;
(* app *)
intros; Refine appPreserveComp; Immed;
Save AllComp;

(* all terms are normalizing *)
Goal AllWNorm:
   {a|prop}{M|term}{thmM:thm M a}WNorm M;
intros; Refine CompWNorm|a; Refine AllComp; Immed;
Save AllWNorm;