Require Export Base UnifConfl.
Require Import Omega.

Inductive term : Type :=
  |var :nat → term
  |K : term
  |S : term
  |app : term → term → term.

Implicit Types X Y Z : term.
Coercion app : term >-> Funclass.
Notation "'#' v" := (var v) (at level 1) : SKv_scope.

Inductive value : term → Prop:=
| valVar x : value (var x)
| valK : value K
| valK1 X : value X → value (K X)
| valS : value S
| valS1 X : value X → value (S X)
| valX2 X Y : value X → value Y → value (S X Y).
Hint Constructors value.

Reserved Notation "X '>>>' Y" (at level 50).

Inductive step : term → term → Prop :=
| stepK X Y: value X → value Y → K X Y >>> X
| stepS X Y Z : value X → value Y → value Z → S X Y Z >>> (X Z) (Y Z)
| stepAppL X X' Y : X >>> X' → app X Y >>> app X' Y
| stepAppR X Y Y' : Y >>> Y' → app X Y >>> app X Y'
where "X '>>>' Y" := (step X Y).
Hint Constructors step.

Notation "X '>>*' Y" := (star step X Y) (at level 50).
Notation "X '>>^' k " := (pow step k X) (at level 8, format "X '>>^' k").
Notation "s '=*=' t" := (ecl step s t)(at level 70).

Instance SKv_eq_dec : eq_dec term.

Ltac inv_SKvvalue :=
  match goal with
    | H : value (var _) |- _ ⇒ inv H
    | H : value (app _ _) |- _ ⇒ inv H
  end.

Instance value_dec X : dec(value X).

Ltac inv_SKvstep :=
  match goal with
    | H : step (app _ _) _ |- _ ⇒ inv H
    | H : step (var _) _ |- _ ⇒ inv H
    | H : step K _ |- _ ⇒ inv H
    | H : step S _ |- _ ⇒ inv H
  end.

Definition I := (S K K).

Lemma I_value: value I.

Hint Resolve I_value : value.

Lemma step_pow_app_l X X' Y n: X >>^n X' → (X Y) >>^n (X' Y).

Lemma step_pow_app_r X Y Y' n: Y >>^n Y' → (X Y) >>^n (X Y').

Lemma step_pow_app X X' Y Y' n m: X >>^n X' → Y >>^m Y' → (X Y) >>^(n+m) (X' Y').

Lemma starStepL X X' Y : X >>* X' → X Y >>* X' Y.

Lemma starStepR X Y Y': Y >>* Y' → X Y >>* X Y'.

Instance star_app_proper :
  Proper (star step ==> star step ==> star step) app.

Lemma eqAppL X X' Y : X =*= X' → X Y =*= X' Y.

Lemma eqAppR X Y Y' : Y =*= Y' → X Y =*= X Y'.

Instance equiv_app_proper :
  Proper (ecl step ==> ecl step ==> ecl step) app.

Lemma value_irred X : value X → irred step X.

Lemma star_value X Y: value X → X >>* Y → X = Y.

Lemma irred_appL X Y: irred step (X Y) → irred step X.

Lemma irred_appR X Y: irred step (X Y) → irred step Y.

Inductive closed : term → Prop :=
|clK : closed K
|clS : closed S
|clapp X Y: closed X → closed Y → closed (X Y).
Hint Constructors closed.

Ltac inv_closed :=
  match goal with
    | H : closed (var _) |- _ ⇒ inv H
    | H : closed (app _ _) |- _ ⇒ inv H
    | H : closed K |- _ ⇒ clear H
    | H : closed S |- _ ⇒ clear H
  end.

Instance closed_dec X: dec (closed X).

Lemma normal_value X : closed X → irred step X → value X.

Lemma I_closed: closed I.

Hint Resolve I_closed : value.

Lemma SK_UC: uniformly_confluent step.

Lemma SK_church_rosser : church_rosser step.

Lemma equiv_value X Y : value Y → X =*= Y → X >>* Y.

Lemma equiv_value_eq X Y : value X → value Y → X =*= Y → X = Y.

Fixpoint size X: nat :=
match X with
    | var n ⇒ 0
    | app X Y ⇒ 1 + size X + size Y
    | _ ⇒ 0
end.

Lemma pow_decompose X Y k: X >>^k Y →
                            k=0 ∧ Y=X
                            ∨ (∃ X1 X2 Y1 Y2 k1 k2,
                                   (X= X1 X2 ∧ X1 >>^k1 Y1 ∧ X2 >>^k2 Y2)
                                   ∧ ((Y=Y1 Y2 ∧ k=k1+k2)
                                       ∨ (∃ Z k', value Y1 ∧ value Y2
                                                        ∧ Y1 Y2 >>> Z
                                                        ∧ Z >>^k' Y
                                                        ∧ k1+k2+1+k'=k))).

Lemma closed_app X Y : closed (X Y) ↔ closed X ∧ closed Y.

Lemma step_closed X Y : closed X → X >>> Y → closed Y.

Lemma star_closed X Y : closed X → X >>* Y → closed Y.

Definition subst X x Y :=
  (fix subst X:=
     match X with
       | var y ⇒ if decision (x=y) then Y else var (if decision (x < y) then y-1 else y)
       | app X1 X2 ⇒ (subst X1) (subst X2)
       | X ⇒ X
     end) X.

Definition maxValue X := value X ∧ ∀ Z, ¬ value (X Z).

Lemma maxValue_Value X : maxValue X → value X.
Hint Resolve maxValue_Value :value.

Lemma value_step_unique X Y Z1 Z2: value X→ value Y → (X Y) >>> Z1 → (X Y) >>> Z2 → Z1=Z2.

Lemma maxValueSubst X Y y: maxValue Y → (value (subst X y Y) → value X).

Lemma valueSubst X Y y: value Y → (value X → value (subst X y Y)).

Lemma valueSubst_iff X Y y: maxValue Y → ((value (subst X y Y) ↔ value X)).

Definition eval X Y:= X >>* Y ∧ value Y.

Hint Unfold eval.

Lemma eval_iff X Y: eval X Y ↔ X =*= Y ∧ value Y.

Inductive varClosed x: term → Prop :=
| varClosedVar y: x ≠ y → varClosed x (var y)
| varClosedK : varClosed x K
| varClosedS : varClosed x S
| varClosedApp X Y: varClosed x X → varClosed x Y → varClosed x (X Y).
Hint Constructors varClosed.

Ltac inv_varClosed :=
  match goal with
    | H : varClosed _ (var _) |- _ ⇒ inv H
    | H : varClosed _ (app _ _) |- _ ⇒ inv H
    | H : varClosed _ K |- _ ⇒ clear H
    | H : varClosed _ S |- _ ⇒ clear H
  end.

Instance freeLvwVar_dec x X: dec (varClosed x X).

Lemma varClosedApp_iff x X Y : varClosed x (X Y) ↔ varClosed x X ∧ varClosed x Y.

Lemma varClosedVar_iff x y : varClosed x (var y) ↔ x ≠ y.

Lemma closed_varClosed x X : closed X → varClosed x X.
Hint Resolve closed_varClosed.
Ltac dec :=
  match goal with
    | [ |- context[decision ?X] ] ⇒ decide X
  end.

Lemma subst_free_iff X Y y: y>0 → varClosed 0 Y → (varClosed 0 X ↔ varClosed 0 (subst X y Y)).

Lemma varClosed_closed X : (∀ x, varClosed x X) ↔ closed X.