Library CoLoR.Term.SimpleType.TermsRed

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-27
Formalization of reductions of simply-typed lambda terms.

Set Implicit Arguments.


Module TermsRed (Sig : TermsSig.Signature).

  Module Export TSC := TermsSubstConv.TermsSubstConv Sig.

  Inductive Reduction (R: relation Term) : Term -> Term -> Prop :=
  | RedStep: forall M N,
      R M N ->
      Reduction R M N
  | RedAppL: forall M N (Mapp: isApp M) (Napp: isApp N),
      Reduction R (appBodyL Mapp) (appBodyL Napp) ->
      appBodyR Mapp = appBodyR Napp ->
      Reduction R M N
  | RedAppR: forall M N (Mapp: isApp M) (Napp: isApp N),
      Reduction R (appBodyR Mapp) (appBodyR Napp) ->
      appBodyL Mapp = appBodyL Napp ->
      Reduction R M N
  | RedAbs: forall M N (Mabs: isAbs M) (Nabs: isAbs N),
      absType Mabs = absType Nabs ->
      Reduction R (absBody Mabs) (absBody Nabs) ->
      Reduction R M N.

  Lemma red_monotonous : forall R, monotonous (Reduction R).

  Section conv_comp.

    Variable R : relation Term.
    Notation Red := (Reduction R).

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

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

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

    Lemma Red_env_preserving : forall M N, Red M N -> env M = env N.

    Lemma Red_type_preserving : forall M N, Red M N -> type M = type N.

    Lemma red_conv_comp : forall M N, Red M N ->
      forall M' N' Q, M ~(Q) M' -> N ~(Q) N' -> env M' = env N' -> Red M' N'.

  End conv_comp.

  Section var_comp.

    Variable R : relation Term.
    Notation Red := (Reduction R).

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

    Lemma red_var_consistent : forall M N,
      Red M N -> envSubset (activeEnv N) (activeEnv M).

  End var_comp.

  Section Decidability.

    Variable R : relation Term.
    Notation Red := (Reduction R).

    Variable step_dec : forall M N, {R M N} + {~R M N}.

    Lemma red_dec : forall M N, {Red M N} + {~Red M N}.

  End Decidability.

End TermsRed.