Library SKv

Require Export Base UnifConfl.
Require Import Omega.

Syntax of SKv


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.

Semantics of SKv


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

Decidability of Basic Predicates


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.

Identity Combinator


Definition I := (S K K).

Lemma I_value: value I.

Hint Resolve I_value : value.

Compatibility Laws


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.

Irreducibility


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.

Closedness


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.

Uniform Confluence

Misc

Size of Term


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

Decomposibility of Reductions


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

Properties involving closedness

Substitution


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

Maximal Values


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

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

Unique Sucessors for Redex

Substitutivity of values

Evaluation in SKv


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

Hint Unfold eval.

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

Closed w.r.t a variable


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.