Require Export L.
Require Import Bool.

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.

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 x ⇒ IHVar x
       | app s t ⇒ IHApp s (f s) t (f t)
       | clos s A ⇒ IHClos s A
         ((fix g A : Pl A :=
            match A with
                [] ⇒ IHNil
              | a::A ⇒ IHCons 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.

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,nil ⇒ true
                                            | (a::B), (a'::B') ⇒ andb (comp_eqb a a') (f B B')
                                            | _,_ ⇒ false
                                              end) sigma sigma')
                              else false
                          | _,_ ⇒ false
  end.

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.

Instance value_dec p : dec (value p).

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

Lemma LC_UC: uniformly_confluent step.

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

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

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.

Lemma value_irred p : value p → irred step p.

Lemma value_iff_irred p : admissible p → value p ↔ irred step p.

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

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

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

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.

Lemma translate_sound_step p q: admissible p → p >[]> q → ∃ k, k ≤ 1 ∧ (translate p) >^k (translate q).

Lemma translate_sound p q: admissible p → p >[]* q → translate p >* translate q.

Lemma emptEnv_admissible s: closed s → admissible (clos s []).

Lemma emptEnv s p: closed s → clos s [] >[]* p → s >* translate p.

Fixpoint simplify' s sigma:=
  match s with
    | L.app s t ⇒ (simplify' s sigma) (simplify' t sigma)
    | L.var x ⇒ nth x sigma (var x)
    | lam s ⇒ clos (lam s) sigma
  end.

Fixpoint simplify p :=
  match p with
    | app p q ⇒ (simplify p) (simplify q)
    | clos s A ⇒ simplify' s A
    | _ ⇒ p
  end.

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.

Lemma translate_lam p s: admissible p → simplify p = p → (λ s) = translate p → ∃ s A, p = clos (lam s) A.

Lemma translate_simplified_complete p t: simplified p → admissible p →
                              translate p >> t → ∃ q, translate q = t ∧ p >[]> q.

Lemma translate_irstep_iff p: admissible p → (irred L.step (translate p) ↔ irred step (simplify p)).

Lemma translate_lambda_iff p: admissible p → (lambda (translate p) ↔ value (simplify p)).

Lemma translate_complete_param p t : admissible p → translate p >> t → ∃ q k, k > 0 ∧ t = translate q ∧ p >[]^k q.

Lemma translate_complete p t : admissible p → translate p >> t → ∃ q, t = translate q ∧ p >[]* q.

Lemma Lstep_complete_star p t : admissible p → translate p >* t → ∃ q, t = translate q ∧ p >[]* q.

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.