# Combinatory Logic

Require Export ARS.

Definition NS := S.

Definition var := nat.

Implicit Types x : var.

Inductive term := Var x | K | S | App (s t : term).

Coercion App : term >-> Funclass.

Implicit Types s t u v : term.

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

Definition I : term := S K K.

Lemma I_correct s :
star step (I s) s.

Proof.

repeat econstructor.

Qed.

Preredexes

Inductive predex : term -> Prop :=
| predexK u : predex (K u)
| predexS u v : predex (S u v).

Lemma predex_dec s :
dec (predex s).

Proof
with try (left; now constructor) ||
(right; intros A; now inv A).

destruct s as [| | |s v]...

destruct s as [| | |s u]...

destruct s...

Qed.

Lemma reducible_dec s :
dec (reducible step s).

Proof
with eauto using step, predex.

induction s as [x| | |s IHs t IHt];
try (right; intros [t A]; now inv A).

destruct IHs as [A|A].

- left.
destruct A...
- destruct IHt as [B|B].

+ left.
destruct B...
+ destruct (predex_dec s) as [C|C].

* left.
inv C...
* right.
intros [u D]. inv D...
Qed.

Parallel Reduction

Inductive pstep : term -> term -> Prop :=
| pstepK s s' t :
pstep s s' -> pstep (K s t) s'
| pstepS s s' t t' u u' :
pstep s s' -> pstep t t' -> pstep u u' ->
pstep (S s t u) (s' u' (t' u'))
| pstepA s s' t t' :
pstep s s' -> pstep t t' -> pstep (s t) (s' t')
| pstepRV x :
pstep (Var x) (Var x)
| pstepRK :
pstep K K
| pstepRS :
pstep S S.

Lemma pstep_refl s :
pstep s s.

Proof.

induction s; eauto using pstep.

Qed.

Lemma step_pstep s t :
step s t -> pstep s t.

Proof.

induction 1; eauto using pstep, pstep_refl.

Qed.

Lemma red_app s s' t t' :
star step s s' -> star step t t' -> star step (s t) (s' t').

Proof
with eauto using star, step, star_trans.

induction 1...
induction 1...
Qed.

Lemma pstep_step s t : pstep s t -> star step s t.

Proof.

induction 1; eauto using star, step, red_app.

Qed.

Lemma star_step_star_pstep :
star step =2 star pstep.

Proof.

apply interpolation.
apply step_pstep. apply pstep_step.
Qed.

Confluence

Fixpoint rho (s : term) : term :=
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)
| s => s
end.

Lemma rho_hom s t :
~ predex s -> rho (s t) = (rho s) (rho t).

Proof
with try reflexivity || (exfalso; apply A; now constructor).

intros A.

destruct s as [| | |s v]...

destruct s as [| | |s u]...

destruct s...

Qed.

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

Lemma rho_triangle :
triangle pstep rho.

Proof
with eauto using pstep.

intros s s' A.
induction A...
destruct (predex_dec s) as [B|B].

- inv B; repeat inv_pstep...

- rewrite (rho_hom _ B)...

Qed.

Theorem step_confluent :
confluent step.

Proof.

apply (@confluent_stable _ _ pstep).

- exact star_step_star_pstep.

- apply semi_confluent_confluent.
apply diamond_to_semi_confluent.
apply (triangle_to_diamond (rho := rho)).
exact rho_triangle.
Qed.

rho sound and cofinal for step

Lemma rho_sound :
sound step rho.

Proof.

apply (@sound_stable _ _ _ pstep).

- exact star_step_star_pstep.

- apply triangle_to_sound.
exact rho_triangle. exact pstep_refl.
Qed.

Lemma rho_cofinal :
cofinal step rho.

Proof.

apply (@cofinal_stable _ _ _ pstep).

- exact star_step_star_pstep.

- apply triangle_to_cofinal.
exact rho_triangle.
Qed.

Substitution

Definition substitution := var -> term.

Implicit Types sigma tau : substitution.

Fixpoint subst sigma s : term :=
match s with
| App s t => (subst sigma s) (subst sigma t)
| Var x => sigma x
| s => s
end.

Notation "sigma '!' s" := (subst sigma s) (at level 52, right associativity).

Lemma step_substitutive s t sigma :
step s t -> step (sigma!s) (sigma!t).

Proof.

induction 1; simpl; eauto using step.

Qed.

Abstraction

Fixpoint lam (x : var) (s : term) : term :=
match s with
| Var y => if decision (x = y) then I else K (Var y)
| App s t => S (lam x s) (lam x t)
| s => K s
end.

Definition sub (x : var) (s : term) : substitution :=
fun y => if decision (x = y) then s else Var y.

Lemma lam_correct x s t :
star step (lam x s t) (sub x t ! s).

Proof
with simpl; try now repeat econstructor.

induction s...

- unfold sub.
decide (x = x0); subst...
- econstructor.

+ constructor.

+ apply red_app; assumption.

Qed.

# Simple Typing

Inductive type : Type := BT (X : nat) | AT (A B : type).

Notation "A '~>' B" := (AT A B) (at level 70, right associativity).

Definition context : Type := var -> type -> Prop.

Inductive ty (Gamma : context) : term -> type -> Prop :=
| tyV A x :
Gamma x A -> ty Gamma (Var x) A
| tyK A B :
ty Gamma K (A~>B~>A)
| tyS A B C :
ty Gamma S ((A~>B~>C)~>(A~>B)~>A~>C)
| tyA A B s t :
ty Gamma s (A~>B) -> ty Gamma t A -> ty Gamma (s t) B.

Lemma ty_I Gamma A :
ty Gamma I (A~>A).

Proof.

repeat econstructor.

Grab Existential Variables.

exact A.

Qed.

Subject Reduction

Ltac inv_ty := match goal with
| H : ty _ K _ |- _ => inv H
| H : ty _ S _ |- _ => inv H
| H : ty _ (App _ _) _ |- _ => inv H
end.

Lemma subject_reduction Gamma s s' A :
ty Gamma s A -> step s s' -> ty Gamma s' A.

Proof.

intros D E.
revert A D.
induction E; intros A D; repeat inv_ty; eauto using ty.

Qed.

Abstraction is well-typed

Section AWT.

Variable Gamma : context.

Variable Gamma_fun : forall x A B, Gamma x A -> Gamma x B -> A = B.

Lemma ty_abs x s A B :
Gamma x A -> ty Gamma s B -> ty Gamma (lam x s) (A~>B).

Proof.

intros D E.

induction E; simpl; eauto using ty.

decide (x=x0).

- subst.
rewrite (Gamma_fun H D). apply ty_I.
- eauto using ty.

Qed.

End AWT.

A substitution lemma

Lemma ty_subst Gamma Delta s A sigma :
ty Gamma s A -> (forall x B, Gamma x B -> ty Delta (sigma x) B) -> ty Delta (sigma!s) A.

Proof.

intros D E.
induction D; simpl; eauto using ty.
Qed.

Strong Normalization

Fixpoint L (s : term) (A : type) : Prop :=
match A with
| BT _ => SN step s
| AT A B => forall t, L t A -> L (s t) B
end.

Lemma L_step A s s' :
L s A -> step s s' -> L s' A.

Proof.

revert s s'.

induction A as [X|A IHA B IHB]; simpl; intros s s' D E.

- inv D; auto.

- intros t F.
eapply IHB.
+ apply D, F.

+ eauto using step.

Qed.

Definition neutral (s : term) : Prop :=
match s with
| K | S | App K _ | App S _ | App (App S _) _ => False
| _ => True
end.

Fact neutral_app s t :
neutral s -> neutral (s t).

Proof.

destruct s as [|Â |Â |s u]; auto.
destruct s; simpl; auto.
Qed.

Definition L_red s A := (forall s', step s s' -> L s' A) -> L s A.

Arguments L_red s A /.

Lemma L_two_in_one A :
(forall s, L s A -> SN step s) /\ (forall s, neutral s -> L_red s A).

Proof.

induction A as [X|A IHA B IHB]; simpl.

- split.
now auto. intros s _. apply SNI.
- destruct IHA as [IHA1 IHA2].

destruct IHB as [IHB1 IHB2].

split.

+ intros s D.

pose (x:=Var 0).

cut (SN step (s x)).

{ apply (SN_preimage_closed (h:= fun s => s x)).
eauto using step. }
apply IHB1, D.

apply IHA2.
now trivial. intros t E; inv E.
+ intros s D E t F.

assert (G := IHA1 t F).

induction G as [t G IHSN].

apply IHB2.

* apply neutral_app, D.

* { intros u H.
- now apply E, F.

- apply IHSN; trivial.
eauto using L_step. }
Qed.

Corollary L_SN A s :
L s A -> SN step s.

Proof.

apply L_two_in_one.

Qed.

Corollary L_neutral A s :
neutral s -> L_red s A.

Proof.

apply L_two_in_one.

Qed.

Corollary L_var A x :
L (Var x) A.

Proof.

apply L_neutral.
now trivial. intros s E. inv E.
Qed.

Ltac inv_step := match goal with
| H : step K _ |- _ => inv H
| H : step S _ |- _ => inv H
| H : step (App _ _) _ |- _ => inv H
end.

Lemma L_K A B :
L K (A~>B~>A).

Proof.

simpl.
intros s Ls.
assert (Ss := L_SN Ls).
induction Ss as [s _ IHs]. intros t Lt.
assert (St := L_SN Lt).
induction St as [t _ IHt].
apply L_neutral.
now trivial. intros u D.
repeat inv_step; eauto using L_step.

Qed.

Lemma L_S A B C :
L S ((A~>B~>C)~>(A~>B)~>A~>C).

Proof.

hnf.
intros s Ls.
assert (Ss := L_SN Ls).
induction Ss as [s _ IHs]. hnf. intros t Lt.
assert (St := L_SN Lt).
induction St as [t _ IHt]. hnf. intros u Lu.
assert (Su := L_SN Lu).
induction Su as [u _ IHu].
apply L_neutral.
now trivial. intros v D. simpl L in *.
repeat inv_step; eauto 6 using L_step, step.

Qed.

Lemma ty_L Gamma s A :
ty Gamma s A -> L s A.

Proof.

intros D.

induction D as [|A B|A B C|A B s t _ IHs _ IHt].

- apply L_var.

- apply L_K.

- apply L_S.

- apply IHs, IHt.

Qed.

Theorem strong_normalization Gamma s A :
ty Gamma s A -> SN step s.

Proof.

intros D.
eapply L_SN, ty_L, D.
Qed.