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

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

Instance LC_eq_dec : eq_dec term.


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

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.

Compatibility Laws

Lemma star_app_l p p' q :
  p >[]* p' p q >[]* p' q.

Lemma star_app_r p q q' :
  q >[]* q' p q >[]* p q'.

Instance star_step_app_proper :
  Proper ((star step) ==> (star step) ==> (star step)) app.

Lemma pow_app_l p p' q n: p >[]^n p' (p q) >[]^n (p' q).

Lemma pow_app_r p q q' n: q >[]^n q' (p q) >[]^n (p q').

Lemma pow_app p p' q q' k l: p >[]^k p' q >[]^l q' (p q) >[]^(k+l) (p' q').

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.

Lemma admissible_star p q: admissible p p >[]* q admissible q.
Hint Immediate admissible_star.

Instance admissible_step_proper :
  Proper ((star step) ==> Basics.impl) admissible.

Values and Irredicibility

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.

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.

Lemma pSubst_dclosed y A s: ( a, a el A closed a) dclosed (y+|A|) s dclosed y (pSubst s y A).

Lemma pSubst_closed A s: ( a, a el A closed a) dclosed (|A|) (s) closed (pSubst s 0 A).

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

Lemma translate_map_closed s sigma: ( p, p el sigma admissible p) s el (map translate sigma) closed s.

Hint Resolve translate_map_closed.


Application of soundness



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.

Lemma simplify_sound p: p >[]* simplify p.

Lemma simplify'_translate_var' x A : translate (clos (L.var x) A) = translate (nth x A (var x)).

Lemma simplify'_translate s A: translate (clos s A) = translate (simplify' s A).

Lemma simplify_translate p: translate p = translate (simplify p).

Lemma simplify'_simplified s sigma: ( p, p el sigma value p) simplify (simplify' s sigma)=simplify' s sigma.

Lemma simplify_simplified p: admissible p simplified (simplify p).

Lemma simplify_admissible p: admissible p admissible (simplify p).

Hint Resolve simplify_admissible.

Lemma simplified_real_step p q: simplified p admissible p p >[]> q translate p >> translate q.


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.

Lemma simulation' s t :
  closed s
  L.eval s t q, t = translate q eval (clos s []) q.

Close Scope LC_scope.