Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
branch: master
Fetching contributors…

Cannot retrieve contributors at this time

177 lines (162 sloc) 6.44 kB
(** This file contains the termination argument via logical relations *)
Require Export Semantics.
Open Scope t_scope.
Open Scope list_scope.
Section Definitions.
(* Logical relation at 2 *)
Inductive R2 : te -> Prop :=
| RT : forall M (HRed : M ↦* TT), R2 M
| RF : forall M (HRed : M ↦* FF), R2 M.
(* Logical relation at type ω *)
Inductive Rω : te -> Prop :=
| Rω_z : forall M (HRed : M ↦* z), Rω M
| Rω_s : forall M M' (HRed : M ↦* s M') (HR : Rω M'), Rω M.
(* Logical relation at type stream, parameterised with the relation at element type *)
CoInductive Rstream : (te -> Type) -> te -> Prop :=
| Rs : forall M P (HHD : P (hd M)) (HTL : Rstream P (tl M)), Rstream P M.
(* The reducibility relation: has to be defined as a fixpoint, since Coq doesn't allow
for negative occurrences of a relation in the A₁ → A₂ case *)
Fixpoint R A M : Prop :=
match A with
| 2 => R2 M
| ω => Rω M
| A₁ → A₂ => forall N (HTN : nil ⊢ N ::: A₁) (HR : R A₁ N), R A₂ (M @ N)
| stream A => Rstream (R A) M
end.
(* Reduciblity for the whole contexts *)
Fixpoint rctx γ Γ :=
match γ, Γ with
| nil, nil => True
| M :: γ, A :: Γ => R A M /\ rctx γ Γ
| _, _ => False
end.
End Definitions.
Section Termination_proof.
Lemma head_expansion : forall A M N
(HR : R A N)
(HS : M ↦ N),
R A M.
Proof.
induction A; intros; simpl in *.
(* bool *)
inversion HR; [ apply RT | apply RF ]; econstructor; eassumption.
(* nat *)
inversion HR.
apply Rω_z; unfold steps; econstructor; eassumption.
apply Rω_s with M'; [| assumption]; econstructor; eassumption.
(* arr *)
intros.
eapply IHA2; [| apply red_appC; eassumption].
apply HR; assumption.
(* stream *)
(* We need coinduction to prove the property here, and a stronger lemma. *)
assert (HT : exists K : te, (M ↦ K) /\ Rstream (R A) K)
by (exists N; tauto).
clear HS HR; destruct HT as [K [HRed HR]]; generalize dependent K; revert M.
cofix; intros.
inversion HR; subst; apply Rs.
eapply IHA; [eassumption | apply red_hdC; eassumption].
eapply head_expansion; [| eassumption].
apply red_tlC; assumption.
Qed.
(* lifting of head expansion to reflexive transitive closure *)
Lemma head_exp_star : forall A M N
(HR : R A N)
(HS : M ↦* N),
R A M.
Proof.
intros; induction HS; [assumption |].
eapply head_expansion; [| eassumption].
tauto.
Qed.
Lemma types_red : forall Γ M A γ
(HT : Γ ⊢ M ::: A)
(HR : rctx γ Γ)
(HΓ : tcmt γ Γ),
R A [γ!0]M.
Proof.
intros; generalize dependent γ; induction HT; intros.
(* var *)
assert (HT := subst_var _ _ _ 0 _ HFind HΓ); rewrite plus_comm in HT; simpl in *.
destruct HT as [HT _].
revert HT; generalize ([γ ! 0](#n)) as M; intros M; generalize dependent Γ;
revert n; induction γ; simpl; destruct Γ; intros; try contradiction; [|].
destruct n; discriminate.
destruct n; simpl in *.
inversion HT; subst a.
inversion HFind; subst t; tauto.
destruct HR as [Ha HR]; destruct HΓ as [Ht HΓ]; eapply IHγ; eassumption.
(* lam *)
simpl; intros; rewrite sub_lam.
eapply head_expansion; [| apply red_β].
rewrite subcomp; apply IHHT; simpl; tauto.
(* appl *)
rewrite sub_app; simpl in IHHT1.
apply IHHT1; intuition; [].
eapply subst_types; simpl; eassumption.
(* z *)
apply Rω_z; rewrite sub_z; constructor.
(* s *)
simpl in *; rewrite sub_s; eapply Rω_s; [constructor | intuition].
(* rec *)
specialize (IHHT1 _ HR HΓ); specialize (IHHT2 _ HR HΓ); simpl in *.
assert (HTR : nil ⊢ [γ ! 0]M ::: ω) by (eapply subst_types; simpl; eassumption).
rewrite sub_rec; revert IHHT1 HTR; generalize ([γ ! 0]M); intros K HRK HTK;
induction HRK.
apply head_exp_star with (rec z [γ ! 0]M₀ [γ ! 2]M₁);
[| apply rec_cong_star; assumption].
eapply head_expansion; [| apply red_recz]; assumption.
eapply head_exp_star with (rec (s M') [γ ! 0]M₀ [γ ! 2]M₁);
[| apply rec_cong_star; assumption].
eapply head_expansion; [| apply red_recs].
assert (HST : nil ⊢ s M' ::: ω).
induction HRed; [assumption |].
eapply IHHRed, preservation; eassumption.
inversion HST; subst.
rewrite subcomp; apply IHHT3; simpl; intuition; [].
apply tc_rec; [assumption | |]; eapply subst_types; simpl; eassumption.
(* hd *)
specialize (IHHT _ HR HΓ); inversion IHHT; subst.
rewrite sub_hd; assumption.
(* tl *)
specialize (IHHT _ HR HΓ); inversion IHHT; subst.
rewrite sub_tl; assumption.
(* seed *)
specialize (IHHT1 _ HR HΓ).
assert (HTR : nil ⊢ [γ ! 0]M ::: A) by (eapply subst_types; simpl; eassumption).
clear HT1; simpl; rewrite sub_seed.
assert (exists K, (seed [γ ! 0]M [γ ! 1]M₀ [γ ! 1]M₁ ↦* seed K [γ ! 1]M₀ [γ ! 1]M₁)
/\ (nil ⊢ K ::: A) /\ R A K).
simpl; eexists; split; [constructor | split; assumption].
simpl in H; destruct H as [K [HRed [HTK HRK]]]; generalize dependent K.
generalize (seed [γ ! 0]M [γ ! 1]M₀ [γ ! 1]M₁) as N.
cofix; intros; apply Rs.
eapply head_exp_star; [| eapply hd_cong_star; eassumption].
eapply head_expansion; [| apply red_hds].
change (R A [K :: nil ! 0]([γ ! 1]M₀)); rewrite subcomp.
apply IHHT2; simpl; tauto.
apply types_red with [K ↑ 0]([γ ! 1]M₁); clear types_red.
apply clos_rt_rt1n; eapply rt_trans;
[apply clos_rt1n_rt, tl_cong_star; eassumption |].
apply rt_step, red_tls.
change (nil ⊢ [K :: nil ! 0]([γ ! 1]M₁) ::: A); rewrite subcomp.
eapply subst_types; [| simpl; eassumption]; simpl; tauto.
change (R A [K :: nil ! 0]([γ ! 1]M₁)); rewrite subcomp.
apply IHHT3; simpl; tauto.
(* TT *)
rewrite sub_TT; apply RT; constructor.
(* FF *)
rewrite sub_FF; apply RF; constructor.
Qed.
Theorem termination : forall M (HT : nil ⊢ M ::: ω),
exists V, value V /\ (M ↦* V).
Proof.
intros.
apply types_red with (γ := nil) in HT; [| exact I | exact I].
inversion HT; subst.
(* z *)
exists z; split; [apply val_z | assumption].
(* s *)
exists (s M'); split; [apply val_s | assumption].
Qed.
End Termination_proof.
Jump to Line
Something went wrong with that request. Please try again.