Library Lvw

Require Export Base ARS.

Hint Constructors ARS.star : cbv.

Syntax of the weak call-by-value lambda calculus

Inductive term : Type :=
| var (n : nat) : term
| app (s : term) (t : term) : term
| lam (s : term).

Coercion app : term >-> Funclass.

Coercion var : nat >-> term.

Notation "'#' v" := (var v) (at level 1).

Notation "(Î» s )" := (lam s) (right associativity, at level 0).

Instance term_eq_dec : eq_dec term.

Proof.

intros s t; unfold dec; repeat decide equality.

Defined.

Definition term_eq_dec_proc s t := if decision (s = t) then true else false.

Hint Resolve term_eq_dec.

Notation using binders

Require Import String.

Inductive bterm : Type :=
| bvar (x : string) : bterm
| bapp (s t : bterm) : bterm
| blam (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)
| blam x s => lam (convert' (x:: F) s)
| bter t => t
end.

Coercion bvar : string >-> bterm.

Coercion bapp : bterm >-> Funclass.

Definition convert := convert' [].

Coercion convert : bterm >-> term.

Notation ".\ x , .. , y ; t" := ((blam x .. (blam y t) .. )) (at level 100, right associativity).

Notation "'Î»' x , .. , y ; t" := ((blam x .. (blam y t) .. )) (at level 100, right associativity).

Notation "'!' s" := (bter s) (at level 0).

Important terms

Definition R := (lam (lam (#0 (lam (#2 #2 #1 #0)))))
(lam (lam (#0 (lam (#2 #2 #1 #0))))).

Definition I : term := .\"x"; "x".

Definition K : term := .\"x","y"; "x".

Definition omega : term := .\"x"; "x" "x".

Definition Omega : term := omega omega.

Hint Unfold R I K Omega : cbv.

Substitution

Fixpoint subst (s : term) (k : nat) (u : term) :=
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)
| lam s => lam (subst s (S k) u)
end.

Hint Unfold subst : cbv.

Important definitions

Definition closed s := forall n u, subst s n u = s.

Definition lambda s := exists t, s = lam t.

Definition proc s := closed s /\ lambda s.

Lemma lambda_lam s : lambda (lam s).

Proof.

exists s; reflexivity.

Qed.

Hint Unfold closed lambda proc.

Hint Resolve lambda_lam.

Alternative definition of closedness

Inductive dclosed : nat -> term -> Prop :=
| dclvar k n : k > n -> dclosed k (var n)
| dclApp k s t : dclosed k s -> dclosed k t -> dclosed k (s t)
| dcllam k s : dclosed (S k) s -> dclosed k (lam s).

Lemma dclosed_closed_k s k u : dclosed k s -> subst s k u = s.

Proof with eauto.

intros H; revert u; induction H; intros u; simpl.

- decide (n = k)...
omega.
- rewrite IHdclosed1, IHdclosed2...

- f_equal...

Qed.

Lemma dclosed_gt k s : dclosed k s -> forall m, m > k -> dclosed m s.

Proof.

induction 1; intros m Hmk; econstructor; eauto.

- omega.

- eapply IHdclosed.
omega.
Qed.

Lemma dclosed_closed s k u : dclosed 0 s -> subst s k u = s.

Proof.

intros H.
destruct k.
- eapply dclosed_closed_k.
eassumption.
- eapply dclosed_gt in H.
eapply dclosed_closed_k. eassumption. omega.
Qed.

Lemma closed_k_dclosed k s : (forall n u, n >= k -> subst s n u = s) -> dclosed k s.

Proof.

revert k.
induction s; intros k H.
- econstructor.
specialize (H n (#(S n))). simpl in H.
decide (n >= k) as [Heq | Heq].

+ decide (n = n) ; [injection (H Heq)|]; omega.

+ omega.

- econstructor; [eapply IHs1 | eapply IHs2]; intros n u Hnk;
injection (H n u Hnk); congruence.

- econstructor.
eapply IHs. intros n u Hnk.
destruct n.
omega.
injection (H n u).
tauto. omega.
Qed.

Lemma closed_dcl s : closed s <-> dclosed 0 s.

Proof.

split; eauto using closed_k_dclosed, dclosed_closed.

Qed.

Lemma closed_app (s t : term) : closed (s t) -> closed s /\ closed t.

Proof.

intros cls.
rewrite closed_dcl in cls. inv cls. split; rewrite closed_dcl; eassumption.
Qed.

Lemma dec_dclosed k s : dec (dclosed k s).

Proof with try ((left; econstructor; try omega; tauto) || (right; inversion 1; try omega; tauto)).

revert k; induction s; intros k.

- destruct (le_lt_dec n k) as [Hl | Hl]...
destruct (le_lt_eq_dec _ _ Hl)...
- destruct (IHs1 k), (IHs2 k)...

- induction k.

+ destruct (IHs 1)...

+ destruct (IHs (S (S k)))...

Qed.

Reduction

Reserved Notation "s '>>' t" (at level 50).

Inductive step : term -> term -> Prop :=
| stepApp s t : app (lam s) (lam t) >> subst s 0 (lam 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 (lam _) _ |- _ => inv H
| H : step (var _) _ |- _ => inv H
| H : star step (lam _) _ |- _ => inv H
| H : star step (var _) _ |- _ => inv H
end.

Lemma closed_subst s t k : dclosed (S k) s -> dclosed k t -> dclosed k (subst s k t).

Proof.

revert k t; induction s; intros k t cls_s cls_t; simpl; inv cls_s; eauto 6 using dclosed, dclosed_gt.

decide (n = k); eauto.
econstructor. omega.
Qed.

Lemma closed_step s t : s >> t -> closed s -> closed t.

Proof.

rewrite !closed_dcl; induction 1; intros cls_s; inv cls_s; eauto using dclosed.

inv H2.
eauto using closed_subst.
Qed.

Lemma comb_proc_red s : closed s -> proc s \/ exists t, s >> t.

Proof with try tauto.

intros cls_s.
induction s.
- eapply closed_dcl in cls_s.
inv cls_s. omega.
- eapply closed_app in cls_s.
destruct IHs1 as [[C [t A]] | A], IHs2 as [[D [t' B]] | B]...
+ right.
subst. eexists. eauto.
+ right; subst.
firstorder; eexists. eapply stepAppR. eassumption.
+ right; subst.
firstorder; eexists. eapply stepAppL. eassumption.
+ right.
subst. firstorder. eexists. eapply stepAppR. eassumption.
- left.
split. eassumption. firstorder.
Qed.

Goal forall s, closed s -> ((~ exists t, s >> t) <-> proc s).

Proof.

intros s cls_s.
split.
destruct (comb_proc_red cls_s).

- eauto.

- tauto.

- destruct 1 as [? [? ?]].
subst. destruct 1 as [? B]. inv B.
Qed.

Properties of the reduction relation

Proof with repeat inv_step; eauto using step.

intros s; induction s; intros t1 t2 step_s_t1 step_s_t2; try now inv step_s_t2.

inv step_s_t1.

- inv step_s_t2; try eauto; inv_step.

- inv step_s_t2...

+ destruct (IHs2 _ _ H2 H3).

* left.
congruence.
* right.
destruct H as [u [A B]]...
+ right...

- inv step_s_t2...

+ right...

+ destruct (IHs1 _ _ H2 H3).

* left.
congruence.
* right.
destruct H as [u [A B]]...
Qed.

Notation "x '>^' n y" := (pow step n x y) (at level 50).

Lemma confluence : confluent step.

Proof.

intros x y z x_to_y x_to_z.

eapply star_pow in x_to_y.
destruct x_to_y as [n x_to_y].
eapply star_pow in x_to_z.
destruct x_to_z as [m x_to_z].
destruct (parametrized_confluence uniform_confluence x_to_y x_to_z) as
[k [l [u [_ [_ [C [D _]]]]]]].

exists u.
split; eapply star_pow; eexists; eassumption.
Qed.

Lemma step_value s v :
lambda v -> (lam s) v >> subst s 0 v.

Proof.

intros [t lamv].

rewrite lamv.

repeat econstructor.

Qed.

Properties of the reflexive, transitive closure of reduction

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

Instance star_PreOrder : PreOrder (star step).

Proof.

constructor; hnf.

- eapply starR.

- eapply star_trans.

Qed.

Lemma star_trans_l s s' t :
s >* s' -> s t >* s' t.

Proof.

induction 1; eauto using star, step.

Qed.

Lemma star_trans_r s s' t :
s >* s' -> (lam t) s >* (lam t) s'.

Proof.

induction 1; eauto using star, step.

Qed.

Equivalence

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 step.

Properties of the equivalence relation

Instance equiv_Equivalence : Equivalence equiv.

Proof.

constructor; hnf.

- apply eqRef.

- intros.
eapply eqSym. eassumption.
- apply eqTrans.

Qed.

Lemma equiv_ecl s t : s == t <-> ecl step s t.

Proof with eauto using ecl, equiv.

split; induction 1...

- eapply ecl_sym...

- eapply ecl_trans...

Qed.

Lemma church_rosser s t : s == t -> exists u, s >* u /\ t >* u.

Proof.

rewrite equiv_ecl.
eapply confluent_CR, confluence.
Qed.

Lemma star_equiv s t :
s >* t -> s == t.

Proof.

induction 1.

- reflexivity.

- eapply eqTrans.
econstructor; eassumption. eassumption.
Qed.

Hint Resolve star_equiv.

Lemma equiv_lambda s t : s == (lam t) -> s >* (lam t).

Proof.

intros H.
destruct (church_rosser H) as [u [A B]]; repeat inv_step; eassumption.
Qed.

Lemma equiv_lambda' u t : lambda t -> u == t -> u >* t.

Proof.

intros.
destruct H; subst. eauto using equiv_lambda.
Qed.

Lemma eqStarT s t u : s >* t -> t == u -> s == u.

Proof.

eauto using equiv.

Qed.

Lemma eqApp s s' u u' : s == s' -> u == u' -> s u == s' u'.

Proof with eauto using equiv, step.

intros H; revert u u'; induction H; intros z z' H'...

- eapply eqTrans.
eapply eqStep. eapply stepAppL. eassumption.
induction H'...

- induction H'...

Qed.

Instance equiv_app_proper :
Proper (equiv ==> equiv ==> equiv) app.

Proof.

cbv.
intros s s' A t t' B.
eapply eqApp; eassumption.

Qed.

Definition of convergence

Definition converges s := exists t, s == lam t.

Lemma converges_equiv s t : s == t -> (converges s <-> converges t).

Proof.

intros H; split; intros [u A]; exists u; rewrite <- A.

- symmetry.
eassumption.
- eassumption.

Qed.

Instance converges_proper :
Proper (equiv ==> iff) converges.

Proof.

intros s t H.
now eapply converges_equiv.
Qed.

Lemma eq_lam s t : lam s == lam t <-> s = t.

Proof.

split.

- intros H.
eapply equiv_lambda in H; repeat inv_step; reflexivity.
- intros [].
reflexivity.
Qed.

Lemma unique_normal_forms (s t t' : term) : s == lam t -> s == lam t' -> lam t = lam t'.

Proof.

intros Ht Ht'.
rewrite Ht in Ht'. eapply eq_lam in Ht'. congruence.
Qed.

Eta expansion

Lemma Eta (s : term ) t : closed s -> lambda t -> (lam (s #0)) t == s t.

Proof.

intros cls_s lam_t.
eapply star_equiv, starC; eauto using step_value. simpl. now rewrite cls_s.
Qed.

Useful lemmas

Lemma pow_trans_lam t v s k n :
pow step n t (lam v) -> pow step (S k) t s -> exists m, m < n /\ pow step m s (lam v).

Proof.

intros A B.

destruct (parametrized_confluence uniform_confluence A B)
as [m [l [u [m_le_Sk [l_le_n [C [D E]]]]]]].

exists l.

cut (m = 0); intros; subst.

assert (E' : n = S(k+l)) by omega.
subst n.
split.
omega. destruct C. eassumption.
destruct m; eauto.
destruct C. destruct H. inv H.
Qed.

Lemma powSk t t' s : t >> t' -> t' >* s -> exists k, pow step (S k) t s.

Proof.

intros A B.

eapply star_pow in B.
destruct B as [n B]. exists n.
unfold pow.
simpl. econstructor. unfold pow in B. split; eassumption.
Qed.