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.
Bind Scope LC_scope with term.
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.
Proof.
  apply term_rec_deep' with (Pl:=fun A ⇒ (∀ a, a el A → P a));auto.
  -simpl. tauto.
  -intros. inv H1; auto.
Qed.

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).
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')...
   +idtac...
  -assert (H1:=IH p1 q1). assert (H2:=(IH p2 q2)). clear IH. inv H1; inv H2...
Qed.

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

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).
Proof with try ((now left; constructor)||(now right;intros C;inv C)).
  destruct p... destruct s...
Qed.

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

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

Lemma star_app_r p q q' :
  q >[]* q' → p q >[]* p q'.
Proof.
  induction 1; eauto using star.
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_app_l, A. apply star_app_r, B.
Qed.

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

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

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

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.
Proof.
  intros ap R. induction R;repeat inv_admissible.
  -eauto.
  -eauto.
  -inv H3. eauto.
  -apply H1. apply nth_In. now inv H3.
  -inv H7. repeat constructor;[intros ? [<-|]..|];try subst;eauto.
Qed.

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

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

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

Lemma value_iff_irred p : admissible p → value p ↔ irred step p.
Proof.
  intros ap. split. apply value_irred.
  intros H. induction ap.
  -exfalso.
   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.
   +auto.
Qed.

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.
Proof.
  revert x. induction s;intros;simpl.
  -decide (x>n). reflexivity. now destruct(n-x).
  -congruence.
  -congruence.
Qed.

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.
Proof.
  revert k;induction s as [x| |];intros k cl.
  -simpl;decide (S k > x); simpl;decide (k>x); decide (x=k);try omega.
   +reflexivity.
   +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.
Qed.

Lemma pSubst_dclosed y A s: (∀ a, a el A → closed a) → dclosed (y+|A|) s → dclosed y (pSubst s y A).
Proof.
  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.
Qed.

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

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

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

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 []].
   +assumption.
   +∃ k...
  -destruct IHR as [k []].
   +assumption.
   +∃ k...
  -∃ 0...
  -∃ 0.
   split;[omega|]. simpl.
   rewrite <- minus_n_O.
   rewrite <-map_nth with (f:=translate).
   reflexivity.
  -∃ 1.
   split;[omega|]. simpl.
   rewrite pSubst_cons;eauto.
   eexists;split;[|reflexivity]. auto.
Qed.

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

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

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

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.
Proof.
  induction s;simpl.
  -now rewrite stepVar.
  -rewrite stepApp.
   now apply star_step_app_proper.
  -reflexivity.
Qed.

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

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

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

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

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

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

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

Hint Resolve simplify_admissible.

Lemma simplified_real_step p q: simplified p → admissible p → p >[]> q → translate p >> translate q.
Proof.
  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.
   congruence.
  -rewrite pSubst_cons.
   apply L.stepApp.
   inv H1. eauto.
Qed.

Lemma translate_lam p s: admissible p → simplify p = p → (λ s) = translate p → ∃ s A, p = clos (lam s) A.
Proof.
  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.
  -eauto.
Qed.

Lemma translate_simplified_complete p t: simplified p → admissible p →
                              translate p >> t → ∃ q, translate q = t ∧ p >[]> q.
Proof.
  intros sp ap R. revert t R. induction p; inv ap;intros t R;simpl in R.
  -simpl in ×. destruct s; simpl in R.
   +exfalso.
    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)).
    split.
    ×simpl.
     rewrite pSubst_cons,eqs1,eqs2.
     reflexivity. eauto.
    ×constructor.
   +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.
Qed.

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

Lemma translate_lambda_iff p: admissible p → (lambda (translate p) ↔ value (simplify p)).
Proof.
  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.
Qed.

Lemma translate_complete_param p t : admissible p → translate p >> t → ∃ q k, k > 0 ∧ t = translate q ∧ p >[]^k q.
Proof.
  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.
   ×omega.
   ×congruence.
   ×eapply pow_add. ∃ (simplify p). apply rcomp_1 in R'. auto.
Qed.

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

Lemma Lstep_complete_star p t : admissible p → translate p >* t → ∃ q, t = translate q ∧ p >[]* q.
Proof.
  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.
Qed.

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.
Proof.
  intros ap. split.
  -intros [R lt].
   apply Lstep_complete_star in R as (q&->&R);auto.
   ∃ (simplify q).
   split;[|split].
   +now rewrite simplify_translate.
   +rewrite R.
    now rewrite <- simplify_sound.
   +apply translate_lambda_iff in lt;auto.
    now rewrite <- R.
  -intros (q&->&R&vq).
   split.
   +now apply translate_sound.
   +apply translate_lambda_iff.
    ×now rewrite <- R.
    ×now inv vq.
Qed.

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

Close Scope LC_scope.