Library SKvAbstraction

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


Flatten is needed as must shift all de Bruijn indices when 'removing' one binder in the pdeudo abstraction.
Fixpoint flatten X :=
  match X with
    | var (Datatypes.S n) ⇒ var n
    | app X Y ⇒ (flatten X) (flatten Y)
    | XX

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

Pseudo Abstraction

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

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

Lemma abs_sound_pow X Y : value Y n, n > 0 ((abs X) Y) >>^n (subst X 0 Y).

For convenient use, we have this variant

Compiling L into SKv

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

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



Inverse of flatten

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

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.

Inverse of Pseudo Abstraction

Fixpoint abs_inv X :=
  match X with
    | app (app S K) Kvar 0
    | app (app S X) Y ⇒ (abs_inv X) (abs_inv Y)
    | app K Xflatten_inv X
    | _var 100

Lemma abs_inv_correct s: abs_inv (abs s) = s.

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

Inverse of C

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

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 xL.var x
    | KL.var 100
    | SL.var 100
    | app X1 X2if decision (value X) then lam (C_inv (abs_inv X)) else (C_inv X1) (C_inv X2)

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

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


Reductions can be Extended

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.

Complete on normalizing terms

Complete on arbitrary terms

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.