Library LC

Require Export L.
Require Import Bool.

Syntax of L with Closures

Inductive term : Type :=
| var (x:nat)
| clos (s : L.term) (sigma : list term) : term
| app (p : term) (q : term) : term.

Inductive value : term Prop :=
  valueLam s A: value (clos (lam s) A).

Hint Constructors value.
Implicit Types p q r : term.
Implicit Types sigma tau : list term.

Coercion app : term >-> Funclass.
Notation "# v" := (var v) (at level 1, format "# v"): LC_scope.
Bind Scope LC_scope with term.
Open Scope LC_scope.

A more usefull induction principle where for closures, the propertie can be assumed for all elements of the environment:

Definition term_rec_deep'
           (P : term Type)
           (Pl : list term Type)
           (IHVar : x : nat, P (var x))
           (IHApp : p , P p q, P q P (p q))
           (IHClos : s sigma,
                       Pl sigma P (clos s sigma))
           (IHNil : Pl nil)
           (IHCons : p sigma,
                       P p Pl sigma Pl (p::sigma))
           p : P p :=
  (fix f p : P p:=
     match p with
       | var xIHVar x
       | app s tIHApp s (f s) t (f t)
       | clos s AIHClos s A
         ((fix g A : Pl A :=
            match A with
              | a::AIHCons a A (f a) (g A)
            end) A)
     end) p

Definition term_ind_deep
           (P : term Prop)
           (IHVar : x : nat, P (var x))
           (IHApp : p , P p q, P q P (p q))
           (IHClos : s sigma,
                       ( a, a el sigma P a) P (clos s sigma)) : p, P p.
  apply term_rec_deep' with (Pl:=fun A ⇒ ( a, a el A P a));auto.
  -simpl. tauto.
  -intros. inv H1; auto.

Equality on terms is decidable

Fixpoint comp_eqb p q:=
  match p,q with
  | var x , var x'Nat.eqb x x'
  | app p q , app p' q'andb (comp_eqb p p') (comp_eqb q q')
  | clos s sigma, clos s' sigma'
    if term_eq_dec s s' then ((fix f A A' := match A,A' with
                                            | nil,niltrue
                                            | (a::B), (a'::B') ⇒ andb (comp_eqb a a') (f B B')
                                            | _,_false
                                              end) sigma sigma')
                              else false
                          | _,_false

Definition comp_eqb_spec p q: reflect (p=q) (comp_eqb p q).
Proof with (try solve [apply ReflectF;congruence|apply ReflectT;congruence]).
  revert p q. fix IH 1.
  destruct p, q;simpl...
  -destruct (Nat.eqb_spec x x0)...
  -destruct (term_eq_dec s s0).
   +revert sigma sigma0. fix IH' 1;intros ? sigma'.
    destruct sigma as [|p ?];destruct sigma' as [|q]...
    destruct (IH p q);destruct (IH' sigma sigma')...
  -assert (H1:=IH p1 q1). assert (H2:=(IH p2 q2)). clear IH. inv H1; inv H2...

Instance LC_eq_dec : eq_dec term.
  intros p q. destruct (comp_eqb_spec p q); auto.


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

Inductive step : term term Prop :=
| stepAppL p p' q : p >[]> p' (p q) >[]> (p' q)
| stepAppR p q q': q >[]> q' (p q) >[]> (p q')
| stepApp (s t:L.term) sigma :
    clos (s t) sigma >[]> (clos s sigma) (clos t sigma)
| stepVar (x:nat) sigma:
    clos (# x) sigma >[]> nth x sigma (var x)
| stepBeta s t sigma tau:
    (clos (lam s) sigma) (clos (lam t) tau) >[]> (clos s ((clos (lam t) tau)::sigma))
where "p '>[]>' q" := (step p q) : LC_scope.

Hint Constructors step.

Notation "p '>[]*' q" := (star step p q) (at level 50) : LC_scope.
Notation "p '>[]^' k" := (pow step k p) (at level 8, format "p '>[]^' k") : LC_scope.

valie is decidable

Instance value_dec p : dec (value p).
Proof with try ((now left; constructor)||(now right;intros C;inv C)).
  destruct p... destruct s...

Uniform Confluence

Local Ltac inv_step :=
  match goal with
    | H : (var _) >[]> _ |- _inv H
    | H : (app _ _) >[]> _ |- _inv H
    | H : (clos _ _) >[]> _ |- _inv H

Lemma LC_UC: uniformly_confluent step.
  apply UD_UC.
  intros p. induction p;intros q1 q2 R1 R;repeat inv_step; try (solve [left;congruence | right;eauto]).
  -destruct (IHp1 _ _ H2 H3) as [? | [? [? ?]]]. subst;auto. right; eauto.
  -destruct (IHp2 _ _ H2 H3) as [? | [? [? ?]]]. subst;auto. right; eauto.

Compatibility Laws

Lemma star_app_l p p' q :
  p >[]* p' p q >[]* p' q.
  induction 1; eauto using star.

Lemma star_app_r p q q' :
  q >[]* q' p q >[]* p q'.
  induction 1; eauto using star.

Instance star_step_app_proper :
  Proper ((star step) ==> (star step) ==> (star step)) app.
  cbv. intros s s' A t t' B. etransitivity.
  apply star_app_l, A. apply star_app_r, B.

Lemma pow_app_l p p' q n: p >[]^n p' (p q) >[]^n (p' q).
  revert p p' q. induction n;intros.
  -inv H. reflexivity.
  -destruct H as [p1 [R R']]. (p1 q). split. auto. apply IHn. exact R'.

Lemma pow_app_r p q q' n: q >[]^n q' (p q) >[]^n (p q').
  revert p q q'. induction n;intros.
  -inv H. reflexivity.
  -destruct H as [q1 [R R']]. (p q1). split. auto. apply IHn. exact R'.

Lemma pow_app p p' q q' k l: p >[]^k p' q >[]^l q' (p q) >[]^(k+l) (p' q').
  intros. apply pow_add. (p' q);split.
  -auto using pow_app_l.
  -auto using pow_app_r.

Connecting L and LC

Admissible Terms

Inductive admissible : term Prop :=
| validLCApp p q : admissible p admissible q admissible (p q)
| validLCclos s (sigma : list term) :
    ( p, p el sigma admissible p)
    ( p, p el sigma value p)
    dclosed (length sigma) s
    admissible (clos s sigma).

Hint Constructors admissible.
Ltac inv_admissible :=
  match goal with
    | H : admissible (app _ _) |- _inv H
    | H : admissible (clos _ _) |- _inv H

Lemma admissible_step p q: admissible p p >[]> q admissible q.
  intros ap R. induction R;repeat inv_admissible.
  -inv H3. eauto.
  -apply H1. apply nth_In. now inv H3.
  -inv H7. repeat constructor;[intros ? [<-|]..|];try subst;eauto.

Lemma admissible_star p q: admissible p p >[]* q admissible q.
  intros ap R. induction R; eauto using admissible_step.
Hint Immediate admissible_star.

Instance admissible_step_proper :
  Proper ((star step) ==> Basics.impl) admissible.
  intros ? ? R H. now apply admissible_star in R.

Values and Irredicibility

Lemma value_irred p : value p irred step p.
  intros vp ? R. inv vp. inv R.

Lemma value_iff_irred p : admissible p value p irred step p.
  intros ap. split. apply value_irred.
  intros H. induction ap.
   destruct IHap1. intros ? R. eapply H;eauto.
   destruct IHap2. intros ? R. eapply H;eauto.
   now eapply H.
  -destruct s.
   +exfalso. now eapply H.
   +exfalso. now eapply H.

Parallel Substitution

Fixpoint pSubst (s:L.term) (k:nat) (A: list L.term): L.term :=
  match s with
    | L.var xif decision (k>x) then L.var x else nth (x-k) A (L.var x)
    | s t ⇒ (pSubst s k A) (pSubst t k A)
    | lam slam (pSubst s (S k) A)

Characteristic Equations

Lemma pSubst_nil s x: pSubst s x [] = s.
  revert x. induction s;intros;simpl.
  -decide (x>n). reflexivity. now destruct(n-x).

Lemma pSubst_cons k s t A: ( a, a el A closed a) pSubst s k (t::A) = subst (pSubst s (S k) A) k t.
  revert k;induction s as [x| |];intros k cl.
  -simpl;decide (S k > x); simpl;decide (k>x); decide (x=k);try omega.
   +subst. now replace (k-k) with 0 by omega.
   +destruct (x-k) as [|m'] eqn:?;[omega|].
    replace (x - S k) with m' by omega.
    destruct (nth_in_or_default m' A (L.var x)) as [H|eq].
    ×now rewrite cl.
    ×rewrite eq. simpl.
     decide (x=k);try omega. reflexivity.
  -simpl. now rewrite IHs1,IHs2.
  -simpl. now rewrite IHs.

Lemma pSubst_dclosed y A s: ( a, a el A closed a) dclosed (y+|A|) s dclosed y (pSubst s y A).
  intros cA. revert y. induction A;intros y dA;simpl in dA.
  -rewrite pSubst_nil.
   now replace (y+0) with y in dA by omega.
  -rewrite pSubst_cons;auto.
   apply closed_subst.
   +apply IHA. auto.
    now rewrite <- plus_n_Sm in dA.
   +apply closed_dclosed.
    now apply cA.

Lemma pSubst_closed A s: ( a, a el A closed a) dclosed (|A|) (s) closed (pSubst s 0 A).
  intros. rewrite closed_dcl. apply pSubst_dclosed; auto.

Translating from LC to L

Fixpoint translate p : L.term :=
  match p with
  | var xL.var x
  | app p q ⇒ (translate p) (translate q)
  | clos s ApSubst s 0 (map translate A)

Lemma translate_closed p: admissible p closed (translate p).
  intros ap. induction ap;simpl.
  -now apply app_closed.
  -apply pSubst_closed.
   +intros a ain. rewrite in_map_iff in ain.
    destruct ain as [a' [<- a'in]].
    now apply H0.
   +now rewrite map_length.

Lemma translate_map_closed s sigma: ( p, p el sigma admissible p) s el (map translate sigma) closed s.
  intros vA H. apply in_map_iff in H as [a' [<- H]]. apply translate_closed,vA. assumption.

Hint Resolve translate_map_closed.


Lemma translate_sound_step p q: admissible p p >[]> q k, k 1 (translate p) >^k (translate q).
Proof with split;repeat (simpl || auto using L.step_pow_app_l, L.step_pow_app_r|| congruence || omega).
  intros cs R. induction R; repeat inv_admissible.
  -destruct IHR as [k []].
   + k...
  -destruct IHR as [k []].
   + k...
  - 0...
  - 0.
   split;[omega|]. simpl.
   rewrite <- minus_n_O.
   rewrite <-map_nth with (f:=translate).
  - 1.
   split;[omega|]. simpl.
   rewrite pSubst_cons;eauto.
   eexists;split;[|reflexivity]. auto.

Lemma translate_sound p q: admissible p p >[]* q translate p >* translate q.
  intros cs R. induction R.
  -destruct (translate_sound_step cs H) as (?&?&R');auto.
   rewrite R'.
   apply IHR. now rewrite <- H.

Application of soundness

Lemma emptEnv_admissible s: closed s admissible (clos s []).
  intros cs. constructor;simpl;[tauto..|]. now apply closed_dcl.

Lemma emptEnv s p: closed s clos s [] >[]* p s >* translate p.
  intros cs R. apply translate_sound in R.
  -simpl in R. now rewrite pSubst_nil in R.
  -now apply emptEnv_admissible.



We simplify a computation by performing all reductions that do not correspond to a beta-reduction.

Fixpoint simplify' s sigma:=
  match s with
    | s t ⇒ (simplify' s sigma) (simplify' t sigma)
    | L.var xnth x sigma (var x)
    | lam sclos (lam s) sigma

Fixpoint simplify p :=
  match p with
    | app p q ⇒ (simplify p) (simplify q)
    | clos s Asimplify' s A
    | _p

Definition simplified s := simplify s = s.

Lemma simplify'_sound s sigma: clos s sigma >[]* simplify' s sigma.
  induction s;simpl.
  -now rewrite stepVar.
  -rewrite stepApp.
   now apply star_step_app_proper.

Lemma simplify_sound p: p >[]* simplify p.
  induction p;simpl.
  -apply simplify'_sound.
  -now apply star_step_app_proper.

Lemma simplify'_translate_var' x A : translate (clos (L.var x) A) = translate (nth x A (var x)).
  replace (x-0) with x by omega.
  rewrite <- (map_nth translate).

Lemma simplify'_translate s A: translate (clos s A) = translate (simplify' s A).
  induction s.
  -now rewrite simplify'_translate_var'.
  -simpl in ×. congruence.
  -simpl in ×. congruence.

Lemma simplify_translate p: translate p = translate (simplify p).
  induction p;simpl;[congruence| |congruence].
  rewrite <- simplify'_translate.

Lemma simplify'_simplified s sigma: ( p, p el sigma value p) simplify (simplify' s sigma)=simplify' s sigma.
  intros vs. induction s;simpl;[|congruence..].
  destruct (nth_in_or_default n sigma (var n)) as [H| → ].
  -apply vs in H. now inv H.

Lemma simplify_simplified p: admissible p simplified (simplify p).
  intros vs.
  unfold simplified.
  induction vs;simpl.
  -now apply simplify'_simplified.

Lemma simplify_admissible p: admissible p admissible (simplify p).
  intros. eauto using simplify_sound.

Hint Resolve simplify_admissible.

Lemma simplified_real_step p q: simplified p admissible p p >[]> q translate p >> translate q.
  intros eq ap R. induction R;inv ap;simpl.
  -injection eq;intros eq1 eq2;clear eq. auto.
  -injection eq;intros eq1 eq2;clear eq. auto.
  -exfalso. discriminate eq.
  -exfalso. simpl in eq.
   assert (H:value (nth x sigma (var x))).
   {apply H2.
    apply nth_In.
    now inv H3. }
   inv H.
   inv eq.
  -rewrite pSubst_cons.
   apply L.stepApp.
   inv H1. eauto.


Lemma translate_lam p s: admissible p simplify p = p (λ s) = translate p s A, p = clos (lam s) A.
  intros vp eq1 eq2. inv vp. discriminate eq2.
  destruct s0.
  -simpl in eq1. destruct (H0 (nth n sigma (var n))).
   +apply nth_In. now inv H1.
   +discriminate eq1.
  -discriminate eq2.

Lemma translate_simplified_complete p t: simplified p admissible p
                              translate p >> t q, translate q = t p >[]> q.
  intros sp ap R. revert t R. induction p; inv ap;intros t R;simpl in R.
  -simpl in ×. destruct s; simpl in R.
    assert (H: value (nth n sigma (var n))).
    { apply H2.
      apply nth_In.
      now inv H3. }
    inv H.
    apply (f_equal translate) in H4.
    rewrite <- map_nth in H4.
    simpl in H4.
    replace (n-0) with n in R by omega.
    rewrite <- H4 in R. inv R.
   +inv sp.
   +inv R.
  -injection sp; intros sp2 sp1; clear sp.
   inversion R as [s1' s2' [eqs1 eqs2] | |].
   +destruct (translate_lam H1 sp1 eqs1) as [s1 [A1 ->]].
    destruct (translate_lam H2 sp2 eqs2) as [s2 [A2 ->]].
    inv H1. inv H2.
    injection eqs1 as eqs1.
    injection eqs2 as eqs2.
     (clos s1 ((clos (lam s2) A2)::A1)).
     rewrite pSubst_cons,eqs1,eqs2.
     reflexivity. eauto.
   +destruct (IHp2 sp2 H2 _ H) as [q [eq' R']].
     (p1 q). split;auto. simpl. congruence.
   +destruct (IHp1 sp1 H1 _ H) as [q [eq' R']].
     (q p2). split;auto. simpl. congruence.

Lemma translate_irstep_iff p: admissible p (irred L.step (translate p) irred step (simplify p)).
  intros ap.
  assert (closed (translate p)) by now apply translate_closed.
  rewrite simplify_translate.
  -intros C q R.
   apply simplified_real_step in R.
   +now apply C in R.
   +now apply simplify_simplified.
  -intros C q R.
   apply translate_simplified_complete in R as (q'&eq&R'); auto using simplify_simplified.
   now apply C in R'.

Lemma translate_lambda_iff p: admissible p (lambda (translate p) value (simplify p)).
  intros ap. assert (closed (translate p)) by now apply translate_closed.
  rewrite <- irred_iff;auto.
  rewrite value_iff_irred;auto.
  now apply translate_irstep_iff.

Lemma translate_complete_param p t : admissible p translate p >> t q k, k > 0 t = translate q p >[]^k q.
  intros ap R.
  rewrite simplify_translate in R.
  destruct translate_simplified_complete with (p:=simplify p) (t:=t) as (q&eq&R').
  +now apply simplify_simplified.
  +now apply simplify_admissible.
  +exact R.
  + q.
   assert (R'':=simplify_sound p).
   apply star_pow in R'' as [k R''].
    (k+1). repeat split.
   ×eapply pow_add. (simplify p). apply rcomp_1 in R'. auto.

Lemma translate_complete p t : admissible p translate p >> t q, t = translate q p >[]* q.
  intros ap R.
  destruct (translate_complete_param ap R) as (q&?&_&eq&R').
  apply pow_star in R'. auto.

Lemma Lstep_complete_star p t : admissible p translate p >* t q, t = translate q p >[]* q.
  intros ap R.

  rewrite star_pow in R. destruct R as [n R]. revert p ap t R. apply complete_induction with (x:=n);clear n;intros n IH;intros.

  destruct n.
  -inv R. eauto using star.
  -rewrite (pow_add _ 1) in R.
   destruct R as [X' [R' R]].
   apply rcomp_1 in R'.
   apply translate_complete in R' as [s'[eq Rs]];auto.
   subst X'.
   apply IH in R as (q&->&R);auto.
   + q. now rewrite Rs.
   +now rewrite <- Rs.

Simulation Lemma

Definition eval p q := p >[]* q value q.

Lemma simulation p t :
  admissible p
  L.eval (translate p) t q, t = translate q eval p q.
  intros ap. split.
  -intros [R lt].
   apply Lstep_complete_star in R as (q&->&R);auto.
    (simplify q).
   +now rewrite simplify_translate.
   +rewrite R.
    now rewrite <- simplify_sound.
   +apply translate_lambda_iff in lt;auto.
    now rewrite <- R.
  -intros (q&->&R&vq).
   +now apply translate_sound.
   +apply translate_lambda_iff.
    ×now rewrite <- R.
    ×now inv vq.

Lemma simulation' s t :
  closed s
  L.eval s t q, t = translate q eval (clos s []) q.
  intros cs.
  replace s with (translate (clos s [])) at 1 by (simpl;apply pSubst_nil).
  apply simulation.
  now apply emptEnv_admissible.

Close Scope LC_scope.