Library CoLoR.HORPO.Computability

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-27
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.