Require Export Preliminaries.
Inductive term : Type :=
| var (n : nat) : term
| app (s : term) (t : term) : term
| lambda (s : term).
Definition lam s := exists t, s = lambda t.
Hint Unfold lam.
Lemma lambda_lam s : lam (lambda s).
Proof.
now exists s.
Qed.
Hint Resolve lambda_lam.
Fixpoint size t :=
match t with
| var n => 1
| app s t => size s + size t
| lambda s => 1 + size s
end.
Coercion app : term >-> Funclass.
Coercion var : nat >-> term.
Instance term_eq_dec : eq_dec term.
Proof.
intros ? ?; hnf; repeat decide equality.
Defined.
Hint Resolve term_eq_dec.
Require Import String.
Inductive bterm : Type :=
| bvar (x : string) : bterm
| bapp (s t : bterm) : bterm
| blambda (x : string) (s : bterm) : bterm
| bter (s : term) : bterm.
Open Scope string_scope.
Instance eq_dec_string : eq_dec string.
Proof.
eapply string_dec.
Defined.
Fixpoint convert' (F : list string) (s : bterm) : term := match s with
| bvar x => match pos x F with None => 100 | Some t => t end
| bapp s t => app (convert' F s) (convert' F t)
| blambda x s => lambda (convert' (x:: F) s)
| bter t => t
end.
Coercion bvar : string >-> bterm.
Coercion bapp : bterm >-> Funclass.
Definition convert := convert' [].
Coercion convert : bterm >-> term.
Arguments convert /.
Hint Unfold convert: cbv.
Notation ".\ x , .. , y ; t" := ((blambda x .. (blambda y t) .. )) (at level 100, right associativity).
Notation "'λ' x , .. , y ; t" := ((blambda x .. (blambda y t) .. )) (at level 100, right associativity).
Notation "'!' s" := (bter s) (at level 0).
Implicit Types s t u v : term.
Implicit Types p q : term -> Prop.
Implicit Types n m k l : nat.
Fixpoint subst s k u :=
match s with
| var n => if decision (n = k) then u else (var n)
| app s t => app (subst s k u) (subst t k u)
| lambda s => lambda (subst s (S k) u)
end.
Hint Unfold subst : cbv.
Fixpoint bound (k : nat) (t : term) : bool :=
match t with
| var n => if decision (n < k) then true else false
| app s t => andb (bound k s) (bound k t)
| lambda s => bound (S k) s
end.
Definition closed s := bound 0 s = true.
Definition proc s := closed s /\ lam s.
Lemma bound_ge k s : bound k s = true -> forall m, m >= k -> bound m s = true.
Proof.
revert k; induction s; cbn; intros.
- unfold bound in *. decide (n < k); decide (n < m); try congruence. omega.
- eapply Bool.andb_true_iff in H as []. erewrite IHs1, IHs2; eauto.
- eapply IHs. eassumption. omega.
Qed.
Lemma bound_closed_k s k n u : bound n s = true -> k >= n -> subst s k u = s.
Proof with eauto.
revert k n; induction s; intros; cbn.
- decide (n = k)... subst. unfold bound in H. decide (k < n0). omega. congruence.
- cbn in H. eapply Bool.andb_true_iff in H as []. erewrite IHs1, IHs2...
- erewrite IHs... omega.
Qed.
Lemma closed_subst s k u : closed s -> subst s k u = s.
Proof.
intros. eapply bound_ge in H. eapply bound_closed_k in H; eauto. omega.
Qed.
Lemma closed_app s t : closed (s t) -> closed s /\ closed t.
Proof.
intros cls. now eapply Bool.andb_true_iff in cls.
Qed.
Lemma app_closed s t : closed s -> closed t -> closed (s t).
Proof.
unfold closed. cbn. now intros -> ->.
Qed.
Definition I : term := .\"x"; "x".
Definition T : term := .\"x","y"; "x".
Definition F : term := .\"x","y"; "y".
Definition omega : term := .\"x"; "x" "x".
Definition Omega := omega omega.
Definition D: term := lambda (omega omega).
Inductive evaluates : term -> term -> Prop :=
evaluates_lam s : evaluates (lambda s) (lambda s)
| evaluates_app s t u v w : evaluates s (lambda u) -> evaluates t v -> evaluates (subst u 0 v) w ->
evaluates (s t) w.
Hint Constructors evaluates.
Notation "s '▷' t" := (evaluates s t) (at level 50).
Definition eva s := exists t, evaluates s t.
Hint Unfold eva.
Lemma evaluates_abst s t : s ▷ t -> lam t.
Proof.
induction 1; eauto.
Qed.
(* Counterexample to Fact 5.2 *)
Lemma evaluates_bound : ~ forall s t n, s ▷ t -> bound n s = true -> bound n t = true.
Proof.
intros H. specialize (H ((lambda (lambda 2)) (lambda 1)) (lambda 2) 1).
cbn in H. eapply Bool.diff_false_true, H; eauto.
repeat econstructor.
Qed.
Lemma bound_subst s t k : bound (S k) s = true -> bound k t = true -> bound k (subst s k t) = true.
Proof.
revert k t; induction s; intros k t cls_s cls_t; cbn.
- decide (n = k). subst. eauto. unfold bound in cls_s.
decide (n < S k). unfold bound. decide (n < k). reflexivity. omega. congruence.
- cbn in cls_s. eapply Bool.andb_true_iff in cls_s as []. rewrite IHs1, IHs2; eauto.
- cbn in cls_s. rewrite IHs; eauto. eapply bound_ge; eauto.
Qed.
Lemma evaluates_closed s t : s ▷ t -> closed s -> closed t.
Proof.
induction 1; cbn; intros.
- eauto.
- unfold closed in H2. cbn in H2. eapply Bool.andb_true_iff in H2 as [].
firstorder using bound_subst.
Qed.
Lemma app_eva s t : eva (s t) -> eva s /\ eva t.
Proof.
inversion 1. inv H0. firstorder.
Qed.
Lemma F_eva s t : eva (F s t) <-> eva s /\ eva t.
Proof.
intuition.
- now eapply app_eva in H as (H % app_eva & ?).
- now eapply app_eva in H.
- destruct H0, H1. exists x0. econstructor. econstructor. econstructor.
eassumption. econstructor. eassumption. cbn. eapply evaluates_abst in H0. firstorder. subst.
econstructor.
Qed.
Lemma F_correct s t : lam s -> lam t -> F s t ▷ t.
Proof.
intros [? ->] [? ->]. repeat econstructor.
Qed.
Lemma eva_Omega : ~ eva Omega.
Proof.
inversion 1. remember Omega as Om. induction H0; inv HeqOm.
inv H0_. inv H0_0. cbn in H0_1. eapply IHevaluates3.
cbn. reflexivity. eassumption.
Qed.
Lemma eva_D s : ~ eva (D s).
Proof.
inversion 1. inversion H0. inv H3. cbn in H6.
eapply eva_Omega. exists x. eassumption.
Qed.
Lemma evaluates_D s v : D s ▷ v <-> False.
Proof.
firstorder using eva_D.
Qed.
Reserved Notation "s '≻' t" (at level 50).
Inductive step : term -> term -> Prop :=
| stepApp s t : app (lambda s) (lambda t) ≻ subst s 0 (lambda t)
| stepAppR s t t' : t ≻ t' -> app s t ≻ app s t'
| stepAppL s s' t : s ≻ s' -> app s t ≻ app s' t
where "s '≻' t" := (step s t).
Hint Constructors step.
Ltac inv_step :=
match goal with
| H : step (app _ _) _ |- _ => inv H
| H : step (lambda _) _ |- _ => inv H
| H : step (var _) _ |- _ => inv H
end.
Inductive step : term -> term -> Prop :=
| stepApp s t : app (lambda s) (lambda t) ≻ subst s 0 (lambda t)
| stepAppR s t t' : t ≻ t' -> app s t ≻ app s t'
| stepAppL s s' t : s ≻ s' -> app s t ≻ app s' t
where "s '≻' t" := (step s t).
Hint Constructors step.
Ltac inv_step :=
match goal with
| H : step (app _ _) _ |- _ => inv H
| H : step (lambda _) _ |- _ => inv H
| H : step (var _) _ |- _ => inv H
end.
Inductive star : term -> term -> Prop :=
star_refl s : star s s
| star_step s u t : step s u -> star u t -> star s t.
Inductive stepn : nat -> term -> term -> Prop :=
stepn_refl s : stepn 0 s s
| stepn_step s u t n : step s u -> stepn n u t -> stepn (S n) s t.
Hint Constructors step star stepn evaluates.
Instance star_trans : Transitive star.
Proof.
intros s t u H1 H2. induction H1; eauto.
Qed.
Notation "s '≻*' t" := (star s t) (at level 40).
Notation "s '≻^' n t" := (stepn n s t) (at level 40, n at level 5).
Instance star_app : Proper (star ==> star ==> star) app.
Proof.
intros s s' H t t' H1.
induction H; intros; eauto.
induction H1; eauto.
Qed.
Lemma star_stepn s t : s ≻* t <-> exists n, stepn n s t.
Proof.
split; intros H.
- induction H; eauto.
destruct IHstar. eauto.
- destruct H. induction H; eauto.
Qed.
Lemma evaluates_star s t : s ▷ t -> s ≻* t /\ lam t.
Proof.
split.
- induction H; eauto.
eapply evaluates_abst in H0 as []. subst.
rewrite star_app; eauto.
- now eapply evaluates_abst in H.
Qed.
Lemma step_evaluates s s' t : s ≻ s' -> s' ▷ t -> s ▷ t.
Proof.
intros H; revert t; induction H; intros; try inv H0; eauto.
Qed.
Lemma steps_evaluates s s' t : s ≻* s' -> s' ▷ t -> s ▷ t.
Proof.
induction 1; eauto using step_evaluates.
Qed.
Lemma star_evaluates s t : s ≻* t -> lam t -> s ▷ t.
Proof.
induction 1; inversion 1; subst; eauto using step_evaluates.
Qed.
Lemma stepn_plus s s' t n m : s ≻^n s' -> s' ≻^m t -> s ≻^(n+m) t.
Proof.
induction 1; cbn; intros; eauto.
Qed.
Instance star_PreOrder : PreOrder star.
Proof.
constructor; hnf; eauto using star_trans.
Qed.
Definition C := .\ "x", "y"; "y" (.\ "z"; "x" "x" "y" "z").
Definition rho s : term := Eval cbv in .\ "x" ; C C !s "x".
Lemma rho_lam s : lam (rho s).
Proof.
unfold rho. firstorder.
Qed.
Lemma rho_closed s : closed s -> closed (rho s).
Proof.
unfold rho, C, closed. cbn. intros. eapply bound_ge in H. now rewrite H. omega.
Qed.
Lemma rho_correct u v : proc u -> proc v -> rho u v ≻^3 u (rho u) v.
Proof.
intros [? [? H1]] [? [? H2]]; rewrite H1 , H2.
do 2 econstructor. rewrite <- H1. cbn. rewrite closed_subst; eauto.
rewrite H1. cbn. eauto.
Qed.
Lemma uniform_confluence s t1 t2 :
s ≻ t1 -> s ≻ t2 -> t1 = t2 \/ exists u, t1 ≻ u /\ t2 ≻ u.
Proof with try subst; repeat inv_step; eauto 10 using step.
intros Hst1. revert t2. induction Hst1; intros t2 Ht2...
- destruct (IHHst1 _ H2)... destruct H as (? & [])...
- destruct (IHHst1 _ H2)... destruct H as (? & [])...
Qed.
Lemma parametric_semi_confluence s t1 t2 n :
s ≻ t1 -> s ≻^n t2 -> exists k l u, k <= n /\ l <= 1 /\ t1 ≻^k u /\ t2 ≻^l u /\ 1 + k = n + l.
Proof.
revert s t1 t2; induction n; intros; inv H0.
- exists 0, 1, t1; eauto 9.
- destruct (uniform_confluence H H2) as [-> | (u' & ? & ?) ]; eauto 10.
destruct (IHn _ _ _ H1 H3) as (k' & l' & u'' & ? & ? & ? & ? & ?).
exists (S k'), l', u''. repeat split; eauto; omega.
Qed.
Lemma parametric_confluence s t1 t2 m n :
s ≻^m t1 -> s ≻^n t2 -> exists k l u, k <= n /\ l <= m /\ t1 ≻^k u /\ t2 ≻^l u /\ m + k = n + l.
Proof.
revert s t1 t2 n; induction m; intros; inv H.
- exists n, 0, t2. eauto.
- destruct (parametric_semi_confluence H2 H0) as (k & l & u' & ? & ? & ? & ? & ?).
destruct (IHm _ _ _ _ H3 H4) as (k' & l' & u'' & ? & ? & ? & ? & ?).
exists k', (l + l'), u''. repeat split; eauto using stepn_plus; try omega.
Qed.
Lemma confluence s t1 t2 : s ≻* t1 -> s ≻* t2 -> exists u, t1 ≻*u /\ t2 ≻* u.
Proof.
intros [] % star_stepn [] % star_stepn.
edestruct (parametric_confluence H H0) as (k & l & u & ? & ? & ? & ? & ?).
exists u. split; eapply star_stepn; eauto.
Qed.
Definition evaluatesin n s t := (s ≻^n t /\ lam t).
Notation "s '▷^' n t" := (evaluatesin n s t) (at level 40, n at level 5).
Definition stepplus s t := (exists s', s ≻ s' /\ s' ≻* t).
Notation "s '≻^+' t" := (stepplus s t) (at level 40).
Lemma unique_step_index s m t n : s ▷^m t -> s ▷^n t -> m = n.
Proof.
intros (? & ? & ->) [].
destruct (parametric_confluence H H0) as (k & l & u & ? & ? & ? & ? & ?).
inv H4; inv H5; [ omega | inv_step.. ].
Qed.
Lemma stepplus_stepn s t : s ≻^+ t <-> exists n, s ≻^(S n) t.
Proof.
intuition.
- destruct H as ( ? & ? & (? & ?) % star_stepn). eauto.
- destruct H as (? & ?). inv H.
econstructor. split. eassumption. eapply star_stepn. eauto.
Qed.
Lemma triangle s n t s' : s ▷^n t -> s ≻^+ s' -> exists k, k < n /\ s' ▷^k t.
Proof.
intros (? & ? & ->) [] % stepplus_stepn.
destruct (parametric_confluence H H0) as (k & l & u & ? & ? & ? & ? & ?).
inv H3. exists l. firstorder. inv_step.
Qed.
Instance step_star_subrelation : subrelation step star.
Proof.
cbv. eauto.
Qed.
Instance stepplus_star_subrelation : subrelation stepplus star.
Proof.
cbv. intros. destruct H as (? & ? & ?). eauto.
Qed.
Reserved Notation "s '≡' t" (at level 50).
Inductive equiv : term -> term -> Prop :=
| eqStep s t : step s t -> s ≡ t
| eqRef s : s ≡ s
| eqSym s t : t ≡ s -> s ≡ t
| eqTrans s t u: s ≡ t -> t ≡ u -> s ≡ u
where "s '≡' t" := (equiv s t).
Hint Constructors equiv.
(* *** Properties of the equivalence relation *)
Instance equiv_Equivalence : Equivalence equiv.
Proof.
constructor; hnf.
- apply eqRef.
- intros. eapply eqSym. eassumption.
- apply eqTrans.
Qed.
Lemma star_equiv s t : s ≻* t -> s ≡ t.
Proof.
induction 1; eauto.
Qed.
Lemma church_rosser s t : s ≡ t -> exists u, s ≻* u /\ t ≻* u.
Proof.
induction 1; firstorder eauto. destruct (confluence H1 H4) as (? & ? & ?). eauto using star_trans.
Qed.
Instance app_equiv : Proper (equiv ==> equiv ==> equiv) app.
Proof with eauto.
intros s s' H.
induction H; intros ? ??...
- eapply eqTrans. eapply eqStep. eapply stepAppL. eassumption.
induction H0...
- induction H...
Qed.
Lemma equiv_star_lam s t : lam t -> s ≡ t <-> s ≻* t.
Proof.
intros. split; eauto using star_equiv.
intros. eapply church_rosser in H0 as (u & H1 & H2). inv H2; eauto.
inv H. inv_step.
Qed.
Lemma unique_normal_forms (s t : term) : lam s -> lam t -> s ≡ t -> s = t.
Proof.
intros ls lt H % equiv_star_lam; eauto. inv ls. inv H. reflexivity. inv H0.
Qed.
Lemma evaluates_equiv s t : s ▷ t <-> s ≡ t /\ lam t.
Proof with eauto using star_equiv, evaluates_abst.
firstorder...
- eapply evaluates_star in H as []...
- eapply star_evaluates... eapply equiv_star_lam...
Qed.
Lemma equiv_evaluates s t v : s ≡ t -> s ▷ v -> t ▷ v.
Proof.
intros. eapply evaluates_star in H0 as [].
eapply church_rosser in H as (? & ? & ?).
destruct (confluence H0 H) as (? & ? & ?). destruct H1; subst. inv H3.
eauto using star_evaluates, star_trans. inv H1.
Qed.
Instance evaluates_proper :
Proper (equiv ==> eq ==> iff) evaluates.
Proof.
intros ? ? ? ? ? ?. subst. firstorder using equiv_evaluates.
Qed.
Instance eva_proper :
Proper (equiv ==> iff) eva.
Proof.
intros ? ? ?. firstorder. rewrite H in H0; firstorder. rewrite <- H in H0; firstorder.
Qed.
Lemma equiv_eva s t : s ≡ t -> eva s <-> eva t.
Proof.
firstorder using equiv_evaluates; exists x; firstorder using equiv_evaluates.
Qed.
Instance evaluates_equiv_subrelation : subrelation evaluates equiv.
Proof.
intros ? ? ?. now eapply evaluates_equiv.
Qed.
Instance star_equiv_subrelation : subrelation star equiv.
Proof.
cbv. apply star_equiv.
Qed.
Instance stepplus_equiv_subrelation : subrelation stepplus equiv.
Proof.
cbv. intros. eapply star_equiv. eapply stepplus_star_subrelation. eauto.
Qed.
Instance evaluatesin_equiv_subrelation n : subrelation (evaluatesin n) equiv.
Proof.
intros ? ? ?. destruct H. eapply star_equiv_subrelation.
eapply star_stepn. firstorder.
Qed.
Lemma stepplus_star_stepplus s s' t : s ≻^+ s' -> s' ≻* t -> s ≻^+ t.
Proof.
intros [? []] ?. exists x. eauto using star_trans.
Qed.
Lemma I_neq_Omega : ~ I ≡ Omega.
Proof.
intros H. eapply eva_Omega. rewrite <- H. cbv. eauto.
Qed.