Library CoLoR.Term.SimpleType.TermsBeta

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-27
The beta-reduction relation of simply typed lambda-calculus is introduced in this file.

Set Implicit Arguments.


Module TermsBeta (Sig : TermsSig.Signature).

  Module Export TR := TermsRed.TermsRed Sig.

  Definition beta_subst : forall M (Mapp: isApp M)
    (MLabs: isAbs (appBodyL Mapp)),
    correct_subst (absBody MLabs) {x/(lift (appBodyR Mapp) 1)}.


  Lemma beta_env : forall M (Mapp: isApp M) (MLabs: isAbs (appBodyL Mapp)),
    env (subst (beta_subst M Mapp MLabs)) = None :: env M.

  Lemma beta_lowering : forall M (Mapp: isApp M) (MLabs: isAbs (appBodyL Mapp)),
    env (subst (beta_subst M Mapp MLabs)) |= 0 :! .

  Inductive BetaStep : relation Term :=
  | Beta: forall M (Mapp: isApp M) (MLabs: isAbs (appBodyL Mapp)),
      BetaStep M
      (lower (subst (beta_subst M Mapp MLabs)) (beta_lowering M Mapp MLabs)).

  Definition BetaReduction := Reduction BetaStep.

  Notation "M -b-> N" := (BetaReduction M N) (at level 30).

  Lemma beta_type: forall M (Mapp: isApp M) (MLabs: isAbs (appBodyL Mapp)),
    absType MLabs = type (appBodyR Mapp).

  Lemma beta_notFunS: forall M N, M -b-> N -> isFunS M -> False.

  Lemma beta_direct_funApp : forall M (Mapp: isApp M)
    (MLabs: isAbs (appBodyL Mapp)), isFunS (appHead M) -> False.

  Lemma app_beta_isapp : forall M N f,
    M -b-> N -> term (appHead M) = ^f -> isApp N.

  Lemma app_beta_headSymbol : forall M N f, M -b-> N -> term (appHead M) = ^f ->
    term (appHead N) = ^f.

  Lemma app_beta_funS : forall M N,
    isFunS (appHead M) -> M -b-> N -> isFunS (appHead N).

  Lemma app_beta_args : forall M N f,
    isApp M -> M -b-> N -> term (appHead M) = ^f ->
    exists l, exists el, isArg (fst el) M /\ isArg (snd el) N
      /\ fst el -b-> snd el /\
      appArgs M = fst l ++ fst el::snd l /\ appArgs N = fst l ++ snd el::snd l.

  Lemma app_beta_args_eq : forall M N Q f,
    isApp M -> M -b-> N -> term (appHead M) = ^f ->
    isArg Q N -> (isArg Q M \/ (exists2 Mb, Mb -b-> Q & isArg Mb M)).

  Lemma beta_funS_normal : forall M N, isFunS M -> ~(M -b-> N).

  Lemma beta_var_normal : forall M N, isVar M -> ~(M -b-> N).

  Lemma betaStep_env_preserving : forall M N, BetaStep M N -> env M = env N.

  Lemma beta_env_preserving : forall M N, M -b-> N -> env M = env N.

  Lemma betaStep_type_preserving : forall M N, BetaStep M N -> type M = type N.

  Lemma subject_reduction : forall M N, M -b-> N -> type M = type N.

  Lemma beta_monotonous : monotonous BetaReduction.

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

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

  Lemma subst_at0 : forall M G (MG: correct_subst M (None :: lift_subst G 1)),
    env M |= 0 :! -> env (subst MG) |= 0 :! .

  Lemma subst_envs_comp_cons : forall G,
    subst_envs_comp G -> subst_envs_comp (None :: G).

  Lemma correct_subst_lift : forall M N G (M0: env M |= 0 :!),
    correct_subst N G -> N = lower M M0 ->
    correct_subst M (None :: lift_subst G 1).

  Lemma lower_subst_aux : forall M G i, env M |= i :! ->
    presubst_aux (prelower_aux (term M) i) i (copy i None ++ G) =
    prelower_aux (presubst_aux (term M) i
      (copy i None ++ None :: lift_subst G 1)) i.

  Lemma lower_subst : forall M N G (M0: env M |= 0 :!) (MG: correct_subst N G)
    (MG': correct_subst M (None :: lift_subst G 1))
    (MG'0: env (subst MG') |= 0 :! := (subst_at0 G MG' M0)),
    N = lower M M0 -> subst MG = lower (subst MG') MG'0.

  Lemma lower_eq : forall M N (M0: env M |= 0 :!) (N0: env N |= 0 :!), M = N ->
    lower M M0 = lower N N0.

  Lemma subst_single_eq : forall M M' P P' (MP: correct_subst M {x/P})
    (MP': correct_subst M' {x/P'}), M = M' -> P = P' -> subst MP = subst MP'.

  Lemma double_subst_aux : forall M P G i
    (PG: correct_subst P (None :: lift_subst G 1)),
    presubst_aux (presubst_aux M i (copy i None ++ {x/P}))
    i (copy (S i) None ++ lift_subst G 1) =
    presubst_aux (presubst_aux M i (copy (S i) None ++ lift_subst G 1))
    i (copy i None ++ {x/subst PG}).

  Lemma double_subst : forall M G P (MP: correct_subst M {x/P})
    (MPG: correct_subst (subst MP) (None :: lift_subst G 1))
    (MG: correct_subst M (None :: lift_subst G 1))
    (PG: correct_subst P (None :: lift_subst G 1))
    (MGP: correct_subst (subst MG) {x/subst PG}), subst MPG = subst MGP.

  Lemma double_lift : forall M G
    (CS: correct_subst (lift M 1) (None :: lift_subst G 1))
    (CS': correct_subst M G), subst CS = lift (subst CS') 1.

  Lemma subst_on_beta : forall M (Mapp: isApp M) (MLabs: isAbs (appBodyL Mapp))
    G (CS: correct_subst M G)
    (CSin: correct_subst (absBody MLabs) (None :: lift_subst G 1))
    (CSapp: isApp (subst CS) := app_subst_app Mapp CS)
    (CSLabs: isAbs (appBodyL CSapp)),
    subst CSin = absBody CSLabs.

  Lemma beta_lower_subst : forall M N G (Mapp: isApp M)
    (MLabs: isAbs (appBodyL Mapp))
    (MN: correct_subst M G) (NS: correct_subst N G)
    (MNS_app: isApp (subst MN) := app_subst_app Mapp MN)
    (MNS_Labs: isAbs (appBodyL MNS_app)),
    N = lower (subst (beta_subst M Mapp MLabs)) (beta_lowering M Mapp MLabs) ->
    subst NS = lower (subst (beta_subst (subst MN) MNS_app MNS_Labs))
      (beta_lowering (subst MN) MNS_app MNS_Labs).

  Lemma betaStep_subst_stable : forall M N G (MS: correct_subst M G)
    (NS: correct_subst N G), BetaStep M N -> BetaStep (subst MS) (subst NS).

  Lemma beta_subst_stable : forall M N G (MS: correct_subst M G)
    (NS: correct_subst N G), M -b-> N -> subst MS -b-> subst NS.

  Lemma beta_abs_reduct : forall M (Mabs: isAbs M) N, M -b-> N ->
    exists Nabs: isAbs N, absBody Mabs -b-> absBody Nabs.

  Lemma beta_app_reduct : forall M N (Mapp: isApp M),
    M -b-> 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 -b-> appBodyR Napp)
      \/ (appBodyL Mapp -b-> appBodyL Napp /\ appBodyR Mapp = appBodyR Napp).

  Lemma beta_var_consistent : forall M N,
    M -b-> N -> envSubset (activeEnv N) (activeEnv M).

  Lemma betaStep_dec: forall M N, {BetaStep M N} + {~BetaStep M N}.

  Lemma beta_dec: forall M N, {M -b-> N} + {~ M -b-> N}.

End TermsBeta.