SKConversion

Section SKTranslation.
  Definition S := (Lam (Lam (Lam ((2 0) (1 0))))).
  Definition K := (Lam (Lam 1)).

  Notation Is := (S K K).

  Notation "s ≡ t" := (star (sym step) s t)(at level 71).

  Lemma EqComEqR s t t': t ≡ t' -> s t ≡ s t'.
  Proof.
    induction 1.
    - constructor.
    - destruct H.
      + econstructor.
        * left. apply stepAppR,H.
        * assumption.
      + econstructor.
        * right. apply stepAppR,H.
        * assumption.
  Defined.

  Lemma EqComEqL s t s': s ≡ s' -> s t ≡ s' t.
  Proof.
    induction 1;trivial.
    destruct H;econstructor;try eassumption;
      [left|right];now apply stepAppL.
  Defined.

  Lemma EqComEq s t s' t': s ≡ s' -> t ≡ t' -> s t ≡ s' t'.
  Proof.
    intros H H1.
    etransitivity.
    - apply EqComEqR,H1.
    - now apply EqComEqL,H.
  Defined.

  Lemma EqLam s s': s ≡ s' -> Lam s ≡ Lam s'.
  Proof.
    induction 1.
    - reflexivity.
    - transitivity (Lam x');trivial.
      inv H;econstructor;[left| |right|];constructor;trivial.
  Defined.

  Lemma StarLam s s': s≻* s' -> Lam s ≻* Lam s'.
  Proof.
    induction 1.
    - constructor.
    - econstructor.
      + constructor. apply H.
      + apply IHstar.
  Defined.

  Lemma StarApp s s' t t': s≻* s' -> t ≻* t' -> s t ≻* s' t'.
  Proof.
    induction 1 in t, t' |- *;intros H1.
    - induction H1.
      + constructor.
      + econstructor.
        * constructor 4. apply H.
        * apply IHstar.
    - econstructor.
      + constructor.
        apply H.
      + now apply IHstar.
  Defined.

  Ltac reduce' := econstructor 2;[repeat constructor|cbn].

  Lemma Id: Lam 0 ≡ S K K.
  Proof.
    unfold S, K.
    symmetry.
    apply star_starsym.
    do 4 reduce'.
    constructor.
  Defined.

  Lemma KLam s: K s ≡ Lam (rename Datatypes.S s).
  Proof.
    unfold K.
    now reduce'.
  Defined.

  Lemma AppLam s t: Lam (s t) ≡ S (Lam s) (Lam t).
  Proof.
    unfold S.
    symmetry.
    apply star_starsym.
    reduce'.
    reduce'.
    reduce'.
    eauto with *.
    autorewrite with basic.
    apply StarLam, StarApp.
    - cbn.
      unfold upr.
      rewrite rename_subst.
      autorewrite with basic.
      unfold scomp.
      unfold funcomp.
      cbn.
      admit.
    - reduce'.
      unfold upr.
      rewrite rename_subst.
      autorewrite with basic.
      eauto with basic.
      unfold funcomp.
      admit.
      (* induction t. *)
      (* + cbn. induction x. *)
      (*   * constructor. *)
      (*   * constructor. *)
      (* + cbn. *)
      (*   apply StarApp;trivial. *)
      (* + cbn. apply StarLam. *)
      (*   rewrite upE. *)
  Admitted. (* I strongly believe this is true *)

  Inductive onlySK : term -> Type :=
    onlyK : onlySK K
  | onlyS : onlySK S
  | onlyVar x : onlySK (Var x)
  | onlyApp s t: onlySK s -> onlySK t -> onlySK (s t).

  Inductive pureSK : term -> Type :=
    pureK : pureSK K
  | pureS : pureSK S
  | pureApp s t: pureSK s -> pureSK t -> pureSK (s t).

  Lemma δ' s: onlySK s -> {t & prod (t ≡ Lam s) (onlySK t)}.
  Proof.
    induction 1 using onlySK_rect.
    - exists (K K);split.
      + apply KLam.
      + do 2 constructor.
    - exists (K S);split.
      + apply KLam.
      + do 2 constructor.
    - destruct x.
      + exists (S K K);split.
        * symmetry. apply Id.
        * repeat constructor.
      + eexists;split.
        * change (Var (Datatypes.S x)) with (rename Datatypes.S (x)).
          apply KLam.
        * repeat constructor.
    - destruct IHonlySK1 as [? []].
      destruct IHonlySK2 as [? []].
      exists (S x x0);split.
      + transitivity (S (Lam s) (Lam t)).
        * repeat apply EqComEq;trivial.
        * symmetry. apply AppLam.
      + repeat constructor;trivial.
  Defined.

  Lemma γ s: {t & prod (t ≡ s) (onlySK t)}.
  Proof.
    induction s as [x|s [s' [IHs H0]] t [t' [IHt H1]]|s [s' [IHs H]]] using term_rect.
    - exists x;split;trivial.
      constructor.
    - eexists;split.
      + apply EqComEq;eassumption.
      + now constructor.
    - destruct (δ' H) as [s'' [H1 H2]].
      exists s'';split;trivial.
      transitivity (Lam s');[|apply EqLam];trivial.
  Defined.

  Definition succ := Lam(Lam(Lam(0 2))).
  Eval cbn in (projT1(γ succ)).

  Lemma pureSKConv s n: (forall m, n<=m -> ~ free m s) -> forall m, n<=m -> ~free m (projT1(γ s)).
  Proof.
    induction s;intros H1 m H2 H3.
    - now apply (H1 m).
    - cbn in H3.
  Abort.

End SKTranslation.