# Library SKvAbstraction

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

# Flatten

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

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

For convenient use, we have this variant
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.

# Compiling L into SKv

Fixpoint C (s : L.term) : term :=
match s with
| L.var x# x
| L.app s t ⇒ (C s) (C t)
| lam sabs (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 (nn0); 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.

## Soundness

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.

# Invertibility

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

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

## Inverse of C

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

# Completeness

## Reductions can be Extended

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.

## Complete on normalizing terms

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.

## 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'.
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 xx) (fun ssize (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.

# Conclusions

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.