Require Import ARS Base L LexSizeInduction.
Require Export SKv SKvTactics.

Fixpoint flatten X :=
  match X with
    | var (Datatypes.S n) ⇒ var n
    | app X Y ⇒ (flatten X) (flatten Y)
    | X ⇒ X
  end.

Lemma flatten_value X : value X → value (flatten X).
Proof.
  intros vs. induction vs;simpl;auto.
  -destruct x;auto.
Qed.
Hint Resolve flatten_value : value.

Lemma flatten_closed_idem X : closed X → X = (flatten X).
Proof.
  intros cs. induction cs;simpl;congruence.
Qed.

Lemma flatten_varClosed_iff y X:
  varClosed 0 X →
  varClosed ( Datatypes.S y) X ↔ varClosed y (flatten X).
Proof.
  intros vc. induction X;[destruct n|..];simpl;try (solve [split;auto]);inv vc.
  -tauto.
  -split; intros H;inv H; constructor; congruence.
  -rewrite !varClosedApp_iff. tauto.
Qed.

Lemma flatten_subst_varClosed X Y : varClosed 0 X → flatten X = subst X 0 Y.
Proof.
  intros vc. induction vc;auto.
  -destruct y.
   +tauto.
   +destruct y; reflexivity.
  -simpl;congruence.
Qed.

Lemma flatten_subst_commute X x Y :
  varClosed 0 X → closed Y →
  subst (flatten X) x Y = flatten (subst X (Datatypes.S x) Y).
Proof.
  intros neq ct. induction X;simpl;auto.
  -destruct n.
   +simpl. inv neq. congruence.
   +dec;simpl.
    ×dec. now apply flatten_closed_idem. congruence.
    ×repeat dec; try congruence;try omega. destruct n;try omega;simpl. destruct n;now simpl.
  -inv neq. now rewrite IHX1,IHX2.
Qed.

Fixpoint abs X :=
  match X with
    | var 0 ⇒ I
    | app u v ⇒ if decision(varClosed 0 (app u v) ∧ value X)
                 then K (flatten X)
                 else S (abs u) (abs v)
    | X ⇒ K (flatten X)
  end.

Lemma abs_maxValue X : maxValue (abs X).
Proof with split;[value|intros ? C;inv C].
  induction X;simpl.
  -destruct n...
  -idtac...
  -idtac...
  -dec... destruct a as [? a]. apply flatten_value in a. inv a; value.
Qed.
Hint Resolve abs_maxValue : value.

Lemma abs_closed_eq X : varClosed 0 X → value X → abs X = K (flatten X).
Proof.
  intros vc vs. destruct X;simpl;auto.
  -destruct n;auto. inv vc. tauto.
  -dec;tauto.
Qed.

Lemma abs_varClosed_iff y X: varClosed (Datatypes.S y) X ↔ varClosed y (abs X).
Proof with try now simpl;(try split);intros;repeat inv_varClosed;auto 20;intuition.
  induction X;[destruct n|..];simpl;repeat dec;unfold I...
  -rewrite flatten_varClosed_iff...
Qed.

Local Ltac redPow :=
  match goal with
    |- _ >>^_ _ ⇒ rewrite (pow_add step 1); eexists; split;[eexists;split;[eauto|reflexivity]|]
  | |- _ >>^_ _ ⇒ reflexivity
  end.

Lemma abs_sound_pow X Y : value Y → ∃ n, n > 0 ∧ ((abs X) Y) >>^n (subst X 0 Y).
Proof with split;[omega|repeat redPow].
  intros vt. induction X;simpl.
  -destruct n;repeat dec;try omega.
   +unfold I. ∃ 2...
   +∃ 1... simpl. now rewrite <- minus_n_O.
  -∃ 1...
  -∃ 1...
  -destruct IHX1 as [n1 [neq1 R1]].
   destruct IHX2 as [n2 [neq2 R2]].
   dec.
   +destruct a as [a' a].
    apply flatten_value in a.
    ∃ 1... inv a'.
    rewrite <- !flatten_subst_varClosed;now auto.
   +∃ (1+(n1+n2))...
    apply stepS;value.
    now apply step_pow_app.
Qed.

Lemma abs_sound X Y : value Y → (abs X) Y >>* (subst X 0 Y).
Proof.
  intros. eapply abs_sound_pow in H as (?&?&?). eapply pow_star. eassumption.
Qed.

Lemma subst_abs_commute x X Y : closed Y → maxValue Y → subst (abs X) x Y = abs (subst X (Datatypes.S x) Y).
Proof.
  intros cY mY. revert x. induction X;intros; simpl;auto.
  -destruct n;simpl.
   +auto.
   +repeat dec;simpl; try (congruence||omega).
    ×rewrite abs_closed_eq;auto.
     rewrite <- flatten_closed_idem;auto. value.
    ×destruct n;simpl.
     --exfalso;omega.
     --destruct n;reflexivity.
  -repeat dec; simpl.
   +destruct a as [a a']. inv a.
    rewrite !flatten_subst_commute;auto.
   +exfalso.
    apply n.
    destruct a. split.
    ×inv H;simpl; constructor; apply subst_free_iff;auto; try omega.
    ×inv H0;simpl; constructor;apply valueSubst;value.
   +exfalso.
    apply n.
    inv a. split.
    ×rewrite subst_free_iff;simpl;try exact H;auto. omega.
    ×eapply (maxValueSubst) with (Y:=Y);auto. exact H0.
   +now rewrite IHX1, IHX2.
Qed.

Fixpoint C (s : L.term) : term :=
  match s with
  | L.var x ⇒ # x
  | L.app s t ⇒ (C s) (C t)
  | lam s ⇒ abs (C s)
  end.

Lemma C_dclosed_iff n s: dclosed n s ↔ (∀ x, x ≥ n → varClosed x (C s)).
Proof.
  revert n. induction s;intros;simpl.
  -setoid_rewrite varClosedVar_iff.
   setoid_rewrite dclosedVar_iff.
   split;intros. omega. decide (n≥n0); firstorder omega.
  -rewrite dclosedApp_iff.
   setoid_rewrite varClosedApp_iff.
   rewrite IHs1,IHs2.
   intuition; now apply H.
  -rewrite dclosedLam_iff.
   rewrite IHs.
   setoid_rewrite <-abs_varClosed_iff.
   intuition. destruct x. omega. intuition.
Qed.

Lemma C_closed_varClosed x s: L.closed s → varClosed x (C s).
  intros cs. apply C_dclosed_iff with (n:=0). now apply closed_dcl. omega.
Qed.

Lemma C_closed s: L.closed s ↔ closed (C s).
Proof.
  rewrite closed_dcl. rewrite C_dclosed_iff. rewrite <- varClosed_closed. intuition.
Qed.

Lemma C_closed_if s: L.closed s → closed (C s).
Proof.
  apply C_closed.
Qed.
Hint Resolve C_closed_if C_closed_varClosed : value.

Lemma C_lam_value X : lambda X → value (C X).
Proof.
  intros;inv H; simpl;value.
Qed.
Hint Resolve C_lam_value :value.

Lemma abs_no_var s n: abs s ≠ var n.
Proof.
  destruct s;try destruct n0;simpl; unfold I;try dec; try congruence.
Qed.

Lemma abs_no_K X: abs X ≠ K.
Proof.
  intros eq. eapply abs_maxValue with (Z:=K). rewrite eq. eauto.
Qed.

Lemma abs_no_S X: abs X ≠ S.
Proof.
  intros eq. eapply abs_maxValue with (Z:=K). rewrite eq. eauto.
Qed.

Lemma abs_no_Ss X Y: abs X ≠ S Y.
Proof.
  intros eq. destruct (abs_maxValue X) as [v H].
  rewrite eq in ×. inv v. eapply (H K). auto.
Qed.

Lemma C_near_value s X:¬ value ((C s) X).
Proof.
  intros H. induction s.
  -inv H.
  -inv H. apply IHs1.
   rewrite <- H0;auto.
  -now apply abs_maxValue in H.
Qed.

Lemma subst_C_commute s x t: dclosed (1+ x) s → L.closed t → lambda t → subst (C s) x (C t)= C (L.subst s x t).
Proof.
  intros cs ct l;subst. revert x cs ;induction s as [ | |s'];intros x cs;simpl in ×.
  -inv cs.
   repeat dec;try omega.
   +reflexivity.
   +reflexivity.
  -inv cs.
   rewrite IHs1, IHs2;auto.
  -inv cs.
   rewrite <- IHs';auto.
   rewrite subst_abs_commute; value.
   inv l... apply abs_maxValue.
Qed.

Lemma C_sound_pow s t: L.closed s → s >> t → ∃ k, k > 0 ∧ (C s) >>^k (C t).
Proof.
  intros cs st. induction st as [s' u'| | ];try apply L.closed_app in cs as [? ?].
  -remember (lam u') as u.
   assert (lambda u) by (subst;value). simpl.
   destruct (abs_sound_pow (C s')) with (Y:= (C u)) as (k & ? & R). value.
   ∃ k. split;auto.
   rewrite <- subst_C_commute; auto.
   rewrite closed_dcl in H.
   inv H. value.
  -destruct IHst as (k&?&R); auto.
   ∃ k. split; auto.
   now apply step_pow_app_r.
  -destruct IHst as (k&?&R); auto.
   ∃ k. split; auto.
   now apply step_pow_app_l.
Qed.

Lemma C_sound s t: L.closed s → s >* t → C s >>* C t.
Proof.
  intros cs st. induction st.
  -eauto using star.
  -destruct (C_sound_pow cs H) as (k&_&R).
   rewrite R. apply IHst.
   eauto using closed_step.
Qed.

Lemma C_value_iff s : L.closed s → (value (C s) ↔ lambda s).
Proof.
  intros cs. split.
  -intros v. induction s.
   +rewrite closed_dcl in cs;now inv cs.
   +exfalso.
    apply L.closed_app in cs as [cs1 cs2]. simpl in v.
    destruct IHs1 as [? ->];value. inv v;value.
    destruct IHs2 as [? ->];value. inv v;value.
    now apply abs_maxValue in v.
   +eauto.
  -intros. inv H. value.
Qed.

Lemma C_sound_equiv s t : L.closed s → L.closed t → s == t → C s =*= C t.
Proof.
  intros cs ct eq. apply L.church_rosser in eq. destruct eq as [u [Xu tu]]. now rewrite (C_sound cs Xu), (C_sound ct tu).
Qed.

Lemma C_eval_sound s t : L.closed s → L.closed t → (L.eval s t → eval (C s) (C t)).
Proof.
  intros cs ct [R lt].
  apply eval_iff;split.
  -apply C_sound in R;auto. now rewrite R.
  -value.
Qed.

Fixpoint flatten_inv X :=
  match X with
    | var x ⇒ var (Datatypes.S x)
    | app X Y ⇒ (flatten_inv X) (flatten_inv Y)
    | _ ⇒ X
  end.

Lemma flattenInv_correct s: varClosed 0 s → flatten_inv (flatten s) = s.
Proof.
  intros H. induction H;try destruct y;simpl;try congruence.
Qed.

Lemma flattenInj X Y : varClosed 0 X → varClosed 0 Y → flatten X = flatten Y → X=Y.
Proof.
  intros A B C. setoid_rewrite <- flattenInv_correct at 2 1;congruence.
Qed.

Fixpoint abs_inv X :=
  match X with
    | app (app S K) K ⇒ var 0
    | app (app S X) Y ⇒ (abs_inv X) (abs_inv Y)
    | app K X ⇒ flatten_inv X
    | _ ⇒ var 100
  end.

Lemma abs_inv_correct s: abs_inv (abs s) = s.
Proof.
  apply size_induction with (f:=size) (x:=s);clear s;intros s IHm.
  destruct s;try reflexivity.
  -destruct n; reflexivity.
  -simpl. dec;simpl.
   +destruct a as [a _]. inv a. rewrite !flattenInv_correct;auto.
   +simpl in IHm. destruct (abs s1) eqn:eq; rewrite <- eq; try now(f_equal;apply IHm; omega).
    now apply abs_no_K in eq.
Qed.

Lemma absInj s t : abs s = abs t → s = t.
Proof.
  intros. setoid_rewrite <- abs_inv_correct at 2 1. congruence.
Qed.

Fixpoint lSize s :=
  match s with
      L.var _ ⇒ 0
    | L.app s t ⇒ 1 + lSize s + lSize t
    | L.lam s ⇒ 1 + lSize s
  end.

Lemma flattenInv_size s : size (flatten_inv s) = size s.
Proof.
  induction s;try destruct n;simpl;try omega.
Qed.

Lemma abs_inv_size_val s : size s = 0 ∨ size (abs_inv s) < (size s).
Proof with repeat rewrite flattenInv_size;eauto;try now simpl in *;try omega.
  apply size_induction with (f:=size) (x:=s);clear s;intros s IH.
  destruct s... right. assert (H:=IH s2). mp H... simpl. destruct s1...
  destruct s1_1... destruct s1_2...
  -destruct s2...
  -destruct s2...
  -destruct s2...
  -specialize (IH (s1_2_1 s1_2_2)). mp IH... destruct IH... inv H... destruct s2...
Qed.

Function C_inv X {measure size X} : L.term :=
  match X with
    | var x ⇒ L.var x
    | K ⇒ L.var 100
    | S ⇒ L.var 100
    | app X1 X2 ⇒ if decision (value X) then lam (C_inv (abs_inv X)) else (C_inv X1) (C_inv X2)
  end.
Proof with subst;repeat (setoid_rewrite flattenInv_size||idtac);try now (simpl in *;omega).
  -intros. destruct (abs_inv_size_val (X1 X2))...
  -intros...
  -intros...
Qed.

Lemma C_inv_correct s: C_inv (C s) = s.
Proof with try now (simpl in *;try eauto;try congruence;try omega).
  apply size_induction with (f:=lSize) (x:=s);clear s;intros s IHm.
  rewrite C_inv_equation. destruct s...
  -simpl. dec. now apply C_near_value in v. rewrite !IHm...
  -simpl. destruct (abs (C s)) eqn:eq.
   +now apply abs_no_var in eq.
   +now apply abs_no_K in eq.
   +now apply abs_no_S in eq.
   +dec.
    ×rewrite <- eq. rewrite abs_inv_correct. rewrite IHm...
    ×destruct n. rewrite <- eq. value.
Qed.

Lemma CInj s t : C s = C t → s = t.
Proof.
  intros. setoid_rewrite <- C_inv_correct at 2 1. congruence.
Qed.

Lemma abs_step_prefix s Y X: value Y → (C (λ s)) Y >>> X → X >>* subst (C s) 0 Y.
Proof.
  intros vY R'.
  destruct (@abs_sound_pow (C s) Y) as [n [ge R]]; value.
  destruct n;try omega.
  rewrite (pow_add _ 1) in R.
  destruct R as [X' [R1 R2]].
  destruct R1 as [? [R1 eq]].
  inv eq.
  apply value_step_unique with (Z1:=X')in R';value. subst X'.
  now apply pow_star in R2.
Qed.

Lemma C_step_app s1 s2 X:
  L.closed s1 →
  L.closed s2 →
  (C s1) (C s2) >>> X →
  (lambda s2 ∧ lambda s1)
  ∨ (∃ X', (C s1 >>> X' ∧ X = X' (C s2)))
  ∨ (∃ X', (C s2 >>> X' ∧ X = (C s1) X')).
Proof.
  intros cs1 cs2 R. assert (R':=R). inv R'.
  -left. split;apply C_value_iff;value. rewrite <- H. auto.
  -left. split;apply C_value_iff;value. rewrite <- H. auto.
  -right. left. ∃ X'. intuition.
  -right. right. ∃ Y'. intuition.
Qed.

Lemma C_step_prefix s X : L.closed s → C s >>> X → ∃ t, s >> t ∧ X >>* C t.
Proof.
  revert X;induction s;intros X cs R.
  -inv R.
  -apply L.closed_app in cs. destruct cs as [cs1 cs2]. simpl in R.
   specialize (C_step_app cs1 cs2 R).
   intros [(l1&l2)|[(Y&R'&->)|(Y&R'&->)]].
   +inv l1. inv l2.
    apply abs_step_prefix in R;value. eexists. split.
    ×now apply step_value.
    ×apply closed_dcl in cs1. inv cs1. now rewrite <- subst_C_commute.
   +destruct (IHs1 Y) as [? [? R1]];value. eexists;split. eauto. now rewrite R1.
   +destruct (IHs2 Y) as [? [? R2]];value. eexists;split. eauto. now rewrite R2.
  -apply value_irred in R. tauto. value.
Qed.

Lemma C_star_prefix s X : L.closed s → C s >>* X → ∃ t, s >* t ∧ X >>* C t.
Proof.
  intros cs R.
  rewrite star_pow in R. destruct R as [n R]. revert s cs X 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'.
   destruct (C_step_prefix cs R') as [s'[Rs RX']].
   rewrite star_pow in RX'. destruct RX' as [n' RX'].

   destruct (SK_UC R RX') as (?&?&?&?&?&?&?&?).
   apply IH in H0;try omega. destruct H0 as [t [R1 R2]]. ∃ t. now rewrite Rs,H. now apply (closed_step Rs).
Qed.

Lemma C_eval_pullback s X : L.closed s → eval (C s) X → ∃ t, C t = X ∧ L.eval s t.
Proof.
  intros cs [R vX].
  apply C_star_prefix in R as (u&R&R');value.
  apply star_value in R';value. subst X. rewrite R in cs. ∃ u. split;[|split];auto.
  now apply C_value_iff.
Qed.

Lemma C_eval_complete s t : L.closed s → eval (C s) (C t) → L.eval s t.
Proof.
  intros cs H.
  apply C_eval_pullback in H as [? [eq H]];auto.
  apply CInj in eq. now subst.
Qed.

Lemma abs_nonLambda_continue s t X :
  ¬ lambda s →
  L.closed (lam s) → proc t →
  C ((lam s) t) >>> X
  →∃ s', L.closed s' ∧ X = C s' ∧ (lam s) t == s'.
Proof.
  intros nls dcl [ct vt] R.
  apply closed_dcl in dcl. inv dcl. rename H1 into dcl.
  destruct s.
  -assert (n=0) by (inv dcl; omega). subst n.
   simpl in R. unfold I in R.
   ∃ ((lam t) (lam t)).
   repeat split;value.
   +repeat inv_SKvstep.
     ×simpl. repeat rewrite abs_closed_eq, <- flatten_closed_idem;value.
     ×apply value_irred in H2;value. tauto.
   +rewrite stepApp,ct. now rewrite step_value.
  -simpl in R. destruct decision as [(cs'& v')| ?].
   +assert (L.closed (s1 s2)).
    { rewrite C_closed. apply varClosed_closed. intros. decide (x=0).
      -subst x. assumption.
      -eapply C_dclosed_iff. eassumption. omega.
    }
    apply L.closed_app in H as [? ?].
    rewrite <- !flatten_closed_idem in R;value.
    inv R.
    ×eexists (s1 s2).
     repeat split;value. inv vt.
     rewrite stepApp. simpl.
     now rewrite H,H0.
    ×inv H4. inv H5. now apply value_irred in H5.
    ×apply value_irred in H4;value. tauto.
   +repeat inv_SKvstep.
    ×inv dcl.
     ∃ (((lam s1) t) ((lam s2) t));repeat split. value.
     repeat setoid_rewrite step_value; now value.
    ×apply value_irred in H2;now value.
    ×apply value_irred in H3;now value.
    ×apply value_irred in H2;now value.
  -simpl in ×. destruct nls. value.
Qed.

Lemma abs_lambda_equiv s t u: lambda s → L.closed (lam s) → proc t →
  C ((lam s) t) >>* C u → ((λ s) t) == u.
Proof with value.
  intros l1 c1 p2 R.
  assert (L.closed u).
  { rewrite C_closed in ×.
    apply star_closed in R. value.
    constructor; value. }
  apply star_ecl in R. simpl in R. rewrite abs_sound in R...
  symmetry in R. apply closed_dcl in c1. inv c1.
  rewrite subst_C_commute in R...
  assert (vs:value (C (L.subst s 0 t))).
  { apply C_lam_value.
    inv l1... }
  apply equiv_value in R...
  destruct (@C_eval_complete u (L.subst s 0 t)) as [R' v];value.
  rewrite R',step_value;value.
Qed.

Lemma C_complete s t:
  L.closed s → C s >>* C t → s == t.
Proof with simpl;eauto using pow_star;value;try omega.
  intros cs R. apply star_pow in R as [k R]. revert t cs R.
  apply (lex_size_induction (fun x ⇒ x) (fun s ⇒ size (C s)) k s);clear s k;intros k s IH.
  intros ? cs R.
  assert (L.closed t).
  { rewrite C_closed in ×.
    apply pow_star in R.
    now apply star_closed in R. }
  destruct s.
  -now apply var_not_closed in cs.
  -destruct t.
   +now apply var_not_closed in H.
   +apply L.closed_app in cs as (cs1&cs2).
    apply pow_decompose in R.
    destruct R as [(->&eq)|(?&?&X1&X2&k1&k2&(eq&?R1&R2)&H')].
    ×apply CInj in eq.
     now rewrite eq.
    ×injection eq;intros <- <-;clear eq.
     destruct H' as [(eq&->)|(Y&k'&?v1&v2&R&R'&<-)].
     --inv eq.
       apply IH in R1...
       apply IH in R2...
       now rewrite R1,R2.
     --destruct (@C_eval_pullback s1 X1) as [? [<- [R1' [u1 ->]]]]...
       destruct (@C_eval_pullback s2 X2) as [? [<- [R2' [u2 ->]]]]...
       assert (L.closed (lam u1)) by now rewrite <- R1'.
       assert (L.closed (lam u2)) by now rewrite <- R2'.
       rewrite R1',R2'.
       decide (lambda u1).
       ++apply abs_lambda_equiv...
         constructor...
         now rewrite R,R'.
       ++apply abs_nonLambda_continue in R as (s'&cs'&->&eq);[..|constructor]...
         apply IH in R'...
         now rewrite eq,R'.
   +apply pow_star in R.
    destruct (@C_eval_complete (s1 s2) (lam t))...
  -apply pow_star in R.
   apply star_value in R...
   now apply CInj in R as <-.
Qed.

Lemma C_complete_equiv s t :L.closed s → L.closed t → C s =*= C t → s == t.
Proof.
  intros cs ct R.
  apply SK_church_rosser in R as [Z [Rs R]].
  apply C_star_prefix in Rs as [s' [R' Rs]];value.
  rewrite Rs in R.
  apply C_complete in R as R;auto.
  now rewrite R', R.
Qed.

Lemma C_equiv_iff s t : L.closed s → L.closed t → (s == t ↔ C s =*= C t).
Proof.
  intros cs ct. split.
  -now apply C_sound_equiv.
  -now apply C_complete_equiv.
Qed.

Lemma C_eval_iff s t : L.closed s → L.closed t → (L.eval s t ↔ eval (C s) (C t)).
Proof.
  intros cs ct.
  unfold L.eval.
  rewrite eval_iff.
  rewrite <- C_equiv_iff, C_value_iff; auto.
  intuition. now apply equiv_lambda.
Qed.