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

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

Module Export H := Horpo.Horpo S Prec.

Section Computability_def.

Variable R : relation Term.
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) : 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.

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.

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

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

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.

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

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

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

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

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

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

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

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

Instance AccR_morph : Proper (terms_conv ==> iff) AccR.

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

Instance Computable_morph : Proper (terms_conv ==> iff) Computable.

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

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.

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

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

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

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

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

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

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

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

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 := LexProd_Lt CompTerm_eq R_Comp R_Comp.

Instance R_Comp_morph : Proper (CompTerm_eq ==> CompTerm_eq ==> impl) R_Comp.

Definition SetTheory_Comp : Setoid_Theory CompTerm CompTerm_eq.

Lemma well_founded_R_comp : well_founded (transp R_Comp).

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.

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.

End Computability_theory.

End Computability_def.

End Computability.