Library CoLoR.HORPO.Computability

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
This file provides definition of computability due to Tait and Girard and introduces, as Variable, some computability properties.

Set Implicit Arguments.

Require Import RelExtras.
Require Import ListExtras.
Require Import LexOrder.
Require Import Horpo.
Require Import LogicUtil.
Require Import Setoid.

Module Computability (S : TermsSig.Signature)
(Prec : Horpo.Precedence with Module S := S).

Module H := Horpo.Horpo S Prec.
Export H.

Section Computability_def.

Variable R : Term -> Term -> Prop.
Notation "X <-R- Y" := (R Y X) (at level 50).
Notation "X -R-> Y" := (R X Y) (at level 50).
Let Rtrans := clos_trans R.
Notation "X -R*-> Y" := (Rtrans X Y) (at level 50).

Definition AccR := Acc (transp R).

Fixpoint ComputableS (M: Term) (T: SimpleType) {struct T} : Prop :=
algebraic M /\
type M = T /\
match T with
| #T => AccR M
| TL --> TR =>
forall P (Papp: isApp P) (PL: (appBodyL Papp) ~ M)
(typeL: type P = TR) (typeR: type (appBodyR Papp) = TL),
algebraic (appBodyR Papp) ->
ComputableS (appBodyR Papp) TL ->
ComputableS P TR
end.

Definition Computable M := ComputableS M (type M).

Definition AllComputable Ts := forall T, In T Ts -> Computable T.

Lemma CompBasic : forall M, isBaseType M.(type) -> algebraic M -> AccR M ->
Computable M.

Proof.
intro M; term_type_inv M; split; trivial.
split; trivial.
Qed.

Lemma CompArrow : forall M, algebraic M -> isArrowType (type M) ->
(forall N (Napp: isApp N), (appBodyL Napp) ~ M ->
algebraic (appBodyR Napp) ->
Computable (appBodyR Napp) -> Computable N) ->
Computable M.

Proof.
intro M; term_type_inv M; intros.
hnf; intros; split; trivial.
split; trivial.
intros; unfold Computable in H1.
rewrite <- typeL.
apply H1 with Papp; trivial.
rewrite (@app_typeR P A0_1 A0_2 Papp); trivial.
rewrite (terms_conv_eq_type PL); trivial.
Qed.

Lemma CompCase : forall M, Computable M ->
{ isBaseType M.(type) /\ AccR M /\ algebraic M } +
{ isArrowType M.(type) /\ algebraic M /\
forall N (Napp: isApp N), algebraic (appBodyR Napp) ->
Computable (appBodyR Napp) ->
(appBodyL Napp) ~ M -> Computable N }.

Proof.
intro M.     destruct M as [E Pt A0 Typ]. gen Typ. destruct A0; intro Typ; try_solve;
intro; unfold Computable in H; simpl in H; inversion H.
inversion H1; left; do 2 split; trivial.
right; do 2 split; trivial.
intros N Napp Nnorm NR NL.
unfold Computable.
term_inv N.
set (w := terms_conv_eq_type NL).
inversion w.
inversion H1.
apply H5 with Napp; trivial.
unfold Computable in NR.
rewrite <- H3; trivial.
Qed.

Lemma CompCaseBasic : forall M, Computable M -> isBaseType M.(type) -> AccR M.

Proof.
intros M Mcomp Mbase.
destruct (CompCase M Mcomp) as [[_ [Macc _]] | [Marr _]].
trivial.
Qed.

Lemma CompCaseArrow : forall M, Computable M -> isArrowType M.(type) ->
forall N (Napp: isApp N), algebraic (appBodyR Napp) ->
Computable (appBodyR Napp) ->
(appBodyL Napp) ~ M -> Computable N.

Proof.
intros M Mcomp Marr.
destruct (CompCase M Mcomp) as [[Mbase _] | [_ [_ H]]].
trivial.
Qed.

Lemma comp_algebraic : forall M, Computable M -> algebraic M.

Proof.
intros.
unfold Computable in H; destruct (type M); simpl in H; destruct H; trivial.
Qed.

Section Computability_theory.

Variable R_type_preserving : forall M N, M -R-> N -> type M = type N.

Variable R_env_preserving : forall M N, M -R-> N -> env M = env N.

Variable R_var_consistent : forall M N, M -R-> N ->
envSubset (activeEnv N) (activeEnv M).

Variable R_algebraic_preserving : forall M N, algebraic M -> M -R-> N ->
algebraic N.

Variable R_var_normal : forall M N, isVar M -> ~M -R-> N.

Variable R_conv_comp : forall M N M' N' Q, M ~(Q) M' -> N ~(Q) N' ->
M -R-> N -> env M' = env N' -> M' -R-> N'.

Variable R_app_reduct : forall M N (Mapp: isApp M),
~isFunApp M \/ isArrowType (type M) ->
M -R-> N ->
(exists MLabs: isAbs (appBodyL Mapp),
N = lower (subst (beta_subst M Mapp MLabs)) (beta_lowering M Mapp MLabs)
)
\/
exists Napp: isApp N,
(appBodyL Mapp = appBodyL Napp /\ appBodyR Mapp -R-> appBodyR Napp) \/
(appBodyL Mapp -R-> appBodyL Napp /\ appBodyR Mapp = appBodyR Napp) \/
(appBodyL Mapp -R-> appBodyL Napp /\ appBodyR Mapp -R-> appBodyR Napp).

Variable R_monotonous : algebraic_monotonicity R.

Variable R_subst_stable : forall M N G (MS: correct_subst M G)
(NS: correct_subst N G),
algebraicSubstitution G -> M -R-> N -> subst MS -R-> subst NS.

Variable R_abs_reduct : forall M (Mabs: isAbs M) N, M -R-> N ->
exists Nabs: isAbs N, absBody Mabs -R-> absBody Nabs.

Hint Resolve R_type_preserving R_env_preserving R_var_normal : comp.

Lemma R_right_app_monotonous : forall M N M' N' (M'app: isApp M')
(N'app: isApp N'),
algebraic M -> M -R-> N -> appBodyL M'app = M -> appBodyL N'app = N ->
appBodyR M'app = appBodyR N'app -> algebraic (appBodyR M'app) -> M' -R-> N'.

Proof.
intros.
term_inv M'; term_inv N'.
assert (EE0: E = E0).
replace E with (env M).
replace E0 with (env N).
apply R_env_preserving; trivial.
rewrite <- H2; trivial.
rewrite <- H1; trivial.
set (Lpos := PAppL T2 (PThis (buildT T1))).
assert (W: {P: PlaceHolder Lpos | proj1_sig2 P = M}).
assert (env (buildT (TApp T1 T2) // Lpos) = env M).
rewrite <- H1; trivial.
assert (type (buildT (TApp T1 T2) // Lpos) = type M).
rewrite <- H1; trivial.
exists (exist2
(fun T => env (buildT (TApp T1 T2) // Lpos) = env T)
(fun T => type (buildT (TApp T1 T2) // Lpos) = type T)
M H5 H6
); trivial.
assert (W': {P: PlaceHolder Lpos | proj1_sig2 P = N}).
assert (env (buildT (TApp T1 T2) // Lpos) = env N).
rewrite <- H2; trivial.
assert (type (buildT (TApp T1 T2) // Lpos) = type N).
simpl.
replace (A0 --> B) with (type M).
apply R_type_preserving; trivial.
rewrite <- H1; trivial.
exists (exist2
(fun T => env (buildT (TApp T1 T2) // Lpos) = env T)
(fun T => type (buildT (TApp T1 T2) // Lpos) = type T)
N H5 H6
); trivial.
replace Tr with (swap (proj1_sig W)); destruct W; simpl in * .
replace Tr0 with (swap (proj1_sig W')); destruct W'; simpl in * .
apply R_monotonous; simpl; trivial.
apply algebraic_app with I; trivial.
simpl; rewrite H1; trivial.
rewrite e; trivial.
rewrite e0; trivial.
apply R_algebraic_preserving with M; trivial.
apply algebraic_arrowType; trivial.
rewrite H1; trivial.
rewrite e; rewrite e0; trivial.
apply term_eq.
rewrite swap_env_eq; trivial.
rewrite swap_term_is; simpl; trivial.
rewrite e0.
rewrite <- H2; simpl.
change PtR with (term (buildT T2)).
rewrite H3; trivial.
apply term_eq.
rewrite swap_env_eq; trivial.
rewrite swap_term_is; simpl; trivial.
rewrite e.
rewrite <- H1; trivial.
Qed.

Lemma R_conv_to : forall M N M', M -R-> N -> M ~ M' ->
exists N', M' -R-> N' /\ N ~ N'.

Proof.
intros.
destruct H0.
destruct (envSub_min_ex H0) as [x' [MM' [x'min xx']]].
destruct (term_build_conv_sim N MM') as [N' [M'N' NN']]; trivial.
apply R_env_preserving; trivial.
apply R_var_consistent; trivial.
exists N'; split.
apply R_conv_comp with M N x'; trivial.
exists x'; trivial.
Qed.

Lemma base_step_base : forall M N, isBaseType (type M) -> M -R-> N ->
isBaseType (type N).

Proof.
intros M N Mbase MN.
rewrite <- (R_type_preserving MN); trivial.
Qed.

Lemma base_comp_step_comp : forall M N, isBaseType (type M) ->
Computable M -> M -R-> N -> Computable N.

Proof.
intros M N Mbase Mcomp MN.
apply CompBasic.
apply base_step_base with M; trivial.
apply R_algebraic_preserving with M; trivial.
apply comp_algebraic; trivial.
unfold AccR; apply Acc_step_acc with M; auto.
apply CompCaseBasic; trivial.
Qed.

Lemma acc_app_acc_L : forall M (Mapp: isApp M), algebraic (appBodyL Mapp) ->
algebraic (appBodyR Mapp) -> AccR M -> AccR (appBodyL Mapp).

Proof.
intros; unfold AccR.
apply Acc_mimic with M (fun M N =>
exists Mapp: isApp M,
algebraic (appBodyL Mapp) /\
algebraic (appBodyR Mapp) /\
appBodyL Mapp = N);
try solve [trivial | exists Mapp; split; trivial].
unfold transp; clear H H0 H1 M Mapp; intros M M' MM' N' M'N'.
destruct MM' as [Mapp [MLnorm [MRnorm MM']]].

assert (envOk: env N' = env (appBodyR Mapp)).
term_inv M.
replace E with (env M').
symmetry; auto with comp.
rewrite <- MM'; auto.
assert (typArrow: isArrowType (type N')).
rewrite <- (R_type_preserving M'N').
rewrite <- MM'; term_inv M.
assert (typCorrect: type_left (type N') = type (appBodyR Mapp)).
rewrite <- (R_type_preserving M'N').
rewrite <- MM'; term_inv M.
set (Ncond := Build_appCond N' (appBodyR Mapp) envOk typArrow typCorrect).
set (N := buildApp Ncond).
exists N.

set (Napp := buildApp_isApp Ncond).
apply R_right_app_monotonous with M' N' Mapp Napp; trivial.
rewrite <- MM'; trivial.
unfold N, Napp; rewrite buildApp_Lok; trivial.
unfold N, Napp; rewrite buildApp_Rok; trivial.
exists (buildApp_isApp Ncond); split.
unfold N; rewrite buildApp_Lok; trivial.
apply R_algebraic_preserving with M'; trivial.
rewrite <- MM'; trivial.
simpl; split.
unfold N; rewrite buildApp_Rok; trivial.
unfold N; rewrite buildApp_Lok; trivial.

exists Mapp; split; trivial.
split; trivial.
Qed.

Lemma comp_app : forall M (Mapp: isApp M), Computable (appBodyL Mapp) ->
Computable (appBodyR Mapp) -> Computable M.

Proof.
intros M; term_inv M.
intros TrApp T1c T2c.
apply CompCaseArrow with (buildT T1) I; auto with terms_eq.
apply comp_algebraic; trivial.
Qed.

Lemma AccR_morph_aux :
forall x1 x2 : Term, x1 ~ x2 -> AccR x1 -> AccR x2.

Proof.
intros M M' M'M AccM'; unfold AccR.
apply Acc_homo with (x := M) (R := transp R) (morphism := terms_conv);
trivial.
unfold transp; intros x y x' x'x xy.
destruct (R_conv_to (M':=x') xy (terms_conv_sym x'x)) as [y' [x'y' yy']].
exists y'; trivial.
apply terms_conv_sym; trivial.
Qed.

with signature terms_conv ==> iff
as AccR_morph.

Proof.
intros M M' M'M.
split; apply AccR_morph_aux; auto using terms_conv_sym.
Qed.

Lemma Computable_morph_aux : forall x1 x2 : Term, x1 ~ x2 ->
(Computable x1 -> Computable x2).

Proof.
intro M.
term_type_inv M; intros M' MM' Mcomp.

apply CompBasic.
rewrite <- (terms_conv_eq_type MM'); try_solve.
rewrite <- MM'; apply comp_algebraic; trivial.
rewrite <- MM'.
apply CompCaseBasic; simpl; trivial.

apply CompArrow.
rewrite <- MM'; apply comp_algebraic; trivial.
rewrite <- (terms_conv_eq_type MM'); try_solve.
intros N Napp Nnorm NR NL.
apply (CompCaseArrow Mcomp I N Napp NR NL).
apply terms_conv_trans with M'; auto with terms_eq.
Qed.

with signature terms_conv ==> iff
as Computable_morph.

Proof.
intros t t' teqt'; split; apply Computable_morph_aux;
auto using terms_conv_sym.
Qed.

Lemma comp_lift_comp : forall M n, Computable M -> Computable (lift M n).

Proof.
intros.
rewrite <- (terms_lift_conv M n); trivial.
Qed.

Lemma apply_var_comp : forall M A B, Computable M -> type M = A --> B ->
(forall P, type P = A -> algebraic P -> isNeutral P ->
(forall S, P -R-> S -> Computable S) -> Computable P) ->
exists Mx, exists Mx_app: isApp Mx,
(appBodyL Mx_app) ~ M /\ term (appBodyR Mx_app) = %(length (env M)) /\
env Mx = env M ++ Some A :: EmptyEnv /\ Computable Mx.

Proof.
intros M C D Mcomp MT IH.
destruct (apply_variable M) as [Mx [Mx_app [MxL [MxR Mx_env]]]].
rewrite MT; simpl; trivial.
exists Mx; exists Mx_app; split; trivial.
repeat split; trivial.
rewrite MT in Mx_env; try_solve.
apply comp_app with Mx_app.
rewrite MxL; trivial.
apply IH.
apply app_typeR with D.
rewrite <- terms_conv_eq_type with M (appBodyL Mx_app); trivial.
term_inv Mx; destruct T2; try_solve.
apply terms_conv_sym; trivial.
apply algebraic_var; apply var_is_var with (length (env M)); trivial.
apply var_neutral.
eapply var_is_var; eauto.
intros S RS.
absurd (appBodyR Mx_app -R-> S); auto with comp.
apply R_var_normal.
apply var_is_var with (length (env M)); try_solve.
Qed.

Lemma comp_step_comp : forall M N, Computable M -> M -R-> N -> Computable N.

Proof.
assert (forall A M N, type M = A -> Computable M -> M -R-> N -> Computable N).
intro B.
induction B.
intros M N MT Mcomp MN.
apply base_comp_step_comp with M; trivial.
rewrite MT; auto with terms.
intros M N Marr Mcomp MN.
apply CompArrow.
apply R_algebraic_preserving with M; trivial.
apply comp_algebraic; trivial.
rewrite <- (R_type_preserving MN); rewrite Marr; simpl; trivial.
intros N'S N'S_app N'S_L N'S_Rnorm N'S_R.
set (N' := appBodyL N'S_app) in * .
set (S := appBodyR N'S_app) in * .
destruct (terms_conv_sym N'S_L) as [Q NQN'].
destruct (envSub_min_ex NQN') as [Q' [NQ'N' [Q'minN _]]].
destruct (term_build_conv_rel M (R_var_consistent MN) NQ'N') as
[Q'' [Q''Q' [M' [MM' M'env]]]]; trivial.
assert (N'S_M'_env: envSubset (env N'S) (env M')).
rewrite <- (appBodyL_env N'S N'S_app); trivial.
assert (N''S't: env M' |- term N'S := type N'S).
apply typing_ext_env with (env N'S); trivial.
exact (typing N'S).
set (N''S' := buildT N''S't).
assert (NS_conv: N'S ~ N''S').
apply terms_conv_criterion; trivial.
simpl; apply env_subset_comp; trivial.
set (N''S'_app := proj1 (isApp_morph NS_conv) N'S_app).
set (SS' := app_conv_app_right N'S_app N''S'_app NS_conv); fold S in SS'.
set (N'' := appBodyL N''S'_app) in * .
set (S' := appBodyR N''S'_app) in * .
set (typeMM' := terms_conv_eq_type (conv_by MM')).
assert (M'S'_envOk: env M' = env S').
unfold S'; rewrite appBodyR_env; trivial.
assert (M'S'_Marr: isArrowType (type M')).
rewrite <- typeMM'; rewrite Marr; simpl; trivial.
assert (M'S'_typeOk: type_left (type M') = type S').
rewrite <- typeMM'.
rewrite (R_type_preserving MN).
rewrite <- (terms_conv_eq_type N'S_L).
set (w := app_conv_app_right N'S_app N''S'_app NS_conv).
unfold S'; rewrite <- (terms_conv_eq_type w).
term_inv N'S.
set (M'S'_cond := Build_appCond M' S' M'S'_envOk M'S'_Marr M'S'_typeOk).
set (M'S' := buildApp M'S'_cond).
set (M'S'_app := buildApp_isApp M'S'_cond).
set (M'S'_L := buildApp_Lok M'S'_cond).
set (M'S'_R := buildApp_Rok M'S'_cond).
assert (M'N': M' -R-> N'').
apply R_conv_comp with M N Q''; trivial.
apply terms_conv_diff_env with N'; trivial.
apply terms_conv_extend_subst with Q'; trivial.
unfold N', N''; apply term_appBodyL_eq; trivial.
unfold N', N''.
apply equiv_term_activeEnv.
apply term_appBodyL_eq; trivial.
repeat rewrite appBodyL_env.
apply env_comp_sym; apply env_subset_comp; trivial.
unfold N''; rewrite appBodyL_env; trivial.
rewrite NS_conv.
apply IHB2 with M'S'; unfold M'S'.
rewrite buildApp_type; simpl.
rewrite <- typeMM'; rewrite Marr; trivial.
apply CompCaseArrow with M' (buildApp_isApp M'S'_cond); trivial.
assert (MeqM' : M ~ M') by (exists Q''; trivial).
rewrite <- MeqM'; trivial.
rewrite M'S'_R; simpl; trivial.
rewrite <- (algebraic_morph SS'); trivial.
rewrite M'S'_R; simpl; trivial.
rewrite <- SS'; trivial.
rewrite M'S'_L; apply terms_conv_refl.
apply R_right_app_monotonous with M' N'' M'S'_app N''S'_app; trivial.
rewrite <- (conv_by MM').
apply comp_algebraic; trivial.
unfold M'S'_app; rewrite M'S'_R.
simpl; rewrite <- SS'; trivial.
intros. apply H with (type M) M; trivial.
Qed.

Lemma comp_prop : forall A,
(
forall M, type M = A -> Computable M -> AccR M
) /\
(
forall P, type P = A -> algebraic P -> isNeutral P ->
(forall S, P -R-> S -> Computable S) -> Computable P).

Proof.
intro B.
induction B.
split.
intros M MT Mcomp.
apply CompCaseBasic; trivial.
rewrite MT; auto with terms.
intros P Pbase Pnorm Pneutral PScomp.
assert (P_base: isBaseType (type P)).
rewrite Pbase; auto with terms.
apply CompBasic; trivial.
constructor.
intros S RS.
apply CompCaseBasic.
apply PScomp; trivial.
apply base_step_base with P; trivial.

destruct IHB1 as [IH_L1 IH_L2].
destruct IHB2 as [IH_R1 IH_R2].
split.

intros M Marr Mcomp.
destruct (apply_var_comp M Mcomp Marr)
as [Mx [Mx_app [MxL [_ [_ Mxcomp]]]]]; trivial.
rewrite <- MxL.
apply acc_app_acc_L; trivial.
rewrite MxL; apply comp_algebraic; trivial.
apply algebraic_appBodyR.
apply comp_algebraic; trivial.
apply IH_R1; trivial.
apply app_typeL_type with B1 Mx_app; trivial.
rewrite <- terms_conv_eq_type with M (appBodyL Mx_app); trivial.
apply terms_conv_sym; trivial.

intros P Parr Palg Pneutral PScomp.
apply CompArrow; trivial.
rewrite Parr; simpl; trivial.
intros N Napp NL NRnorm NR.
assert (Hyp:
forall W,
Computable W ->
type W = B1 ->
forall N (Napp: isApp N),
(appBodyL Napp) ~ P ->
appBodyR Napp = W ->
Computable N
).
intros W Wcomp Wtyp.
assert (Wacc: Acc (transp R) W).
apply IH_L1; trivial.
cut (type W = B1); trivial.
cut (Computable W); trivial.
cut (algebraic P); trivial.
apply Acc_rect with (R := transp R)(P :=
fun W =>
algebraic P ->
Computable W ->
type W = B1 ->
forall N (Napp: isApp N),
(appBodyL Napp) ~ P ->
appBodyR Napp = W ->
Computable N
); trivial.
clear N NRnorm Napp NL NR W Wcomp Wtyp Wacc.
intros W _ IH Pnorm Wcomp Wtype N Napp NL NR.
apply IH_R2; trivial.
apply app_typeL_type with B1 Napp; trivial.
rewrite (terms_conv_eq_type NL); trivial.
apply algebraic_app with Napp.
rewrite NL; trivial.
rewrite NR; apply comp_algebraic; trivial.
apply app_neutral; trivial.
intros S NS.
destruct (R_app_reduct (N:=S) Napp) as
[NLabs_red | [Sapp [[Leq Rgt] | [[Lgt Req] | [Lgt Rgt]]]]]; trivial.
left.
apply algebraic_app_notFunApp with Napp.
rewrite NL; trivial.
rewrite NR; apply comp_algebraic; trivial.
destruct NLabs_red.
absurd (isAbs P); trivial.
rewrite <- NL; trivial.

apply IH with (appBodyR Sapp) Sapp; trivial.
unfold transp; simpl.
rewrite <- NR; trivial.
apply comp_step_comp with (appBodyR Napp); trivial.
rewrite NR; trivial.
rewrite <- (R_type_preserving Rgt).
rewrite NR; trivial.
rewrite <- Leq; trivial.

apply comp_app with Sapp.
destruct (R_conv_to (M':=P) Lgt NL) as [S' [PS' SLS']].
rewrite SLS'.
apply PScomp; trivial.
rewrite <- Req.
rewrite NR; trivial.

apply comp_app with Sapp.
destruct (R_conv_to (M':=P) Lgt NL) as [S' [PS' SLS']].
rewrite SLS'.
apply PScomp; trivial.
apply comp_step_comp with W; trivial.
rewrite <- NR; trivial.

apply Hyp with (appBodyR Napp) Napp; trivial.
apply app_typeR with B2.
rewrite (terms_conv_eq_type NL); trivial.
Qed.

Lemma comp_imp_acc : forall M, Computable M -> AccR M.

Proof.
intros M MC.
destruct (comp_prop (type M)) as [P1 P2].
apply P1; trivial.
Qed.

Lemma comp_manysteps_comp : forall M N, Computable M -> M -R*-> N ->
Computable N.

Proof.
intros M N Mcomp M_rew_N.
induction M_rew_N.
apply comp_step_comp with x; trivial.
auto.
Qed.

Lemma neutral_comp_step : forall M, algebraic M -> isNeutral M ->
(Computable M <-> (forall N, M -R-> N -> Computable N)).

Proof.
intros M Mneutral.
destruct (comp_prop (type M)) as [P1 P2].
split.
intros Mcomp N MN.
apply comp_step_comp with M; trivial.
intros MNcomp.
apply P2; trivial.
Qed.

Lemma var_comp : forall M, isVar M -> Computable M.

Proof.
intros M Mvar.
assert (Mneutral: isNeutral M).
term_inv M.
apply (proj2 (neutral_comp_step (algebraic_var M Mvar) Mneutral)).
intros N MN.
absurd (M -R-> N); trivial.
apply R_var_normal; trivial.
Qed.

Lemma comp_units_comp : forall M, (forall N, isAppUnit N M -> Computable N) ->
Computable M.

Proof.
destruct M as [E Pt T TypM]; induction TypM; intro compUnits;
try solve [apply compUnits; compute; auto].
apply comp_app with I; simpl.
apply IHTypM1.
intros N NunitL; apply compUnits.
apply appUnit_left with I; trivial.
apply compUnits.
red.
rewrite (appUnits_app (buildT (TApp TypM1 TypM2)) I).
auto with datatypes.
Qed.

Lemma comp_pflat : forall N Ns, isPartialFlattening Ns N ->
AllComputable Ns -> Computable N.

Proof.
intro N.
case (isApp_dec N).
destruct N as [E Pt T TypN]; induction TypN; try contradiction.
intros Napp Ns Ns_pflat Ns_comp.
unfold isPartialFlattening in Ns_pflat.
repeat (destruct Ns; [contradiction | idtac]).
rewrite (appUnits_app (buildT (TApp TypN1 TypN2)) I) in Ns_pflat.
simpl in Ns_pflat.
destruct Ns.
destruct (app_inj_tail (appUnits t) (appUnits (buildT TypN1))
t0 (buildT TypN2)) as [t_L t0_R]; trivial.
apply comp_app with I; simpl.
rewrite <- (eq_units_eq_terms t (buildT TypN1) t_L).
apply Ns_comp; auto with datatypes.
rewrite <- t0_R.
apply Ns_comp; auto with datatypes.
destruct (@list_drop_last Term ((appUnits t) ++ t0::nil)
(t1::Ns) (appUnits (buildT TypN1)) (buildT TypN2)) as [x xIn leq].
rewrite list_app_first_last; trivial.
auto with datatypes.
apply comp_app with I; simpl.
set (pf := t::t0::x).
case (isApp_dec (buildT TypN1)).
intro N1app; apply IHTypN1 with pf; trivial.
unfold isPartialFlattening; simpl.
rewrite <- list_app_first_last; trivial.
unfold pf; intros p pIn.
apply Ns_comp.
assert (inc: incl (t::t0::x) (t::t0::t1::Ns)).
repeat (apply incl_cons; auto with datatypes).
apply inc; trivial.
intro N1napp.
rewrite (appUnits_notApp (buildT TypN1)) in Ns_pflat; trivial.
simpl in Ns_pflat.
assert (N1_in: In (buildT TypN1) (t0::x)).
rewrite (appUnits_notApp (buildT TypN1)) in leq; trivial.
apply list_app_last with (appUnits t) (nil (A:=Term)).
rewrite <- list_app_first_last; trivial.
auto with datatypes.
apply Ns_comp.
destruct (in_inv N1_in).
rewrite H; auto with datatypes.
auto with datatypes.
assert (N2_in: In (buildT TypN2) (t1::Ns)).
apply list_app_last with
(appUnits t ++ t0::nil) (appUnits (buildT TypN1)).
rewrite list_app_first_last; trivial.
auto with datatypes.
apply Ns_comp; auto with datatypes.
intros N_nApp Ns Ns_pflat Ns_comp.
absurd (isApp N); trivial.
apply partialFlattening_app with Ns; trivial.
Qed.

Definition CompTerm := { T: Term | Computable T }.
Definition R_Comp (T1 T2: CompTerm) := proj1_sig T1 -R-> proj1_sig T2.
Definition CompTerm_eq (T1 T2: CompTerm) := proj1_sig T1 = proj1_sig T2.
Definition TermsPairLex := lp_LexProd_Lt CompTerm_eq R_Comp R_Comp.

Definition SetTheory_Comp : Setoid_Theory CompTerm CompTerm_eq.

Proof.
constructor; unfold Reflexive, Symmetric, Transitive.
constructor.
intros; inversion H.
unfold CompTerm_eq; auto.
intros; inversion H; inversion H0.
unfold CompTerm_eq; transitivity (proj1_sig y); trivial.
Defined.

Lemma well_founded_R_comp : well_founded (transp R_Comp).

Proof.
set (w := Acc_ind (R := transp R) (fun M =>
forall T,
proj1_sig T = M ->
Acc (transp R_Comp) T
)).
intro T.
apply w with (proj1_sig T); trivial.
intros; constructor; intros.
eapply H0 with (proj1_sig y); trivial.
unfold R_Comp, transp in * .
rewrite <- H1; trivial.
apply comp_imp_acc.
destruct T; trivial.
Qed.

Lemma comp_abs_ind : forall (P: CompTerm * CompTerm)
W (Wapp: isApp W) (WLabs: isAbs (appBodyL Wapp)),
(forall G (cs: correct_subst (absBody WLabs) G) T, isSingletonSubst T G ->
Computable T -> Computable (subst cs)) ->
algebraic W -> absBody WLabs = proj1_sig (fst P) ->
appBodyR Wapp = proj1_sig (snd P) -> Computable W.

Proof.
intro P.
apply well_founded_ind with (R := TermsPairLex) (P :=
fun (P: CompTerm * CompTerm) =>
forall W (Wapp: isApp W) (WLabs: isAbs (appBodyL Wapp)),
(forall G (cs: correct_subst (absBody WLabs) G) T,
isSingletonSubst T G ->
Computable T ->
Computable (subst cs)
) ->
algebraic W ->
absBody WLabs = proj1_sig (fst P) ->
appBodyR Wapp = proj1_sig (snd P) ->
Computable W
).
unfold TermsPairLex.
eapply lp_lexprod_wf; try solve
[ eexact SetTheory_Comp
| unfold R_Comp; intros x x' y y' xx' yy' xy;
inversion xx'; inversion yy'; trivial
| apply well_founded_R_comp
].
clear P; intros P IH W Wapp WLabs WL_Hyp Wnorm PL PR.
assert (WLnorm: algebraic (appBodyL Wapp)).
apply algebraic_appBodyL; trivial.
unfold isFunApp; intro WFapp.
rewrite (appHead_app W Wapp) in WFapp.
(abs_isnot_app (appBodyL Wapp) WLabs)) in WFapp.
term_inv (appBodyL Wapp).
assert (WRnorm: algebraic (appBodyR Wapp)).
apply algebraic_appBodyR; trivial.
rewrite_rl (neutral_comp_step Wnorm (app_neutral W Wapp)).
intros W' WW'.
destruct P as [[PLT PLC] [PRT PRC]]; simpl in * .
destruct (R_app_reduct (N:=W') Wapp) as [[W'abs W'beta] |
[W'app [[W'L_eq W'R_red] | [[W'L_red W'R_eq] | [W'L_red W'R_red]]]]];
trivial.
left; apply funAbs_notFunApp.
term_inv (appBodyL Wapp).

rewrite W'beta.
rewrite <- (Computable_morph (terms_lower_conv
(subst (beta_subst W Wapp W'abs)) (beta_lowering W Wapp W'abs))).
rewrite (abs_proof_irr (appBodyL Wapp) W'abs WLabs).
apply WL_Hyp with (lift (appBodyR Wapp) 1).
apply singletonSubst_cond.
apply comp_lift_comp.
rewrite PR; trivial.

assert (W'Labs: isAbs (appBodyL W'app)).
rewrite <- W'L_eq; trivial.
set (WL_W'L := absBody_eq WLabs W'Labs W'L_eq).
assert (W'Lcomp: Computable (absBody W'Labs)).
rewrite <- WL_W'L; rewrite PL; trivial.
assert (W'Rcomp: Computable (appBodyR W'app)).
apply comp_step_comp with (appBodyR Wapp); trivial.
rewrite PR; trivial.
set (P'L := exist (fun (W: Term) => Computable W) (absBody W'Labs) W'Lcomp).
set (P'R := exist (fun (W: Term) => Computable W) (appBodyR W'app) W'Rcomp).
apply (IH (P'L, P'R)) with W'app W'Labs; trivial.
constructor 2.
unfold CompTerm_eq; simpl.
rewrite <- PL; trivial.
unfold R_Comp; simpl; rewrite <- PR; trivial.
intros G cs T GT Tcomp.
assert (cs': correct_subst (absBody WLabs) G).
destruct cs; constructor; try solve
[ trivial
| rewrite (absBody_eq WLabs W'Labs); trivial
].
replace (subst cs) with (subst cs').
apply WL_Hyp with T; trivial.
apply term_eq.
repeat rewrite subst_env; rewrite (absBody_eq WLabs W'Labs); trivial.
repeat rewrite subst_term; rewrite (absBody_eq WLabs W'Labs); trivial.
apply algebraic_app with W'app.
rewrite <- W'L_eq; trivial.
apply R_algebraic_preserving with (appBodyR Wapp); trivial.

destruct (R_abs_reduct WLabs W'L_red) as [W'Labs W'Lbody_red].
assert (W'Lcomp: Computable (absBody W'Labs)).
apply comp_step_comp with (absBody WLabs); trivial.
rewrite PL; trivial.
assert (W'Rcomp: Computable (appBodyR W'app)).
rewrite <- W'R_eq; rewrite PR; trivial.
set (P'L := exist (fun (W: Term) => Computable W) (absBody W'Labs) W'Lcomp).
set (P'R := exist (fun (W: Term) => Computable W) (appBodyR W'app) W'Rcomp).
apply (IH (P'L, P'R)) with W'app W'Labs; trivial.
constructor 1.
unfold R_Comp; simpl; rewrite <- PL; trivial.
intros G cs T TG Tcomp.
assert (CS: correct_subst (absBody WLabs) G).
destruct cs; constructor; trivial.
rewrite (R_env_preserving W'Lbody_red); trivial.
rewrite (R_env_preserving W'Lbody_red); trivial.
apply comp_step_comp with (subst CS).
apply WL_Hyp with T; trivial.
apply R_subst_stable; trivial.
apply singletonSubst_algebraic with T; trivial.
apply comp_algebraic; trivial.
apply algebraic_app with W'app.
apply R_algebraic_preserving with (appBodyL Wapp); trivial.
rewrite <- W'R_eq; trivial.

destruct (R_abs_reduct WLabs W'L_red) as [W'Labs W'Lbody_red].
assert (W'Lcomp: Computable (absBody W'Labs)).
apply comp_step_comp with (absBody WLabs); trivial.
rewrite PL; trivial.
assert (W'Rcomp: Computable (appBodyR W'app)).
apply comp_step_comp with (appBodyR Wapp); trivial.
rewrite PR; trivial.
set (P'L := exist (fun (W: Term) => Computable W) (absBody W'Labs) W'Lcomp).
set (P'R := exist (fun (W: Term) => Computable W) (appBodyR W'app) W'Rcomp).
apply (IH (P'L, P'R)) with W'app W'Labs; trivial.
constructor 1.
unfold R_Comp; simpl; rewrite <- PL; trivial.
intros G cs T GT Tcomp.
assert (CS: correct_subst (absBody WLabs) G).
destruct cs; constructor; trivial.
rewrite (R_env_preserving W'Lbody_red); trivial.
rewrite (R_env_preserving W'Lbody_red); trivial.
apply comp_step_comp with (subst CS).
apply WL_Hyp with T; trivial.
apply R_subst_stable; trivial.
apply singletonSubst_algebraic with T; trivial.
apply comp_algebraic; trivial.
apply algebraic_app with W'app.
apply R_algebraic_preserving with (appBodyL Wapp); trivial.
apply R_algebraic_preserving with (appBodyR Wapp); trivial.
Qed.

Lemma comp_abs : forall M (Mabs: isAbs M), algebraic M ->
(forall G (cs: correct_subst (absBody Mabs) G) T, isSingletonSubst T G ->
Computable T -> Computable (subst cs)) -> Computable M.

Proof.
intros M Mabs Mnorm H.
apply CompArrow; trivial.
term_inv M.
intros W Wapp WL WRnorm WR.
assert (WLabs: isAbs (appBodyL Wapp)).
rewrite WL; trivial.
set (TL := absBody WLabs).
set (TR := appBodyR Wapp).
assert (M0: env (absBody Mabs) |= 0 := absType Mabs).
term_inv M.
assert (TLC: Computable (absBody WLabs)).
set (idS1 := idSubst_correct (absBody Mabs)).
simpl; setoid_replace (absBody WLabs) with (subst (idS1))
using relation terms_conv.
set (S1eqS2 := idSubst_decl0 (absBody Mabs) M0).
assert (idS2 : correct_subst (absBody Mabs) {x/buildT (TVar M0)}).
rewrite <- S1eqS2; trivial.
replace (subst idS1) with (subst (idS2)).
apply H with (buildT (TVar M0)).
apply singletonSubst_cond.
apply var_comp; simpl; trivial.
apply term_eq.
repeat rewrite subst_env.
rewrite S1eqS2; trivial.
repeat rewrite subst_term.
rewrite S1eqS2; trivial.
unfold idS1; rewrite (idSubst_neutral (absBody (M:=M) Mabs)).
apply abs_conv_absBody; trivial.
set (PL := (exist (fun T => Computable T) TL TLC)).
set (PR := (exist (fun T => Computable T) TR WR)).
apply comp_abs_ind with (Wapp := Wapp) (WLabs := WLabs) (P := (PL, PR));
trivial.
intros.
destruct WL.
set (WLM := abs_conv_absBody_aux WLabs Mabs H2).
destruct (isVarDecl_dec (activeEnv (absBody WLabs)) 0) as [[B DB] | ND].
destruct (envSub_min_ex WLM) as [Q [Qconv [Qmin Qext]]].
assert (Q00: envSub Q 0 0).
destruct (terms_conv_activeEnv Qconv DB).
assert (x0 = 0).
apply envSub_Lok with (envSubst_lift1 x) 0.
apply (Qext 0 x0); trivial.
destruct x; simpl; trivial.
rewrite H4 in H3; trivial.
destruct (conv_subst_singleton_build Q00 Qconv Qmin H0 cs) as
[Q' [G' [T' [MG' [T'G' [Q'Q GG']]]]]].
set (Conv :=
conv_subst_conv cs MG' (terms_conv_extend_subst Qconv Q'Q) GG').
assert (Conv' : terms_conv (subst cs) (subst MG')) by (exists Q'; trivial).
rewrite Conv'.
apply H with T'; trivial.
setoid_replace T' with T using relation terms_conv; trivial.
apply terms_conv_sym; exists Q'; trivial.
apply singletonSubst_conv with G G'; trivial.
rewrite <- (uneffective_singleton_subst_conv cs H0 ND); trivial.
apply algebraic_app with Wapp; trivial.
rewrite WL; trivial.
Qed.

End Computability_theory.

End Computability_def.

End Computability.