Library SK

Require Import ARS.
Set Implicit Arguments.
Unset Strict Implicit.


Inductive term : Type :=
| Var : nat -> term
| K : term
| S : term
| App : term -> term -> term.

Coercion App : term >-> Funclass.
Implicit Types s t u : term.

Reserved Notation "s ´>>´ t" (at level 50).
Inductive pstep : term -> term -> Prop :=
| pstepR s :
    s >> s
| pstepK s s´ t:
    s >> s´ -> K s t >> s´
| pstepS s s´ t t´ u u´ :
    s >> s´ -> t >> t´ -> u >> u´ -> S s t u >> s´ u´ (t´ u´)
| pstepA s s´ t t´ :
    s >> s´ -> t >> t´ -> s t >> s´ t´
where "s ´>>´ t" := (pstep s t).

Fixpoint rho s :=
  match s with
  | App (App K s) t => rho s
  | App (App (App S s) t) u => (rho s) (rho u) ((rho t) (rho u))
  | App s t => (rho s) (rho t)
  | u => u
  end.

Functional Scheme rho_ind := Induction for rho Sort Prop.

Ltac inv H := inversion H; clear H; subst.

Ltac inv_pstep :=
  match goal with
    | H : pstep (Var _) _ |- _ => inv H
    | H : pstep (App _ _) _ |- _ => inv H
    | H : pstep K _ |- _ => inv H
    | H : pstep S _ |- _ => inv H
  end.

Lemma rho_triangle :
  triangle pstep rho.
Proof.
  intros s. apply rho_ind; intros; subst;
  do 4 (inv_pstep; auto using pstep).
Qed.

Inductive step : term -> term -> Prop :=
| stepK s t : K s t > s
| stepS s t u : S s t u > s u (t u)
| stepAL s s´ t : s > s´ -> s t > s´ t
| stepAR s t t´ : t > t´ -> s t > s t´
where "s ´>´ t" := (step s t).

Notation "s ´>*´ t" := (star step s t) (at level 50).

Lemma step_pstep s t :
  s > t -> s >> t.
Proof.
  induction 1; auto using pstep.
Qed.

Lemma step_star_comp s s´ t t´ :
  s >* s´ -> t >* t´ -> s t >* s´ t´.
Proof.
  apply star_proper2; now constructor.
Qed.

Lemma pstep_star_step s t :
  s >> t -> s >* t.
Proof.
  induction 1.
  - apply starR.
  - eapply starRS. econstructor. assumption.
  - eapply starRS. econstructor. auto using step_star_comp.
  - auto using step_star_comp.
Qed.

Theorem church_rosser :
  CR step.
Proof.
  apply (cr_method (S := pstep) (rho := rho)).
  - apply step_pstep.
  - apply pstep_star_step.
  - apply rho_triangle.
Qed.