Library L

Require Export Base UnifConfl.

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

Implicit Types s t u : term.
Coercion app : term >-> Funclass.
Notation "# v" := (var v) (at level 1, format "# v"): L_scope.
Bind Scope L_scope with term.
Open Scope L_scope.

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.

Arguments convert /.

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 : term := Eval simpl in .\"r","f";"f" (.\"x";"r" "r" "f" "x").
Definition R : term := r r.

Definition rho s : term := Eval simpl in .\"x";!!r !!r !!s "x".

Definition I : term := Eval simpl in .\"x"; "x".
Definition K : term := Eval simpl in .\"x","y"; "x".

Definition omega : term := Eval simpl in .\"x"; "x" "x".
Definition Omega : term := omega omega.

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.

Important definitions

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

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

Definition proc s := closed s ∧ lambda s.

Lemma lambda_lam s : lambda (lam s).
Proof.
  ∃ s; reflexivity.
Qed.

Hint Resolve lambda_lam.

Instance lambda_dec s : dec (lambda s).
Proof.
  destruct s;[right;intros C;inv C;congruence..|left;eexists;eauto].
Defined.

Lemma var_not_closed n: ¬closed (var n).
Proof.
  intros H. specialize (H n (lam (#n))). simpl in H. decide (n=n);congruence.
Qed.

Lemma closed_l (s t:term): closed (s t) → closed s.
Proof.
  intros cs s' x. specialize (cs s' x). simpl in cs. congruence.
Qed.

Lemma closed_r (s t:term): closed (s t) → closed t.
Proof.
  intros cs s' x. specialize (cs s' x). simpl in cs. congruence.
Qed.

Size of terms

Fixpoint size (t : term) :=
  match t with
  | var n ⇒ 0
  | app s t ⇒ 1+ size s + size t
  | lam s ⇒ 1 + size s
  end.

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 dclosedApp_iff n (s t : term): dclosed n (s t) ↔ dclosed n s ∧ dclosed n t.
Proof.
  split;intros H;inv H;auto using dclosed.
Qed.

Lemma dclosedVar_iff n x : dclosed n (# x) ↔ x < n.
Proof.
  split;intros H;inv H;auto using dclosed.
Qed.

Lemma dclosedLam_iff n s : dclosed n (lam s) ↔ dclosed (S n) s.
Proof.
  split;intros H;inv H;auto using dclosed.
Qed.

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_ge k s : dclosed k s → ∀ m, m ≥ k → dclosed m s.
Proof.
  induction 1; intros m Hmk; econstructor; eauto.
  - omega.
  - eapply IHdclosed. omega.
Qed.

Lemma dclosed_gt k s : dclosed k s → ∀ m, m > k → dclosed m s.
Proof.
  intros. apply (dclosed_ge H). 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 : (∀ 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.
  -unfold closed. eauto using dclosed_closed.
Qed.

Lemma closed_dclosed s k : closed s → dclosed k s.
Proof.
  intros H. apply dclosed_ge with (k:=0). now apply closed_dcl. omega.
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 app_closed (s t : term) : closed s → closed t → closed (s t).
Proof.
  intros H H' k u. simpl. now rewrite H, H'.
Qed.

Instance dclosed_dec 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)))...
Defined.

Instance closed_dec s : dec (closed s).
Proof.
  decide (dclosed 0 s);[left|right];now rewrite closed_dcl.
Defined.

Lemma proc_dec s : dec (proc s).
Proof.
  exact _.
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.

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 ∨ ∃ 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.

Lemma irred_iff s : closed s → (irred step s ↔ lambda s ).
Proof.
  intros cs. split.
  destruct (comb_proc_red cs) as [[]|[]].
  - tauto.
  - intros C. now destruct (C x).
  - destruct 1 as (?&->). intros ? R. inv R.
Qed.

Ltac inv_step :=
  match goal with
    | H : step (app _ _) _ |- _ ⇒ inv H
    | H : step (lam _) _ |- _ ⇒ inv H
    | H : step (var _) _ |- _ ⇒ inv H
  end.

Properties of the reduction relation

Theorem uniform_confluence : uniformly_confluent step.
Proof.
  apply UD_UC.
  intros s t1 t2 R. revert t2. induction R;intros; repeat inv_step; eauto 7 using step.
  -destruct (IHR _ H3) as [|[? []]];subst;eauto 7 using step.
  -destruct (IHR _ H3) as [|[? []]];subst;eauto 7 using step.
Qed.

Notation "s '>^' k" := (pow step k s) (at level 9, format "s '>^' k").

Lemma step_pow_app_l s s' t n: s >^n s' → (s t ) >^n (s' t).
Proof.
  revert s s' t. induction n;intros.
  -inv H. reflexivity.
  -destruct H as [s1 [R R']]. ∃ (s1 t). split. auto. apply IHn. exact R'.
Qed.

Lemma step_pow_app_r s t t' n: t >^n t' → (s t ) >^n (s t').
Proof.
  revert s t t'. induction n;intros.
  -inv H. reflexivity.
  -destruct H as [t1 [R R']]. ∃ (s t1). split. auto. apply IHn. exact R'.
Qed.

Lemma step_pow_app s s' t t' k l: s >^k s' → t >^l t' → (s t ) >^(k +l ) (s' t').
Proof.
  intros. apply pow_add. ∃ (s' t);split;auto using step_pow_app_l,step_pow_app_r.
Qed.

Lemma confluence : confluent step.
Proof.
  apply UC_confluent. exact uniform_confluence.
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).

Lemma step_star s s':
  s >> s' → s >* s'.
Proof.
  eauto using star.
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:term):
  s >* s' → t s >* t s'.
Proof.
  induction 1; eauto using star, step.
Qed.

Instance star_step_app_proper :
  Proper ((star step ) ==> (star step ) ==> (star step )) app.
Proof.
  cbv. intros s s' A t t' B.
  etransitivity. apply (star_trans_l _ A). now apply star_trans_r.
Defined.

Lemma closed_star s t: s >* t → closed s → closed t.
Proof.
  intros R. induction R;eauto using closed_step.
Qed.

Instance star_closed_proper :
  Proper ((star step ) ==> Basics.impl) closed.
Proof.
  exact closed_star.
Defined.

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 Immediate eqRef.

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 → ∃ 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.

Instance star_equiv_subrelation : subrelation (star step) equiv.
Proof.
  cbv. apply star_equiv.
Qed.

Instance step_equiv_subrelation : subrelation step equiv.
Proof.
  cbv. intros ? ? H. apply star_equiv, step_star. assumption.
Qed.

Lemma equiv_lambda s t : lambda t → s == t → s >* t.
Proof.
  intros H eq. destruct (church_rosser eq) as [u [A B]]. inv B. assumption. inv H. inv H0.
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 eval s t := s >* t ∧ lambda t.

Hint Unfold eval.

Definition converges s := ∃ t, s == t ∧ lambda t.

Lemma converges_equiv s t : s == t → (converges s ↔ converges t ).
Proof.
  intros H; split; intros [u [A lu]]; ∃ u;split;try assumption; rewrite <- A.
  - symmetry. eassumption.
  - eassumption.
Qed.

Instance converges_proper :
  Proper (equiv ==> iff) converges.
Proof.
  intros s t H. now eapply converges_equiv.
Qed.

Lemma unique_normal_forms (s t : term) : lambda s → lambda t → s == t → s = t.
Proof.
  intros ls lt. intros H. apply equiv_lambda in H;try assumption. inv ls. inv H. reflexivity. inv H0.
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 :
  lambda v → pow step n t v → pow step (S k) t s → ∃ m, m < n ∧ pow step m s v.
Proof.
  intros lv A B.
  destruct (uniform_confluence A B)
     as [u [m [l [C [D [E [m_le_Sk l_le_n]]]]]]].
  ∃ 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 lv. inv H.
Qed.

Lemma pow_trans_lam t v s k n :
  lambda v → pow step n t v → pow step (S k) t s → ∃ m, m < n ∧ pow step m s v.
Proof.
  intros [? ?]. subst. apply pow_trans_lam'. auto.
Qed.

Lemma powSk t t' s : t >> t' → t' >* s → ∃ k, pow step (S k) t s.
Proof.
  intros A B.
  eapply star_pow in B. destruct B as [n B]. ∃ n.
  unfold pow. simpl. econstructor. unfold pow in B. split; eassumption.
Qed.

Close Scope L_scope.