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

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.