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.
Bind Scope SKv_scope with term.

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.
Proof.
  unfold dec; repeat decide equality.
Defined.

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

Instance value_dec X : dec(value X).
Proof with try (now ( right; intro; repeat inv_SKvvalue;try tauto))|| now (left;repeat inv_SKvvalue;eauto).
  induction X... destruct IHX2... destruct X1... destruct IHX1; destruct X1_1... right. intro. inv_SKvvalue;auto.
Defined.

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.
Proof.
  repeat constructor.
Qed.

Hint Resolve I_value : value.

Compatibility Laws


Lemma step_pow_app_l X X' Y n: X >>^n X' (X Y) >>^n (X' Y).
Proof.
  revert X X' Y. induction n;intros.
  -inv H. reflexivity.
  -destruct H as [X1 [R R']]. (X1 Y). split. auto. apply IHn. exact R'.
Qed.

Lemma step_pow_app_r X Y Y' n: Y >>^n Y' (X Y) >>^n (X Y').
Proof.
  revert X Y Y'. induction n;intros.
  -inv H. reflexivity.
  -destruct H as [Y1 [R R']]. (X Y1). split. auto. apply IHn. exact R'.
Qed.

Lemma step_pow_app X X' Y Y' n m: X >>^n X' Y >>^m Y' (X Y) >>^(n+m) (X' Y').
Proof.
  intros. apply pow_add. (X' Y);split.
  -auto using step_pow_app_l.
  -auto using step_pow_app_r.
Qed.

Lemma starStepL X X' Y : X >>* X' X Y >>* X' Y.
  induction 1; econstructor;eauto.
Qed.

Lemma starStepR X Y Y': Y >>* Y' X Y >>* X Y'.
  induction 1; econstructor;eauto.
Qed.

Instance star_app_proper :
  Proper (star step ==> star step ==> star step) app.
Proof.
  repeat intro. subst. etransitivity. now apply (starStepL _ H). now apply starStepR.
Qed.

Lemma eqAppL X X' Y : X =*= X' X Y =*= X' Y.
Proof.
  induction 1;eauto using ecl.
Qed.

Lemma eqAppR X Y Y' : Y =*= Y' X Y =*= X Y'.
Proof.
    induction 1;eauto using ecl.
Qed.

Instance equiv_app_proper :
  Proper (ecl step ==> ecl step ==> ecl step) app.
Proof.
  cbv. intros X X' A Y Y' B;subst. transitivity (X Y'). now eapply eqAppR. now eapply eqAppL.
Qed.

Irreducibility


Lemma value_irred X : value X irred step X.
Proof.
  intros vs Y C. induction C; repeat inv_SKvvalue;eauto.
Qed.

Lemma star_value X Y: value X X >>* Y X = Y.
Proof.
  intros vs st. inv st. reflexivity. destruct (value_irred vs H).
Qed.

Lemma irred_appL X Y: irred step (X Y) irred step X.
Proof.
  intros H. intros t' C; induction C; eapply H; eauto.
Qed.

Lemma irred_appR X Y: irred step (X Y) irred step Y.
Proof.
  intros H. intros t' C; induction C; eapply H; eauto.
Qed.

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).
Proof.
  induction X.
  -right. intros x. inv x.
  -left. auto.
  -left. auto.
  -destruct IHX1. destruct IHX2.
   +left. now constructor.
   +right. intros H. now inv H.
   +right. intros H. now inv H.
Defined.

Lemma normal_value X : closed X irred step X value X.
Proof with eauto.
  intros cX iX. induction cX. eauto. eauto. pose (irred_appL iX). pose (irred_appR iX). assert (value X) by auto. assert (value Y) by auto. destruct H; auto. inv cX1. edestruct iX;eauto. edestruct iX;eauto.
Qed.

Lemma I_closed: closed I.
Proof.
  repeat constructor.
Qed.

Hint Resolve I_closed : value.

Uniform Confluence


Lemma SK_UC: uniformly_confluent step.
Proof.
  apply UD_UC.
  intros X. induction X;intros Y Z R1 R;repeat inv_SKvstep;auto 2;try ( now (edestruct value_irred;[ |eauto]);eauto) || now (right;eexists;eauto) .
  -destruct (IHX1 _ _ H2 H3) as [? | [? [? ?]]]. subst;eauto. right; eexists;eauto.
  -destruct (IHX2 _ _ H2 H3) as [? | [? [? ?]]]. subst;eauto. right; eexists;eauto.
Qed.

Lemma SK_church_rosser : church_rosser step.
Proof.
  apply confluent_CR. apply UC_confluent. exact SK_UC.
Qed.

Lemma equiv_value X Y : value Y X =*= Y X >>* Y.
Proof.
  intros v H. destruct (SK_church_rosser H) as [u [su tu]]. now apply star_value in tu;subst.
Qed.

Lemma equiv_value_eq X Y : value X value Y X =*= Y X = Y.
Proof.
  intros vs vt H. destruct (SK_church_rosser H) as [u [su tu]]. now apply star_value in tu;apply star_value in su;subst.
Qed.

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))).
Proof.
  revert X Y. induction k;intros ? ? R. inv R. tauto. right.
  rewrite (pow_add _ 1) in R. destruct R as (X' & S & R). apply rcomp_1 in S. destruct S as [| | X1 X1' X2 S|X1 X2 X2' S].
  -eexists _,_,_,_,0,0. repeat split. right. repeat eexists; eauto.
  -eexists _,_,_,_,0,0. repeat split. right. repeat eexists; eauto.
  -apply IHk in R as [[-> ->]|(? & ? &?&?&?&?&HHH)];[|intuition;subst].
   +eexists _,_,X1',_,1,0. repeat split. firstorder. left. intuition.
   +inv H1. eexists _,_,x1,x2,(1+x3),x4. repeat eexists; eauto.
   +inv H1. destruct H2 as (?&?&?). intuition.
    eexists _,_,x1,x2,(1+x3),x4. repeat eexists;eauto. right. repeat eexists;eauto. omega.
  -apply IHk in R as [[-> ->]|(? & ? &?&?&?&?&HHH)];[|intuition;subst].
   +eexists _,_,_,X2',0,1. repeat split. firstorder. left. intuition.
   +inv H1. eexists _,_,x1,x2,x3,(1+x4). repeat eexists; eauto.
   +inv H1. destruct H2 as (?&?&?). intuition.
    eexists _,_,x1,x2,x3,(1+x4). repeat eexists;eauto. right. repeat eexists;eauto. omega.
Qed.

Properties involving closedness


Lemma closed_app X Y : closed (X Y) closed X closed Y.
Proof.
  split;intros H;inv H;intuition.
Qed.

Lemma step_closed X Y : closed X X >>> Y closed Y.
Proof.
  intros C R. induction R; repeat inv_closed; eauto.
Qed.

Lemma star_closed X Y : closed X X >>* Y closed Y.
Proof.
  intros C R. induction R; repeat inv_closed; eauto using step_closed.
Qed.

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.
Proof.
  cbv. tauto.
Qed.
Hint Resolve maxValue_Value :value.

Unique Sucessors for Redex


Lemma value_step_unique X Y Z1 Z2: value X value Y (X Y) >>> Z1 (X Y) >>> Z2 Z1=Z2.
Proof.
  intros vX vY R1 R2. repeat inv_SKvstep; repeat inv_SKvvalue;try reflexivity; assert (C:=value_irred); cbv in C; firstorder.
Qed.

Substitutivity of values


Lemma maxValueSubst X Y y: maxValue Y (value (subst X y Y) value X).
Proof.
  intros [vY mY]. apply size_induction with (f:=size) (x:=X);clear X;intros X IH vss.
  destruct X;auto. simpl in vss. assert (value X2). {apply IH; simpl in ×. omega. now inv vss. } destruct X1;auto.
  -simpl in vss. decide (y=n);subst;auto. destruct (mY _ vss). decide (y<n); inv vss.
  -assert (value X1_2). {apply IH; simpl in ×. omega. now inv vss. } destruct X1_1;auto;simpl in vss.
   +decide (y=n); subst;auto; inv vss. destruct (mY S);auto.
   +inv vss.
   +inv vss.
Qed.

Lemma valueSubst X Y y: value Y (value X value (subst X y Y)).
Proof.
  intros vt vs. induction vs;simpl;auto.
  decide (y=x);auto.
Qed.

Lemma valueSubst_iff X Y y: maxValue Y ((value (subst X y Y) value X)).
Proof.
  split. now apply maxValueSubst. apply valueSubst. now apply maxValue_Value.
Qed.

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.
Proof.
  unfold eval. intuition auto using equiv_value. now rewrite H0.
Qed.

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).
Proof.
  induction X as [y| | | X Hs Y Ht];try now (left;auto).
  -decide (x=y);subst.
   +right. intros H. inv H. congruence.
   +left. auto.
  -destruct Hs. destruct Ht.
   +left;auto.
   +right;intros H;now inv H.
   +right;intros H;now inv H.
Defined.

Lemma varClosedApp_iff x X Y : varClosed x (X Y) varClosed x X varClosed x Y.
Proof.
  split;intros H;inv H;auto.
Qed.

Lemma varClosedVar_iff x y : varClosed x (var y) x y.
Proof.
  split;intros H;try inv H;auto.
Qed.

Lemma closed_varClosed x X : closed X varClosed x X.
  induction 1; eauto.
Qed.
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)).
Proof.
  intros ? ?. induction X;simpl;split;
  repeat (dec || inv_varClosed || intuition).
Qed.

Lemma varClosed_closed X : ( x, varClosed x X) closed X.
Proof.
  induction X;try now (split;intros H;try inv H;eauto 10).
  -setoid_rewrite varClosedVar_iff. split;intros H. specialize (H n). intuition. inv H.
  -setoid_rewrite varClosedApp_iff. rewrite closed_app. firstorder.
Qed.