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).
Hint Resolve flatten_value : value.

Lemma flatten_closed_idem X : closed X → X = (flatten X).

Lemma flatten_varClosed_iff y X:
  varClosed 0 X →
  varClosed ( Datatypes.S y) X ↔ varClosed y (flatten X).

Lemma flatten_subst_varClosed X Y : varClosed 0 X → flatten X = subst X 0 Y.

Lemma flatten_subst_commute X x Y :
  varClosed 0 X → closed Y →
  subst (flatten X) x Y = flatten (subst X (Datatypes.S x) Y).

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).
Hint Resolve abs_maxValue : value.

Lemma abs_closed_eq X : varClosed 0 X → value X → abs X = K (flatten X).

Lemma abs_varClosed_iff y X: varClosed (Datatypes.S y) X ↔ varClosed y (abs X).

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

Lemma abs_sound X Y : value Y → (abs X) Y >>* (subst X 0 Y).

Lemma subst_abs_commute x X Y : closed Y → maxValue Y → subst (abs X) x Y = abs (subst X (Datatypes.S x) Y).

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

Lemma C_closed_varClosed x s: L.closed s → varClosed x (C s).

Lemma C_closed s: L.closed s ↔ closed (C s).

Lemma C_closed_if s: L.closed s → closed (C s).
Hint Resolve C_closed_if C_closed_varClosed : value.

Lemma C_lam_value X : lambda X → value (C X).
Hint Resolve C_lam_value :value.

Lemma abs_no_var s n: abs s ≠ var n.

Lemma abs_no_K X: abs X ≠ K.

Lemma abs_no_S X: abs X ≠ S.

Lemma abs_no_Ss X Y: abs X ≠ S Y.

Lemma C_near_value s X:¬ value ((C s) X).

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

Lemma C_sound_pow s t: L.closed s → s >> t → ∃ k, k > 0 ∧ (C s) >>^k (C t).

Lemma C_sound s t: L.closed s → s >* t → C s >>* C t.

Lemma C_value_iff s : L.closed s → (value (C s) ↔ lambda s).

Lemma C_sound_equiv s t : L.closed s → L.closed t → s == t → C s =*= C t.

Lemma C_eval_sound s t : L.closed s → L.closed t → (L.eval s t → eval (C s) (C t)).

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.

Lemma flattenInj X Y : varClosed 0 X → varClosed 0 Y → flatten X = flatten Y → X=Y.

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.

Lemma absInj s t : abs s = abs t → s = t.

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.

Lemma abs_inv_size_val s : size s = 0 ∨ size (abs_inv s) < (size s).

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.

Lemma C_inv_correct s: C_inv (C s) = s.

Lemma CInj s t : C s = C t → s = t.

Lemma abs_step_prefix s Y X: value Y → (C (λ s)) Y >>> X → X >>* subst (C s) 0 Y.

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

Lemma C_step_prefix s X : L.closed s → C s >>> X → ∃ t, s >> t ∧ X >>* C t.

Lemma C_star_prefix s X : L.closed s → C s >>* X → ∃ t, s >* t ∧ X >>* C t.

Lemma C_eval_pullback s X : L.closed s → eval (C s) X → ∃ t, C t = X ∧ L.eval s t.

Lemma C_eval_complete s t : L.closed s → eval (C s) (C t) → L.eval s t.

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

Lemma abs_lambda_equiv s t u: lambda s → L.closed (lam s) → proc t →
  C ((lam s) t) >>* C u → ((λ s) t) == u.

Lemma C_complete s t:
  L.closed s → C s >>* C t → s == t.

Lemma C_complete_equiv s t :L.closed s → L.closed t → C s =*= C t → s == t.

Lemma C_equiv_iff s t : L.closed s → L.closed t → (s == t ↔ C s =*= C t).

Lemma C_eval_iff s t : L.closed s → L.closed t → (L.eval s t ↔ eval (C s) (C t)).