Library CL
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.
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. inv H; try contradiction D.
- 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.